---- MODULE SimpleElection ----
EXTENDS Naturals, Integers, FiniteSets, Sequences, TLC

CONSTANTS Server
CONSTANTS Secondary, Primary, Nil
CONSTANT InitTerm

VARIABLE currentTerm
VARIABLE state

vars == <<currentTerm, state>>

\* The set of all quorums in a given set.
Quorums == {i \in SUBSET Server : Cardinality(i) * 2 > Cardinality(Server)}

\* Node 'i' gets elected as a primary.
BecomeLeader(i, voteQuorum) == 
    LET newTerm == currentTerm[i] + 1 IN
    /\ i \in voteQuorum \* The new leader should vote for itself.
    /\ \A v \in voteQuorum : currentTerm[v] < newTerm
    \* Update the terms of each voter.
    /\ currentTerm' = [s \in Server |-> IF s \in voteQuorum THEN newTerm ELSE currentTerm[s]]
    /\ state' = [s \in Server |->
                    IF s = i THEN Primary
                    ELSE IF s \in voteQuorum THEN Secondary \* All voters should revert to secondary state.
                    ELSE state[s]]    \* Allow new leaders to write a no-op on step up if they want to. It is optional, but permissible.

Init == 
    /\ currentTerm = [i \in Server |-> InitTerm]
    /\ state       = [i \in Server |-> Secondary]

Next == \E s \in Server : \E Q \in Quorums : BecomeLeader(s, Q)

Spec == Init /\ [][Next]_vars

UniqueLeader == \A s,t \in Server : 
    (/\ state[s] = Primary 
     /\ state[t] = Primary
     /\ currentTerm[s] = currentTerm[t]) => (s = t)

------------------------------------------------

CONSTANTS MaxTerm

StateConstraint == \A s \in Server : currentTerm[s] <= MaxTerm

Range(T) == { T[x] : x \in DOMAIN T }
Min(S) == CHOOSE x \in S: \A y \in S \ {x}: y > x

\*
\* Define a view expression that shifts all terms so 
\* that the minimum term value in the current state is shifted
\* down to zero.
\*

MinTerm == Min(Range(currentTerm))

currentTermsShifted == [s \in Server |-> (currentTerm[s] - MinTerm)]

View == <<currentTermsShifted, state>>

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