lts.override.aut — sanctioned per-model LTS override (user-authorized).

nucleos is the proven-correct/refining side; dzn nested-composition
over-generates relative to its OWN flattened-equivalent (see analysis
below). Hold nucleos lts as the golden per no-overfit-to-dzn. Was
lts.xfail. dzn gold retained as baseline/lts.aut for reference.

----------------------------------------------------------------------
Camera (nested-foreign): ours is weak-failures INCOMPARABLE to the raw dzn gold, but OURS IS THE CORRECT/CONSISTENT SIDE — this is not an ours composition bug, and not a foreign-handling bug.

Proven (2026-06-15), with `--system` wf-check (fork-at-reply transform via
scripts/lbs_system_transform.py + tau self-loops dropped from both sides, the
two standard sanctioned canonicalizations):
  1. dzn treats a contained foreign IDENTICALLY to a boundary-requires port:
     a minimal `foreign Dev` system and the same system with the interface at
     the boundary produce the byte-identical LTS modulo the label prefix
     (`sut.d.p.X` vs `d.X`). So foreign == boundary-requires in dzn.
  2. ours composes nested Camera IDENTICALLY to flattened Camera (foreigns
     promoted to boundary requires): EQUAL.
  3. ours flattened Camera == dzn flattened Camera: EQUAL.
  => ours-nested == dzn-FLATTENED, yet ours-nested (OURS ⊑ GOLD) ⊏ dzn-NESTED.
  => dzn-NESTED-Camera STRICTLY EXCEEDS dzn-FLATTENED-Camera: dzn's nested
     composition adds interleavings its own flattened-equivalent does not,
     even though dzn itself establishes foreign == boundary (point 1). ours
     matches the flattened/boundary form; it is the consistent, refining side.

The Optics subsystem alone is fully EQUAL to dzn after the two canonicalizations
(self-loops + fork-at-reply); the residual only appears at the full-Camera
(Driver + Acquisition + Optics) level, as dzn's mCRL2 early-value-commit
(fork-at-CALL) on the foreign Contrast reply threaded across the two subsystems
— the "two-forks-across-an-RTC" shape scripts/lbs_system_transform.py cannot
canonicalize in a single pass.

So this xfail records a dzn nested-composition over-generation (relative to its
own flattened-equivalent), NOT an ours defect. Earlier notes here that called it
an "ours urgency bug" or an unfixed foreign-spontaneous gap are SUPERSEDED:
nested foreign spontaneous deliveries now render observably and ours' nested
composition is proven equal to its (dzn-correct) flattened form. To drop this
xfail, either extend the value-fork transform to canonicalize cross-subsystem
fork-at-call, or regenerate Camera's gold with the full transform and compare
ours with self-loops dropped — but neither is an ours composition change.

----------------------------------------------------------------------
simulate.{1,2,3}.override — sanctioned per-trace simulate overrides
(user-authorized 2026-07-02, state-assert arbitration).

Arbitrated with `dzn graph -b state -m Camera Camera.dzn` (the sanctioned
state-truth tool; it DOES work on this multi-leaf system — 8 quiescent
nodes). The traces' entry-state preambles are CORRECT (trace.1/trace.3 =
graph node 5, trace.2 = graph node 8). The dzn goldens' RENDERED state
vectors are the known `dzn simulate --state` stale internal-port-mirror
artifact (formerly waived via `stateartifact` judge sidecars):

  trace.1/trace.3 jump line: golden shows driver acquisition.state/
    optics.state = Idle/Idle, optics port.state = Idle, focus.idle = true,
    focus port.idle = true, acquire port.state = Idle — graph node 5 says
    Ready/Prepare, Prepare, false, false, Ready. Ours matches node 5.
  trace.1 RTC-end (post-shoot, node 6): golden keeps acquisition.state and
    acquire port.state = Idle; graph says Acquiring/Acquiring. Ours matches.
  trace.2 jump line (node 8): golden shows acquisition.state and acquire
    port.state = Idle; graph says Acquiring/Acquiring. Ours matches.
  trace.3 RTC-end (node 4): golden and ours both match (all Idle).

Arrows/trail/labels/eligible are byte-identical golden-vs-ours on all three
traces; ONLY `(state …)` lines differ. The overrides are ours' batch render
(graph-verified) and now gate states strictly (judge sidecars dropped).
Known residual display-form nit: dzn (golden AND graph node 1) spells the
INITIAL contrast_was as `IContrast.EContrast:Blurrier` but the same value
unqualified everywhere else; ours spells it unqualified consistently.
Raw dzn goldens retained as baseline/simulate.{1,2,3} for reference.
