- Spot - LRE

Re: [Spot] syntactic stutter-invariance
by Victor Khomenko 27 Apr '19

27 Apr '19

Thanks Alexandre, > The syntactic SI subset we catch should correspond to siPSL. (If you know a > larger subset, that would be a welcome addition.) What I'd like is to extend the ssi syntax to "sugar" operators too. Unfortunately, my intuition is unreliable with ssi :-( To recap, Dax et. al. syntax for siSERE is: r ::= [*0] | b[+] | b[*];r | r;b[*] | r:r | r|r | r&&r | r[:+] I believe one can add the following: - b[*], as b[*]=([*0] | b+), e.g. Spot doesn't recognise it's ssi - (r & r), as (A & B) = (A;[*] && B)| (A && B;[*]) - any_formula[*0], as it's [*0] - if the overall formula is {b}, it's ssi. Another problem is that, say, (a[*];b[*]);(c[*];d[*]) is not ssi, but can be transformed to ssi form using associativity of ";". Now, for special cases of i and j, the r[*i:j], b[*i:j], r[=i:j], r[->i:j] may be ssi (I tried to work these out, but was confused by the {a[=2:3]}|->b result). PSL closures: cl(r) is part of ssi syntax so ok not sure about {r} - it might be obvious, but I don't understand closures well, especially if negations are involved... {r}! is equivalent to {r}|->1, so I think it's ssi Bindings: |-> is ssi, but I'm not sure about when |=> might be ssi? If you ever going to support SVA-like "throughout" and "within", they are ssi: A throughout B = (A* && B), A is Boolean A within B = (([*];A;[*]) && B) Also, SVA's first_match operator is interesting - do you know of a general way of translating it to other operators, or, alternatively, do you plan to ever add it? (BTW, it would also be nice to have C-like ternary operator ?: to avoid the exponential blow-up in its translation.) > > {a[->2:3]}|->b > I can't reproduce this one. It is shown as stutter-sensitive for me. Sorry, my bad, it's indeed ss. Thanks, Victor.

2 1

syntactic stutter-invariance
by Victor Khomenko 26 Apr '19

26 Apr '19

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.

2 1

Bug if generating deterministic Emerson-Lei
by David Müller 26 Apr '19

26 Apr '19

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

2 1

check equivalence from files?
by Stephen Siegel 05 Apr '19

05 Apr '19

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).

2 1

Spot documentation
by Yannick Molinghen 03 Apr '19

03 Apr '19

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

2 1

Exclusive-AP and Merge Transitions
by hashim ali 01 Apr '19

01 Apr '19

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)

2 1

Highlight Words on the Automaton
by hashim ali 01 Apr '19

01 Apr '19

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)

2 1

Generate Words for verification
by hashim ali 27 Mar '19

27 Mar '19

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)

2 4

Weighted Automata
by hashim ali 25 Mar '19

25 Mar '19

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)

2 1

C interface for Spot?
by Stephen Siegel 25 Mar '19

25 Mar '19

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

2 1