- Spot - LRE

[bug] ltl2tgba gets stuck with this formula
by Jacopo Binchi 31 Oct '22

31 Oct '22

Dear Spot support team, I am a researcher at Developair Technologies. I write you looking for help with a formula that ltl2tgba cannot handle, possibly a bug. Here at Developair we have been using Spot for the past few months with great satisfaction. However, it seems that *ltl2tgba *cannot process the formula in attached file gb_formula.ltl . We let it run for quite some time (like hours) and it didn't terminate. On the other hand, Owl can process the same formula in a matter of a few milliseconds. We don't have any problem using ltl2tgba with other, similar formulas. It seems strange to us that Spot gets stuck with such a relatively simple formula, especially since in our experience Spot worked reliably well with other, way more complex formulas. Is it maybe a bug or something that we are doing wrong? Could you please help us? Please find some more details (version and command) below. Thank you. Best regards, J. Spot version: ltl2tgba --version > ltl2tgba (spot) 2.10.6 > > Copyright (C) 2022 Laboratoire de Recherche et Développement de l'Epita. > License GPLv3+: GNU GPL version 3 or later < > http://gnu.org/licenses/gpl.html>. > This is free software: you are free to change and redistribute it. > There is NO WARRANTY, to the extent permitted by law. > Command: ltl2tgba -S --deterministic --dot=s --output=output.txt -F gb_formula.ltl Using the "simplest" command "ltl2tgba -F gb_formula.ltl" produces the same result (that is, no result). For comparison, with Owl we used command: owl ltl2ldgba --state-acceptance -i gb_formula.ltl -o owl_gb.txt -- Jacopo Binchi jbinchi(a)developair.es Paseo de Miramón 170 20014 San Sebastián – Donostia Gipuzkoa (Spain) www.developair.es

2 2

Number of states and transitions
by pierreganty＠gmail.com 28 Oct '22

28 Oct '22

Hi all, I did not find how to get the number of states (reachable or not) of an automaton using autfilt (in particular the `--stats` option). The option provided by `autfilt --stats` is for reachable states only. I did find a workaround with `--hoaf` which outputs the automaton in HOA format and then getting the number from the `States:` header. For the number of transitions (reachable or not) I don't have a workaround. Since spot can compute these numbers easily, it seems handy (at least for me) to have a direct access to them thru the `--stats` interface. Thank you, Pierre.

3 3

Issue with Debian package signature
by Ocan Sankur 07 Oct '22

07 Oct '22

Hi all, I am trying to install spot on Ubuntu 20.04 following instructions from: https://spot.lrde.epita.fr/install.html But apt update complains about the signature: W: An error occurred during the signature verification. The repository is not updated and the previous index files will be used. GPG error: http://www.lrde.epita.fr/repo/debian stable/ InRelease: The following signatures were invalid: EXPKEYSIG 03D99E7444F2A84A LRDE Repository <admin(a)lrde.epita.fr> W: Failed to fetch http://www.lrde.epita.fr/repo/debian/stable/InRelease The following signatures were invalid: EXPKEYSIG 03D99E7444F2A84A LRDE Repository <admin(a)lrde.epita.fr> Could the signature be expired? I can actually install spot from source but Debian packages are useful for preparing artifact submissions. Thanks, Ocan

2 4

How to identify invalid transitions
by Raven Rothkopf 05 Aug '22

05 Aug '22

Dear Spot developers, Thank you so much for your helpful tool! We are undergraduate researchers at Barnard college and are using your tool for our summer research project. We are writing to ask if you would be able to help us understand a behavior of spot on a spec we are working with. We have the following small spec: ASSUME { G (! ((i1) && (i2))); } GUARANTEE { G (((o1) && (! (o2))) || ((o2) && (! (o1)))); (G (! ((i1) && (i2)))) -> (G (F (o2))); } From this, ltlsynt gives us: AP: 4 "i1" "i2" "o1" "o2" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic --BODY-- State: 0 [0&1&!2&!3 | 0&1&2&3] 0 [!0&!2&3 | !1&!2&3] 0 --END– Due to the ASSUME { G (! ((i1) && (i2)));}, the first transition in the hoa output should never happen. We understand that if a transition violates an assumption, it's still generated in hoa format because the system is free to choose any behavior and make any update. Some questions we have are: how does spot figure out if an assumption has been violated? Is there a flag that spot gives a transition that violates an assumption so that it can be dealt with differently? Instead of generating every possible behavior for the invalid transition, we are interested in removing it altogether. Is this possible to do through spot or do we need to come up with our own postprocessing algorithm? For context, we are working on a tool that takes a spec written in temporal logic and generates program code in a mealy machine format. We want to optimize the generated code so that it is as human-readable as possible. We appreciate any advice you can provide! Best, Leyi and Raven

2 2

Kripke, twa_product and twa_graph
by Pierre 22 Jun '22

22 Jun '22

Dear Spot devs, I am not sure how I am supposed to work with Kripke structures (which I imported using ltsmin) or `twa_product` (which I obtained using `otf_product` on the Kripke structure). In the screenshot below I can invoke 'exclusive_word' with no problems on a `kripke` and `twa_product` but the same is not true for 'contains' which returns a type error. The way I found to invoke 'contains' without errors is to use 'save' and then 'automaton' to read that same file again in order to get `twa_graph` as expected by `contains`. I am not sure this workaround is what the devs had in mind. Thank you for clarifying, PierreG [image: image.png]

