CanvasRenderingNonBlocking.tla

-------------------------- MODULE CanvasRendering --------------------------
EXTENDS FiniteSets, Integers, Sequences
VARIABLES images_updated, display_lists_applied, 
           compositor_messages, canvas_state,
           pending_display_list
CONSTANT N
----------------------------------------------------------------------------

Messages == {"DISPLAY_LIST", "UPDATE_IMAGE"}

CanvasState == {"PENDING", "UPDATED"}

TypeOk == /\ images_updated \in Int
          /\ display_lists_applied \in Int
          /\ compositor_messages \in Seq(Messages)
          /\ canvas_state \in CanvasState
          /\ pending_display_list \in BOOLEAN

ReadyToApplyDisplayList == images_updated = display_lists_applied + 1
ImageUpdatedAndDisplayListApplied == images_updated = display_lists_applied

IsUpdateMessage(m) == m = "UPDATE_IMAGE"

\* Why is the ImageUpdatesAndDisplayListsInSync invariant respected?
\* Because, when the canvas has been updated:
InductiveInvariant == canvas_state = "UPDATED" 
                       => \* Either the "UPDATE_IMAGE" is in the queue,
                          \* and the compositor is not ready to apply any display list.
                          \* So any received display list must be buffered until the image has been updated.
                          \/ /\ Len(SelectSeq(compositor_messages, IsUpdateMessage)) = 1
                             /\ \neg ReadyToApplyDisplayList
                          \* Or we're ready to apply a display list.
                          \/ ReadyToApplyDisplayList
                          \* Or we've ready processed everything.
                          \/ ImageUpdatedAndDisplayListApplied


\* At all times
\* Updates of images and applying of display list must be either:
\* in sync, or
\* an image has been updated but the display list hasn't been received yet.
\* This means that for an update cycle, 
\* a display list must not be processed ahead of having updated an image.
ImageUpdatesAndDisplayListsInSync == \/ ImageUpdatedAndDisplayListApplied
                                     \/ ReadyToApplyDisplayList

\* Canvas starts in pending state.
Init == /\ images_updated = 0
        /\ display_lists_applied = 0
        /\ compositor_messages = <<>>
        /\ canvas_state = "PENDING"
        /\ pending_display_list = FALSE
       
\* Layout sets canvas state to pending, 
\* but does not block on the canvas update. 
\* Limiting model size with first two conditions.
LayoutSendsDisplayList == 
                          /\ images_updated < N
                          /\ Len(compositor_messages) < N
                          /\ compositor_messages' = Append(compositor_messages, "DISPLAY_LIST")
                          /\ canvas_state' = "PENDING"
                          /\ UNCHANGED<<images_updated, display_lists_applied, pending_display_list>>

\* Canvas updates itself whenever it is pending. 
\* Limiting model size with first two conditions.
CanvasSendsUpdateImage == 
                          /\ images_updated < N
                          /\ Len(compositor_messages) < N
                          /\ compositor_messages' = Append(compositor_messages, "UPDATE_IMAGE")
                          /\ canvas_state' = "UPDATED"
                          /\ canvas_state = "PENDING"
                          /\ UNCHANGED<<images_updated, display_lists_applied, pending_display_list>>

\* For a given update cycle,
\* display lists are only applied after an image update.
\* Any display list received before are "buffered" as pending.
CompositorReceivesMessage ==
                             LET 
                                msg == Head(compositor_messages)
                             IN /\ Len(compositor_messages) # 0
                                /\ CASE msg = "DISPLAY_LIST" /\ ReadyToApplyDisplayList -> 
                                            /\ display_lists_applied' = display_lists_applied + 1
                                            /\ UNCHANGED<<images_updated, canvas_state, pending_display_list>>
                                     [] msg = "DISPLAY_LIST" -> 
                                            /\ pending_display_list' = TRUE
                                            /\ UNCHANGED<<images_updated, canvas_state, display_lists_applied>>
                                     [] msg = "UPDATE_IMAGE" -> 
                                            /\ images_updated' = images_updated + 1
                                            /\ display_lists_applied' = 
                                               IF pending_display_list 
                                               THEN display_lists_applied + 1
                                               ELSE display_lists_applied
                                            /\ pending_display_list' = FALSE
                                            /\ UNCHANGED<<canvas_state>>
                                /\ compositor_messages' = Tail(compositor_messages)

\* End with infinite stuttering steps.
Done == /\ images_updated >= N
        /\ Len(compositor_messages) = 0
        /\ UNCHANGED<<images_updated, 
                               display_lists_applied, 
                               compositor_messages,
                               canvas_state, 
                               pending_display_list>>

Next == \/ LayoutSendsDisplayList
        \/ CanvasSendsUpdateImage
        \/ CompositorReceivesMessage
        \/ Done

Spec  ==  Init  /\  [][Next]_<<images_updated, 
                               display_lists_applied, 
                               compositor_messages,
                               canvas_state,
                               pending_display_list>>
----------------------------------------------------------------------------
THEOREM  Spec  =>  [](TypeOk /\ InductiveInvariant /\ ImageUpdatesAndDisplayListsInSync)
=============================================================================

Ok with N = 3