Actions and Next

An action relates one state to the next

Next describes how the system is allowed to move from its current state to its next state. To talk about both at once, TLA+ uses primed variables: color means the value now, color' (read "color prime") means the value in the next state. An action is just a predicate that can mention both:

color = "red" /\ color' = "green"

Read this exactly like the logic you already know: "color is currently "red", and in the next state color is "green"." That's the entire idea — an action is a fact about a pair of states instead of one.

Guards

The left-hand side above — color = "red" — is called a guard: a condition on the current state that must hold for this particular action to apply. Without a guard, an action would have to make sense from every possible current state, which is rarely what you want.

Combining actions with \/

A system usually has more than one way to move. You combine alternative actions with \/, and TLA+'s indentation-based bulleted list syntax makes a long disjunction easy to read (and, as a bonus, sidesteps the /\/\/ precedence gotcha from Chapter 0.2 entirely, since every bullet at the same indentation is unambiguously one disjunct):

Next ==
  \/ color = "red"    /\ color' = "green"
  \/ color = "green"  /\ color' = "yellow"
  \/ color = "yellow" /\ color' = "red"

This reads as "Next holds if any one of these three things happens" — red goes to green, green goes to yellow, or yellow goes back to red.

UNCHANGED

When an action doesn't care about a variable, you still have to say so — TLA+ doesn't assume anything stays the same on its own. UNCHANGED x is shorthand for x' = x, and UNCHANGED <<x, y>> covers several variables at once. You already saw this in Chapter 1.1's Next == UNCHANGED color; once you have more than one variable, you'll reach for it constantly to say "this action doesn't touch that one."

When nothing can happen: deadlock

Every action you write can have a guard, and it's entirely possible to write a system where, from some reachable state, no action's guard is satisfied — there's nowhere left to go. TLC calls this a deadlock and treats it as an error by default, on the theory that an unintentionally stuck system is almost always a bug worth knowing about. For example, a countdown that only knows how to count down:

Next == count > 0 /\ count' = count - 1

will deadlock the moment count reaches 0 — count > 0 is the only action's guard, and it's false. Run this and TLC stops with:

Error: Deadlock reached.
State 4: count = 0

Sometimes that's exactly right (a countdown should stop). Sometimes it's a sign your Next forgot a case. Either way, the fix is always in Next itself — never something you paper over with the Spec formula, which is the subject of the next chapter.

What you'll do in this exercise

Write the real Next for the traffic light from last chapter: it cycles red → green → yellow → red, forever. Every state has somewhere to go, so you won't see a deadlock here — but now you know what one looks like when you do.