Two invariants answer different questions

TypeOK catches malformed state: an unknown phase, a function with the wrong domain, or a tracking set containing a non-job value. It does not establish the business rule. NoCanceledPublication says exactly that no job belongs to both sets. It assumes those names are sets of jobs; checking both predicates makes that assumption executable.

Repair the cause, not the displayed state

The broken action permits every complete job to publish:

PublishBug(job) ==
  /\ phase[job] = "complete"
  /\ published' = published \union {job}
  /\ UNCHANGED <<phase, canceled>>

The repaired action strengthens its enabling condition:

PublishFixed(job) ==
  /\ phase[job] = "complete"
  /\ job \notin canceled
  /\ published' = published \union {job}
  /\ UNCHANGED <<phase, canceled>>

Clearing canceled during completion would also make the final intersection empty. It would “fix” the displayed bad state by deleting the evidence that the job was canceled. Reading the trace causally rejects that repair: the intended rule is that cancellation disables publication, not that completion rewrites history.

Prove the check is not asleep

Three observations belong together:

1. a normal trace can reach publication for a job that was not canceled;
2. the broken action produces the expected counterexample; and
3. the repaired action exhausts the declared finite model without violation.

The first resists vacuity, the second tests the test, and the third checks the repair. None justifies claims about jobs, steps, or environmental behavior that the finite model does not include.

Under the hood: invariant means every reachable state

For an initial predicate Init and relation Next, the reachable states are the least set containing every Init state and closed under Next. An invariant Inv must hold for each member of that set. TLC searches for a reachable state satisfying ~Inv and reports the path used to reach it.

Merely showing Inv on a few examples is weaker. Merely checking that the formula parses is weaker still. The executable claim is tied to reachability, which is why the model's actions and configuration are part of the evidence.

Lessons

• Type and domain invariants have distinct jobs and should both be checked.
• A safety violation is useful when its trace explains the causal schedule.
• A negative control demonstrates that the property can fail in the model.
• Repair the enabling condition that admits the failure, not its final display.
• A finite green result retains the model's constants and reachability boundary.

Practice

1. Retrieval. State NoCanceledPublication without looking back.
2. Discrimination. Why is deleting a job from canceled during publication a suspicious repair?
3. Transfer. For a seat map owner from seats to people or None, write an invariant saying no person owns two different seats.

References

1. Leslie Lamport. Specifying Systems, Chapters 4 and 14. — invariance and model checking
2. TLA+ Foundation. TLA+ documentation. — running specifications and interpreting TLC results