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 · Before the Machine Acts · Workshop 2

budding

Check Every Reachable State

Run TLC and turn its counterexample into a repair.

tlc, tla-plus, counterexamples, checkbox, learn

You will run TLC, read an invariant counterexample, distinguish a terminal state from a deadlock, and run a repaired configuration to graph exhaustion.

Run the negative control

The configuration chooses Init and NextBug. It also names both invariants.

CheckboxBug.cfg

INIT Init
NEXT NextBug
CHECK_DEADLOCK FALSE
INVARIANTS TypeOK DisplayMatches

This configuration asks TLC to explore the broken transition. A run that reports no violation means the lab is not reproducing the defect.

In the directory holding those two files, run:

java -jar tla2tools.jar -config CheckboxBug.cfg Checkbox.tla

This run is a negative control: the violation is the expected result, and anything else — a clean run, a parse error, a crash — means the lab told you nothing. Search the output for the states in the error trace.

State 1: loaded = {}, displayed = "unknown"
State 2: loaded = {"a"}, displayed = "checked"
State 3: loaded = {"a", "b"}, displayed = "unchecked"

The exact leaf names may appear in the opposite order. The important shape is stable: one true leaf arrives, then one false leaf arrives, and the last truth overwrites the aggregate. DisplayMatches expects mixed in state 3.

Prediction — locate the first false state.

Repair the transition

The repair does not add a special case for the observed trace. NextFixed derives the display from the complete next loaded set. Run the fixed configuration:

java -jar tla2tools.jar -config CheckboxFixed.cfg Checkbox.tla

TLC reports sixteen distinct states and no invariant violation for this model. The model has terminal states once both leaves load. CHECK_DEADLOCK FALSE tells TLC that a terminal state is expected. That setting would be dishonest for a server that promises to keep accepting work. It is honest for a finite loading exercise.

State-space exploration visits reachable states and follows every action enabled in each state. A finite exhausted graph gives a stronger claim than a sampled run.

Read the green result precisely

The clean run establishes TypeOK and DisplayMatches for every state reachable from Init through NextFixed with exactly two named leaves. The result says nothing about toggles, unloads, remote summaries, or the UI code. The next engineering step would map implementation fields and reducer events to the model vocabulary, then replay this trace against the reducer.

Practice

  1. Change NextFixed to use Correct(loaded, truth) without the prime. Predict the trace before running TLC.
  2. Remove DisplayMatches from the fixed configuration. Explain why the remaining green result says less.
  3. Decide whether a terminal state should count as deadlock in a request server.

Worked answer

  1. The display lags one step behind. The first load leaves displayed unknown while Correct expects a definite value.
  2. TypeOK checks only shapes and domains. A wrong but well-typed display can pass.
  3. A request server normally promises another receive action. A reachable state with no receive or recovery action is therefore a real deadlock unless shutdown is explicit.

Lessons

  • Run a known defect before trusting a green model.
  • Read a counterexample from the first false state backward to the enabling choice.
  • Repair the general transition, not the printed example.
  • State graph exhaustion covers only the model's finite domain and action alphabet.
  • Deadlock policy depends on the system's promised behavior.

References

  1. TLA+ Project. “TLA+.” GitHub. — TLC source, releases, and tool documentation.
  2. Leslie Lamport. “A High-Level View of TLA+.” — behaviors, state machines, and checking.