---- MODULE watchdog ----
EXTENDS Integers, FiniteSets
CONSTANTS N, T
VARIABLE components, watchdog
vars == <<components, watchdog>>
TypeOK == /\ components \in [1..N -> [timer : 0..T,
timeout : 0..T,
crashed : BOOLEAN]]
/\ watchdog \in [1..N -> [timer : 0..T + 1]]
Init == /\ components \in [1..N -> {[timer |-> x,
timeout |-> x,
crashed |-> FALSE] : x \in 1..T}]
/\ watchdog = [uid \in 1..N |-> [timer |-> components[uid].timeout + 1]]
Run(uid) == /\ watchdog[uid].timer /= 0
/\ components' = LET Advance(c) == IF c.crashed
THEN c
ELSE IF c.timer > 0
THEN [c EXCEPT !.timer = @ - 1]
ELSE [c EXCEPT !.timer = c.timeout]
IN [components EXCEPT ![uid] = Advance(components[uid])]
/\ watchdog' = LET Dec(id) == IF watchdog[id].timer > 0
THEN watchdog[id].timer - 1
ELSE 0
Poke(id) == IF components[id].crashed
THEN Dec(id)
ELSE IF (components[id].timer = 0)
THEN components[id].timeout + 1
ELSE Dec(id)
IN [watchdog EXCEPT ![uid].timer = Poke(uid)]
Crash(uid) == /\ ~components[uid].crashed
/\ components' = [components EXCEPT ![uid].crashed = TRUE]
/\ UNCHANGED watchdog
Reset == /\ \E uid \in 1..N : watchdog[uid].timer = 0
/\ watchdog' = [uid \in 1..N |-> [timer |-> components[uid].timeout + 1]]
/\ components' = [uid \in 1..N |-> [timer |-> components[uid].timeout,
timeout |-> components[uid].timeout,
crashed |-> FALSE]]
Next == (\E uid \in 1..N : Run(uid)) \/ (\E uid \in 1..N : Crash(uid)) \/ Reset
Spec == Init /\ [][Next]_vars
FairSpec == Spec /\ WF_vars(Next)
AlwaysReset == (\E uid \in 1..N : components[uid].crashed) => <>[](\A uid \in 1..N : ~components[uid].crashed)
====
Components have a timer which they decrease.
Watchdog maintains its own set of timers for each component, with starting
value one greater than the given component timer. If component timer
reaches zero, the timer and the corresponding watchdog timer are reset.
A component can crash and in this case it won't decrease its timer.
If one of the watchdog timers reaches zero, the whole system is restarted.
Here is a graph for N=1 and T=1:
I've added one temporal property:
AlwaysReset == (\E uid \in 1..N : components[uid].crashed) => <>[](\A uid \in 1..N : ~components[uid].crashed)
TLC seems to verify it successfully.