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
Hello,
I notice that `product_or` necessarily runs `complete` on both input
automata [see this line in spot/twaalgos/product.cc
<https://gitlab.lre.epita.fr/spot/spot/-/blob/b487ff4190cdec4094154486bb8c04…>].
In contrast, this is not the case for the "normal" `product`.
If my thinking is correct, this would not be necessary if both input
automata are Büchi automata, correct? Because the union of two incomplete
Büchi automata is an incomplete Büchi automaton again, and the product
automaton construction applies as normal as far as I can tell.
Would it be possible to allow for this, potentially by introducing another
method or exposing the `product_aux` function (incl. from Python)?
Right now, running `product_or`, even on small input automata, produces
absolutely unwieldy automata that are impossible to interpret.
This is mostly due to my use case, where I'm using letters of an alphabet
more akin to a standard DFA model, and encoding a symbol of `a` into the
preposition formula `a & !b & !c` etc.
This works well with single automata and with intersections, but not with
unions sadly.
Your help would be very much appreciated,
Marcel
Hi,
I'm a master student at RWTH Aachen, and am using spot as part of my master
thesis. Thank you very much for developing and providing this awesome tool!
However, I noticed that when attempting to install python3-spot via `apt
install`, it fails with:
The following packages have unmet dependencies:
python3-spot : Depends: python3 (< 3.10) but 3.10.6-1~22.04 is to be
installed
E: Unable to correct problems, you have held broken packages.
Checking out the package index at
https://www.lrde.epita.fr/repo/debian/stable/Packages (Cmd-F for
`python3-spot_2.11.5.0-1`), I notice that the package indeed specifies
`python3 >= 3.9, python3 << 3.10` as a dependency, making it so it can only
be installed alongside Python 3.9.
I don't know what this restriction is used for, and would greatly
appreciate it if it can be removed.
Thank you,
Marcel
Dear spot team,
I think I found a bug in spot.
When I run
% cat foo.hoa
HOA: v1
States: 1
Start: 0
AP: 3 "l0" "l1" "l2"
acc-name: generalized-Buchi 0
Acceptance: 0 t
--BODY--
State: 0
[(0&1)] 0
[(2)] 0
[(!2)] 0
—-END--
%autfilt --small -S foo.hoa
I get a bus error.
It seems that options —small and -S are both necessary to reproduce the bug. Similarly, none of the transitions in the automaton can be removed.
I am running spot version 2.11.4 on an MacBook Pro with M1 Pro CPU compiled with --disable-python.
Given that this seems to be a “low-level” system error, it could very well be that it is an issue with my machine setup. In this case: Do you have any idea how to fix this?
Thanks already for your help!
All the best,
Raven
PS: The current download link for the most recent version of spot (https://spot.lre.epita.fr/install.html) claims to download version 2.11.4 but actually still points to version 2.11.3.
