Skip to content

Instantly share code, notes, and snippets.

@mwhittaker
Last active April 24, 2019 20:59
Show Gist options
  • Save mwhittaker/7ade82b2b2b5e37e28f0b2ef1e4f89df to your computer and use it in GitHub Desktop.
Save mwhittaker/7ade82b2b2b5e37e28f0b2ef1e4f89df to your computer and use it in GitHub Desktop.
TLA Misc
--------------------------------- MODULE AB ---------------------------------
EXTENDS Integers, Sequences
CONSTANT Data
(***************************************************************************)
(* We first define Remove(i, seq) to be the sequence obtained by removing *)
(* element number i from sequence seq. *)
(***************************************************************************)
Remove(i, seq) ==
[j \in 1..(Len(seq)-1) |-> IF j < i THEN seq[j]
ELSE seq[j+1]]
VARIABLES AVar, BVar, \* The same as in module ABSpec
AtoB, \* The sequence of data messages in transit from sender to receiver.
BtoA \* The sequence of ack messages in transit from receiver to sender.
\* Messages are sent by appending them to the end of the sequence.
\* and received by removing them from the head of the sequence.
vars == << AVar, BVar, AtoB, BtoA >>
TypeOK == /\ AVar \in Data \X {0,1}
/\ BVar \in Data \X {0,1}
/\ AtoB \in Seq(Data \X {0,1})
/\ BtoA \in Seq({0,1})
Init == /\ AVar \in Data \X {1}
/\ BVar = AVar
/\ AtoB = << >>
/\ BtoA = << >>
(***************************************************************************)
(* The action of the sender sending a data message by appending AVar to *)
(* the end of the message queue AtoB. It will keep sending the same *)
(* message until it receives an acknowledgment for it from the receiver. *)
(***************************************************************************)
ASnd == /\ AtoB' = Append(AtoB, AVar)
/\ UNCHANGED <<AVar, BtoA, BVar>>
(***************************************************************************)
(* The action of the sender receiving an ack message. If that ack is for *)
(* the value it is sending, then it chooses another message to send and *)
(* sets AVar to that message. If the ack is for the previous value it *)
(* sent, it ignores the message. In either case, it removes the message *)
(* from BtoA. *)
(***************************************************************************)
ARcv == /\ BtoA # << >>
/\ IF Head(BtoA) = AVar[2]
THEN \E d \in Data : AVar' = <<d, 1 - AVar[2]>>
ELSE AVar' = AVar
/\ BtoA' = Tail(BtoA)
/\ UNCHANGED <<AtoB, BVar>>
(***************************************************************************)
(* The action of the receiver sending an acknowledgment message for the *)
(* last data item it received. *)
(***************************************************************************)
BSnd == /\ BtoA' = Append(BtoA, BVar[2])
/\ UNCHANGED <<AVar, BVar, AtoB>>
(***************************************************************************)
(* The action of the receiver receiving a data message. It sets BVar to *)
(* that message if it's not for the data item it has already received. *)
(***************************************************************************)
BRcv == /\ AtoB # << >>
/\ IF Head(AtoB)[2] # BVar[2]
THEN BVar' = Head(AtoB)
ELSE BVar' = BVar
/\ AtoB' = Tail(AtoB)
/\ UNCHANGED <<AVar, BtoA>>
(***************************************************************************)
(* LoseMsg is the action that removes an arbitrary message from queue AtoB *)
(* or BtoA. *)
(***************************************************************************)
LoseMsg == /\ \/ /\ \E i \in 1..Len(AtoB):
AtoB' = Remove(i, AtoB)
/\ BtoA' = BtoA
\/ /\ \E i \in 1..Len(BtoA):
BtoA' = Remove(i, BtoA)
/\ AtoB' = AtoB
/\ UNCHANGED << AVar, BVar >>
Next == ASnd \/ ARcv \/ BSnd \/ BRcv \/ LoseMsg
Spec == Init /\ [][Next]_vars
-----------------------------------------------------------------------------
ABS == INSTANCE ABSpec
THEOREM Spec => ABS!Spec
-----------------------------------------------------------------------------
(***************************************************************************)
(* FairSpec is Spec with fairness conditions added. *)
(***************************************************************************)
FairSpec == Spec /\ SF_vars(ARcv) /\ SF_vars(BRcv) /\
WF_vars(ASnd) /\ WF_vars(BSnd)
=============================================================================
--------------------------------- MODULE AB2 ---------------------------------
(***************************************************************************)
(* This is a modification of spec AB in which instead of losing messages, *)
(* messages are detectably "corrupted"--represented by being changed to *)
(* the value Bad. The to communication channels are represented by the *)
(* variables AtoB2 and BtoA2. *)
(***************************************************************************)
EXTENDS Integers, Sequences\* , TLC
CONSTANT Data, Bad
ASSUME Bad \notin (Data \X {0,1}) \cup {0,1}
\* We need to asssume that Bad is different from any of the legal
\* messsages.
VARIABLES AVar, BVar, \* The same as in module ABSpec
AtoB2, \* The sequence of data messages in transit from sender to receiver
BtoA2 \* The sequence of ack messages in transit from receiver to sender
\* Messages are sent by appending them to the end of the sequence
\* and received by removing them from the head of the sequence.
vars == << AVar, BVar, AtoB2, BtoA2 >>
TypeOK == /\ AVar \in Data \X {0,1}
/\ BVar \in Data \X {0,1}
/\ AtoB2 \in Seq((Data \X {0,1}) \cup {Bad})
/\ BtoA2 \in Seq({0,1, Bad})
Init == /\ AVar \in Data \X {1}
/\ BVar = AVar
/\ AtoB2 = << >>
/\ BtoA2 = << >>
(***************************************************************************)
(* The action of the sender sending a data message by appending AVar to *)
(* the end of the message queue AtoB2. It will keep sending the same *)
(* message until it receives an acknowledgment for it from the receiver. *)
(***************************************************************************)
ASnd == /\ AtoB2' = Append(AtoB2, AVar)
/\ UNCHANGED <<AVar, BtoA2, BVar>>
(***************************************************************************)
(* The action of the sender receiving an ack message. If that ack is for *)
(* the value it is sending, then it chooses another message to send and *)
(* sets AVar to that message. If the ack is for the previous value it *)
(* sent, it ignores the message. In either case, it removes the message *)
(* from BtoA2. Note that Bad cannot equal AVar[2], which is in {0,1}. *)
(***************************************************************************)
ARcv == /\ BtoA2 # << >>
/\ IF Head(BtoA2) = AVar[2]
THEN \E d \in Data: AVar' = <<d, 1 - AVar[2]>>
ELSE AVar' = AVar
/\ BtoA2' = Tail(BtoA2)
/\ UNCHANGED <<AtoB2, BVar>>
(***************************************************************************)
(* The action of the receiver sending an acknowledgment message for the *)
(* last data item it received. *)
(***************************************************************************)
BSnd == /\ BtoA2' = Append(BtoA2, BVar[2])
/\ UNCHANGED <<AVar, BVar, AtoB2>>
(***************************************************************************)
(* The action of the receiver receiving a data message. It ignores a Bad *)
(* message. Otherwise, it sets BVar to the message if it's not for the *)
(* data item it has already received. *)
(***************************************************************************)
BRcv == /\ AtoB2 # << >>
/\ IF (Head(AtoB2) # Bad) /\ (Head(AtoB2)[2] # BVar[2])
THEN BVar' = Head(AtoB2)
ELSE BVar' = BVar
/\ AtoB2' = Tail(AtoB2)
/\ UNCHANGED <<AVar, BtoA2>>
(***************************************************************************)
(* CorruptMsg is the action that changes an arbitrary message in AtoB2 or *)
(* BtoA2 to Bad. (We don't bother testing if the message in AtoB2 already *)
(* equals Bad, since setting to Bad a message that already equals Bad is *)
(* just a stuttering step.) *)
(***************************************************************************)
CorruptMsg == /\ \/ /\ \E i \in 1..Len(AtoB2):
AtoB2' = [AtoB2 EXCEPT ![i] = Bad]
/\ BtoA2' = BtoA2
\/ /\ \E i \in 1..Len(BtoA2):
BtoA2' = [BtoA2 EXCEPT ![i] = Bad]
/\ AtoB2' = AtoB2
/\ UNCHANGED << AVar, BVar >>
Next == ASnd \/ ARcv \/ BSnd \/ BRcv \/ CorruptMsg
Spec == Init /\ [][Next]_vars
-----------------------------------------------------------------------------
ABS == INSTANCE ABSpec
THEOREM Spec => ABS!Spec
-----------------------------------------------------------------------------
(***************************************************************************)
(* FairSpec is the analogue of formula FairSpec of module AB2. That is, *)
(* it is obtained by conjoining to formula Spec the fairness conditions *)
(* that correspond to the ones in module AB2. However, specification *)
(* FairSpec of this module does not implement ABS!FairSpec. You can use *)
(* TLC to find a behavior in which no new values are ever sent. *)
(***************************************************************************)
FairSpec ==
Spec /\ SF_vars(ARcv) /\ SF_vars(BRcv) /\ WF_vars(ASnd) /\ WF_vars(BSnd)
(***************************************************************************)
(* A little thought reveals that, since messages are corrupted but not *)
(* deleted, strong fairness of ARcv and BRcv is equivalent to weak *)
(* fairness of those actions. The shortest counterexample showing that *)
(* FairSpec does not implement ABS!FairSpec, which is probably the one *)
(* found by TLC, is a behavior in which a message is sent on an empty *)
(* message channel, but is always corrupted before it can received. This *)
(* suggests that in addition to weak fairness of ARcv and BRcv, we want *)
(* strong fairness of those actions when the head of the queue is not *)
(* corrupt. That leads to the following spec. *)
(***************************************************************************)
FairSpec2 ==
Spec /\ WF_vars(ARcv) /\ WF_vars(BRcv) /\ WF_vars(ASnd) /\ WF_vars(BSnd)
/\ SF_vars(ARcv /\ Head(BtoA2) # Bad)
/\ SF_vars(BRcv /\ Head(AtoB2) # Bad)
(***************************************************************************)
(* Running TLC shows that FairSpec2 also does not implement ABS!FairSpec. *)
(* In fact, I believe that it is impossible to obtain a specification that *)
(* implements ABS!FairSpec by conjoining to Spec fairness conditions on *)
(* subactions of Next. Module AB2P shows how we can modify the AB2 *)
(* specification to obtain a specification that implements ABS!Spec. *)
(***************************************************************************)
-----------------------------------------------------------------------------
(***************************************************************************)
(* We define RemoveBad so that RemoveBad(seq) is the value obtained by *)
(* removing from the sequence seq all elements that equal Bad. *)
(***************************************************************************)
RECURSIVE RemoveBad(_)
RemoveBad(seq) ==
IF seq = << >>
THEN << >>
ELSE (IF Head(seq) = Bad THEN << >> ELSE <<Head(seq)>>)
\o RemoveBad(Tail(seq))
(***************************************************************************)
(* There's an easy way to define RemoveBad using the SelectSeq operator of *)
(* the Sequences module. Here's the alternative definition. *)
(***************************************************************************)
RemoveBadAlt(seq) == LET Test(elt) == elt # Bad
IN SelectSeq(seq, Test)
(***************************************************************************)
(* The following statement defines AB!Spec to be the specification Spec of *)
(* module AB with RemoveBad(AtoB2) substituted for AtoB and *)
(* RemoveBad(BtoA2) substituted for BtoA. *)
(***************************************************************************)
AB == INSTANCE AB WITH AtoB <- RemoveBad(AtoB2), BtoA <- RemoveBad(BtoA2)
(***************************************************************************)
(* The following theorem asserts that the specification Spec of this *)
(* module implements the specification Spec of module AB under the *)
(* refinement mapping that substitutes RemoveBad(AtoB2) for AtoB and *)
(* substitutes for every other variable and every constant of module AB *)
(* the variable or constant of the same name. This theorem is checked by *)
(* having TLC check that the temporal property AB!Spec is satisfied by the *)
(* specification Spec. *)
(***************************************************************************)
THEOREM Spec => AB!Spec
=============================================================================
\* Modification History
\* Last modified Wed Jan 24 16:33:07 PST 2018 by lamport
\* Created Wed Mar 25 11:53:40 PDT 2015 by lamport
CONSTANT
a = a
b = b
c = c
Data <- abc
CONSTRAINT SmallQueueConstraint
SPECIFICATION FairSpec
INVARIANT TypeOK
PROPERTY ABSpecFairSpec
---- MODULE ABModel ----
EXTENDS AB
CONSTANT a, b, c
abc == {a, b, c}
SmallQueueConstraint ==
/\ Len(AtoB) =< 4
/\ Len(BtoA) =< 4
ABSpecSpec == ABS!Spec
ABSpecFairSpec == ABS!FairSpec
====
------------------------------ MODULE ABSpec --------------------------------
EXTENDS Integers
CONSTANT Data \* The set of all possible data values.
VARIABLES AVar, \* The last <<value, bit>> pair A decided to send.
BVar \* The last <<value, bit>> pair B received.
(***************************************************************************)
(* Type correctness means that AVar and BVar are tuples <<d, i>> where *)
(* d \in Data and i \in {0, 1}. *)
(***************************************************************************)
TypeOK == /\ AVar \in Data \X {0,1}
/\ BVar \in Data \X {0,1}
(***************************************************************************)
(* It's useful to define vars to be the tuple of all variables, for *)
(* example so we can write [Next]_vars instead of [Next]_<< ... >> *)
(***************************************************************************)
vars == << AVar, BVar >>
(***************************************************************************)
(* Initially AVar can equal <<d, 1>> for any Data value d, and BVar equals *)
(* AVar. *)
(***************************************************************************)
Init == /\ AVar \in Data \X {1}
/\ BVar = AVar
(***************************************************************************)
(* When AVar = BVar, the sender can "send" an arbitrary data d item by *)
(* setting AVar[1] to d and complementing AVar[2]. It then waits until *)
(* the receiver "receives" the message by setting BVar to AVar before it *)
(* can send its next message. Sending is described by action A and *)
(* receiving by action B. *)
(***************************************************************************)
A == /\ AVar = BVar
/\ \E d \in Data: AVar' = <<d, 1 - AVar[2]>>
/\ BVar' = BVar
B == /\ AVar # BVar
/\ BVar' = AVar
/\ AVar' = AVar
Next == A \/ B
Spec == Init /\ [][Next]_vars
(***************************************************************************)
(* For understanding the spec, it's useful to define formulas that should *)
(* be invariants and check that they are invariant. The following *)
(* invariant Inv asserts that, if AVar and BVar have equal second *)
(* components, then they are equal (which by the invariance of TypeOK *)
(* implies that they have equal first components). *)
(***************************************************************************)
Inv == (AVar[2] = BVar[2]) => (AVar = BVar)
-----------------------------------------------------------------------------
(***************************************************************************)
(* FairSpec is Spec with the addition requirement that it keeps taking *)
(* steps. *)
(***************************************************************************)
FairSpec == Spec /\ WF_vars(Next)
=============================================================================
SPECIFICATION FairSpec
CONSTANT Data <- abc
INVARIANT
TypeOK
Inv
PROPERTY
BEventuallyCopiesA
---- MODULE ABSpecModel ----
EXTENDS ABSpec
abc == {"a", "b", "c"}
BEventuallyCopiesA ==
\A x \in (Data \X {0, 1}): AVar = x ~> BVar = x
====
---- MODULE TCommit ----
EXTENDS TLC
(***************************************************************************)
(* 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. *)
(*************************************************************************)
=========================
INIT TCInit
NEXT TCNext
CONSTANT
a = a
b = b
c = c
RM <- abc
SYMMETRY
AbcSymmetry
INVARIANT
TCTypeOK
TCConsistent
---- MODULE TCommitModel ----
EXTENDS TCommit
CONSTANT a, b, c
abc == {a, b, c}
AbcSymmetry == Permutations(abc)
====
---- MODULE TwoPhase ----
(***************************************************************************)
(* This specification is discussed in "Two-Phase Commit", Lecture 6 of the *)
(* TLA+ Video Course. It describes the Two-Phase Commit protocol, in *)
(* which a transaction manager (TM) coordinates the resource managers *)
(* (RMs) to implement the Transaction Commit specification of module *)
(* TCommit. In this specification, RMs spontaneously issue Prepared *)
(* messages. We ignore the Prepare messages that the TM can send to the *)
(* RMs. *)
(* *)
(* For simplicity, we also eliminate Abort messages sent by an RM when it *)
(* decides to abort. Such a message would cause the TM to abort the *)
(* transaction, an event represented here by the TM spontaneously deciding *)
(* to abort. *)
(***************************************************************************)
CONSTANT RM \* The set of resource managers
VARIABLES
rmState, \* rmState[r] is the state of resource manager r.
tmState, \* The state of the transaction manager.
tmPrepared, \* The set of RMs from which the TM has received "Prepared"
\* messages.
msgs
(***********************************************************************)
(* In the protocol, processes communicate with one another by sending *)
(* messages. For simplicity, we represent message passing with the *)
(* variable msgs whose value is the set of all messages that have been *)
(* sent. A message is sent by adding it to the set msgs. An action *)
(* that, in an implementation, would be enabled by the receipt of a *)
(* certain message is here enabled by the presence of that message in *)
(* msgs. For simplicity, messages are never removed from msgs. This *)
(* allows a single message to be received by multiple receivers. *)
(* Receipt of the same message twice is therefore allowed; but in this *)
(* particular protocol, that's not a problem. *)
(***********************************************************************)
Messages ==
(*************************************************************************)
(* The set of all possible messages. Messages of type "Prepared" are *)
(* sent from the RM indicated by the message's rm field to the TM. *)
(* Messages of type "Commit" and "Abort" are broadcast by the TM, to be *)
(* received by all RMs. The set msgs contains just a single copy of *)
(* such a message. *)
(*************************************************************************)
[type : {"Prepared"}, rm : RM] \cup [type : {"Commit", "Abort"}]
TPTypeOK ==
(*************************************************************************)
(* The type-correctness invariant *)
(*************************************************************************)
/\ rmState \in [RM -> {"working", "prepared", "committed", "aborted"}]
/\ tmState \in {"init", "done"}
/\ tmPrepared \subseteq RM
/\ msgs \subseteq Messages
TPInit ==
(*************************************************************************)
(* The initial predicate. *)
(*************************************************************************)
/\ rmState = [r \in RM |-> "working"]
/\ tmState = "init"
/\ tmPrepared = {}
/\ msgs = {}
-----------------------------------------------------------------------------
(***************************************************************************)
(* We now define the actions that may be performed by the processes, first *)
(* the TM's actions, then the RMs' actions. *)
(***************************************************************************)
TMRcvPrepared(r) ==
(*************************************************************************)
(* The TM receives a "Prepared" message from resource manager r. We *)
(* could add the additional enabling condition r \notin tmPrepared, *)
(* which disables the action if the TM has already received this *)
(* message. But there is no need, because in that case the action has *)
(* no effect; it leaves the state unchanged. *)
(*************************************************************************)
/\ tmState = "init"
/\ [type |-> "Prepared", rm |-> r] \in msgs
/\ tmPrepared' = tmPrepared \cup {r}
/\ UNCHANGED <<rmState, tmState, msgs>>
TMCommit ==
(*************************************************************************)
(* The TM commits the transaction; enabled iff the TM is in its initial *)
(* state and every RM has sent a "Prepared" message. *)
(*************************************************************************)
/\ tmState = "init"
/\ tmPrepared = RM
/\ tmState' = "done"
/\ msgs' = msgs \cup {[type |-> "Commit"]}
/\ UNCHANGED <<rmState, tmPrepared>>
TMAbort ==
(*************************************************************************)
(* The TM spontaneously aborts the transaction. *)
(*************************************************************************)
/\ tmState = "init"
/\ tmState' = "done"
/\ msgs' = msgs \cup {[type |-> "Abort"]}
/\ UNCHANGED <<rmState, tmPrepared>>
RMPrepare(r) ==
(*************************************************************************)
(* Resource manager r prepares. *)
(*************************************************************************)
/\ rmState[r] = "working"
/\ rmState' = [rmState EXCEPT ![r] = "prepared"]
/\ msgs' = msgs \cup {[type |-> "Prepared", rm |-> r]}
/\ UNCHANGED <<tmState, tmPrepared>>
RMChooseToAbort(r) ==
(*************************************************************************)
(* Resource manager r spontaneously decides to abort. As noted above, r *)
(* does not send any message in our simplified spec. *)
(*************************************************************************)
/\ rmState[r] = "working"
/\ rmState' = [rmState EXCEPT ![r] = "aborted"]
/\ UNCHANGED <<tmState, tmPrepared, msgs>>
RMRcvCommitMsg(r) ==
(*************************************************************************)
(* Resource manager r is told by the TM to commit. *)
(*************************************************************************)
/\ [type |-> "Commit"] \in msgs
/\ rmState' = [rmState EXCEPT ![r] = "committed"]
/\ UNCHANGED <<tmState, tmPrepared, msgs>>
RMRcvAbortMsg(r) ==
(*************************************************************************)
(* Resource manager r is told by the TM to abort. *)
(*************************************************************************)
/\ [type |-> "Abort"] \in msgs
/\ rmState' = [rmState EXCEPT ![r] = "aborted"]
/\ UNCHANGED <<tmState, tmPrepared, msgs>>
TPNext ==
\/ TMCommit \/ TMAbort
\/ \E r \in RM :
TMRcvPrepared(r) \/ RMPrepare(r) \/ RMChooseToAbort(r)
\/ RMRcvCommitMsg(r) \/ RMRcvAbortMsg(r)
-----------------------------------------------------------------------------
(***************************************************************************)
(* The material below this point is not discussed in Video Lecture 6. It *)
(* will be explained in Video Lecture 8. *)
(***************************************************************************)
TPSpec == TPInit /\ [][TPNext]_<<rmState, tmState, tmPrepared, msgs>>
(*************************************************************************)
(* The complete spec of the Two-Phase Commit protocol. *)
(*************************************************************************)
THEOREM TPSpec => []TPTypeOK
(*************************************************************************)
(* This theorem asserts that the type-correctness predicate TPTypeOK is *)
(* an invariant of the specification. *)
(*************************************************************************)
-----------------------------------------------------------------------------
(***************************************************************************)
(* We now assert that the Two-Phase Commit protocol implements the *)
(* Transaction Commit protocol of module TCommit. The following statement *)
(* imports all the definitions from module TCommit into the current *)
(* module. *)
(***************************************************************************)
INSTANCE TCommit
THEOREM TPSpec => TCSpec
(*************************************************************************)
(* This theorem asserts that the specification TPSpec of the Two-Phase *)
(* Commit protocol implements the specification TCSpec of the *)
(* Transaction Commit protocol. *)
(*************************************************************************)
(***************************************************************************)
(* The two theorems in this module have been checked with TLC for six *)
(* RMs, a configuration with 50816 reachable states, in a little over a *)
(* minute on a 1 GHz PC. *)
(***************************************************************************)
====
INIT TPInit
NEXT TPNext
CONSTANT
a = a
b = b
c = c
RM <- abc
SYMMETRY
AbcSymmetry
INVARIANT
TPTypeOK
PROPERTY
TCSpec
---- MODULE TwoPhaseModel ----
EXTENDS TwoPhase
CONSTANT a, b, c
abc == {a, b, c}
AbcSymmetry == Permutations(abc)
====
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment