EventLoopWrong.tla

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

Count == 0..N
Task == {"One", "Two"}
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]
----------------------------------------------------------------------------

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

RunTask(t, s) == /\ task_counter[t] < N
                 /\ task_counter' = [task_counter EXCEPT ![t] = @+1]
                 /\ step_counter' = [step_counter EXCEPT ![s] = @+1]

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

Next == \/ \E t \in Task, s \in Step: RunTask(t, s)
        \/ Stop

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