April 2023 - Spot

SPOT questions
by Yoav Ben Shimon 06 Jun '23

06 Jun '23

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

2 3

Possible to allow for product_or without completing left/right automata
by Marcel Gerber 09 May '23

09 May '23

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

2 1

APT install of python3-spot requires python version <<3.10
by Marcel Gerber 28 Apr '23

28 Apr '23

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

1 0

Spot bus error
by Beutner, Raven 20 Apr '23

20 Apr '23

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.

2 1