The smallest complete frame

Create JobLifecycle.tla. A module begins and ends with ruled lines; the name must match the file name. The checked specimen begins this way:

EXTENDS Naturals imports operators from a standard module. This model does not yet use arithmetic, but importing deliberately now makes the dependency visible when capacity arrives later. CONSTANT Jobs says only that Jobs does not change within a behavior. It does not choose the members. Chapter 11 will give TLC a concrete two-job set.

VARIABLES declares the coordinates of a state. The tuple vars is a convenient operator used later by temporal formulas; it creates no fourth variable. Phases is another operator: evaluating it always returns the same set because it mentions no variables.

One word can move across the boundary

Suppose operators may change the worker limit at runtime. Then Limit is not a constant for that question. It belongs in VARIABLES, Init must give it an initial value, and every action must determine Limit' or declare it unchanged. The same production field can be constant in one model and variable in another because the modeled question changed.

This is not looseness. A constant quantifies over behaviors selected by model assignments; a variable ranges over states inside a behavior. Moving a name between them changes the mathematical object being checked.

Define vocabulary, not helper procedures

An operator definition uses ==:

Waiting == {job \in Jobs : phase[job] = "queued"}

Read it as a value definition: Waiting is the subset of jobs whose current phase is queued. Because it refers to phase, its value may differ by state. It does not cache a set or run a helper procedure. Parameterized operators such as CanStart(job) are expressions with names, not methods on mutable objects.

Under the hood: a module is not a model

The module permits many interpretations of Jobs. An empty set, a singleton, and a thousand abstract identifiers all satisfy the declaration. TLC cannot enumerate that open world until a configuration binds it to a finite value. Keeping specification and model separate is useful: one behavioral definition can be checked under several finite assignments without rewriting its meaning.

It also creates an honesty obligation. A passing run with two jobs is evidence about that finite model, not automatically every cardinality. Later we may use symmetry or a proof to widen the claim. The module header alone does neither.

Lessons

• Constants stay fixed within one behavior but may differ between models.
• Variables are the coordinates whose values may change between states.
• Operators name expressions; they are not hidden mutation or storage.
• The module name must match its file and its ruled frame must close.
• A general module becomes an executable finite model only after configuration.

Practice

1. Retrieval. Name the three categories introduced by a module: fixed, changing, and defined.
2. Discrimination. Should a network partition be a constant or variable when the question asks whether service recovers after connectivity returns?
3. Transfer. From a blank file, write Turnstile.tla with constant People, variable inside, and operator Empty = inside = {}=.

References

1. Leslie Lamport. Specifying Systems, Chapters 2–4. — modules, constants, variables, and definitions
2. TLA+ Foundation. Getting started with TLA+. — public tooling and module workflow