FGEventLoop.tla

----------------------------- MODULE FGEventLoop ---------------------------
EXTENDS FiniteSets, Naturals
VARIABLES task_state, step_state
CONSTANT N
----------------------------------------------------------------------------

Count == 0..N
Task == {"Other", "Update"}
Step == {"A", "B"}


FGTypeOk == /\ task_state \in [Task -> [running: BOOLEAN, count: Count]]
            /\ step_state \in [Step -> Count]

FGStepUpdateInvariant == 
                /\ task_state["Update"].running = FALSE =>
                       \A a, b \in Step: 
                           /\ step_state[a] = step_state[b]
                           /\ step_state[a] = task_state["Update"].count
                /\ step_state["B"] = task_state["Update"].count 
                    => step_state["A"] = step_state["B"]
                /\ Cardinality({tt \in Task: task_state[tt].running}) \in {0,1}
----------------------------------------------------------------------------

FGInit == /\ task_state = [t \in Task |-> [running |-> FALSE, count |-> 0]]
          /\ step_state = [s \in Step |-> 0]
        
StartRunTask(t) == /\ task_state[t].count < N
                   /\ Cardinality({tt \in Task: task_state[tt].running}) = 0
                   /\ task_state' = 
                        [task_state EXCEPT ![t].running = TRUE, 
                                           ![t].count = @+1]
                   /\ UNCHANGED<<step_state>>

FinishOtherTask(t) == /\ t = "Other"
                      /\ task_state[t].running
                      /\ task_state' = 
                            [task_state EXCEPT ![t].running = FALSE]
                      /\ UNCHANGED<<step_state>>      

FGRunUpdateTask(t) == LET
                           step == 
                            IF step_state["A"] = task_state[t].count
                            THEN "B"
                            ELSE "A"
                      IN
                         /\ t = "Update"
                         /\ task_state[t].running
                         /\ step_state[step] < task_state[t].count
                         /\ step_state' = [step_state EXCEPT ![step] = @+1]
                         /\ UNCHANGED<<task_state>> 

FinishUpdateTask(t) == /\ t = "Update"
                       /\ task_state[t].running
                       /\ \A s \in Step: step_state[s] = task_state[t].count
                       /\ task_state' = 
                            [task_state EXCEPT ![t].running = FALSE]
                       /\ UNCHANGED<<step_state>>  

FGStop == /\ \A t \in Task: task_state[t].count = N
          /\ UNCHANGED<<task_state, step_state>>

FGNext == \/ \E t \in Task: \/ StartRunTask(t)
                            \/ FinishOtherTask(t)
                            \/ FGRunUpdateTask(t)
                            \/ FinishUpdateTask(t)
          \/ FGStop

FGSpec  ==  FGInit /\ [][FGNext]_<<task_state, step_state>>
----------------------------------------------------------------------------
THEOREM  FGSpec  =>  [](FGTypeOk /\ FGStepUpdateInvariant)
----------------------------------------------------------------------------
Bar == INSTANCE EventLoop WITH 
        step_counter <- [s \in Step |-> IF task_state["Update"].running 
                                        THEN task_state["Update"].count 
                                        ELSE step_state[s]],
        task_counter <- [t \in Task |-> task_state[t].count]
BarSpec == Bar!Spec
THEOREM FGSpec => Bar!Spec
=============================================================================