---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/2PCwithBTM.tla
---
------------------------------ MODULE 2PCwithBTM -------------------------------
EXTENDS Integers, Sequences, FiniteSets, TLC
CONSTANT RM, \* The set of participating resource managers RM=1..3
RMMAYFAIL,
TMMAYFAIL \* Whether TM may fail MAYFAIL=TRUE or FALSE
(***************************************************************************
A modified version of P2TCommit at http://lamport.azurewebsites.net/tla/two-phase.html
Transaction manager (TM) is added.
`.
--algorithm TransactionCommit {
variable rmState = [rm \in RM |-> "working"],
tmState = "init";
define {
canCommit == \A rmc \in RM: rmState[rmc] \in {"prepared"}
\/ \E rm \in RM : rmState[rm] \in {"committed"} \* for when BTM takes over
canAbort == \E rm \in RM : rmState[rm] \in {"aborted","failed"}
/\ ~\E rmc \in RM : rmState[rmc]= "committed" \* inconsistent if commented
}
macro Prepare(p) {
await rmState[p] = "working";
rmState[p] := "prepared" ; }
macro Decide(p) {
either { await tmState="commit";
rmState[p] := "committed";}
or { await rmState[p]="working" \/ tmState="abort";
rmState[p] := "aborted";}
}
macro Fail(p) {
if (RMMAYFAIL /\ ~\E rm \in RM:rmState[rm]="failed") rmState[p] := "failed";
}
fair process (RManager \in RM) {
RS: while (rmState[self] \in {"working", "prepared"}) {
either Prepare(self) or Decide(self) or Fail(self)}
}
fair process (TManager=0) {
TS:either{ await canCommit;
TC: tmState := "commit";
F1: if (TMMAYFAIL) tmState := "hidden";}
or { await canAbort;
TA: tmState := "abort";
F2: if (TMMAYFAIL) tmState := "hidden";}
}
fair process (BTManager=10) {
BTS:either{await canCommit /\ tmState="hidden";
BTC: tmState := "commit";}
or { await canAbort /\ tmState="hidden";
BTA: tmState := "abort";}
}
}
.'
***************************************************************************)
\* BEGIN TRANSLATION
VARIABLES rmState, tmState, pc
(* define statement *)
canCommit == \A rmc \in RM: rmState[rmc] \in {"prepared"}
\/ \E rm \in RM: rmState[rm] \in {"committed"}
canAbort == \E rm \in RM: rmState[rm] \in {"aborted", "failed"}
/\ ~\E rmc \in RM: rmState[rmc] = "committed"
vars == << rmState, tmState, pc >>
ProcSet == (RM) \union {0} \union {10}
Init == (* Global variables *)
/\ rmState = [rm \in RM |-> "working"]
/\ tmState = "init"
/\ pc = [self \in ProcSet |-> CASE self \in RM -> "RS"
[] self = 0 -> "TS"
[] self = 10 -> "BTS"]
RS(self) ==
/\ pc[self] = "RS"
/\ IF rmState[self] \in {"working", "prepared"}
THEN
/\
\/
/\ rmState[self] = "working"
/\ rmState' = [rmState EXCEPT ![self] = "prepared"]
\/
/\
\/
/\ tmState = "commit"
/\ rmState' = [rmState EXCEPT ![self] = "committed"]
\/
/\ rmState[self] = "working" \/ tmState = "abort"
/\ rmState' = [rmState EXCEPT ![self] = "aborted"]
\/
/\ IF RMMAYFAIL /\ ~\E rm \in RM: rmState[rm] = "failed"
THEN
/\ rmState' = [rmState EXCEPT ![self] = "failed"]
ELSE
/\ TRUE
/\ UNCHANGED rmState
/\ pc' = [pc EXCEPT ![self] = "RS"]
ELSE
/\ pc' = [pc EXCEPT ![self] = "Done"]
/\ UNCHANGED rmState
/\ UNCHANGED tmState
RManager(self) == RS(self)
TS ==
/\ pc[0] = "TS"
/\
\/
/\ canCommit
/\ pc' = [pc EXCEPT ![0] = "TC"]
\/
/\ canAbort
/\ pc' = [pc EXCEPT ![0] = "TA"]
/\ UNCHANGED << rmState, tmState >>
TC ==
/\ pc[0] = "TC"
/\ tmState' = "commit"
/\ pc' = [pc EXCEPT ![0] = "F1"]
/\ UNCHANGED rmState
F1 ==
/\ pc[0] = "F1"
/\ IF TMMAYFAIL
THEN
/\ tmState' = "hidden"
ELSE
/\ TRUE
/\ UNCHANGED tmState
/\ pc' = [pc EXCEPT ![0] = "Done"]
/\ UNCHANGED rmState
TA ==
/\ pc[0] = "TA"
/\ tmState' = "abort"
/\ pc' = [pc EXCEPT ![0] = "F2"]
/\ UNCHANGED rmState
F2 ==
/\ pc[0] = "F2"
/\ IF TMMAYFAIL
THEN
/\ tmState' = "hidden"
ELSE
/\ TRUE
/\ UNCHANGED tmState
/\ pc' = [pc EXCEPT ![0] = "Done"]
/\ UNCHANGED rmState
TManager == TS \/ TC \/ F1 \/ TA \/ F2
BTS ==
/\ pc[10] = "BTS"
/\
\/
/\ canCommit /\ tmState = "hidden"
/\ pc' = [pc EXCEPT ![10] = "BTC"]
\/
/\ canAbort /\ tmState = "hidden"
/\ pc' = [pc EXCEPT ![10] = "BTA"]
/\ UNCHANGED << rmState, tmState >>
BTC ==
/\ pc[10] = "BTC"
/\ tmState' = "commit"
/\ pc' = [pc EXCEPT ![10] = "Done"]
/\ UNCHANGED rmState
BTA ==
/\ pc[10] = "BTA"
/\ tmState' = "abort"
/\ pc' = [pc EXCEPT ![10] = "Done"]
/\ UNCHANGED rmState
BTManager == BTS \/ BTC \/ BTA
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating ==
/\ \A self \in ProcSet: pc[self] = "Done"
/\ UNCHANGED vars
Next == TManager \/ BTManager
\/ (\E self \in RM: RManager(self))
\/ Terminating
Spec ==
/\ Init /\ [][Next]_vars
/\ \A self \in RM: WF_vars(RManager(self))
/\ WF_vars(TManager)
/\ WF_vars(BTManager)
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION
(***************************************************************************)
(* The invariants: *)
(***************************************************************************)
TypeOK ==
(*************************************************************************)
(* The type-correctness invariant *)
(*************************************************************************)
/\ rmState \in [RM -> {"working", "prepared", "committed", "aborted", "failed"}]
/\ tmState \in {"init", "commit", "abort", "hidden"}
Consistency ==
(*************************************************************************)
(* A state predicate asserting that two RMs have not arrived at *)
(* conflicting decisions. *)
(*************************************************************************)
\A rm1, rm2 \in RM: ~
/\ rmState[rm1] = "aborted"
/\ rmState[rm2] = "committed"
NotCommitted == \A rm \in RM: rmState[rm] /= "committed"
================================================================================
\* Modification History
\* Last modified Wed Dec 13 14:34:34 EST 2017 by mad
\* Last modified Fri Nov 17 12:18:24 EST 2017 by murat
\* Last modified Tue Oct 11 08:14:15 PDT 2011 by lamport
\* Created Mon Oct 10 05:31:02 PDT 2011 by lamport