- Spot - LRE

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

Segfault when postprocessing large automaton
by Reed Oei 20 Apr '20

20 Apr '20

Hello, I am encountering a bug where Spot segfaults when I try to postprocess a relatively large automaton. I have uploaded the file to http://reedoei.com/files/smaller-inner.aut.zip; it has 113930 states and 1537155 edges. I tried to come up with a smaller example but was having trouble doing so. Below is the sequence of commands, using the Python bindings, to reproduce this bug for me: import spot A = spot.automaton('smaller-inner.aut') B = A.postprocess('BA', 'Deterministic', 'Low') # Crashes here B.save('postprocessed.aut') I also tried using various other others for postprocess such as Small and Low, or Any and High (because Any and Low/Medium does nothing). I am using Ubuntu 18.04, Python 3.6.9, and Spot 2.8.7 (but also tried with 2.8.6). Thank you, Reed Oei

2 3