Init describes a set of starting states

The lifecycle starts every job queued and both tracking sets empty:

The conjunction does not run top to bottom. It simultaneously constrains all three variable values. Reordering the conjuncts changes typography, not meaning.

Read one action as a relation

Start(job) admits a pair of states when the old phase is queued, the new phase function changes that job to running, and the two other variables keep their values. The EXCEPT expression calculates a whole new function value; the prime tells us it belongs to the new state.

Cancel(job) leaves phase unchanged and gives canceled' the old set plus the selected job. Because set union is idempotent, canceling an already canceled running job may be a stuttering step: the new state equals the old. Whether to admit that step is a modeling decision, not an implementation fact.

Next keeps every admitted choice

The complete relation existentially chooses a job and disjoins actions:

Next == \E job \in Jobs:
  Start(job) \/ Cancel(job) \/ Complete(job) \/ Publish(job)

This says that some job and some listed action relate the current state to the next. It does not choose a priority. If two jobs can start, both outgoing edges belong to the graph. If cancellation and completion are both enabled, TLC may explore each ordering. Writing if cancellation then ... else completion would erase one race unless that priority is itself part of the system contract.

Under the hood: actions are sets of pairs

Mathematically, an action denotes a relation: a set of ordered pairs (oldState, newState). Conjunction intersects constraints on those pairs; disjunction unions permitted pairs; existential quantification hides which job witness made the relation true. This is why statement-order intuition fails.

The model is declarative but not vague. A new state is admitted only when every relevant primed coordinate satisfies the formula. The discipline is to close the frame explicitly. A useful review is mechanical: for every action, list every variable and point to either its primed constraint or its UNCHANGED membership.

Lessons

• Init is a predicate describing permitted starting states.
• An action is true or false of an old-state/new-state pair.
• A prime selects the next value; it is not an ordered assignment.
• Omitted primed variables are unconstrained, not implicitly preserved.
• Disjunction and existential choice preserve alternatives for exploration.

Practice

1. Retrieval. Explain the difference between phase and phase'.
2. Discrimination. When two enabled actions update distinct jobs, should Next select one by priority merely to reduce states?
3. Transfer. Write Enter(person) for a turnstile that adds one person to inside and leaves locked unchanged.

References

1. Leslie Lamport. Specifying Systems, Chapters 3–4. — state predicates, actions, primes, and next-state relations
2. Leslie Lamport. A High-Level View of TLA+. — behaviors as sequences of states