fix(tla): unmask EnvironmentController panic — nested-disjunction split + UNCHANGED-tuple staging - #187
Merged
Conversation
…it + UNCHANGED-tuple staging
Two independent evaluator bugs cause `next_states` to panic
("function application unsupported for value ModelValue(\"failed'\")")
on the Chandra-Toueg EnvironmentController spec. Both stem from a prime
that should be staged being left unstaged, so a later read resolves it to
an unbound ModelValue.
1. Exists-quantified conjunction with a trailing nested disjunction.
`split_action_body_disjuncts` mis-split `\E i : /\ g /\ (\/ A \/ B)` —
an `\E` body whose top-level connective is `/\` — into three top-level
disjuncts `[\E i : guards, \E i : A, \E i : B]`, distributing the `\E`
and treating the inner disjunction's `\/` as top-level. The orphaned
A/B branches dropped the surrounding guards (`moved[i] = "NO"`) and the
shared primed conjuncts (`procPause'`, `UNCHANGED failed`), so they
fired from every state — even where the guard is false — and produced
spurious partial branches. The existing conjunction guard inspects the
whole `\E …` text (which `split_action_body_clauses` reports as one
clause), so it never fired; the fix runs the same check on the exists
*body*. This is the ProcTick spurious-partial-branch bug and the ACP
parProgNB over-generation.
2. UNCHANGED of a defined variable-tuple. `UNCHANGED envVars` where
`envVars == << procPause, moved, failed, F >>` staged one phantom name
`envVars`, not the component primes. The successor state is still
correct (unchanged vars survive the state clone), so the gap is
invisible until an action READS its own unchanged prime — as
EnvironmentController's DELTAConstraint/PHIConstraint read `failed'`
after the Crash/ProcTick crashed branch's `UNCHANGED envVars`. New
`expand_unchanged_var` resolves a defined nullary tuple operator to its
component variables (recursively) at eval time, in both the interpreted
and compiled Unchanged handlers.
With both fixes EnvironmentController no longer panics and runs to
completion. (It still under-explores relative to TLC due to a separate,
pre-existing disjunction-under-trailing-constraint issue — tracked
separately; not addressed here.)
Gate: diff_tlc 18/18 (adds ExistsGuardedNestedDisjunction 170==TLC and
UnchangedDefinedTuple 4==TLC), cargo test --release 1485 passed / 0 failed.
zoratu
added a commit
that referenced
this pull request
Jul 19, 2026
…ction split + instance primed-arg staging (#188) EnvironmentController (Chandra-Toueg detector) explored only 36 distinct states vs TLC's ~129,630 after the panic was fixed in #187. Root cause was `localClock` never advancing: the ProcTick RECEIVE branch's `Detector!Receive(i, inDelivery')` produced no successor, so its nested `LocallyTick(i)` never ran, so every guard requiring `localClock > 0` (message send/predict) stayed disabled and the whole message-passing state space (the bulk of TLC's 130k) went unexplored. Two independent bugs, both needed: 1. Leading guard-disjunction with shared conjuncts. `split_action_body_disjuncts` split `/\ (\/ a \/ b) /\ LocallyTick(i) /\ UNCHANGED ...` into `[/\ a, /\ b /\ LocallyTick /\ UNCHANGED]` — it stripped the leading `/\` and split at the guard's `\/`, absorbing the shared trailing conjuncts into only the LAST `\/` branch. The first guard-disjunct then fired WITHOUT the shared `LocallyTick`/primed conjuncts, so the clock never advanced. The `/\`+`\/` strip now only fires when the disjunction is the body's sole top-level conjunct (`/\ \/ b1 \/ b2 \/ b3`, e.g. 2PC `RS`), detected by layout via the new `leading_conjunct_is_sole` (count `/\` lines shallower than the `\/` bullets — robust to `expr.trim()` dedenting the first line, unlike a `split_action_body_clauses` count, which over-counts a lone disjunction-conjunct). 2. Instance-action arguments that read a next-state variable. `expand_action_call_multi` value-bound call arguments against the bare `ctx`, so `Detector!Receive(i, inDelivery')` (with `inDelivery'` staged by the preceding `CommChan!Deliver(i)`) read `inDelivery'` as an unbound ModelValue; Receive's `\E m \in incomingMessages` then errored and it produced no successor. Evaluate arguments in the caller's staged context (a superset — unprimed arguments are unaffected). With both fixes EnvironmentController explores the full ~130k-state space (36 -> 116k+ and matching TLC's scale; it still hits the pre-existing pathological slow-tail near the end, tracked separately). Gate: diff_tlc 19/19 (adds ClockDetectorMC, a self-contained instance-action spec needing both fixes, 9 == TLC), cargo test --release 1486 passed / 0 failed. New unit test pins the RS-vs-Receive split distinction.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Two independent evaluator bugs cause
next_statesto panic (function application unsupported for value ModelValue("failed'")) on the Chandra-Toueg EnvironmentController spec (specifications/detector_chan96). Both stem from a prime that should be staged being left unstaged, so a later read resolves it to an unboundModelValue. Each was isolated to a standalone minimal repro and given a differential-gate regression spec.1.
\E-quantified conjunction with a trailing nested disjunctionsplit_action_body_disjunctsmis-split\E i : /\ g /\ (\/ A \/ B)— an\Ebody whose top-level connective is/\— into three top-level disjuncts[\E i : guards, \E i : A, \E i : B], distributing the\Eand treating the inner disjunction's\/as top-level. The orphaned A/B branches dropped the surrounding guards (moved[i] = "NO") and the shared primed conjuncts (procPause',UNCHANGED failed), so they fired from every state — even where the guard is false — producing spurious partial branches. A trailing constraint then read an unstagedfailed'and panicked.The existing conjunction guard in this function inspects the whole
\E …text (whichsplit_action_body_clausesreports as a single clause), so it never fired for the quantified shape; the fix runs the same conjunction check on the exists body.This is EnvironmentController's
ProcTickspurious-partial-branch bug and the same mechanism behind ACP'sparProgNBover-generation.2.
UNCHANGEDof a defined variable-tupleUNCHANGED envVarswhereenvVars == << procPause, moved, failed, F >>staged one phantom nameenvVars, not the component primes. The successor state is still correct (unchanged vars survive the state clone), so the gap is invisible until an action reads its own unchanged prime — as EnvironmentController'sDELTAConstraint/PHIConstraintreadfailed'after theCrash/ProcTickcrashed branch'sUNCHANGED envVars.New
expand_unchanged_varresolves a defined nullary tuple operator to its component variables (recursively) at eval time, in both the interpreted and compiledUnchangedhandlers.Result
With both fixes EnvironmentController no longer panics and runs to completion. It still under-explores relative to TLC because of a separate, pre-existing disjunction-under-trailing-constraint issue in this spec (the constraint accepts each branch it sees, but the disjunction under a trailing conjunct yields too few branches) — tracked separately, not addressed here.
Validation
scripts/diff_tlc.sh: 18/18 — adds two regression specs, each matching TLC exactly:ExistsGuardedNestedDisjunction— 170 distinct (== TLC), no violation; panics/over-generates without fix 1.UnchangedDefinedTuple— 4 distinct (== TLC), no violation; panics without fix 2.cargo test --release: 1485 passed / 0 failed.split_action_body_disjuncts_keeps_exists_conjunction_with_trailing_nested_disjunction.