Spot

spot@lrde.epita.fr

212 discussions

by Victor Khomenko

Dear Spotters, Could anyone explain Spot's algorithm for checking whether a PSL formula is syntactically stutter-invariant (ssi), including all supported PSL operators? I'm aware of Dax et al. ATVA'09 paper, but the syntax there is rather rudimentary, and there seems to be more to this. E.g. {a[=2:3]}|->b is rewritten (using the online spot's toolkit) into a R (!a | X({a[->1..2]}[]-> (b & X(b W a)))) and yet it is classified as ssi in spite of all the Xs. On the other hand, a seemingly similar {a[->2:3]}|->b is classified as si but not ssi for some reason... Many thanks, Victor.

6 years, 2 months

Bug if generating deterministic Emerson-Lei

by David Müller

Hi Alexandre, I run the experiments and found two formulas where ltl2tgba did not finish correctly. The formulas were & | G F p0 F G p1 | G F ! p1 F G p2 & & | G F p0 F G p1 | G F ! p1 F G p2 | G F ! p2 F G ! p0 The according command-line was: ltl2tgba -D --generic -C -S --lbt-input -f ${FORMULA} Output was: ltl2tgba: direct_simulation() requires separate Inf and Fin sets Best, David

6 years, 2 months

check equivalence from files?

by Stephen Siegel

Question about the command line interface. I know something like ltlfilt -f 'a U (b U a)' --equivalent-to 'b U a’ can be used to determine if two LTL formulas are equivalent. Is there a way to do that if both formulas are in files? From the man page I could only see how to make the first formula come from a file (-F).

6 years, 2 months

Spot documentation

by Yannick Molinghen

Dear Madam, dear Sir, I am just starting using spot (with python) for a university project (ULB, Brussels) and my team mates and I have spent quite some time just figuring out how to use accepting states in a Buchi automaton. We found it inconvenient and more importantly very difficult to find in the documentation (it was located in the far end of the doc...) to use `automaton.prop_state_acc(True)` in order to set states accepting instead of edges. It could be interesting to specify how to do this in a clear way, why not in the code examples? A good place for this would be this page <https://spot.lrde.epita.fr/tut22.html> for instance. Yours sincerely, Yannick Molinghen

6 years, 2 months

Exclusive-AP and Merge Transitions

by hashim ali

Hi, How can I use Exclusive-AP and merge transitions in python to reduce my automaton and the number of transitions? An example would suffice. Thanks and Regards, Hashim Ali Research Assistant Laboratory for Cyber-Physical Networks and Systems (Cyphynets) Lahore University of Management Sciences (LUMS)

6 years, 3 months

Highlight Words on the Automaton

by hashim ali

Hi, Similar to highlighting runs on the automaton, is it possible that I can convert a word to a corresponding run and then I can highlight it on the automaton? Thanks and Regards, Hashim Ali Research Assistant Laboratory for Cyber-Physical Networks and Systems (Cyphynets) Lahore University of Management Sciences (LUMS)

6 years, 3 months

Generate Words for verification

by hashim ali

Hi, I am using spot.from_ltlf().translate() to translate LTL rules into a finite automata (with alive property). Now I want to verify certain words that whether they are accepted by the automata or not. These words will be generated from a powerset of the set of atomic propositions. Lets suppose I have AP = {a,b,c,d}. How do I generate words from the powerset of AP and verify it on the automata. Should the word always contain a cycle and a prefix part. If yes, what should be the cycle part and what should be the prefix part. I will be waiting for your response. Thanks and Regards, Hashim Ali Research Assistant Laboratory for Cyber-Physical Networks and Systems (Cyphynets) Lahore University of Management Sciences (LUMS)

6 years, 3 months

Weighted Automata

by hashim ali

Hi, Is there any support for weighted Automata in spot. Here is a thing I want to implement. I want to test certain words on a certain automata, if a word is rejected by the automata I want to add a new transition (weighted transition) to this automata and later on if that same word comes for verification, I want this automata to return this weight corresponding to this transition. Thanks and Regards, Hashim Ali Research Assistant Laboratory for Cyber-Physical Networks and Systems (Cyphynets) Lahore University of Management Sciences (LUMS)

6 years, 3 months

C interface for Spot?

by Stephen Siegel

Is there a C (not C++) interface for Spot? I want to call Spot from my C program. Thanks.

6 years, 3 months

Re: [Spot] Questions regarding handling of Kripke structures in Spot

by Alexandre Duret-Lutz

Dear Patrick, (Please keep the mailing list in copy so that these explanations get archived and then indexed by search engines.) On Tue, Mar 5, 2019 at 8:58 AM Halder, Patrick <patrick.halder(a)tum.de> wrote: > When I have the twa_product automaton with its respective acceptance states, > how can I find out, to which states of my original Kripke structure they correspond to. > I read somewhere in the spot examples that the labeling of the twa_product states > (of the form <*,*>) has just cosmetic reasons and does therefor not give any help. Let's say you have built the product between two automata autx and auty: prod = spot.product(autx, auty) then pairs = prod.get_product_states() will return an array of pairs of the form [(x0,y0),(x1,y1),....]. State i in the product corresponds to states pairs[i][0] in autx, and pairs[i][1] in auty. See https://spot.lrde.epita.fr/ipynb/product.html around cell 10 for a concrete example, and a tip about using show("1") in this context. > Is it even possible to do this, meaning getting directly from the acc states of the product automaton to the acc states/runs of the Kripke structure? You should probably look for the accepting SCCs of the product, not only its accepting states. You could list all states that belong to acceptings SCCs of the product with something like si = spot.scc_info(prod) n = si.scc_count() for i in range(n): if si.is_accepting_scc(i): for s in si.states_of(i): print(s) Unfortunately, we do not yet have any online example of use of scc_info in Python. You can find some in the test suite, or simply look at the C++ documentation for this class https://spot.lrde.epita.fr/doxygen/classspot_1_1scc__info.html > Or do I have to get the accepting runs of the product automaton, e.g., with the x.intersecting_run(y) method and reason with it about the accepting runs in the Kripke structure? This will only return one accepting run. -- Alexandre Duret-Lutz

6 years, 3 months

← Newer
1
...
10
11
12
13
14
15
16
...
22
Older →

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Spot