Skip to content

Instantly share code, notes, and snippets.

@gterzian

gterzian/RafDelivery.tla

Last active September 6, 2024 09:37
Download ZIP

Revisions

  1. gterzian revised this gist Sep 6, 2024. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion RafDelivery.tla
    View file
    Original file line number Diff line number Diff line change
    @@ -1,4 +1,4 @@
    ----------------------------- MODULE RafBroken -----------------------------
    ----------------------------- MODULE RafDelivery -----------------------------
    EXTENDS FiniteSets, Naturals
    VARIABLES raf_requested, tick_received
    CONSTANT N
  2. gterzian created this gist Sep 5, 2024.
    35 changes: 35 additions & 0 deletions RafDelivery.tla
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,35 @@
    ----------------------------- MODULE RafBroken -----------------------------
    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)
    =============================================================================