1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
VARIABLE can Can == {0, 1} Init == can = 0 PickAction == /\ can = 0 /\ can' = 1 Next == \/ PickAction \/ UNCHANGED can TypeInvariant == can \in Can