Hi Yoav,
Sorry for this delayed answer.
Yoav Ben Shimon yoavbenshimon@gmail.com writes:
I ran into a couple of issues when using SPOT in a project. I'll be glad for any assistance.
- 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.
- 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.
