Each LTL formula is checked for every execution trace. Run it using spin -run -a test.pml, and assertion failure or acceptance cycle means that the
property denoted by the LTL formula does not hold.

active proctype t1() { x-- } ltl { [] (x == 0) } // fails, since x could be 1 or -1 during the execution ltl { <> (x == 0) } // succeeds, since x == 0 initially // since the traces are finite, the final state is the one that matters ltl { [] <> (x == 0) } // succeeds ltl { <> [] (x == 0) } // succeeds

byte x = 0 active proctype t0() { if :: skip :: x++ fi }

active proctype t1() { x++ }

// x == 2 is *not* guaranteed ltl { <> (x == 2) } // fails; doesn't hold for some trace // but x == 2 is reachable; proved using contradiction ltl { [] (x != 2) } // fails;

// [] P and <> ! P are dual, but both of them fails here, because SPIN considers all traces; // for a particular trace, one and only one of them holds