Skip to content

Commit ca36eec

Browse files
muenchnerkindlmuenchnerkindl
authored
Majority (#93)
* Boyer-Moore majority vote algorithm Signed-off-by: merz <[email protected]> * add Majority algorithm to README and manifest Signed-off-by: merz <[email protected]> * added standard TLAPS module to Majority example Signed-off-by: merz <[email protected]> * fixed time format for model checking Signed-off-by: merz <[email protected]> * removing TLAPS module from Majority Signed-off-by: merz <[email protected]> --------- Signed-off-by: merz <[email protected]>
1 parent b6c1bf6 commit ca36eec

File tree

7 files changed

+280
-1
lines changed

7 files changed

+280
-1
lines changed

‎README.md

+1
Original file line numberDiff line numberDiff line change
@@ -118,6 +118,7 @@ A central manifest of specs with descriptions and accounts of their various mode
118118
| 101 | Learn TLA⁺ Proofs | <a href="specifications/LearnProofs">Basic PlusCal algorithms and formal proofs of their correctness</a> | Andrew Helwer | &#10004; | &#10004; | Sequences, Naturals, Integers, TLAPS | &#10004; | |
119119
| 102 | Lexicographically-Least Circular Substring | <a href="specifications/LeastCircularSubstring">Booth's 1980 algorithm to find the lexicographically-least circular substring</a> | Andrew Helwer | | &#10004; | FiniteSets, Integers, Naturals, Sequences | &#10004; | |
120120
| 103 | Distributed Checkpoint Coordination | <a href="specifications/CheckpointCoordination">Algorithm for coordinating checkpoint/snapshot leases in a Paxos ring</a> | Andrew Helwer | | &#10004; | FiniteSets, Naturals, Sequences, TLC | | |
121+
| 104 | Boyer-Moore Majority Vote | <a href="specifications/Majority">Efficient algorithm for finding a majority value</a> | Stephan Merz | &#10004; | &#10004; | Integers, Sequences, FiniteSets, TLAPS | | |
121122

122123
## License
123124

‎manifest.json

+46-1
Original file line numberDiff line numberDiff line change
@@ -546,7 +546,7 @@
546546
"tlaLanguageVersion": 2,
547547
"features": [],
548548
"models": []
549-
}
549+
}
550550
]
551551
},
552552
{
@@ -3698,6 +3698,51 @@
36983698
"models": []
36993699
}
37003700
]
3701+
},
3702+
{
3703+
"path": "specifications/Majority",
3704+
"title": "Boyer-Moore majority vote algorithm",
3705+
"description": "An efficient algorithm for detecting a majority value in a sequence",
3706+
"source": "",
3707+
"authors": [
3708+
"Stephan Merz"
3709+
],
3710+
"tags": ["beginner"],
3711+
"modules": [
3712+
{
3713+
"path": "specifications/Majority/Majority.tla",
3714+
"communityDependencies": [],
3715+
"tlaLanguageVersion": 2,
3716+
"features": [],
3717+
"models": []
3718+
},
3719+
{
3720+
"path": "specifications/Majority/MCMajority.tla",
3721+
"communityDependencies": [],
3722+
"tlaLanguageVersion": 2,
3723+
"features": [],
3724+
"models": [
3725+
{
3726+
"path": "specifications/Majority/MCMajority.cfg",
3727+
"runtime": "00:00:05",
3728+
"size": "small",
3729+
"mode": "exhaustive search",
3730+
"config": ["ignore deadlock"],
3731+
"features": [],
3732+
"result": "success"
3733+
}
3734+
]
3735+
},
3736+
{
3737+
"path": "specifications/Majority/MajorityProof.tla",
3738+
"communityDependencies": [],
3739+
"tlaLanguageVersion": 2,
3740+
"features": [
3741+
"proof"
3742+
],
3743+
"models": []
3744+
}
3745+
]
37013746
}
37023747
]
37033748
}

‎specifications/Majority/MCMajority.cfg

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
SPECIFICATION Spec
2+
3+
CONSTANTS
4+
A = A
5+
B = B
6+
C = C
7+
bound = 5
8+
Seq <- BoundedSeq
9+
10+
INVARIANTS
11+
TypeOK
12+
Correct
13+
Inv
14+
15+
CHECK_DEADLOCK FALSE

