named temporal operators
Spin's LTL syntax allows
next for the command line (i.e.,
spin -f). The syntax for LTL formula specified inside a promela model additionally accept
before_. Where the
! denotes the strong variant.
It would be nice to support these operators as well. Unfortunately, there is one semantics incompatibility:
U for Spin, and
W for PSL.