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.
