- Spot - LRE

Encode input formula into URL
by John Lång 23 Feb '21

23 Feb '21

Hello, I'd like to thank the developers for the awesome Spot's online LTL toolset! It's helping me a lot with my model checking project with Spin. This is exactly how formal methods should look like in the 2020'ies... If I may be so bold to request a feature, would it be possible to encode the input formula into URL, so that I could share a link with my fellow students? Best regards, John Lång

2 1

defrag_states: does it delete edges to erased states?
by Michaël Cadilhac 18 Feb '21

18 Feb '21

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.

2 2

LTLf simplification
by Walke, Homer 04 Jan '21

04 Jan '21

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

2 1

model checking using spot
by Philip Schwartz 31 Dec '20

31 Dec '20

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

2 1

Spot question
by Roei Nahum 08 Dec '20

08 Dec '20

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

2 2

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