MODULE main
VAR
y : 0..15;
ASSIGN
init(y) := 0;
TRANS
case
y = 7 : next(y) = 0;
TRUE : next(y) = ((y + 1) mod 16);
esac
LTLSPEC G ( y=4 -> X y=6 ) -- it is always true that after 4 comes 6
-- LTLSPEC !G F (y = 2) -- it is not always true that you can always reach y = 2