ImageEpoch.tla

----------------------------- MODULE ImageEpoch -----------------------------
EXTENDS FiniteSets, Integers
CONSTANT N
VARIABLES image, display_list, state, submitted
-----------------------------------------------------------------------------
Epoch == 0..N

None == N+1

TypeOk == /\ image \in {None} \cup Epoch
          /\ display_list \in {None} \cup Epoch
          /\ state \in {"Pending", "Submitted"}
          /\ submitted \in 0..N+1
     
\* Invariant: for a display list to be submitted, the image must be updated,
\* and we must not run ahead of `submitted`.     
Inv == state = "Submitted" => /\ image = display_list
                              /\ display_list = submitted-1

\* Used to update the `submitted` variable, 
\* if the state went from pending to submitted
\* (note the comparison of the primed with the unprimed `state` variable).
newSubmitted == IF state' = "Submitted" /\ state = "Pending" THEN submitted + 1 ELSE submitted
                            
-----------------------------------------------------------------------------

Init == /\ image = None
        /\ display_list = None
        /\ state = "Pending"
        /\ submitted = 0
        
UpdateImage == LET 
                  \* Note: here we use the primed `image` variable.
                  new_state == IF (display_list \in Epoch
                                        /\ image' \in Epoch)
                                  THEN IF image' = display_list THEN "Submitted" ELSE "Pending"
                                  ELSE "Pending"
               IN
               /\ image' = IF image = None THEN 0 ELSE image + 1
               /\ state' = new_state
               /\ submitted' = newSubmitted
               \* Note: both here and in `ReceiveDisplayList`, 
               \* we only update if the previous epoch submitted a display list.  
               /\ \/ image < submitted
                  \/ image = None
               /\ \/ image < N
                  \/ image = None
               /\ UNCHANGED<<display_list>>

ReceiveDisplayList == LET 
                        \* Note: here we use the primed `display_list` variable.
                        new_state == IF (display_list' \in Epoch
                                        /\ image \in Epoch)
                                  THEN IF image = display_list' THEN "Submitted" ELSE "Pending"
                                  ELSE "Pending"
                      IN
                      /\ display_list' = IF display_list = None THEN 0 ELSE display_list + 1
                      /\ state' = new_state
                      /\ submitted' = newSubmitted
                      /\ \/ display_list < N
                         \/ display_list = None
                      /\ \/ display_list < submitted
                         \/ display_list = None
                      /\ UNCHANGED<<image>>

Done == /\ submitted = N+1
        /\ UNCHANGED<<image, display_list, state, submitted>>

Next == \/ UpdateImage
        \/ ReceiveDisplayList
        \/ Done
-----------------------------------------------------------------------------
Spec  ==  Init  /\  [][Next]_<<image, display_list, state, submitted>>

THEOREM  Spec  =>  [](TypeOk /\ Inv)
=============================================================================