October 2020 - Spot

Walking through BDD formula in python
by Ayrat Khalimov 26 May '21

26 May '21

hi! With the aid of SPOT I am developing a counter-example guided synthesizer in python. See [1] if interested for details. My question is: I am trying to parse twa_run in python, namely, parse the labels of the each step (`spot.impl.step`). Is there a python way to walk through BDD? (The label is a simple cube expressed in BDD, and I need to convert it into my internal structure) (yes, this is rather a question about python interface for buddy) (no, that is not feature request:) if not possible, I will simply print the label and parse the string, that is not crucial) [1] The idea is - guess the model, - then model check it and get a counter-example - then encode the counter-example into the "guesser" (which uses an SMT solver) thanks, Ayrat

2 5

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