fix(tla): EnvironmentController explores fully — leading guard-disjunction split + instance primed-arg staging

[zoratu]

After #187 fixed the panic, EnvironmentController (Chandra-Toueg detector, specifications/detector_chan96) still explored only 36 distinct states vs TLC's ~129,630. Root cause: localClock never advanced — 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 — each isolated to a deterministic repro.

1. Leading guard-disjunction with shared conjuncts

split_action_body_disjuncts split

/\ \/ /\ localClock[i] % PredictPoint = 0
      /\ localClock[i] % SendPoint = 0
   \/ /\ localClock[i] % PredictPoint # 0
      /\ localClock[i] % SendPoint # 0
/\ LocallyTick(i)
/\ UNCHANGED ...

into [/\ %P=0 /\ %S=0, /\ %P#0 /\ %S#0 /\ LocallyTick /\ UNCHANGED] — it stripped the leading /\ and split at the guard's \/, absorbing the shared trailing conjuncts (LocallyTick, UNCHANGED) into only the last \/ branch. The first guard-disjunct then fired without them, 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 — which must still split into 3). This is detected by layout via the new leading_conjunct_is_sole: count /\ lines shallower than the \/ bullets. A split_action_body_clauses count won't work — it over-counts a lone disjunction-conjunct (flattens the branches' inner /\, returning 6 for RS), and expr.trim() dedents the first line so an absolute per-line column won't line up either; comparing against the \/ bullet indent is robust to both.

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. Arguments now evaluate in the caller's staged context (a superset — unprimed arguments are unaffected).

Result

With both fixes EnvironmentController explores the full state space: 36 → 116k+ distinct and matching TLC's ~129,630 scale. (It still hits a pre-existing pathological slow-tail near the very end — a separate perf issue, tracked with the ACP over-generation.)

Validation

• scripts/diff_tlc.sh: 19/19 — adds ClockDetectorMC, a self-contained instance-action spec that needs both fixes (a primed-arg chan'[i] read + a callee body with a leading guard-disjunction), 9 distinct == TLC.
• cargo test --release: 1486 passed / 0 failed.
• New unit test split_action_body_disjuncts_keeps_leading_guard_disjunction_with_shared_conjuncts pins the Receive-vs-RS split distinction (and the pre-existing RS test still passes).