‎specifications/Majority/MCMajority.tla

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
------------------------- MODULE MCMajority ----------------------------------
2+
(****************************************************************************)
3+
(* TLA+ module for model checking the majority vote algorithm for all *)
4+
(* sequences over three elements of bounded length. *)
5+
(****************************************************************************)
6+
EXTENDS Integers
7+
CONSTANTS A, B, C, bound
8+
ASSUME bound \in Nat
9+
10+
Value == {A,B,C}
11+
BoundedSeq(S) == UNION { [1 .. n -> S] : n \in 0 .. bound }
12+
13+
VARIABLES seq, i, cand, cnt
14+
15+
INSTANCE Majority
16+
17+
==============================================================================

‎specifications/Majority/Majority.tla

+79
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,79 @@
1+
-------------------------------- MODULE Majority -----------------------------
2+
(****************************************************************************)
3+
(* TLA+ specification and proof of the majority vote algorithm due to Boyer *)
4+
(* and Moore. *)
5+
(* R.S. Boyer, J.S. Moore: MJRTY - A Fast Majority Vote Algorithm. *)
6+
(* In: R.S. Boyer (ed.): Automated Reasoning: Essays in Honor of Woody *)
7+
(* Bledsoe, pp. 105-117. Dordrecht, The Netherlands, 1991. *)
8+
(* Originally published in a technical report from 1981. *)
9+
(* The algorithm takes as input a sequence of values, makes one pass over *)
10+
(* the sequence, and reports an element cand such that no element other *)
11+
(* than cand may have an absolute majority in the sequence. *)
12+
(****************************************************************************)
13+
EXTENDS Integers, Sequences, FiniteSets
14+
15+
CONSTANT Value
16+
ASSUME ConstAssump == Value # {}
17+
18+
(****************************************************************************)
19+
(* Although seq is an input to the algorithm, we make it a variable so that *)
20+
(* we can use the model checker to verify the algorithm for all sequences *)
21+
(* up to some bounded size. *)
22+
(****************************************************************************)
23+
VARIABLES
24+
seq, \* input sequence of values, never changes
25+
i, \* next position of sequence to be checked
26+
cand, \* current candidate for having a majority
27+
cnt \* lower bound for the number of occurrences of the candidate so far
28+
29+
vars == <<seq, i, cand, cnt>>
30+
31+
TypeOK ==
32+
/\ seq \in Seq(Value)
33+
/\ i \in 1 .. Len(seq)+1
34+
/\ cand \in Value
35+
/\ cnt \in Nat
36+
37+
Init ==
38+
/\ seq \in Seq(Value)
39+
/\ i = 1
40+
/\ cand \in Value
41+
/\ cnt = 0
42+
43+
Next ==
44+
/\ i <= Len(seq)
45+
/\ i' = i+1 /\ seq' = seq
46+
/\ \/ /\ cnt = 0
47+
/\ cand' = seq[i]
48+
/\ cnt' = 1
49+
\/ /\ cnt # 0 /\ cand = seq[i]
50+
/\ cand' = cand
51+
/\ cnt' = cnt + 1
52+
\/ /\ cnt # 0 /\ cand # seq[i]
53+
/\ cand' = cand
54+
/\ cnt' = cnt - 1
55+
56+
Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
57+
58+
(****************************************************************************)
59+
(* Definitions used for stating correctness. *)
60+
(****************************************************************************)
61+
\* set of indexes in the prefix of the sequence strictly before j holding v
62+
PositionsBefore(v,j) == { k \in 1 .. (j-1) : seq[k] = v }
63+
\* number of times v occurs in that prefix
64+
OccurrencesBefore(v,j) == Cardinality(PositionsBefore(v,j))
65+
\* number of times v occurs in all of the sequence
66+
Occurrences(x) == OccurrencesBefore(x, Len(seq)+1)
67+
68+
\* main correctness property: cand can be the only value that has a majority
69+
Correct ==
70+
i > Len(seq) =>
71+
\A v \in Value : 2 * Occurrences(v) > Len(seq) => v = cand
72+
73+
\* inductive invariant for proving correctness
74+
Inv ==
75+
/\ cnt <= OccurrencesBefore(cand, i)
76+
/\ 2 * (OccurrencesBefore(cand, i) - cnt) <= i - 1 - cnt
77+
/\ \A v \in Value \ {cand} : 2 * OccurrencesBefore(v, i) <= i - 1 - cnt
78+
79+
==============================================================================

