- Spot - LRE

ltlfilt filtering duplicates
by David Müller 18 Mar '21

18 Mar '21

Hi Alexandre, I hope you are not affected too badly by COVID and you and your family can deal with it in a good way. Simon and I stumbled over some slight problems with ltlfilt in combination with the flags -u and --relabel-bool=pnn. We expected to remove the duplicates, and thus being idempotent. However, we came across a set of LTL formulas, where two applications of ltlfilt -u --relabel-bool=pnn delivered a different result from applying it once. I attach the set of LTL formulas (ltlfilt-duplicates/ base.ltl in the archive) and a short script to evaluate the problem (ltlfilt- duplicates/reproduce.sh). I also tried to input a sorted list, it changed the numbers, but not the problem of being not idempotent. Could you tell us, whether we misunderstood something? Best regards, David

2 1

Re: [Spot] set property "original-states" in function "purge_dead_states()
by Alexandre Duret-Lutz 06 Mar '21

06 Mar '21

Tobias John <tobias.john(a)tu-dresden.de> writes: > thanks for your quick response. Your suggestion solves my problem. > > I think a function like "set_default_original_states()" would be > helpful but it is not necessary. In my opinion, it is more important > to mention somewhere in the documentation, e.g. at > > https://spot.lrde.epita.fr/concepts.html#named-properties > > that one needs to set the property somewhen before transforming the > automaton. Yes. The usage is however not very uniform. Some functions, like degeneralize() have to maintain the equivalent of "original-states" in order to work. This function will always define "original-states" if it wasn't present, because that comes for free. However if "original-states" was defined previously, the two mappings will be composed at an extra-cost.

1 0

set property "original-states" in function "purge_dead_states()
by Tobias John 05 Mar '21

05 Mar '21

Hello, I am using Spot for my Master Thesis. I try to simplify omega-automata by removing unnecessary states, e.g. states that are unreachable. The function "purge_dead_states()" does the job but there is an issue: for my application, I need to know the original state numbers of the states in the resulting (smaller) automaton, i.e. I need to map the states of the resulting automaton to the states of the original automaton. Is there some way to get the original state numbers from the reduced automaton? My intuition is that the property "original-states" would be suitable to store the original state numbers but the function "purge_dead_states()" does not set this property. In my opinion, the function "purge_dead_states()" setting the property "original-states" would be a useful feature to be included in future releases of Spot. Best regards, Tobias

2 1

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