RafBroken.tla

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

TypeOk == /\ raf_requested \in [Pipeline -> BOOLEAN]
          /\ tick_received \in [Pipeline -> BOOLEAN]
  
RafInSync == \A p, pp \in Pipeline: 
                tick_received[p] => IF raf_requested[pp] 
                                    THEN tick_received[pp] 
                                    ELSE TRUE
----------------------------------------------------------------------------

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

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

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

RunRaf(p) == /\ tick_received[p] = TRUE
             /\ raf_requested' = [raf_requested EXCEPT ![p] = FALSE]
             /\ tick_received' = [tick_received EXCEPT ![p] = FALSE]

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

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