-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathTCommit.tla
87 lines (76 loc) · 5.12 KB
/
TCommit.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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
------------------------------ MODULE TCommit ------------------------------
(***************************************************************************)
(* This specification is explained in "Transaction Commit", Lecture 5 of *)
(* the TLA+ Video Course. *)
(***************************************************************************)
CONSTANT RM \* The set of participating resource managers
VARIABLE rmState \* rmState[rm] is the state of resource manager r.
-----------------------------------------------------------------------------
TCTypeOK ==
(*************************************************************************)
(* The type-correctness invariant *)
(*************************************************************************)
rmState \in [RM -> {"working", "prepared", "committed", "aborted"}]
TCInit == rmState = [r \in RM |-> "working"]
(*************************************************************************)
(* The initial predicate. *)
(*************************************************************************)
canCommit == \A r \in RM : rmState[r] \in {"prepared", "committed"}
(*************************************************************************)
(* True iff all RMs are in the "prepared" or "committed" state. *)
(*************************************************************************)
notCommitted == \A r \in RM : rmState[r] # "committed"
(*************************************************************************)
(* True iff no resource manager has decided to commit. *)
(*************************************************************************)
-----------------------------------------------------------------------------
(***************************************************************************)
(* We now define the actions that may be performed by the RMs, and then *)
(* define the complete next-state action of the specification to be the *)
(* disjunction of the possible RM actions. *)
(***************************************************************************)
Prepare(r) == /\ rmState[r] = "working"
/\ rmState' = [rmState EXCEPT ![r] = "prepared"]
Decide(r) == \/ /\ rmState[r] = "prepared"
/\ canCommit
/\ rmState' = [rmState EXCEPT ![r] = "committed"]
\/ /\ rmState[r] \in {"working", "prepared"}
/\ notCommitted
/\ rmState' = [rmState EXCEPT ![r] = "aborted"]
TCNext == \E r \in RM : Prepare(r) \/ Decide(r)
(*************************************************************************)
(* The next-state action. *)
(*************************************************************************)
-----------------------------------------------------------------------------
TCConsistent ==
(*************************************************************************)
(* A state predicate asserting that two RMs have not arrived at *)
(* conflicting decisions. It is an invariant of the specification. *)
(*************************************************************************)
\A r1, r2 \in RM : ~ /\ rmState[r1] = "aborted"
/\ rmState[r2] = "committed"
-----------------------------------------------------------------------------
(***************************************************************************)
(* The following part of the spec is not discussed in Video Lecture 5. It *)
(* will be explained in Video Lecture 8. *)
(***************************************************************************)
TCSpec == TCInit /\ [][TCNext]_rmState
(*************************************************************************)
(* The complete specification of the protocol written as a temporal *)
(* formula. *)
(*************************************************************************)
THEOREM TCSpec => [](TCTypeOK /\ TCConsistent)
(*************************************************************************)
(* This theorem asserts the truth of the temporal formula whose meaning *)
(* is that the state predicate TCTypeOK /\ TCInvariant is an invariant *)
(* of the specification TCSpec. Invariance of this conjunction is *)
(* equivalent to invariance of both of the formulas TCTypeOK and *)
(* TCConsistent. *)
(*************************************************************************)
(*************************************************************************)
(* This is some stuff that's in a box. *)
(*************************************************************************)
=============================================================================
\* Modification History
\* Last modified Mon Oct 23 15:46:41 CDT 2017 by chris
\* Created Sun Oct 22 20:26:04 CDT 2017 by chris