26 Apr
2019
26 Apr
'19
2:21 p.m.
Hi Victor,
On Fri, Apr 26, 2019 at 1:00 PM Victor Khomenko
<victor.khomenko(a)newcastle.ac.uk> wrote:
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.
This looks like a bug, {a[=2:3]}|->b is definitely not stutter invariant.
The syntactic SI subset we catch should correspond to siPSL. (If you
know a larger subset, that would be a welcome addition.)
a[=2:3] is internally stored as ((!a)[*];a)[*2..3];(!a)[*], and I see
that the code matching the r;b* rule of siPSL is broken. I'll fix
that, thanks for reporting this.
On the other hand, a seemingly similar
{a[->2:3]}|->b
is classified as si but not ssi for some reason...
I can't reproduce this one. It is shown as stutter-sensitive for me.