New subject: syntactic stutter-invariance

26 Apr 2019

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.

Re: [Spot] syntactic stutter-invariance