On Fri, Apr 26, 2019 at 3:46 PM Victor Khomenko <victor.khomenko@newcastle.ac.uk> wrote:
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 :-(
Getting the intuitions with those PSL operators is quite hard. The online app should now be fixed. Note that this online check is lazy: if the syntactic check says it's SI, it will not try the automaton-based check. In doubt, you can always go to http://spot-sandbox.lrde.epita.fr/notebooks/examples%20(read%20only)/stutter... and use the function in cells 11-12 to test the sutter-invariance of PSL formulas without relying on the syntactic checks.
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
Agreed (and done).
- (r & r), as (A & B) = (A;[*] && B)| (A && B;[*])
This was already implemented.
- any_formula[*0], as it's [*0]
That's a trivial simplification : Spot always store [*0] in this case so there is nothing to implement.
- if the overall formula is {b}, it's ssi.
Again, when the SERE is just a Boolean formula, trivial identities for bindings operators replace those by conjunctions or disjunctions, so the case is automatically solved.
Another problem is that, say, (a[*];b[*]);(c[*];d[*]) is not ssi, but can be transformed to ssi form using associativity of ";".
For Spot that's a n-ary concatenation, regardless of where you put the parentheses. That's currently recognized as siSERE if it contains at least n-1 terms of the form b* and if the remaining term is siSERE.
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).
Currently r[*i:j] is SSI iff j=inf and i<=1 (used to be i==1 before your mail). [=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.)
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
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
Bindings: |-> is ssi, but I'm not sure about when |=> might be ssi?
since {s}|=>t equals {s;1}|->t my intuition is that as far as SI goes, this patterns behaves likes s;t (where s is regular and t is ω-regular) 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. Doing so would catch patterns such as {(a[+]|b[*]);(c[+]|d[*])}|->e which are SI, but not SSI without this extended rule. 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 For instance {(b[*]|a[+]);c[*]}|=>d is SI.
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)
These could easily be added as syntactic sugar in the parser and printer, but there is no need to support those in the AST, so no need for siPSL rules.
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.)
I discussed with some SVA user about one year ago, and noted that it would be nice if Spot could support more SVA/PSL features "disable iff" (called "abort" in PSL), $rose/$fell/$stable, first_match, and maybe clocks. But so far there is not enough time to work on that. Ideally, I'd like to have a PhD student working on these and other similar topics (like LDL translation). If we had complementation of SERE, would first_match(r) be implementable as r && ((!r);1[+]) ? -- Alexandre Duret-Lutz