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
Hi Alexandre,
> However now that you have written this down, I think your interpretation r
> SSI => r[+] SSI and r[*] SSI is also sound, but I have no proof for this.
I tried to prove this, but failed, and then found a counterexample: e.g. if L = a[+];(!a)[+];a[+], then L is si but both L[+] and L[*] are not si. I believe if one in addition requires that L is prefix-closed or suffix-closed, then the result would hold (I have an idea how to prove this).
> > > I would suggest that at the SERE level the rule for the n-ary
> concatenation
> > > r1;r2;r3;...;rn
> > > could be extended so that the entire concatenation is SSI iff each
> > > ri is SSI and at most one of them rejects the empty word.
Again, this seems wrong, with the following counterexample:
If K=[*0] | ((!a)[+] ; a[+]) and L=a[+] then K contains the empty word, K and L are si, but K;L is not si: it accepts !a;a;a but rejects !a;a.
I think the result would hold if one replaces the assumption that K or L contains the empty word by K being prefix-closed or L being suffix-closed.
> > > Transposed to {s}|=>t, that rule would state that {s}|=>t is SSI iff
> > > - s and t are both SSI, and
> > > - s recognizes the empty word
Again, I think we could require either s being prefix-closed or t being suffix-closed. Note the symmetry with s;t :-)
Regards,
Victor.
Hi Alexandre,
> Currently r[*i:j] is SSI iff j=inf and i<=1 (used to be i==1 before your mail).
I'm not sure if this is correct, as it implies that r* is ssi if r is ssi, even if r is not a Boolean, but Dax at al. mentioned that the use of * has to be restricted (but without giving an example of ssi violation). So it's your word against theirs :-) Do you have a proof? (I played with Spot a couple of minutes and could not quickly find a violation, so you may well be right.)
> [=i:j] and [->i:j] are sugar on top of ; and [*i:j], so it follows from those
> definitions.
> (Spot's AST has no representation of those operators, they only exist in the
> parser and printer.)
The situation with [=i:j] and [->i:j] is less boring than that! E.g. b[->1:$] would be translated to something like (!b[*];b)[+], which is si but not ssi. I've worked out the cases for these operators as follows (the proofs rely on the magic regex equivalence (a[*];b)[+];a[*] = (a|b)[*];b[+] which can be checked e.g. here: https://regex-equality.herokuapp.com/):
Lemma: b[->i:j] is si iff j=0 or (j=$ and i<=1)
j=0: then i=0 and so b[->i..j] = (!b[*];b)[*0] = [*0], so si
j!=0 and j!=$: then b[->i..j] accepts b[*j] but not b[*j+1], so not si
j=$ and i>1: then b[->i..j] accepts b[*i] but not b[*i-1], so not si
j=$ and i=1: then b[->i..j]=(!b[*];b)[+]=[by regex magic]=(!b|b)[*];b[+]=[*];b[+], so si
j=$ and i=0: then b[->i..j]=(!b[*];b)[*]=[*0]|above line, so si
Lemma: b[=i:j] is si iff j=0 or (j=$ and i<=1)
j=0: then i=0 and so b[=i..j] = (!b[*];b)[*0];!b[*] = !b[*], so si
j!=0 and j!=$: then b[=i..j] accepts b[*j] but not b[*j+1], so not si
j=$ and i>1: then b[=i..j] accepts b[*i] but not b[*i-1], so not si
j=$ and i=1: then b[=i..j] = (!b[*];b)[+];!b[*] = [by regex magic] = (!b|b)[*];b[+];!b[*] = [*];b[+];!b[*], so si
j=$ and i=0: then b[=i..j] = (!b[*];b)[*]];!b[*] = (e|(!b[*];b)[+]);!b[*] = !b[*] | (!b[*];b)[+];!b[*] = [due to previous case] = !b[*] | [*];b[+];!b[*] = [*] so si
> cl(r) in Dax et al. is the same as {r} in Spot.
>
> But you are not the only one having trouble with closure :-) See
> https://gitlab.lrde.epita.fr/spot/spot/issues/242
So, just to confirm, Dax et al.'s cl(), PSL's {}, and Spot's {} are all the same, aren't they?
> I would suggest that at the SERE level the rule for the n-ary concatenation
> r1;r2;r3;...;rn
> could be extended so that the entire concatenation is SSI iff each ri is SSI and
> at most one of them rejects the empty word.
Wow, that is a nice generalisation! Do you have a proof? I think it will be nicer and easier to state for the binary ";", and then the n-ary case immediately follows.
> Transposed to {s}|=>t, that rule would state that {s}|=>t is SSI iff
> - s and t are both SSI, and
> - s recognizes the empty word
I did some experiments with the online tool, and what you say seems correct, but I don't understand why there is asymmetry w.r.t. s (but not t) recognising the empty word - the intuition of s;t seems symmetric?
> If we had complementation of SERE, would first_match(r) be implementable
> as r && ((!r);1[+]) ?
I think you meant r && !(r;[+]), which is a nice idea, but Spot won't accept it (I guess), and generally it seems computationally expensive. I think at the level of automata one can simply get an NFA for r, and then delete all arcs from accepting states?
The other things you mentioned, like $rose etc. seem to need past modalities? Or you can mix state-based and action-based logics?
Generally, "throughout" and "within" are just syntactic sugar, so should be easy to add. The ?: can be added as syntax sugar, but hopefully one can do better than that and avoid the exponential blow-up due to repeating A in A&B|!A&C - this is in fact just a theoretical blow-up, unlikely to happen in practice. The first_match requires some work with automata, but seems possible. I'd say Spot is just a few steps away from full alignment with SVA and PSL.
Regards,
Victor.
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.
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.
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
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).
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
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)
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)
