RenderingUpdateBatchingBroken.tla

---------------------- MODULE RenderingUpdateBatchingBroken ----------------------
EXTENDS FiniteSets, Naturals
VARIABLES task_queue, rendering_task_queued
CONSTANT N
----------------------------------------------------------------------------
Pipeline == 0..N

TypeOk == /\ task_queue \in [Pipeline -> BOOLEAN]
          /\ rendering_task_queued \in BOOLEAN

QueuedTaskRuns == rendering_task_queued => \E p \in Pipeline: task_queue[p]  
----------------------------------------------------------------------------

Init == /\ task_queue = [p \in Pipeline |-> FALSE]
        /\ rendering_task_queued = FALSE

QueueTask(p) == /\ rendering_task_queued = FALSE
                /\ rendering_task_queued' = TRUE
                /\ task_queue' = [task_queue EXCEPT ![p] = TRUE]

RunTask(p) == /\ task_queue[p] = TRUE
              /\ task_queue' = [task_queue EXCEPT ![p] = FALSE]
              /\ rendering_task_queued' = FALSE

ClosePipeline(p) == /\ task_queue' = [task_queue EXCEPT ![p] = FALSE]
                    /\ UNCHANGED<<rendering_task_queued>>

Next == \E p \in Pipeline: \/ QueueTask(p)
                           \/ RunTask(p)
                           \/ ClosePipeline(p)

Spec  ==  Init /\ [][Next]_<<task_queue, rendering_task_queued>>
----------------------------------------------------------------------------
THEOREM  Spec  =>  [](TypeOk /\ QueuedTaskRuns)
=============================================================================