Spin Temporal Logic Modeling

强力软件

Promela / spin use boolean temporal logic to ensure safety property and liveness property of program.

Syntax:

ltl <ltlname> { <ltl> }

For Example:

ltl NeverEnter { [] !cs }

TIPs: It's a god damn good idea to surround logic statement with ().

A run is called weakly fair iff the following holds: each continuously executable statement is executed eventually. If statement is not continuously executable (perhaps, block), fairness is not guaranteed.