There's no "process" primitive
TLA+ has no built-in notion of a process, thread, or "running in parallel."
Everything you've written so far — Next, actions, \/ — is already
everything TLA+ has. Concurrency is modeled the same way you modeled a single
traffic light or clock: by writing more named actions and combining them with
\/.
Take two counters that don't know about each other — think of two clerks, each stamping their own tally sheet:
VARIABLES x, y
IncX == x' = (x + 1) % 3 /\ y' = y
IncY == y' = (y + 1) % 3 /\ x' = x
Next == IncX \/ IncY
IncX only mentions what happens to x (and says y doesn't change);
IncY is the mirror image. Next is their disjunction, exactly like
Next == Advance \/ Reset would be for a single state machine with two kinds
of steps. Nothing here says "IncX and IncY are different processes" —
that's a story we're choosing to tell about the spec, not something the
notation enforces.
What \/ in Next actually means to TLC
When Next is a disjunction, each step of the behavior is: pick exactly
one disjunct that's enabled, and take it. From the state x=0, y=0, both
IncX and IncY are enabled — TLC doesn't run them "at the same time," and
it doesn't run all of them before moving on. It explores every choice,
one at a time, and treats each choice as a separate branch of the state
graph:
x=0,y=0 --IncX--> x=1,y=0
x=0,y=0 --IncY--> x=0,y=1
This is called interleaving: real concurrency is modeled as all possible
orderings of individually-atomic steps, never as two things happening in the
same instant. It's a modeling choice, not a limitation — it turns out to be
enough to catch almost every real concurrency bug, because those bugs come
from some interleaving going wrong, and TLC checks all of them. (What
IncX and IncY don't do here is touch a shared variable — when two
actions both read and write the same variable, interleaving is where races
come from. That's coming in a later part; this chapter is just the
combining-actions mechanics.)
Run TypeOK == x \in 0..2 /\ y \in 0..2 through TLC on the spec above and
it'll report 9 distinct states — every pair (x, y) with x, y \in 0..2 is
reachable, because interleaving lets IncX and IncY fire in any order and
any mixture. If you've used the state graph view on an earlier exercise,
picture it here: it's a 3×3 grid, not a single line, because at (almost)
every state there are two enabled actions instead of one.
What you'll do in this exercise
You'll write TwoCounters.tla: two independent counters x and y, each
cycling through 0, 1, 2 and wrapping back to 0, combined into one Next
with \/. Same shape as HourClock, just two variables advancing
independently instead of one.