-
Notifications
You must be signed in to change notification settings - Fork 0
/
diehard.tla
57 lines (45 loc) · 1.14 KB
/
diehard.tla
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
------------------------------ MODULE diehard ------------------------------
\* Use 3 and 5 gallon unmarked mugs to get exact 4 gallon water
EXTENDS Integers
VARIABLES small, big
TypeOK ==
/\ small \in 0..3
/\ big \in 0..5
Init ==
/\ small = 0
/\ big = 0
SmallToBig ==
IF (big + small) > 5
THEN /\ big' = 5
/\ small' = small - (5 - big)
ELSE /\ big' = big + small
/\ small' = 0
BigToSmall ==
IF (big + small) > 3
THEN /\ small' = 3
/\ big' = big - (3 - small)
ELSE /\ small' = big + small
/\ big' = 0
SmallDrain ==
/\ small' = 0
/\ big' = big
BigDrain ==
/\ small' = small
/\ big' = 0
FillSmall ==
/\ small' = 3
/\ big' = big
FillBig ==
/\ small' = small
/\ big' = 5
Next ==
\/ FillSmall
\/ FillBig
\/ SmallToBig
\/ BigToSmall
\/ SmallDrain
\/ BigDrain
=============================================================================
\* Modification History
\* Last modified Wed Oct 28 01:02:37 PDT 2020 by asnegi
\* Created Tue Oct 27 23:58:27 PDT 2020 by asnegi