Assembling Spec
Everything so far — Init, Next — describes one step. A specification
describes an entire, unending behavior: start in an Init state, then take
Next steps forever. TLA+'s idiomatic way to say that is:
Spec == Init /\ [][Next]_vars
Two pieces of this are new: the box [], and the _vars subscript. Both
matter, and both are easy to get wrong in ways that look reasonable — so
this chapter is really about those two symbols specifically.
_vars: what counts as "no change"
[Next]_vars (read together, not [] and Next separately — this is one
symbol) means "either Next happens, or vars doesn't change at all." It
expands to exactly Next \/ (vars' = vars). The vars here should be a
tuple of every variable your spec declares — _color for one variable,
_<<x, y>> for two. This is what lets a specification stay well-defined
even during a step where, from the outside, nothing visibly happened.
[]: making it last forever
Next and [Next]_vars are both facts about a single step — one state and
the next. [] ("always") is what turns a single-step fact into a claim
about every step, for the entire behavior. Try leaving it out and using
[Next]_vars directly as your SPECIFICATION, and — importantly — this
still parses fine, because [Next]_vars is a perfectly good formula on
its own. It just isn't one TLC can use to generate an infinite behavior:
Error: TLC cannot handle this conjunct of the spec
This is worth sitting with for a second: the syntax checker (SANY) sees
nothing wrong with a Spec missing its []. It's completely valid
TLA+. Only the model checker (TLC), when it actually tries to use Spec to
generate behaviors, discovers the problem. "Check Syntax" and "Run Model
Checker" are genuinely different checks, doing different jobs — you'll see
this gap again.
What stuttering does not do
It's tempting to assume [Next]_vars exists to avoid the deadlock you saw
last chapter — "if nothing changes, at least stuttering keeps things
going." That's not what it does. TLC's deadlock check specifically asks
"does Next itself have anywhere to go from this state?", independent of
whether stuttering is allowed — a spec written with [][Next]_vars
deadlocks at exactly the same states as one that isn't. Try it yourself: if
you paste last chapter's countdown into Spec == Init /\ [][Next]_count,
it still reports Error: Deadlock reached. at count = 0.
So what is _vars actually for? Composability. It lets your specification
be refined by a more detailed one that takes extra steps of its own
between the ones you modeled — a whole system built out of pieces, each
allowed to quietly do its own thing while another piece's Spec is
"stuttering." You'll see this pay off directly once we get to fairness and
liveness in Part 2. For now: always write [][Next]_vars because it's the
correct, idiomatic form — not because it's a fix for deadlock. A deadlock
is telling you something true about Next, and the fix always lives there.
The .cfg file, one more time
Now that you have a real Spec, tell TLC to use it directly instead of the
INIT/NEXT pair from the last two chapters:
SPECIFICATION Spec
INVARIANT TypeOK
This is exactly the .cfg shape from Chapter 1.4 — you've now built up to
it from first principles.
What you'll do in this exercise
starter.tla has a Spec that's missing its [] — it'll pass Check
Syntax with no complaints at all, and fail Run Model Checker with the
exact error from above. Add the missing box.