libtlafmt 0.4.1

A formatter library for TLA+ specs, core of tlafmt
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/Majority.tla
---
------------------------------- MODULE Majority --------------------------------
(****************************************************************************)
(* TLA+ specification and proof of the majority vote algorithm due to Boyer *)
(* and Moore.                                                               *)
(* R.S. Boyer, J.S. Moore: MJRTY - A Fast Majority Vote Algorithm.          *)
(* In: R.S. Boyer (ed.): Automated Reasoning: Essays in Honor of Woody      *)
(* Bledsoe, pp. 105-117. Dordrecht, The Netherlands, 1991.                  *)
(* Originally published in a technical report from 1981.                    *)
(* The algorithm takes as input a sequence of values, makes one pass over   *)
(* the sequence, and reports an element cand such that no element other     *)
(* than cand may have an absolute majority in the sequence.                 *)
(****************************************************************************)
EXTENDS Integers, Sequences, FiniteSets

CONSTANT Value
ASSUME ConstAssump == Value # {}

(****************************************************************************)
(* Although seq is an input to the algorithm, we make it a variable so that *)
(* we can use the model checker to verify the algorithm for all sequences   *)
(* up to some bounded size.                                                 *)
(****************************************************************************)
VARIABLES
    seq,  \* input sequence of values, never changes 
    i,    \* next position of sequence to be checked
    cand, \* current candidate for having a majority
    cnt   \* lower bound for the number of occurrences of the candidate so far

vars == << seq, i, cand, cnt >>

TypeOK ==
    /\ seq \in Seq(Value)
    /\ i \in 1..Len(seq) + 1
    /\ cand \in Value
    /\ cnt \in Nat

Init ==
    /\ seq \in Seq(Value)
    /\ i = 1
    /\ cand \in Value
    /\ cnt = 0

Next ==
    /\ i <= Len(seq)
    /\ i' = i + 1 /\ seq' = seq
    /\
        \/
            /\ cnt = 0
            /\ cand' = seq[i]
            /\ cnt' = 1
        \/
            /\ cnt /= 0 /\ cand = seq[i]
            /\ cand' = cand
            /\ cnt' = cnt + 1
        \/
            /\ cnt /= 0 /\ cand /= seq[i]
            /\ cand' = cand
            /\ cnt' = cnt - 1

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

(****************************************************************************)
(* Definitions used for stating correctness.                                *)
(****************************************************************************)
\* set of indexes in the prefix of the sequence strictly before j holding v
PositionsBefore(v, j) == {k \in 1..(j - 1): seq[k] = v}
\* number of times v occurs in that prefix
OccurrencesBefore(v, j) == Cardinality(PositionsBefore(v, j))
\* number of times v occurs in all of the sequence
Occurrences(x) == OccurrencesBefore(x, Len(seq) + 1)

\* main correctness property: cand can be the only value that has a majority
Correct ==
    i > Len(seq) =>
        \A v \in Value: 2 * Occurrences(v) > Len(seq) => v = cand

\* inductive invariant for proving correctness
Inv ==
    /\ cnt <= OccurrencesBefore(cand, i)
    /\ 2 * (OccurrencesBefore(cand, i) - cnt) <= i - 1 - cnt
    /\ \A v \in Value \ {cand}: 2 * OccurrencesBefore(v, i) <= i - 1 - cnt

================================================================================