[tlaplus] Re: General help with a simple spec

[Jones Martins <jonesmvc@xxxxxxxxx>]

Hi Mariusz,

Regarding the `AlwaysReset` property, this property is satisfied only in the first state of a behavior because it lacks a Box (“always”) operator ([]).

Your property asserts that, if some component is crashed in the first state, then eventually all components stay not crashed forever.

Is that what you meant to express?

A stronger version of this property would add include an “always” operator around it, such that we'd expect the property to be true in every state of a behavior.

[]((\E uid \in 1..N: components[uid].crashed) => <>[](\A uid \in 1..N: ~components[uid].crashed))

We could simplify it further with a “leads to” operator (~>):

(\E uid \in 1..N: components[uid].crashed) ~> <>[](\A uid \in 1..N: ~components[uid].crashed)

Jones

On Thursday 2 May 2024 at 14:23:17 UTC-3 Mariusz Ryndzionek wrote:

Hello everyone,

I have a fairly simple spec:

---- 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.

Dose this property make sens?
Are there any stricter properties that would make sense for this spec?
Can the spec be improved somehow?

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6c9b1eb7-507a-4fb9-b1ca-166bd533bfa0n%40googlegroups.com.