Log repair tla+ specification

LogRepair.tla

---- MODULE LogRepair ----
EXTENDS TLC, Naturals

CONSTANTS Process, MaxLog

ASSUME Process \in SUBSET Nat

ASSUME MaxLog \in Nat \ {0}

VARIABLES state, missings, max_logs, logs, decisions
vars == <<state, missings, max_logs, logs, decisions>>

Init ==
    /\ state = [ i \in Process |-> "Running" ]
    /\ missings = [ i \in Process |-> {} ]
    /\ logs = [ i \in Process |-> {} ]
    /\ max_logs = [ i \in Process |-> 0 ]
    /\ decisions = {}

(*******************************************************************)
(* There's a consensus on the next log_id, leader decides candidate. *)
(* If the leader fails, paxos/raft ensure that this values will always *)
(* be chosen for log_id. Since we don't model the consensus itself, *)
(* any decided value remain until the end. *)
(*******************************************************************)
Decide(p, candidate) ==
    /\ state[p] = "Running"
    /\ max_logs[p] + 1 = candidate
    /\ logs' = [logs EXCEPT ![p] = logs[p] \union {candidate}]
    /\ max_logs' = [max_logs EXCEPT ![p] = candidate]
    /\ decisions' = decisions \union {candidate}
    /\ UNCHANGED <<state, missings>>

(*******************************************************************)
(* Any currently running node (it thinks it is up-to-date) receives a decision result. *)
(* Either the decision is the log next value, and every keeps on going. *)
(* Or, the node is not up to date and considers itself in "Repair" state. *)
(*******************************************************************)
Learn(p, l) ==
    /\ state[p] = "Running"
    /\ max_logs[p] = l
    /\ \E learned \in decisions:
        \/ /\ learned = l
           /\ max_logs' = [max_logs EXCEPT ![p] = learned]
           /\ logs' = [logs EXCEPT ![p] = logs[p] \union {learned}]
           /\ UNCHANGED <<state, missings, decisions>>
        \/ /\ learned > l
           /\ state' = [state EXCEPT ![p] = "Repair"]
           /\ max_logs' = [max_logs EXCEPT ![p] = learned]
           /\ missings' = [missings EXCEPT ![p] = l..learned]
           /\ logs' = [logs EXCEPT ![p] = logs[p] \union {learned}]
           /\ UNCHANGED <<decisions>>

(*******************************************************************)
(* Node in repair state learns (through the consensus algorithm *)
(* implementation details) some missing value. *)
(* Once the last missing value is recovered the node consider itself *)
(* running again. *)
(*******************************************************************)
Repair(p, l) ==
    /\ state[p] = "Repair"
    /\ l \in missings[p]
    /\ \E decision \in decisions:
        /\ decision = l
        /\ \/ /\ missings[p] = {l}
              /\ missings' = [missings EXCEPT ![p] = missings[p] \ {l}]
              /\ logs' = [logs EXCEPT ![p] = logs[p] \union {l}]
              /\ state' = [state EXCEPT ![p] = "Running"]
              /\ UNCHANGED <<decisions, max_logs>>
           \/ /\ missings[p] /= {l}
              /\ missings' = [missings EXCEPT ![p] = missings[p] \ {l}]
              /\ logs' = [logs EXCEPT ![p] = logs[p] \union {l}]
              /\ UNCHANGED <<state, decisions, max_logs>>

----

Next ==
    \/ \E l \in 1..MaxLog: \E p \in Process:
        \/ Learn(p, l)
        \/ Decide(p, l)
        \/ Repair(p, l)
    \/ UNCHANGED vars

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

----

(*******************************************************************)
(* eventually every process logged every values and is running *)
(*******************************************************************)
EveryRunningProcessLearnAllValues == <>(\A p \in Process: state[p] = "Running" /\ logs[p] = 1..MaxLog)

(*******************************************************************)
(* There is always a running node, such as progress is always garanteed  *)
(* by the consensus algorithm. *)
(*******************************************************************)
AtLeastOneProcessIsRunning == [](\E s \in DOMAIN state: state[s] = "Running")

====