Spot

spot@lrde.epita.fr

209 discussions

by Jueming Hu

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

3 years, 9 months

Question about Transfoming from Non-deterministic Automata to Deterministic Automata

by Meng Ruijie

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

3 years, 10 months

Translations to DPA

by Tobias Meggendorfer

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

3 years, 10 months

ltlfilt filtering duplicates

by David Müller

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

3 years, 10 months

Re: [Spot] set property "original-states" in function "purge_dead_states()

by Alexandre Duret-Lutz

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.

3 years, 11 months

set property "original-states" in function "purge_dead_states()

by Tobias John

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

3 years, 11 months

Encode input formula into URL

by John Lång

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

3 years, 11 months

defrag_states: does it delete edges to erased states?

by Michaël Cadilhac

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.

3 years, 11 months

LTLf simplification

by Walke, Homer

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

4 years, 1 month

model checking using spot

by Philip Schwartz

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

4 years, 1 month

← Newer
1
...
4
5
6
7
8
9
10
...
21
Older →

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Spot