- Spot - LRE

LTL formula accepts/rejects a word
by Philipp schwartz 12 Nov '20

12 Nov '20

Hello, My name is Phillip and I tried to use Spot tool to "play" with LTL formulas. My question is, is it possible to get boolean result if LTL formula accepts or rejects a word? e.g. In case the LTL formula is "aUb" is it possible to check that the formula is accepting "cycle(b)"? Best regards, Phillip

3 10

comapre spot automata
by רועי פוגלר 08 Nov '20

08 Nov '20

Hello, 1. I tried to compare 2 spot automata as described here -> https://spot-sandbox.lrde.epita.fr/notebooks/examples%20(read%20only)/conta… (last section) but, I got a counterexample which I think is not correct since both automata are not accepting this counterexample: I tried to compare automata which presents P1 U p2 and automata which answers "no" to everything and I got cycle{P1 & !p2} as a counterexample. attached picture with the code and examples from Ide. 2. Is there a way to transfer spot automata to LTL? Regards, Roi

3 8

check if word exists in language
by רועי פוגלר 22 Oct '20

22 Oct '20

Hello, When my input is a word (string such as 'p1 & !p2; cycle{p2}') and spot automata, (e.g. f = spot.formula("p1 U p2") aut = spot.translate(f, 'low') ) is it possible to check if the word exists in automata? Regards, Roi

1 1

print spot automata using graphviz
by רועי פוגלר 21 Oct '20

21 Oct '20

Hello, How can I print the automata graph? aut.show() and display(aut) does not work in simple python file (not jupyter notebook) Regards, Roi

2 1

Spot tool
by רועי פוגלר 20 Oct '20

20 Oct '20

My name is Roi and I'm an Msc student at Bar Ilan University (Israel). I'm trying to use the spot tool (python version) and I'm trying to figure out how to build spot-automata (spot.twa_graph object) type when my input is the edges, states and accepting states. can you help me please with that? In addition, is there an example of Angluin implementation using Spot? Regards, Roi

2 4

Spot tool
by רועי פוגלר 19 Oct '20

19 Oct '20

My name is Roi and I'm an Msc student at Bar Ilan University (Israel). I'm trying to use the spot tool (python version) and I'm trying to figure out how to build spot-automata (spot.twa_graph object) type when my input is the edges, states and accepting states. can you help me please with that? In addition, is there an example of Angluin implementation using Spot? Regards, Roi

1 0

Re: [Spot] Explicit order of sub-formulas in formula constructor
by Alexandre Duret-Lutz 06 Oct '20

06 Oct '20

On Tue, Oct 6, 2020 at 5:09 PM Niklas Metzger <niklas.metzger(a)cispa.saarland> wrote: > > Hi Alexandre, > > thank you for your fast response! I’m a bit confused on the meaning of creation time: > > >>> import spot > >>> f = spot.formula("Fa") > >>> ff = spot.formula("Ga") > >>> spot.formula.Or([f, ff]) > spot.formula("Fa | Ga") > >>> f = spot.formula("Ga") > >>> ff = spot.formula("Fa") > >>> spot.formula.Or([f, ff]) > spot.formula("Fa | Ga") > >>> n = spot.formula("Ga") > >>> nn = spot.formula("Fa") > >>> spot.formula.Or([n, nn]) > spot.formula("Fa | Ga") > > Is there some internal representation that does not create new objects if seen before? Yes. You can also use print(f.id()) to display the "serial number" of formula f. That's an identifier incremented for each new formula (new in the sense "not seen before"). This value is used to sort formulas (e.g., order the operands), or as hash value. But it is not necessarily unique in the case that so many formulas are created that the counter loops. -- Alexandre Duret-Lutz

1 0

Explicit order of sub-formulas in formula constructor
by Niklas Metzger 06 Oct '20

06 Oct '20

Hi! I’m currently using Spot to manipulate LTL formulas (using Python) and encountered the following behaviour: The result of "spot.formula.Or([x,y])” possibly changes the order of the subformulas, e.g. globally will appear in front of finally. Is there a way to build formulas that stick to the given order? Best and thanks in advance Niklas

2 1

Question on LTL to buechi automata
by Zhen Dong 24 Sep '20

24 Sep '20

Dear Spot team, Thanks for developing the nice tool Spot. I am a researcher at National University of Singapore using Spot in my research. I have a question about translating LTL to buechi automata using spot. My LTL properties are constraints over input/output sequences of a program, e.g., output W, output P always responds to input B (false R (! iB | (true U (oW & X (true U oP))))) where iB indicates that input B and oP indicates output P. The buechi automata of the negation of above formula given by Spot is in the following: [image: image.png] Here is a input/output trace to be evaluated: iH oZ iH oR iC oR iH oX iC oR iH oX iD oZ iJ oT iD oT iF oR iH oP iH oR iH oP iH oR iH oP iH oR iH oP iH oR iH oP iH oR iH oP iH oR iH oP iH *What I do not understand is that the proposition on the transition from state 0 to state 2 is iB & oW. How can I interpret it?* Given the input/output trace, there is no element that is iB and at the same time is oW. I assume the verification feeds element in the trace to the automata one by one. Do I miss something e.g., wrong configuration on the translation or some basic knowledge about verification? Can you give me some advice on this issue? Thank you very much. Best regards Zhen -- Zhen Dong Senior Research Fellow National University of Singapore https://www.comp.nus.edu.sg/~dongz/

2 2

Spot Polish Notation Parsing
by Niklas Metzger 31 Jul '20

31 Jul '20

Hi Spot Team! First of all, thanks for providing and maintaining such a great tool! I stumbled over a problem with formulas in polish notation: Parsing a formula like “-> a b” returns the “syntax error, unexpected implication operator” (Also tested on the website). It seems like implication and equivalence are not supported by that parser. Is there a technical reason for that and if not, could you give me a hint how to implement it? Thanks in advance Niklas Metzger

2 1