Keep one behavioral language

The checkbox source contains Init, NextBug, NextFixed, and DisplayMatches. TLC reads those operators through a configuration file. Apalache reads the same operators through command options. Keeping one module prevents two checker-specific models from drifting apart.

Apalache needs types before symbolic translation. The comments above the variables say that loaded is a set of strings, truth maps strings to Booleans, and displayed is a string. TLC ignores those annotations.

------------------------------ MODULE Checkbox ------------------------------
EXTENDS FiniteSets

Leaf == {"a", "b"}
Value == {"unknown", "checked", "unchecked", "mixed"}

VARIABLES
  \* @type: Set(Str);
  loaded,
  \* @type: Str -> Bool;
  truth,
  \* @type: Str;
  displayed
vars == <<loaded, truth, displayed>>

\* @type: (Set(Str), Str -> Bool) => Str;
Correct(ld, tr) ==
  IF ld = {} THEN "unknown"
  ELSE IF \A x \in ld : tr[x] THEN "checked"
  ELSE IF \A x \in ld : ~tr[x] THEN "unchecked"
  ELSE "mixed"

Init ==
  /\ loaded = {}
  /\ truth \in [Leaf -> BOOLEAN]
  /\ displayed = "unknown"

\* The defect lets the last arrival overwrite the aggregate.
NextBug ==
  \E x \in Leaf \ loaded :
    /\ loaded' = loaded \cup {x}
    /\ truth' = truth
    /\ displayed' = IF truth[x] THEN "checked" ELSE "unchecked"

\* The repair derives the display from every resident leaf.
NextFixed ==
  \E x \in Leaf \ loaded :
    /\ loaded' = loaded \cup {x}
    /\ truth' = truth
    /\ displayed' = Correct(loaded', truth)

TypeOK ==
  /\ loaded \subseteq Leaf
  /\ truth \in [Leaf -> BOOLEAN]
  /\ displayed \in Value

DisplayMatches == displayed = Correct(loaded, truth)

=============================================================================

Run the broken and repaired searches

apalache-mc check --init=Init --next=NextBug --inv=DisplayMatches Checkbox.tla
apalache-mc check --init=Init --next=NextFixed --inv=DisplayMatches Checkbox.tla

The first run asks for a trace of at most two steps that violates DisplayMatches, and it is informative only when Apalache finds that trace. The second asks the same bounded question of the repaired transition and expects no violation.

Compare the search claims

For this finite checkbox graph, TLC reaches a fixed point: its queue becomes empty after every reachable state has been visited. Apalache's length-two run asks whether a violating trace exists within two transitions. The two tools find the same bug. Only TLC's run establishes exhaustion of this finite graph.

Symbolic search becomes useful when explicit states multiply faster than the constraint encoding. The solver may represent many concrete values in one formula. That advantage has a cost: bounds and encodings become part of the claim, and solver work can have a larger fixed cost on tiny models.

From bounded checking to induction

An inductive invariant needs three separate arguments. First, every initial state satisfies the candidate. Second, every step from a state satisfying the candidate reaches another state satisfying the candidate. Third, the candidate implies the property you care about.

An ordinary invariant can be true over every reachable state yet fail the second argument because the candidate also describes unreachable states. The repair is often a stronger invariant that records the missing relationship. That strengthening is not decorative. It supplies the fact the one-step proof needs.

For Apalache, the three checks use length zero for initialization, length one with the candidate as the initial predicate for preservation, and a separate implication check for the property. The checkbox lab stops at bounded search because TLC already exhausts its graph. A later production model may justify the extra induction work.

Practice

1. Change the Apalache length from two to one. Predict whether the broken transition still yields the defect.
2. Explain why a type error must not count as a found counterexample.
3. Write the three sentences required to claim that Inv inductively implies Safe.

Worked answer

1. No. One arrival cannot expose disagreement between two leaf truths.
2. A type error means the checker never evaluated the property. Treating an error as a violation would make the negative control pass without evidence.
3. Every Init state satisfies Inv. Every Next step from an Inv state preserves Inv. Every state satisfying Inv also satisfies Safe.

Lessons

• TLC and Apalache can read one TLA+ behavioral model.
• Apalache needs explicit type information for symbolic translation.
• A length-bounded result does not imply unbounded safety.
• An inductive invariant needs initialization, preservation, and implication checks.
• A negative control must distinguish a counterexample from a tool error.

References

1. Apalache Project. “Running Apalache.” — commands, bounds, invariant options, and outputs.
2. Apalache Project. “Apalache Documentation.” — symbolic checking architecture and TLA+ support.