RafDelivery.tla

----------------------------- MODULE RafDelivery -----------------------------
EXTENDS FiniteSets, Naturals
VARIABLES raf_requested, tick_received
CONSTANT N
----------------------------------------------------------------------------
Pipeline == 0..N

TypeOk == /\ raf_requested \in [Pipeline -> BOOLEAN]
          /\ tick_received \in BOOLEAN
  
RafInSync == tick_received => \E p \in Pipeline: raf_requested[p]
----------------------------------------------------------------------------

Init == /\ raf_requested = [p \in Pipeline |-> FALSE]
        /\ tick_received = FALSE

RequestRaf(p) == /\ raf_requested' = [raf_requested EXCEPT ![p] = TRUE]
                 /\ UNCHANGED<<tick_received>>

ReceiveTick == /\ \E p \in Pipeline: raf_requested[p]
               /\ tick_received' = TRUE
               /\ UNCHANGED<<raf_requested>>

RunRaf == /\ tick_received = TRUE
          /\ raf_requested' = [p \in Pipeline |-> FALSE]
          /\ tick_received' = FALSE

Next == \E p \in Pipeline: \/ RequestRaf(p)
                           \/ ReceiveTick
                           \/ RunRaf

Spec  ==  Init /\ [][Next]_<<raf_requested, tick_received>>
----------------------------------------------------------------------------
THEOREM  Spec  =>  [](TypeOk /\ RafInSync)
=============================================================================