Spot November 2020

spot@lrde.epita.fr

5 participants
7 discussions

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

intersection spot automatas
by Philip Schwartz 24 Nov '20

24 Nov '20

Hello Prof. Alexandre Duret-Lutz Is it possible to do a straightforward intersection between 2 automatas and check if the intersection has an accepting state? Regards, Phillip

2 5

membership query using spot
by רועי פוגלר 24 Nov '20

24 Nov '20

Hello, Is there a way to "ask" an automata if it accepts a word? e.g. a = spot.translate('a U b') a.accepts('b') ?T/F Regards, Roi

2 3

Question regarding Spot and MTL
by Edmond Irani Liu 18 Nov '20

18 Nov '20

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 will explain a bit about how we have used Spot in our research and then pose my questions below. We are recently working on formalization of traffic rules to further obtain traffic rule-compliant motion trajectories for automated vehicles. As a simple prototype, we have used Spot to translated some simple rules in LTL into a Büchi Automaton and later obtained its product automaton with the transition system of the discrete states of the vehicle. We could obtain some nice results with it : ) We are now trying to take one step further and to formalize more traffic rules, but came across the limitations of LTL, and switched to MTL for the reason that it is able to specify timed constraints, e.g. Always keep a safe distance to a leading vehicle if it did not perform a cut-in maneuver for the last 3 seconds. My questions are as follows: By any chance, is there some kind of workaround in Spot with which one can incorporate the mentioned timed constraints? (Last x seconds, future x seconds, ..) Of course our system state is also discrete with a 0.1 seconds step in time. If it is not possible with Spot, do you know some related model checker which can potentially handle this situation? I have been looking around but so far did not come across a tool which handles MTL/timed-automaton as nicely as Spot handles LTL. Thank you very much for your time reading this mail. I appreciate in advance for any feedback regarding the content. Kind Regards, Edmond

2 1

compare automata with exclusive_word
by Philip Schwartz 16 Nov '20

16 Nov '20

Hello Prof. Alexandre Duret-Lutz Thank you again for all your answers. I tried to compare 2 automats created using spot and got a a counterexample although they seems to be equal: aut2 = spot.translate(spot.formula("p1 U p2")) aut = spot.make_twa_graph(aut2.get_dict()) p1 = buddy.bdd_ithvar(aut.register_ap("p1")) p2 = buddy.bdd_ithvar(aut.register_ap("p2")) aut.new_states(2) aut.set_init_state(0) aut.new_edge(0, 0, p1 & buddy.bdd_not(p2)) aut.new_edge(0, 1, p2) aut.new_edge(1, 1, p1 & buddy.bdd_not(p2)) aut.new_edge(1, 1, p2) aut.set_acceptance(1, "Inf(1)") print(aut2.exclusive_word(aut)) # actual result - “p2; cycle{p1 & !p2}” # expected - None Best Regards, Phillipp

2 8

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

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Spot November 2020