You already know one temporal operator
Chapter 1.4 defined an invariant as a predicate true in every reachable
state. There's a precise way to say "every reachable state" as a formula
about a whole behavior (an infinite sequence of states), not just one state
at a time: the Always operator, written [] (box) in TLA+ source, and
sometimes shown as the mathematical symbol □ in prose. For any state
predicate P:
Spec => []P
reads "every behavior satisfying Spec has P true in every state."
That's exactly what INVARIANT TypeOK in a .cfg file already checks — it's
just been spelled INVARIANT, not [], so far. They're the same claim. In
fact, the [] you've already been typing in Spec == Init /\ [][Next]_vars
is this same operator, applied to [Next]_vars instead of a plain state
predicate — "at every step, [Next]_vars holds."
The .cfg file has a second keyword for temporal formulas beyond
INVARIANT: PROPERTY. INVARIANT TypeOK and PROPERTY AlwaysTypeOK (where
AlwaysTypeOK == []TypeOK) tell TLC to check the exact same thing, two
different ways of asking for it.
The genuinely new operator: Eventually
<> (diamond, ◇ in prose) is Eventually: <>P means P becomes true at
some point in the behavior — maybe not now, but eventually. This is a
fundamentally different kind of claim than an invariant. An invariant is
about every single state in isolation; <>P is about the behavior as a
whole, and there's no way to check it by looking at one state at a time —
TLC has to reason about entire infinite futures.
It's tempting to reach for <> immediately: on the TwoCounters spec from
the last chapter, "eventually x reaches 2" seems like an obviously true
thing to claim:
Live == <>(x = 2)
Try it — add PROPERTY Live to TwoCounters.cfg and run it. TLC reports a
violation, with this counterexample:
State 1: <Initial predicate>
/\ x = 0
/\ y = 0
State 2: <IncX ...>
/\ x = 1
/\ y = 0
State 3: Stuttering
x gets to 1 and then... the behavior just stops changing, forever. That's
legal — [][Next]_vars has always permitted stuttering (Chapter 1.3), and
"take one step, then stutter forever" is a perfectly valid behavior of this
Spec. It never gets x to 2, so <>(x = 2) is false for it. This isn't
a bug in the spec — it's what <> claims actually cost: any <> claim
on any spec written the way you've written specs so far will fail this
same way, because nothing has ever ruled out "eventually just stop." Making
<> claims meaningful is the subject of the next chapter: fairness.
What you'll do in this exercise
No fairness needed yet — this exercise only uses []. You'll extend
TwoCounters with a property that's a compound [] claim (both variables
bounded and their sum bounded) to get comfortable writing PROPERTY
formulas before Eventually claims need fairness underneath them.