-
Notifications
You must be signed in to change notification settings - Fork 2
/
Dekker.tla
72 lines (53 loc) · 2.16 KB
/
Dekker.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
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
-------------------------------- MODULE Dekker --------------------------------
EXTENDS Naturals, Integers, FiniteSets, Bags, Sequences, TLC
(*
\* http://en.wikipedia.org/wiki/Dekker%27s_algorithm. We only model 2 processes
--algorithm Dekker {
variables entrance_intents=[i \in 0..1 |-> FALSE], \* intent to enter critical section
turn=0; \* who's turn is it (first: p0)
process (proc \in 0..1)
variables other=1-self; \* the other process; works only with 2 processes
{
p0:
entrance_intents[self] := TRUE;
p1:
await ~entrance_intents[other] /\ turn = self;
cs: \* critical section
print <<self, "critical section">>;
turn := other;
entrance_intents[self] := FALSE;
}
}
*)
\* BEGIN TRANSLATION
VARIABLES entrance_intents, turn, pc, other
vars == << entrance_intents, turn, pc, other >>
ProcSet == (0..1)
Init == (* Global variables *)
/\ entrance_intents = [i \in 0..1 |-> FALSE]
/\ turn = 0
(* Process proc *)
/\ other = [self \in 0..1 |-> 1-self]
/\ pc = [self \in ProcSet |-> "p0"]
p0(self) == /\ pc[self] = "p0"
/\ entrance_intents' = [entrance_intents EXCEPT ![self] = TRUE]
/\ pc' = [pc EXCEPT ![self] = "p1"]
/\ UNCHANGED << turn, other >>
p1(self) == /\ pc[self] = "p1"
/\ ~entrance_intents[other[self]] /\ turn = self
/\ pc' = [pc EXCEPT ![self] = "cs"]
/\ UNCHANGED << entrance_intents, turn, other >>
cs(self) == /\ pc[self] = "cs"
/\ PrintT(<<self, "critical section">>)
/\ turn' = other[self]
/\ entrance_intents' = [entrance_intents EXCEPT ![self] = FALSE]
/\ pc' = [pc EXCEPT ![self] = "Done"]
/\ other' = other
proc(self) == p0(self) \/ p1(self) \/ cs(self)
Next == (\E self \in 0..1: proc(self))
\/ (* Disjunct to prevent deadlock on termination *)
((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)
Spec == Init /\ [][Next]_vars
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION
=============================================================================