CanvasRenderingBroken.tla

-------------------------- MODULE CanvasRenderingBroken --------------------------
EXTENDS FiniteSets, Integers, Sequences
VARIABLES images_updated, display_lists_applied, compositor_messages
----------------------------------------------------------------------------

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

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

TypeOk == /\ images_updated \in Int
          /\ display_lists_applied \in Int
          /\ compositor_messages \in Seq(Messages)

ImageUpdatesAndDisplayListsInSync == \/ ImageUpdatedAndDisplayListApplied
                                     \/ ReadyToApplyDisplayList

Init == /\ images_updated = 0
        /\ display_lists_applied = 0
        /\ compositor_messages = <<>>
        
LayoutSendsDisplayList == /\ compositor_messages' = Append(compositor_messages, "DISPLAY_LIST")
                          /\ UNCHANGED<<images_updated, display_lists_applied>>

CanvasSendsUpdateImage == /\ compositor_messages' = Append(compositor_messages, "UPDATE_IMAGE")
                          /\ UNCHANGED<<images_updated, display_lists_applied>>

CompositorReceivesMessage ==
                             LET msg == Head(compositor_messages)
                             IN /\ Len(compositor_messages) # 0
                                /\ CASE msg = "DISPLAY_LIST" -> 
                                            /\ display_lists_applied' = display_lists_applied + 1
                                            /\ UNCHANGED<<images_updated>>
                                     [] msg = "UPDATE_IMAGE" -> 
                                            /\ images_updated' = images_updated + 1
                                            /\ UNCHANGED<<display_lists_applied>>
                                /\ compositor_messages' = Tail(compositor_messages)

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

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