HI,
My name is Roei Nahum. I recently got to know SPOT, and first of all, I want to thank you for this great platform. I'm having an issue and I'll appreciate if you can assist.
I use SPOT in order to translate temporal formulas into automata. To do so, I downloaded spot, and wrote a C++ program based on SPOT API.
The program I wrote is basically like this:
...get the formula...
spot::parsed_formula cex_pf = spot::parse_infix_psl(formula);
if(cex_pf.format_errors(std::cerr)){
cout << "Invalid formula syntax: " << formula << endl;
exit(1)
}
spot::translator trans;
trans.set_type(spot::postprocessor::BA);
trans.set_pref(spot::postprocessor::Small);
twa_graph_ptr aut = trans.run(cex_pf.f);
...print the automata...
I tried running this code on several formulas, and it works great.
The problems started when I processed this formula:
G({(a)} |=> {(b)[*32]})
The code is running for a long time (more than a hour) without giving a result.
Did it get stuck? Is there any way I can make it work?
Thanks,
Roei Nahum
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
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
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
