- Spot - LRE

Walking through BDD formula in python
by Ayrat Khalimov 26 May '21

26 May '21

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

2 5

fail to install spot
by Jueming Hu 15 Apr '21

15 Apr '21

Good afternoon, I am Jueming, a Ph. D. student at Arizona State University. I would like to use spot for my research, such as getting the graph of an LTL formula. I downloaded 'linux-64/spot-2.9.6-py38_2.tar.bz2' and ran 'conda install -c adl spot' within the extracted folder. 'spot 2.5.2' is shown in conda list and also in python packages. However, 'import spot' doesn't work. The error says, 'No module named 'spot''. I have also tried 'linux-64/spot-2.9.4-py38_2.tar.bz2', 'conda install -c adl/label/adl spot', 'conda install -c adl/label/dev spot', append system path before import spot, and export LD_LIBRARY_PATH. But spot still doesn't work on my pc. Could you please help me install spot? Thanks in advance and looking forward to hearing from you. Best, Jueming

2 1

Question about Transfoming from Non-deterministic Automata to Deterministic Automata
by Meng Ruijie 23 Mar '21

23 Mar '21

Dear Spot Team, Thanks for providing a wonderful tool. During constructing Buchi automata for LTL, Spot always shows non-determinism automata although I select the "deterministic" item. Would you mind telling me how to construct deterministic automata with Spot? Here is one LTL: !(false R (iusr2_ai3_re13 & (! X (true U iusr2_ai3_re14) | X (true U (iusr2_ai3_re14 & (true U ousr2_ai3_ce8)))))). The following is its automata but non-determinism. [cid:83ad2cd0-bc60-443c-b387-4bc7953c05d2] Looking forward to your response. Kind Regards, Ruijie

2 1

Translations to DPA
by Tobias Meggendorfer 18 Mar '21

18 Mar '21

Hi, I'm using / comparing Spot and other tools in the Rabin to Parity translation. I have two questions (to ensure my comparison is fair): 1) I want to minimize the input automata using Spot to remove the effects of preprocessing done by each tool as much as possible. However, I require that the acceptance condition remains a Rabin condition. Right now, I am using the call autfilt --remove-dead-states --cleanup-acceptance --remove-unused-ap --simplify-exclusive-ap --simplify-acc --partial-degeneralize --generalized-rabin --deterministic The last two are an effort to ensure that simplify-acc doesn't change the acceptance condition. 2) What are the ways to tell spot to translate DRA to DPA? Right now, I am using autfilt --hoa --deterministic --parity. This seems to be a sort of black box (which is fine with me). Just to make sure: Are there other DRA-to-DPA translations included in Spot which are worthwhile to be investigated? Cheers, Tobias

2 3

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