fix(tla): trust the compiled empty result in execute_branch's inline path (EnvironmentController)

[zoratu]

Problem

execute_branch's inline-body path evaluated Next via the compiled action IR and, on a non-successful result, fell back to the interpreted evaluator unconditionally and propagated its error.

That is wrong for the common Next == /\ Act /\ Constraint shape where:

• Act is an action (\E i : g /\ procPause' = .. /\ UNCHANGED failed /\ ( \/ .. \/ .. ) — outer assignments + a nested inner disjunction), and
• Constraint is a post-state predicate that reads a prime (\A i : failed'[i] = FALSE => ..), assigning nothing.

In a reachable state where Act is disabled, the compiled evaluator correctly returns zero successors — but the unconditional fallback re-evaluated Act /\ Constraint interpreted. With Act staging nothing, Constraint's failed' resolved to an unbound ModelValue("failed'") and failed'[i] raised function application unsupported for value ModelValue(...). That error propagated out of next_states as a panic, stalling exploration at 1 state — the Chandra-Toueg EnvironmentController failure-detector spec (detector_chan96) never got past its initial state.

Fix

Mirror the careful compiled→interpreted fallback the operator-call path already uses:

• a non-empty compiled result is always trusted;
• an empty compiled result is trusted (the guards legitimately blocked the transition) unless the body reaches an instance-action call or a LET-with-primes — the only shapes where the compiled path can spuriously return empty for an enabled action — and only then is it cross-checked;
• the interpreted cross-check's errors are swallowed (a disabled action whose trailing post-state constraint reads an unstaged prime errors there, but that is a correct 0-successor result, not a crash).

Validation (on spot)

• New diff_tlc gate spec NestedActionConstraint — 9 distinct states == TLC v2.19; verified genuine regression (neutering the fix reproduces the exact panic + 1-state stall).
• scripts/diff_tlc.sh: 16/16.
• cargo test --release: 0 failures (one concurrency proptest, prop_pause_visibility, flaked once under full-gate CPU load and passes in isolation — unrelated to this action-eval change).

Scope note

This fixes the panic/stall. EnvironmentController's full exploration remains slow (TLC itself takes ~2 hours on it), which is inherent to the model and out of scope here.

An earlier, broader approach (making the action classifier staging-aware so a prime-reading predicate isn't treated as an action) was explored and dropped: it was unnecessary (this fallback fix alone resolves the panic), carried regression risk for universal-quantified / CASE actions, and introduced a per-classification compile_action_ir perf regression on complex specs.