This web page was written on:
30 August 2021
The video was produced on:
14 May 2017
Type a space to stop the video.
Stop the video and write
down your definitions.
Copy
button below it, or by your usual method of copying
text.
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 == /\ big' = 5 /\ small' = small EmptySmall == /\ small' = 0 /\ big' = big 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 /\ big' = small - (3 - big) /\ small' = 3 Next == \/ FillSmall \/ FillBig \/ EmptySmall \/ EmptyBig \/ SmallToBig \/ BigToSmall
DieHard
.