2 Apr
2023
2 Apr
'23
4:41 p.m.
Hi,
I ran into a couple of issues when using SPOT in a project. I'll be glad
for any assistance.
1) I am calling sat_minimize from a python script using the spot python
library. Is there any way to set a timeout on this function call? Or do I
have to use the CLI if I want a timeout?
2) I am manipulating an automaton generated from an LTL formula, and then
printing it in HOA format. Is there a way to guarantee that the initial
state is the state numbered 0? If not, is there any other way to control
the naming of states?
Thank you,
Yoav Ben Shimon
13 Apr
13 Apr
5:47 p.m.
Hi Yoav,
Sorry for this delayed answer.
Yoav Ben Shimon <yoavbenshimon(a)gmail.com> writes:
I ran into a couple of issues when using SPOT in a
project. I'll be
glad for any assistance.
1) I am calling sat_minimize from a python script using the spot
python library. Is there any way to set a timeout on this function
call? Or do I have to use the CLI if I want a timeout?
I'm not aware of easy ways to deal with timeouts at the function level.
Those are usually set at the process level by using alarm() to trigger a
signal, and then usually killing the process when receiving this signal.
It seems easier to just runs this minimization as a separate process,
and use Python's subprocess module with a timeout.
2) I am manipulating an automaton generated from an
LTL formula, and
then printing it in HOA format. Is there a way to guarantee that the
initial state is the state numbered 0?
You should generally not assume that the initial state is 0.
You could swap the initial state with state 0 in a rather crude way
by iterating on the edge vector and fixing all source and destinations,
but that will cause issue if some named-properties are attached to the
automaton as those could be vectors indexed by state numbers (e.g., a
vector of strings naming each state). See the attachment for an
example that also removes all named properties as a security.
Another idea: the current version of the formater for the LBTT format
(compatible only with generalized Büchi acceptance) does relabels all
states in such a way that the initial state is 0. So while
ltl2tgba XXXGa
will print an HOA that does not start at state 0, using
ltl2tgba XXXGa --lbtt | autfilt
will print an HOA that start at 0. There is however nothing in the LBTT
format that forces us to start at 0, so this is unfortunately just
a side effect of how things are implemented.
If not, is there any other way to control the naming
of states?
You are probably talking about the numbering of states, but just for
completeness I'll add that the HOA format also allows you to name
states: those are strings attached to each state. In python you can
do
aut.set_state_names(["name for state 0",
"name for state 1", ...,
"name for state n-1"])
and those will be preserved in the HOA.
4 Jun
4 Jun
5:34 p.m.
Hi Alexandre,
Thank you very much for the detailed response!
Python subprocess seems to work well for giving a timeout externally.
For the other issue, I modified the next tool in my toolchain to work
correctly when receiving as input automata where the initial state is not
numbered 0.
I'll be happy if you can give me some further advice on my use of SPOT:
My goal is to take TLSF specifications from syntcomp
<http://www.syntcomp.org/> and check realizability using the tool Spectra
<https://smlab.cs.tau.ac.il/syntech/index.html#spectra>. Since this tool is
made for the GR(1) fragment, I attempt to translate individual LTL formulas
from the TLSF spec into this fragment. In particular, for some of the
formulas I use SPOT to translate them into a deterministic Buchi automata
in HOA format, which is then given as input to a tool called DBW2GR1
<http://smlab.cs.tau.ac.il/syntech/patterns/MR15patterns.pdf> (a part of
Spectra) generating a GR(1) equivalent formula if such exists.
I use the following command (LTL_FORMULA here is already translated via
syfco <https://github.com/reactive-systems/syfco> to the required syntax):
ltl2tgba -D -B -H -x sat-minimize -f LTL_FORMULA | autfilt
--is-deterministic
My aim is to fail if the result is not deterministic, since a minimal DBA
is a requirement for the correctness of DBW2GR1.
I'll be happy if you have any advice, especially on the use of
sat-minimize: are there any parameters I should alter to get the best
possible results from the sat solver? (I am aware that inherently some
inputs will be difficult.)
Is there any quicker way to tell if a translation to DBA is possible,
perhaps separately from the minimization procedure?
As a side note, I also use SPOT's ltlsynt to compare with my results. For
this I use:
ltlsynt --realizability --tlsf FILE
Thank you,
Yoav
On Thu, Apr 13, 2023 at 6:47 PM Alexandre Duret-Lutz <adl(a)lrde.epita.fr>
wrote:
Hi Yoav,
Sorry for this delayed answer.
Yoav Ben Shimon <yoavbenshimon(a)gmail.com> writes:
I ran into a couple of issues when using SPOT in
a project. I'll be
glad for any assistance.
1) I am calling sat_minimize from a python script using the spot
python library. Is there any way to set a timeout on this function
call? Or do I have to use the CLI if I want a timeout?
I'm not aware of easy ways to deal with timeouts at the function level.
Those are usually set at the process level by using alarm() to trigger a
signal, and then usually killing the process when receiving this signal.
It seems easier to just runs this minimization as a separate process,
and use Python's subprocess module with a timeout.
2) I am manipulating an automaton generated from
an LTL formula, and
then printing it in HOA format. Is there a way to guarantee that the
initial state is the state numbered 0?
You should generally not assume that the initial state is 0.
You could swap the initial state with state 0 in a rather crude way
by iterating on the edge vector and fixing all source and destinations,
but that will cause issue if some named-properties are attached to the
automaton as those could be vectors indexed by state numbers (e.g., a
vector of strings naming each state). See the attachment for an
example that also removes all named properties as a security.
Another idea: the current version of the formater for the LBTT format
(compatible only with generalized Büchi acceptance) does relabels all
states in such a way that the initial state is 0. So while
ltl2tgba XXXGa
will print an HOA that does not start at state 0, using
ltl2tgba XXXGa --lbtt | autfilt
will print an HOA that start at 0. There is however nothing in the LBTT
format that forces us to start at 0, so this is unfortunately just
a side effect of how things are implemented.
If not, is there any other way to control the
naming of states?
You are probably talking about the numbering of states, but just for
completeness I'll add that the HOA format also allows you to name
states: those are strings attached to each state. In python you can
do
aut.set_state_names(["name for state 0",
"name for state 1", ...,
"name for state n-1"])
and those will be preserved in the HOA.
6 Jun
6 Jun
11:30 a.m.
Hi Yoav,
Yoav Ben Shimon <yoavbenshimon(a)gmail.com> writes:
I use the following command (LTL_FORMULA here is
already translated
via syfco to the required syntax):
ltl2tgba -D -B -H -x sat-minimize -f LTL_FORMULA | autfilt
--is-deterministic
Hum... I don't think that running
ltl2tgba -DB -x sat-minimize φ
will always give you a DBA if one exists.
I'm sure that -DB alone does not. (Since -D expresses only a
preference, it's never clear when ltl2tgba to spend additional time
looking for a DBA that might not exist. Maybe we need another switch.)
Adding '-x sat-minimize' will activate an extra determinization
procedure based on powerset. Basically, it builds a powerset of the NBA,
and attempt to determine the accepting transitions of the powerset by
looking at the cycles of the NBA. See section 3.2 of "Mechanizing the
Powerset Construction for Restricted Classes of ω-Automata" by Dax,
Eisinger, & Klaedtke. The state-based version of this algorithm only
works for a subset of recurrence formulas, and I _believe_ the
transition-based version (that we do) only works with a larger subset.
Additionally, because that determinization code is currently based on a
cycle enumeration, it will also abort in presence of too many cycles.
I suspect this old code for attempting deterimization was written
before we had a Safra-like determinization in Spot, and the code
path for -x sat-minimize could now be improved. (Even enumerating
cycles in the NBA to fix the acceptance of Powerset(NBA) sounds crazy
to me — why aren't we looking at the product of these two?)
My aim is to fail if the result is not deterministic,
since a minimal
DBA is a requirement for the correctness of DBW2GR1.
I'll be happy if you have any advice, especially on the use of
sat-minimize: are there any parameters I should alter to get the best
possible results from the sat solver? (I am aware that inherently
some inputs will be difficult.)
Is there any quicker way to tell if a translation to DBA is possible,
perhaps separately from the minimization procedure?
I think https://spot.lre.epita.fr/hierarchy.html#org9007bec is what you
want:
First, request a DPA.
ltl2tgba -DP φ
the output will always be deterministic, and it will use the minimal
number of colors for that language. For any recurrence formula, the
produced DPA should have an acceptance of: f, t, or Inf(0). So accept
for f and t, it's already a DBA. If you Get any other acceptance, you
can abort your procedure here, as no DBA exist.
Then force convert your automaton into a DBA and minimize it:
ltl2tgba -DP φ | autfilt -DB --sat-minimize
Alternatively, you can also check whether a DBA exists for φ by
just checking the output of:
ltlfilt -c --recurrence -f φ
If the answer is not syntactically obvious, that will just construct the
above DPA and check its acceptance condition under the hood.
Best regards,
Alexandre
756
days inactive
821
days old
3 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
Yoav Ben Shimon