Start with the scene

The screen knows four display values: unknown, checked, unchecked, and mixed. The data source knows the truth for leaves a and b. The UI may receive the leaves in either order.

The model does not contain DOM nodes, click handlers, colors, or network requests. None of those details changes the question: does the display equal the fold over every loaded leaf? The model keeps loaded, truth, and displayed because each value can change a later answer.

Read the module as a story

TLA+ describes states with ordinary values and steps with predicates over an old state and a new state. A primed name such as loaded' means the value after one step. \E x \in S means that the action may choose at least one x from S. The checker will explore every choice in the finite set.

------------------------------ 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)

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

Init admits four initial states because each of two leaf truths can be true or false. NextBug chooses an unloaded leaf. The backslash in Leaf \ loaded means set difference. The action then adds that leaf and copies its truth into the display. NextFixed instead calls Correct over the full loaded set.

DisplayMatches is the central claim. The claim is an invariant because the claim must hold in every reachable state. TypeOK catches a different class of mistake: a transition that puts the wrong kind of value into a variable.

Write the model card

The question is whether arrival order can make the parent display disagree with its resident children. The refusal boundary excludes remote summaries, unloading, toggles, and trees larger than two leaves. The action alphabet has one action: load one previously unloaded leaf. The observation is displayed. The safety property is DisplayMatches. The finite domains are two leaf names, two Boolean truth values, and four display words.

The exclusions make the model small. The exclusions also limit every later result. A model is not improved by hiding that trade.

Practice

1. Predict how many distinct initial states Init admits.
2. Find the line where NextBug forgets earlier evidence.
3. Add a third leaf on paper. State which definitions change and which claim stays the same.

Worked answer

1. truth has two Boolean entries, so Init admits four truth functions.
2. displayed' uses only truth[x]. The expression ignores every element already in loaded.
3. Leaf gains one name. Correct and DisplayMatches need no structural change because both already quantify over loaded.

Lessons

• A useful state records differences that can change a later observation.
• A TLA+ action relates one state to every admitted next state.
• Primed variables name the next state.
• An invariant states what every reachable state must preserve.
• A refusal boundary belongs beside the model, not in an author's memory.

References

1. Leslie Lamport. “The TLA+ Home Page.” — language, tools, and learning resources.
2. Leslie Lamport. “Specifying Systems.” Addison-Wesley, 2002. — the complete TLA+ language and method.