RenderingUpdateBatching.tla

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

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

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

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

QueueTask(p) == /\ p \notin closed
                /\ rendering_task_queued[p] = FALSE
                /\ rendering_task_queued' 
                    = [rendering_task_queued EXCEPT ![p] = TRUE]
                /\ task_queue' = [task_queue EXCEPT ![p] = TRUE]
                /\ UNCHANGED<<closed>>

RunTask(p) == /\ task_queue[p] = TRUE
              /\ task_queue' = [task_queue EXCEPT ![p] = FALSE]
              \* The below resets the batching for all pipelines.
              /\ rendering_task_queued' = [pp \in Pipeline |-> FALSE]
              /\ UNCHANGED<<closed>>

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

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

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