Skip to content
This repository has been archived by the owner on Oct 13, 2022. It is now read-only.

Commit

Permalink
Fixed minor typos.
Browse files Browse the repository at this point in the history
  • Loading branch information
lemmy committed Apr 13, 2022
1 parent 29c7a2d commit 8cfbcb3
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 3 deletions.
2 changes: 1 addition & 1 deletion specifications/PaxosHowToWinATuringAward/Consensus.tla
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 11,7 @@
(* initially empty, it can be set to a single value, and then it can never *)
(* change. *)
(* *)
(* We are ignoring liveness, so we do not any requirement that a value is *)
(* We are ignoring liveness, so we do not require that a value is *)
(* eventually chosen. *)
(***************************************************************************)

Expand Down
4 changes: 2 additions & 2 deletions specifications/PaxosHowToWinATuringAward/Voting.tla
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 65,7 @@ TypeOK ==
(***************************************************************************)
VotedFor(a, b, v) == <<b, v>> \in votes[a]
(************************************************************************)
(* True iff (if and only if) acceptor a has votted for value v in *)
(* True iff (if and only if) acceptor a has voted for value v in *)
(* ballot number b. *)
(************************************************************************)

Expand All @@ -86,7 86,7 @@ chosen == {v \in Value : \E b \in Ballot : ChosenAt(b, v)}

DidNotVoteAt(a, b) == \A v \in Value : ~ VotedFor(a, b, v)
(************************************************************************)
(* True iff acceptor `a' has not voted in ballot number . *)
(* True iff acceptor `a' has not voted in ballot number. *)
(************************************************************************)

CannotVoteAt(a, b) == /\ maxBal[a] > b
Expand Down

0 comments on commit 8cfbcb3

Please sign in to comment.