-------------------- MODULE SimpleDependencySetAlgorithm --------------------
(***************************************************************************)
(* Specification of the dependency-set algorithm describe in the PODC *)
(* brief announcement "A Family of Leaderless Algorithms". *)
(***************************************************************************)
EXTENDS Quorums, Maps, TLC
CONSTANTS
C \* the set of commands
(*
--algorithm DependencySet {
variables
\* announced[p] is the set of commands announced by p:
announced = [p \in P |-> {}],
\* deps[p][c] is the set of dependencies computed by p for
\* the command c:
deps = [p \in P |-> <<>>],
\* heardFrom[p][c] is the set of processes that responded with
\* dependencies for the command c:
heardFrom = [p \in P |-> <<>>]
define {
Proc(x) == x[1]
Cmd(x) == x[2]
\* The commands that p has seen so far:
Seen(p) == DOMAIN deps[p]
Correctness == \A p1,p2 \in P : \A c1,c2 \in C :
c1 # c2 /\ pc[<>] = "Done" /\ pc[<>] = "Done" =>
c2 \in deps[p1][c1] \/ c1 \in deps[p2][c2]
}
(***********************************************************************)
(* This process describes the process of p determining dependencies *)
(* for a command c. *)
(***********************************************************************)
process (announcer \in (P \times C)) {
l1: with (p = Proc(self), c = Cmd(self)) {
announced[p] := announced[p] \cup {c};
heardFrom[p] := @ ++ <>
};
l2: while (heardFrom[Proc(self)][Cmd(self)] \notin Quorum) with (q \in P) {
when Cmd(self) \in DOMAIN deps[q];
heardFrom[Proc(self)] := [@ EXCEPT ![Cmd(self)] = @ \cup {q}];
};
l3: with (Q = heardFrom[Proc(self)][Cmd(self)]) {
assert Q \in Quorum;
deps[Proc(self)] := @ ++ <>
}
}
process (acceptor \in P) {
l1: while (TRUE) with (q \in P, c \in C) {
when c \notin Seen(self) /\ c \in announced[q];
deps[self] := @ ++ <>
}
}
}
*)
\* BEGIN TRANSLATION
\* Label l1 of process announcer at line 41 col 18 changed to l1_
VARIABLES announced, deps, heardFrom, pc
(* define statement *)
Proc(x) == x[1]
Cmd(x) == x[2]
Seen(p) == DOMAIN deps[p]
Correctness == \A p1,p2 \in P : \A c1,c2 \in C :
c1 # c2 /\ pc[<>] = "Done" /\ pc[<>] = "Done" =>
c2 \in deps[p1][c1] \/ c1 \in deps[p2][c2]
vars == << announced, deps, heardFrom, pc >>
ProcSet == ((P \times C)) \cup (P)
Init == (* Global variables *)
/\ announced = [p \in P |-> {}]
/\ deps = [p \in P |-> <<>>]
/\ heardFrom = [p \in P |-> <<>>]
/\ pc = [self \in ProcSet |-> CASE self \in (P \times C) -> "l1_"
[] self \in P -> "l1"]
l1_(self) == /\ pc[self] = "l1_"
/\ LET p == Proc(self) IN
LET c == Cmd(self) IN
/\ announced' = [announced EXCEPT ![p] = announced[p] \cup {c}]
/\ heardFrom' = [heardFrom EXCEPT ![p] = @ ++ <>]
/\ pc' = [pc EXCEPT ![self] = "l2"]
/\ deps' = deps
l2(self) == /\ pc[self] = "l2"
/\ IF heardFrom[Proc(self)][Cmd(self)] \notin Quorum
THEN /\ \E q \in P:
/\ Cmd(self) \in DOMAIN deps[q]
/\ heardFrom' = [heardFrom EXCEPT ![Proc(self)] = [@ EXCEPT ![Cmd(self)] = @ \cup {q}]]
/\ pc' = [pc EXCEPT ![self] = "l2"]
ELSE /\ pc' = [pc EXCEPT ![self] = "l3"]
/\ UNCHANGED heardFrom
/\ UNCHANGED << announced, deps >>
l3(self) == /\ pc[self] = "l3"
/\ LET Q == heardFrom[Proc(self)][Cmd(self)] IN
/\ Assert(Q \in Quorum,
"Failure of assertion at line 50, column 17.")
/\ deps' = [deps EXCEPT ![Proc(self)] = @ ++ <>]
/\ pc' = [pc EXCEPT ![self] = "Done"]
/\ UNCHANGED << announced, heardFrom >>
announcer(self) == l1_(self) \/ l2(self) \/ l3(self)
l1(self) == /\ pc[self] = "l1"
/\ \E q \in P:
\E c \in C:
/\ c \notin Seen(self) /\ c \in announced[q]
/\ deps' = [deps EXCEPT ![self] = @ ++ <>]
/\ pc' = [pc EXCEPT ![self] = "l1"]
/\ UNCHANGED << announced, heardFrom >>
acceptor(self) == l1(self)
Next == (\E self \in (P \times C): announcer(self))
\/ (\E self \in P: acceptor(self))
Spec == Init /\ [][Next]_vars
\* END TRANSLATION
THEOREM Spec => []Correctness
TwoDecisions == \E p1,p2 \in P : \E c1,c2 \in C :
c1 # c2 /\ pc[<>] = "Done" /\ pc[<>] = "Done"
=============================================================================
\* Modification History
\* Last modified Tue May 24 11:37:31 EDT 2016 by nano
\* Created Mon May 23 21:42:49 EDT 2016 by nano