2 1

Alphabet abstraction
by Pierre 04 Jun '22

04 Jun '22

Dear Spot devs, Is there a way for Spot to perform the alphabet abstraction available in GOAL as triggered with the `-a` switch when invoking the `alphabet` command? I paste the GOAL documentation about it below. Thank you, Pierre. - Alphabet -NAMEalphabet - Manipulate the alphabet of an automaton or a game.SYNOPSISalphabet -s [ -ap ] FILE_OR_LVALalphabet -e EXPR [ -ap ] FILE_OR_LVALalphabet -c EXPR [ -ap ] FILE_OR_LVALalphabet -r EXPR [ -ap ] FILE_OR_LVALalphabet -a EXPR [-R | -A | -S EXPR | -P EXPR | -ap ] FILE_OR_LVALDESCRIPTIONManipulate the alphabet of an automaton (or a game). This operation is directly applied to the input automaton. The returned value is always the new alphabet of the automaton (or the new atomic propositions if -ap is present). -s Simply return the alphabet of the input automaton or game. -ap Return the atomic propositions (or classical symbols) instead of the alphabet. -e Expand the alphabet by a list of propositions. -c Contract the alphabet by removing a list of propositions. -r Rename the propositions based on a map from a proposition to its new name. -a Abstract the alphabet based on a map from a predicate to its definition. -R Retain the transition symbols in alphabet abstraction. -A Only annotate the transitions with properties specified by -S and -P. -S Specify the name of the property that will store the symbols on the transitions in alphabet abstraction. -P Specify the name of the property that will store the evaluations of the predicates in alphabet abstraction. EXAMPLE alphabet -e "r" aut.gff alphabet -c "p" aut.gff alphabet -r "p=>r,q=>s" aut.gff alphabet -a "r=>p/\q" aut.gff alphabet -a "r=>p/\q" -A -P "Predicates" aut.gff

2 3

Building with Clang (on Mac)
by Shachar Itzhaky 17 May '22

17 May '22

Hello, There is a small hack in the lexer definition files `scanlt.ll` and `scanaut.ll` which fails the compilation on my Mac (macOS 12.3 arm64, Clang 13.1.6); they override `__STDC_VERSION__` which in turn wreaks havoc in the libc includes. I was able to fix the compilation using this small patch, which includes `libc-config.h` at the top in addition to `config.h`. I hope it would be useful to you. Cheers.

2 1

Regarding LTL with past
by David Lidell 16 May '22

16 May '22

3 4

Question regarding Spot operations on automata
by Edmond Irani Liu 22 Apr '22

22 Apr '22

Dear Spot team, greetings. This is Edmond Irani Liu, a Ph.D student at the Cyber-Physical Systems Group, Technical University of Munich. First of all, I would say thank you for your effort in developing such a great platform and tool! I have been using Spot lately, and have a few questions regarding automata manipulation in Spot. I attach a Jupyter notebook explaining my use case: we are using spot to compute the product automata of some LTLf formulas and our system described in Kripke structure. If I understand this (https://spot.lrde.epita.fr/tut12.html) page correctly, we need to append a new state at the end of the system that holds a proposition which becomes inactive at the end of our system. Could you give us a quick feedback if our formulation in the notebook is correct? There states z1-z8 are system states, and z9 is the extra state for Spot to correctly handle LTLf formulas. As we are trying to obtain the product automaton of a relatively large formula with our system, we assume that breaking down the formula and paralellizing the computation will observe a speed up in the computation. We would like to inquire if there exist operations like taking the union or intersection of the accepting runs of the automata? The concrete example is illustrated in the note book. Is there a documentation available somewhere explaining the functions of objects in the Python wrapper? I tried looking around but couldn't find one explaining those. An example is also attached. Thank you for your attention. Looking forward to hearing from you. Kind Regards, Edmond

2 1

How to read disjunction output?
by Mark Santolucito 15 Feb '22

15 Feb '22

Hi there, Thanks so much for the great tool! I am having trouble understanding the disjunction on state transitions. For example, I have the following small spec: ASSUME { G (p1); } GUARANTEE { G ((x) && (! (y)) || ((y) && (! (x)))); G (F x); G (F y); } From this, ltlsynt gives me: AP: 3 "x" "y" "p1" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic --BODY-- State: 0 [!0&!1&!2 | 0&1&!2] 1 [!0&1&2] 1 State: 1 [!0&!1&!2 | 0&1&!2] 1 [0&!1&2] 0 --END-- Should I understand the "[!0&!1&!2 | 0&1&!2] 1" to mean that when !2 is true, the system is free to choose from !0&!1 or 0&1? On a related note, due to the ASSUME in the spec, !2 should never be true anyway. Is there a way to filter this out of the model? For context, I am really looking to get a Mealy Machine out of ltlsynt which I can then convert into program code that would run in an infinite loop. Maybe I am just going about this the wrong way? Mark

2 1