Presentation.tla

---------------------------- MODULE Presentation ----------------------------
EXTENDS FiniteSets, Integers, Sequences
VARIABLES next_presentation_id, current_presentation_id, pending_ids
CONSTANT N
----------------------------------------------------------------------------

TypeOk == /\ next_presentation_id \in Int
          /\ current_presentation_id \in Int
          /\ pending_ids \in Seq(Int)
  
\* When there are no pending map asyncs, current is always next minus one.
PresentationSync == Len(pending_ids) = 0 
                        => current_presentation_id = next_presentation_id - 1
----------------------------------------------------------------------------

Init == /\ next_presentation_id = 1
        /\ current_presentation_id = 0
        /\ pending_ids = <<>>

SwapchainPresent == /\ next_presentation_id' = next_presentation_id + 1
                    /\ pending_ids' = Append(pending_ids, next_presentation_id)
                    /\ UNCHANGED<<current_presentation_id>>
  
UpdateContext == /\ next_presentation_id' = next_presentation_id + 1
                 /\ current_presentation_id' = next_presentation_id
                 /\ UNCHANGED<<pending_ids>>

UpdateImage == /\ Len(pending_ids) = 1
               /\ current_presentation_id' = IF Head(pending_ids) > current_presentation_id 
                                             THEN Head(pending_ids)
                                             ELSE current_presentation_id
               /\ pending_ids' = Tail(pending_ids)
               /\ UNCHANGED<<next_presentation_id>>

Next == \/ SwapchainPresent
        \/ UpdateContext
        \/ UpdateImage

Spec  ==  Init /\ [][Next]_<<next_presentation_id, 
                                current_presentation_id, 
                                pending_ids>>
----------------------------------------------------------------------------
THEOREM  Spec  =>  [](TypeOk /\ PresentationSync)
=============================================================================