54 lines
1.7 KiB
Text
54 lines
1.7 KiB
Text
---- MODULE DieHard ----
|
|
EXTENDS Integers
|
|
|
|
VARIABLES small, big
|
|
|
|
TypeOK == /\ small \in 0..3
|
|
/\ big \in 0..5
|
|
|
|
Init == /\ big = 0
|
|
/\ small = 0
|
|
|
|
\* That would be wrong FillSmall == small' = 3
|
|
\* That's because we think of this as setting small to 3
|
|
\* But it's a formula that's true for some steps (those where small=3 in the second state) and false for others
|
|
\* The following is the correct version: it is only true when the step is just filling the small jug
|
|
FillSmall == /\ small' = 3
|
|
/\ big' = big
|
|
|
|
FillBig == /\ big' = 5
|
|
/\ small' = small
|
|
|
|
EmptySmall == /\ small' = 0
|
|
/\ big' = big
|
|
|
|
EmptyBig == /\ big' = 0
|
|
/\ small' = small
|
|
|
|
SmallToBig == IF big + small =< 5
|
|
THEN \* There is room: empty small
|
|
/\ big' = big + small
|
|
/\ small' = 0
|
|
ELSE \* There isn't room: fill big
|
|
/\ big' = 5
|
|
/\ small' = small - (5 - big)
|
|
BigToSmall == IF big + small =< 3
|
|
THEN \* There is room: empty big
|
|
/\ small' = big + small
|
|
/\ big' = 0
|
|
ELSE \* There isn't room: fill small
|
|
/\ small' = 3
|
|
/\ big' = small - (3 - big)
|
|
|
|
|
|
Next == \/ FillSmall \* Fill small jug
|
|
\/ FillBig \* Fill big jug
|
|
\/ EmptySmall
|
|
\/ EmptyBig
|
|
\/ SmallToBig
|
|
\/ BigToSmall
|
|
|
|
=============================================================================
|
|
\* Modification History
|
|
\* Last modified Mon Feb 03 12:11:57 CET 2025 by fredericmarand
|
|
\* Created Mon Feb 03 11:38:13 CET 2025 by fredericmarand
|