[devin-ai-integration]

Summary

Moves the OpenSysML tool pin from 0a5fa2d94 to develop 5cd37f288fef171d62737d6045f4caff772b6014 and applies the model follow-ups that pin unblocks. Stacked on wp/consistency (#12).

Pin. The source build was resolved by the moving nightly installer plus a --depth 1 clone of develop (so runs/ were not reproducible from a fresh checkout); scripts/fetch-tools.sh now fetches and builds sysml at the full commit (OPENSYSML_COMMIT), takes the "OpenSysML Libraries" from the same checkout, and passes COMMIT= to make build-sysml so a shallow checkout still reports the full commit. The Go toolchain is pinned with it (GOTOOLCHAIN=go1.25.11, fetched when the host's go differs), because runs/tool-version.txt records it: the file stays commit (9 chars) + Go version only, 5cd37f288 / go1.25.11. CI (.github/workflows/check.yml) builds the same way and installs z3, which the recorded fdir-inhibit-chain-smt run needs on PATH (the base's CI never reached runs-check: its nightly installer step failed on the checksum).

The pin contains #1376 (installer manifest), #1379 (enum identity by load order, F-B01), #1380 (nested state-space action dispatch, F-F05), #1381 (variant feature-chain reads, F-A03/B02/F02), #1382 (requirement-group validate blow-up, F-A02/A05), #1383 (metadata in case bodies, F-A06/F03), #1384 (accept after <in param>, F-E02), #1385 (DocumentQueries valuation and <metadata def>::<feature> paths, F-D04/H01), #1386 (through-bindings into performed actions, F-C04/I02), #1387 (exhibited-state attribute writes, F-E01). Not in the pin: #1388 (send via a state-def port, F-E03), #1389 (node-pin reads), #1390 (vacuous satisfaction, F-I01), #1391 (individual #Tag def parser, F-C01/C02) — those finding rows stay open.

Model follow-ups (one commit each, each verified with the new binary):

• model/54-icds-tooling.sysml: the ICD parameter tables project the bound value through valuation; the tug–inspector ICD shows 28 V / 15 W / 9600 bit/s, the launch ICD its adapter diameter and loads (runs/documents/TethysIcdDocuments-*.md).
• model/24-verification-tooling.sysml, model/91-documents.sysml: Method / Level / Stage columns through Verification::method, Verification::level, Verification::stage (runs/vv-report.txt, runs/documents/TethysDocuments-VerificationMatrix.md).
• model/60-modes.sysml, model/62-fdir.sysml: explicit bind modes.command = command (ModedTug, ModedInspector) and bind fdir.command = command (FdirTug) — the spec-compliant form, accepted by both validators. The runtime send-via path still needs #1388, so F-E03 stays open; no pinned run exercises that path, and the modes/fdir/sequence runs are unchanged in substance.
• model/73-dynamics.sysml, model/74-analyses-tooling.sysml: DroStabilityAnalysis::revolution now binds its integrator per analysis usage — the mission-tier droStability keeps the model's own RungeKutta4 (kept exactly, as is model/probes/F-F01-state-space-integrator.sysml), and the tool-tier TethysAnalysesTooling::droStabilityRk4 binds StateSpaceIntegration::RK4 with the xAxisCrossing guard on stateSpace.elements#(2). StateSpaceIntegration is an OpenSysML library, so the RK4 binding lives in the tooling file to keep 73-dynamics.sysml portable to the pilot. On this build the analysis form does not evaluate: redefinitions of a nested action's features from a redefining usage are not applied (new finding F-F10). The closure comes from the tool-tier action droRevolutionRk4 (runs/tooling-dynamics.txt): after one full period of 3.20467695 time units = 13.9155 d the state returns to x = 0.8057474419, y = 2.79·10⁻⁸ (start x₀ = 0.8057474388), a closure of 0.011 km — not the ~3.95 km the consistency pass expected.
• Findings: F-A02, F-A05, F-A03, F-B02, F-F02, F-A06, F-F03, F-B01, F-C04, F-I02, F-D04, F-H01, F-E01, F-E02, F-F05 marked fixed in pin with the OpenSysML PR number and the observed after-output; coverage rows that were partial only because of them re-evaluated against the new runs/ (WP-B, WP-C, WP-D, WP-E, WP-F, WP-H). The F-F02 probe names the model's current members (CaptureTargetCase::large, targetCases.large); it had gone stale on wp/consistency.
• Budgets: with F-B01 fixed the budgets read real demand. satisfy powerBudgetCloses by powerBudget fails — demandThrusting 35 518 W + bus 778 W against arrayAtAphelionEol 39 757 W is thrustingMargin 0.119 < the 0.15 policy. No decision attribute was changed.

New finding rows, each with a standalone probe (tool defects, no model workaround):

• F-C05 — a nested action's in parameter bound from the enclosing action's in reads [] (model/probes/F-C05-…, runs/probe-F-C05.txt); this is what still fails CaptureSequence::commit.go after F-C04.
• F-F09 — the same state-space action run twice in one process gives ⟨55.855, −29.43⟩ then ⟨100.0, 0.0⟩ (runs/probe-F-F09.txt; also visible as the standalone fall after drop in runs/probe-F-F05.txt).
• F-F10 — nested-action redefinitions from a redefining usage or specialising analysis def are not applied; the same bindings at the declaration site work (runs/probe-F-F10.txt, runs/tooling-dro-stability.txt).

runs/ diff against wp/consistency (72 files)

• fixed, now-correct values (53): modes-table (per-mode power 822 W … 35 518 W instead of 0 W), wpb-power-budget-safe (832 W), wpb-margin-policy (0.1), wpb-sep-thrust-aphelion, wpb-thrusting-time-large, analyses-transfer (823 / 1 039 d thrust), analyses-external-tool, analyses-sweep, montecarlo-return, montecarlo-missed-thrust, wpc-envelope-cases (4 cases pass), notation-readiness (F-I02 evaluates), probe-F-F02, probe-F-F03, tool-version, vv-matrix-l2, vv-report, document-queries, wpd-space-ground-icd-document, and the 34 rendered documents (16 ICD documents × md/html, VerificationMatrix, VvReport).
• newly failing conditions (3): requirements-satisfy, wpb-budgets-satisfy, as-built-satisfy — ✗ satisfy powerBudgetCloses by powerBudget fails (real demand, see above).
• new errors, all pinned as findings (7): dynamics-standard (the build now refuses RungeKutta4 explicitly — F-F01; droStability stops at the unbound guard — F-F10), wpc-capture-sequence (instantiates now; commit.go fails — F-C05), probe-F-F05 (drop correct, the following fall wrong — F-F09), and the new probe-F-C05, probe-F-F09, probe-F-F10, tooling-dro-stability.
• unchanged in substance (9): fdir-thruster-restarting, modes-inspector-imaging, modes-inspector-retired, modes-tug-dense-target, modes-tug-early-ops, modes-tug-full-flight, modes-tug-proximity-ops, sequence-nominal-trace (materialisation ids / wren → wrenFM names, trace lines), house-rules (element count).

Gate

sysml -validate -strict -warnings-as-errors model/*.sysml 0 · make pilot-mission 0 · make pilot-all 0 · sysml -validate -self-check-package TethysHouseRules model/*.sysml 0 violations · make check 0 (including runs-check).

Open finding rows after this PR

Open: F-A01, F-C01, F-C02 (#1391 not in pin), F-C03, F-C05 (new), F-D01, F-D02, F-E03 (#1388 not in pin), F-F01, F-F07, F-F08, F-F09 (new), F-F10 (new), F-G02, F-G04, F-H03, F-H04, F-H05, F-I01 (#1390 not in pin), F-I03, F-J01, F-J02, F-J03. Adjudicated or closed rows (F-A04, F-B03, F-D03, F-F04, F-F06, F-G01, F-G03, F-H02) are unchanged.

Link to Devin session: https://nasa-jpl-demo.devinenterprise.com/sessions/3d026c8838554bbdb7d11687d024f2a4
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/3d026c8838554bbdb7d11687d024f2a4?variant=devin
Requested by: @HuiJun

[devin-ai-integration]

I'll fix CI failures and address comments from users with write access. I'll skip comments containing "(aside)".

• Disable automatic comment, CI, and merge conflict monitoring