Spot October 2020

spot@lrde.epita.fr

3 participants
8 discussions

by Ayrat Khalimov

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

3 years, 8 months

comapre spot automata

by רועי פוגלר

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

4 years, 2 months

check if word exists in language

by רועי פוגלר

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

4 years, 3 months

print spot automata using graphviz

by רועי פוגלר

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

4 years, 3 months

Spot tool

by רועי פוגלר

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

4 years, 3 months

Spot tool

by רועי פוגלר

4 years, 3 months

Re: [Spot] Explicit order of sub-formulas in formula constructor

by Alexandre Duret-Lutz

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

4 years, 4 months

Explicit order of sub-formulas in formula constructor

by Niklas Metzger

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

4 years, 4 months

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Spot October 2020