------------------------------ MODULE DieHard ------------------------------

EXTENDS Integers
VARIABLES small, big

TypeOK == /\ small \in 0..3
          /\ big \in 0..5
          
 Init == /\ small = 0
         /\ big = 0
         
 FillSmall == /\ big' = big
              /\ small' = 3
         
 FillBig == /\ big' = 5
            /\ small' = small
                     
 EmptySmall == /\ big' = big
               /\ small' = 0
                        
 EmptyBig == /\ big' = 0
             /\ small' = small
             
 SmallToBig == IF big + small <= 5
                 THEN /\ big' = big + small
                      /\ small' = 0
                 ELSE /\ big' = 5
                      /\ small' = small - (5 - big)
              
 BigToSmall == IF big + small <= 3
                 THEN /\ big' = 0
                      /\ small' = big + small
                 ELSE /\ small' = 3
                      /\ big' = big - (3 - small)
         
 Next == \/ FillSmall
         \/ FillBig
         \/ EmptySmall
         \/ EmptyBig
         \/ SmallToBig
         \/ BigToSmall
              
=============================================================================
\* Modification History
\* Last modified Fri Dec 21 16:33:15 CET 2018 by veitheller
\* Created Fri Dec 21 16:16:46 CET 2018 by veitheller