Re: [Spot] syntactic stutter-invariance

Thanks Alexandre, 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.) Sorry, my bad, it's indeed ss. Thanks, Victor.