Am new in TLA+, am trying to solve DieHard problem and I wrote code to solve the same. But in the Initial Predicate and next state relation, My Init and Next state are not coming. The following is my code.
------------------------------ MODULE DieHard ------------------------------
EXTENDS Integers
VARIABLES small,big
TypeOK == /\ small \in 0 .. 3
/\ big \in 0 .. 5
Init == /\ big = 0
/\ small = 0
FillSmall == /\ small'=3
/\ big'= big
FillBig == /\ small'= small
/\ big' = 5
EmptySmall == /\ small'= 0
/\ big'= big
EmptyBig == /\ big' = 0
/\ small'=small
SmallToBig == IF big+small =< 5
THEN /\ big' = big + small
/\ small' = 0
ELSE /\ big' = big + (small-small')
/\ small' = big -small
BigToSmall == IF big+small =< 3
THEN /\ small' = big + small
/\ big' = 0
ELSE /\ big' = big - small
/\ small' = small + ( big - big')
Next == \/ FillSmall
\/ FillBig
\/ EmptySmall
\/ EmptyBig
\/ SmallToBig
\/ BigToSmall
Spec == Init /\ [][Next]_<<big, small>>
=============================================================================
\* Modification History
\* Last modified Tue Feb 27 19:39:03 IST 2018 by nikhila
\* Created Tue Feb 27 18:41:39 IST 2018 by nikhila