Hi there,
In a preprocessing step, I want to flush a few states from a TωA. The one
method that seems to be available is defrag_states, the description of
which having the expected semantics.
However, after defrag, it sometimes happens that the dst of some
transitions points to delete states (-1U). The code of defrag_states in
graph.hh removes the outgoing transitions of deleted states but does not
seem to flush the transitions *pointing to* deleted states—is this the
expected behavior?
Cheers,
M.
Hi!
I know Spot doesn't provide much support for LTLf (LTL with finite trace
semantics) but I need to simplify some LTLf formulas. I was wondering which
tl_simplifier_options, if any, would simplify according to the semantics of
LTLf, i.e reduce_basics, synt_impl, etc. I know that using all the
rewritings wouldn't work since many of them only apply to LTL and not LTLf
but I'd like to use any rewritings that do apply to LTLf. Would anyone be
able to point me in the right direction? Alternatively do you know of
another software package that might do LTLf simplification?
Thanks!
Homer
Hello,
If I have a deterministic automata and an LTL or python function which gets
a word and return T/F.
Is it possible to set model checking for the dfa? to get a counterexample
which distinguishes the dfa and the LTL/ python target function?
Regards,
Phillip
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