‎specifications/Majority/MajorityProof.tla

+99
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,99 @@
1+
-------------------------- MODULE MajorityProof ------------------------------
2+
EXTENDS Majority, FiniteSetTheorems, TLAPS
3+
4+
(***************************************************************************)
5+
(* Proving type correctness is easy. *)
6+
(***************************************************************************)
7+
LEMMA TypeCorrect == Spec => []TypeOK
8+
<1>1. Init => TypeOK
9+
BY DEF Init, TypeOK
10+
<1>2. TypeOK /\ [Next]_vars => TypeOK'
11+
BY DEF TypeOK, Next, vars
12+
<1>. QED BY <1>1, <1>2, PTL DEF Spec
13+
14+
(***************************************************************************)
15+
(* Auxiliary lemmas about positions and occurrences. *)
16+
(***************************************************************************)
17+
LEMMA PositionsOne == \A v : PositionsBefore(v,1) = {}
18+
BY DEF PositionsBefore
19+
20+
LEMMA PositionsType == \A v, j : PositionsBefore(v,j) \in SUBSET (1 .. j-1)
21+
BY DEF PositionsBefore
22+
23+
LEMMA PositionsFinite ==
24+
ASSUME NEW v, NEW j \in Int
25+
PROVE IsFiniteSet(PositionsBefore(v,j))
26+
BY 1 \in Int, j-1 \in Int, PositionsType, FS_Interval, FS_Subset, Zenon
27+
28+
LEMMA PositionsPlusOne ==
29+
ASSUME TypeOK, NEW j \in 1 .. Len(seq), NEW v
30+
PROVE PositionsBefore(v, j+1) =
31+
IF seq[j] = v THEN PositionsBefore(v,j) \union {j}
32+
ELSE PositionsBefore(v,j)
33+
BY DEF TypeOK, PositionsBefore
34+
35+
LEMMA OccurrencesType == \A v : \A j \in Int : OccurrencesBefore(v,j) \in Nat
36+
BY PositionsFinite, FS_CardinalityType DEF OccurrencesBefore
37+
38+
LEMMA OccurrencesOne == \A v : OccurrencesBefore(v,1) = 0
39+
BY PositionsOne, FS_EmptySet DEF OccurrencesBefore
40+
41+
LEMMA OccurrencesPlusOne ==
42+
ASSUME TypeOK, NEW j \in 1 .. Len(seq), NEW v
43+
PROVE OccurrencesBefore(v, j+1) =
44+
IF seq[j] = v THEN OccurrencesBefore(v,j) + 1
45+
ELSE OccurrencesBefore(v,j)
46+
<1>1. CASE seq[j] = v
47+
<2>1. IsFiniteSet(PositionsBefore(v,j))
48+
BY PositionsFinite
49+
<2>2. j \notin PositionsBefore(v,j)
50+
BY PositionsType
51+
<2>3. PositionsBefore(v, j+1) = PositionsBefore(v,j) \union {j}
52+
BY <1>1, PositionsPlusOne, Zenon
53+
<2>. QED BY <1>1, <2>1, <2>2, <2>3, FS_AddElement DEF OccurrencesBefore
54+
<1>2. CASE seq[j] # v
55+
BY <1>2, PositionsPlusOne, Zenon DEF OccurrencesBefore
56+
<1>. QED BY <1>1, <1>2
57+
58+
(***************************************************************************)
59+
(* We prove correctness based on the inductive invariant. *)
60+
(***************************************************************************)
61+
LEMMA Correctness == Spec => []Correct
62+
<1>1. Init => Inv
63+
BY OccurrencesOne DEF Init, Inv
64+
<1>2. TypeOK /\ Inv /\ [Next]_vars => Inv'
65+
<2>. SUFFICES ASSUME TypeOK, Inv, Next PROVE Inv'
66+
BY DEF Inv, vars, OccurrencesBefore, PositionsBefore
67+
<2>. i <= Len(seq) /\ i' = i+1 /\ seq' = seq
68+
BY DEF Next
69+
<2>0. \A v \in Value : OccurrencesBefore(v, i)' = OccurrencesBefore(v, i')
70+
BY DEF OccurrencesBefore, PositionsBefore
71+
<2>. USE OccurrencesType DEF TypeOK
72+
<2>1. CASE cnt = 0 /\ cand' = seq[i] /\ cnt' = 1
73+
<3>1. i \in PositionsBefore(seq[i], i+1)
74+
BY DEF PositionsBefore
75+
<3>2. 1 <= OccurrencesBefore(seq[i], i+1)
76+
BY <3>1, PositionsFinite, FS_EmptySet DEF OccurrencesBefore
77+
<3>3. 2 * (OccurrencesBefore(seq[i], i+1) - 1) <= (i+1) - 1 - 1
78+
BY <2>1, OccurrencesPlusOne DEF Inv
79+
<3>4. ASSUME NEW v \in Value \ {seq[i]}
80+
PROVE 2 * OccurrencesBefore(v, i+1) <= (i+1) - 1 - 1
81+
BY <2>1, OccurrencesPlusOne DEF Inv
82+
<3>. QED BY <2>0, <2>1, <3>2, <3>3, <3>4 DEF Inv
83+
<2>2. CASE cnt # 0 /\ cand = seq[i] /\ cand' = cand /\ cnt' = cnt + 1
84+
BY <2>0, <2>2, OccurrencesPlusOne DEF Inv
85+
<2>3. CASE cnt # 0 /\ cand # seq[i] /\ cand' = cand /\ cnt' = cnt - 1
86+
<3>10. cnt' <= OccurrencesBefore(cand', i')
87+
BY <2>3, OccurrencesPlusOne DEF Inv
88+
<3>20. 2 * (OccurrencesBefore(cand', i') - cnt') <= i' - 1 - cnt'
89+
BY <2>3, OccurrencesPlusOne DEF Inv
90+
<3>30. ASSUME NEW v \in Value \ {cand'}
91+
PROVE 2 * OccurrencesBefore(v, i') <= i' - 1 - cnt'
92+
BY <2>3, OccurrencesPlusOne DEF Inv
93+
<3>. QED BY <2>0, <2>3, <3>10, <3>20, <3>30 DEF Inv
94+
<2>. QED BY <2>1, <2>2, <2>3 DEF Next
95+
<1>3. TypeOK /\ Inv => Correct
96+
BY OccurrencesType DEF TypeOK, Inv, Correct, Occurrences
97+
<1>. QED BY <1>1, <1>2, <1>3, TypeCorrect, PTL DEF Spec
98+
99+
==============================================================================

‎specifications/Majority/README.md

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
# Efficient majority vote algorithm
2+
3+
A specification of an efficient algorithm due to R.S. Boyer and J.S. Moore
4+
for computing the only candidate in a sequence who may occur in a strict
5+
majority of positions in the sequence. The algorithm makes a single pass
6+
over the sequence and uses only two integer variables and one variable
7+
holding the current candidate. A very simple second pass over the sequence
8+
could then detect whether the candidate actually holds a majority.
9+
10+
The algorithm was published in a technical report in 1981, but only
11+
appeared in print ten years later.
12+
13+
R.S. Boyer, J.S. Moore: MJRTY - A Fast Majority Vote Algorithm.
14+
In: R.S. Boyer (ed.): Automated Reasoning: Essays in Honor of Woody
15+
Bledsoe, pp. 105-117. Dordrecht, The Netherlands, 1991.
16+
17+
18+
The module Majority contains the specification of the algorithm in TLA+, as well
19+
as its main correctness property, a type-correctness invariant, and an
20+
inductive invariant used for establishing correctness. Module MCMajority
21+
can be used to model check the algorithm for all sequences of three elements
22+
of bounded length. Module MajorityProof contains an interactive proof of
23+
correctness that can be checked using TLAPS.

0 commit comments

Comments
 (0)