[Spot] syntactic stutter-invariance

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.