## Chandra-Toueg

### Safety properties

Below are the safety properties we want to verify, in negated form.

Exists only one Coordinator in the system:

∃ x,y. x≠y ∧ (
Coord[x] = True ∧ Coord[y] = True
)

If 'c' is Coordinator, all other process with Id < c have
already been Coordinator:

∃ x,y. x≠y ∧ (
Coord[x] = True ∧ ACoord[y] = False ∧ y < x
)

A Coordinator can't have Id[] greater than his Identificator:

∃ x. (
Coord[x] = True ∧ Id_valid[x] = MValid ∧ x < Id[x]
)

A process can't have Id[] greater than Coordinator's Identificator:

∃ x,y. x≠y ∧ (
Coord[x] = True ∧ Id_valid[y] = MValid ∧ x < Id[y]
)

In the first Round a process can't have Id[] equals to the
Coordinator's Identificator:

∃ x,y. x≠y ∧ (
Round = R1 ∧ Coord[x] = True ∧ Id_valid[y] = MValid ∧ Id[y] = x
)

A correct process can't receive any Nack:

∃ x. (
Faulty[x] = False ∧ Nack[x] = True
)

Coordinators are elected in order by Identificator:

∃ x,y. x≠y ∧ (
Coord[x] = True ∧ ACoord[y] = True ∧ x < y
)

LEMMA 2.1:

∃ x,y,z. x≠y≠z ∧ (
State[x] = True ∧ Received[x] = True ∧ Coord[y] = True ∧

State[z] = False ∧ Faulty[z]= False ∧ Estimate[y] ≠ Estimate[z]
)

LEMMA 2.2:

∃ x,y. x≠y ∧ (
Round ≠ R1 ∧ State[x] = False ∧ Faulty[x] = False ∧

ProcessReceivedEstimate[x] = True ∧ Coord[y] = True ∧
Estimate[x] ≠ Estimate[y]
)

LEMMA 2.3:

∃ x,y. x≠y ∧ (
Coord[x] = True ∧ Faulty[x] = False ∧ Round = R6 ∧
State[y] = False ∧ Faulty[y] = False
)

AGREEMENT - complete:

∃ x,y. x≠y ∧ (
State[x] = True ∧ Faulty[x] = False ∧
State[y] = True ∧ Faulty[y] = False ∧

DecisionValue[x] ≠ DecisionValue[y]
)

### Options used

-brab 2

### Inferred invariants

All invariants are shown in their negated form, where
#1 and #2
are distinct existentially quantified variables.

Received[#1] = True && Id_valid[#1] = M1 State[#1] = False && ACoord[#1] = True Id_valid[#1] = M1 && ProcessReceivedEstimate[#1] = True Round = R1 && Received[#1] = True Round = R7 && Coord[#1] = True

You can find the list of all invariants that can be extracted from BRAB here (also in negated form), this collection being inductive.

### Search graph

The algorithm starts from the formula located at the bottom,
inside a red
octagon. Variables #1, #2,
… that appear
in the nodes are distinct skolem variables so we show a formula
φ(#1, #2) as equivalent to ∃
z_{1}, z_{2}.
z_{1} ≠ z_{2} ∧ φ(z_{1},
z_{2}). Plain black edges represent
pre-image relations and are annotated by the transition instance that
was considered. Black circles denote nodes that were obtained by
pre-image computation and were not covered by already visited
nodes. The nodes circled in gray are the one that were not
useful because they were subsumed by formulas pointed by the
gray dashed
arrows. Approximations are shown
in blue rectangles. Each approximation originates from the node that
connects its rectangle with a bold dashed blue edge.

- Graph of first run on Chandra-Toueg in dot format (1.7 MB)
- Graph of first run on Chandra-Toueg in SVG format (13 MB)
- Graph of second run on Chandra-Toueg in dot format (3 MB)
- Graph of second run on Chandra-Toueg in SVG format (22 MB)
- Final graph of on Chandra-Toueg in dot format (5.6 MB)
- Final graph of on Chandra-Toueg in SVG format (40 MB)