You're viewing the readable version of this site. The interactive extras (search, diagrams, read-aloud) need JavaScript and a current browser. Enable JavaScript; if it is already enabled, update your browser.

Learn · All the Ways It Can Break

growing

Give the Infinite Language a Finite Model

TLC explores only after a configuration binds constants and names the predicates to check.

formal-methods, tla-plus, tlc, model-configuration, learn

You will write a TLC configuration, run the pinned public tool from a blank directory, interpret its completion status, and distinguish constant bounds from state constraints. You will retain both the expected failing run and the repaired run as executable evidence.

The cast list for one exploration

The failing configuration is complete:

CONSTANT Jobs = {job_a, job_b}
INIT Init
NEXT NextBug
INVARIANTS TypeOK NoCanceledPublication
CHECK_DEADLOCK FALSE

Copy JobLifecycle.tla and the two configuration files into the directory containing the TLA+ 1.7.4 tla2tools.jar. Run:

java -cp tla2tools.jar tlc2.TLC -config JobLifecycleBug.cfg JobLifecycle.tla

The run must fail with NoCanceledPublication is violated. That failure is the test's expected verdict, not a broken tutorial. Then run:

java -cp tla2tools.jar tlc2.TLC -config JobLifecycleFixed.cfg JobLifecycle.tla

The repaired model must report that model checking completed with no error and that no states remain on the queue. Record the TLC version, generated and distinct state counts, graph depth, configuration, and completion line.

If Java reports that it cannot find tlc2.TLC, confirm that tla2tools.jar is in the current directory and that the filename matches the command. If TLC reports a module-name error, confirm that the opening module line says JobLifecycle and that the file is named JobLifecycle.tla. These are setup failures; neither is evidence about the model.

Prediction — identify the configuration change that weakens the evidence most directly.

Bounds and constraints do different work

The constant assignment chooses a finite domain. A state constraint removes states from exploration. Both can control cost, but neither is a harmless performance flag. Two job identities may be enough to reveal this defect; that does not prove every cardinality. A constraint that forbids cancellation makes the property vacuous even at two jobs.

CHECK_DEADLOCK FALSE states that terminal states are permitted here. It does not ignore invariant or temporal-property failures. If the modeled protocol must always offer another real action, deadlock checking should remain enabled.

Lessons

  • The module defines general behavior; the configuration defines one finite model.
  • Constants, constraints, predicates, and completion status travel with the result.
  • An expected failing configuration is a durable negative control.
  • Zero states left on the queue matters: interruption is not exhaustion.
  • A finite exhaustive result is not an unbounded theorem.

Practice

  1. Retrieval. Name the five load-bearing lines in the failing configuration.
  2. Discrimination. Does increasing Jobs from two to three strengthen the mathematical claim or only explore another finite model?
  3. Transfer. Configure the turnstile module from Chapter 8 for two people and name its type invariant.

Worked answers

  1. Constant assignment, INIT, NEXT, invariants, and deadlock policy.
  2. It explores another finite model. A separate argument is required to generalize across cardinalities.
  3. Bind People to two model values, select Init and Next, and check that inside \subseteq People.

References

  1. Leslie Lamport. Specifying Systems, Chapter 14. — TLC models, configurations, and constraints
  2. TLA+ Foundation. TLA+ 1.7.4 release. — the tool version used by the specimen

← Make the Forbidden State Executable Read the Trace Backward →