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