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. On the other hand, a seemingly similar {a[->2:3]}|->b is classified as si but not ssi for some reason...
Many thanks, Victor.
Hi Victor,
On Fri, Apr 26, 2019 at 1:00 PM Victor Khomenko victor.khomenko@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.
-
Alexandre Duret-Lutz -
Victor Khomenko