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
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
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
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
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
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
