EventLoopFixed.tla

----------------------------- MODULE EventLoop -----------------------------
EXTENDS FiniteSets, Naturals
VARIABLES task_counter, step_counter
CONSTANT N
----------------------------------------------------------------------------

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

TypeOk == /\ task_counter \in [Task -> Count]
          /\ step_counter \in [Step -> Count]

StepAtomicUpdateInvariant == \A a, b \in Step: 
                               /\ step_counter[a] = step_counter[b]
                               /\ step_counter[a] = task_counter["Update"]
----------------------------------------------------------------------------

Init == /\ task_counter = [t \in Task |-> 0]
        /\ step_counter = [s \in Step |-> 0]

RunOtherTask(t) == /\ task_counter[t] < N
                   /\ t = "Other"
                   /\ task_counter' = [task_counter EXCEPT ![t] = @+1]
                   /\ UNCHANGED<<step_counter>>

RunUpdateTask(t) == /\ task_counter[t] < N
                    /\ t = "Update"
                    /\ step_counter' = [s \in Step |-> step_counter[s] + 1]
                    /\ task_counter' = [task_counter EXCEPT ![t] = @+1]

Stop == /\ \A t \in Task: task_counter[t] = N
        /\ UNCHANGED<<task_counter, step_counter>>

Next == \/ \E t \in Task: \/ RunOtherTask(t)
                          \/ RunUpdateTask(t)
        \/ Stop

Spec  ==  Init  /\  [][Next]_<<task_counter, step_counter>>
----------------------------------------------------------------------------
THEOREM  Spec  =>  [](TypeOk /\ StepAtomicUpdateInvariant)
============================================================================