----------------------------- MODULE DieHard -----------------------------
EXTENDS Naturals 
VARIABLES small, big

Init == /\ small = 0
        /\ big = 0

TypeOk == /\ big \in 0..5
          /\ small \in 0..3

FillBig == /\ big' = 5
           /\ small' = small

FillSmall == /\ small' = 3
             /\ big' = big

EmptyBig == /\ big' = 0
            /\ small' = small

EmptySmall == /\ small' = 0
              /\ big' = big

Small2Big == IF big + small > 5
            THEN /\ big' = 5
                 /\ small' = (big + small) - 5
            ELSE /\ big' = big + small
                 /\ small' = 0

Big2Small == IF big + small > 3
            THEN /\ small' = 3
                 /\ big' = (big + small) - 3
            ELSE /\ small' = big + small
                 /\ big' = 0

Next == \/ Big2Small
        \/ Small2Big
        \/ EmptyBig
        \/ EmptySmall
        \/ FillBig
        \/ FillSmall

Impossible == big # 4

=============================================================================
\* Modification History
\* Last modified Fri Feb 28 17:31:43 EST 2025 by danesabo
\* Created Fri Feb 28 17:23:34 EST 2025 by danesabo