diff --git a/MCFPaxosFourAcc.tla b/MCFPaxosFourAcc.tla index 4c62aff..57e2297 100644 --- a/MCFPaxosFourAcc.tla +++ b/MCFPaxosFourAcc.tla @@ -3,9 +3,9 @@ EXTENDS FPaxos, TLC MCAcceptor == {"a1", "a2", "a3", "a4"} -MCValue == 0..1 +MCValue == 0..2 MCQuorum1 == {{"a1", "a2"}, {"a3", "a4"}} MCQuorum2 == {{"a1", "a3"}, {"a2", "a4"}} -MCBallot == 0..1 +MCBallot == 0..2 ==== \ No newline at end of file