token_ring_protocol_v1.tla

----------------------------- MODULE TokenRing -----------------------------

EXTENDS Naturals, Sequences

CONSTANT N, Data, NULL, MaxLength

ASSUME N > 0

Nodes == 1..N

VARIABLES token, active, messages, buffer

TypeOK == 
    /\ token \in Nodes
    /\ active \in [Nodes -> BOOLEAN]
    /\ messages \in [Nodes -> Seq(Data)]
    /\ buffer \in [Nodes -> Data \union {NULL}]

Init == 
    /\ token = 1
    /\ active = [n \in Nodes |-> IF n = 1 THEN TRUE ELSE FALSE]
    /\ messages = [n \in Nodes |-> << >>]
    /\ buffer = [n \in Nodes |-> NULL]

SendMessage(n) ==
    /\ active[n]
    /\ buffer[n] = NULL
    /\ Len(messages[n]) < MaxLength
    /\ \E d \in Data:
        /\ messages' = [messages EXCEPT ![n] = Append(@, d)]
        /\ UNCHANGED <<token, active, buffer>>

ReceiveMessage(n) ==
    /\ active[n]
    /\ buffer[n] = NULL
    /\ messages[n] # << >>
    /\ buffer' = [buffer EXCEPT ![n] = Head(messages[n])]
    /\ messages' = [messages EXCEPT ![n] = Tail(@)]
    /\ UNCHANGED <<token, active>>

DeactivateNode ==
    /\ active[token]
    /\ active' = [active EXCEPT ![token] = FALSE]
    /\ UNCHANGED <<token, messages, buffer>>

ActivateNextNode ==
    /\ ~active[token]
    /\ token' = IF token = N THEN 1 ELSE token + 1
    /\ active' = [active EXCEPT ![token'] = TRUE]
    /\ buffer' = [buffer EXCEPT ![token'] = NULL]
    /\ UNCHANGED messages

Next ==
    \/ \E n \in Nodes: 
        /\ active[n]
        /\ (SendMessage(n) \/ ReceiveMessage(n))
    \/ DeactivateNode
    \/ ActivateNextNode
    

Spec == Init /\ [][Next]_<<token, active, messages, buffer>>

=============================================================================
\* Modification History
\* Last modified Sun Oct 20 15:53:52 CEST 2024 by yio
\* Created Sat Oct 19 20:39:00 CEST 2024 by yio