Pin OpenSysML to develop 5cd37f288 and apply the model follow-ups it unblocks

.github/workflows/check.yml

@@ -10,13 +10,10 @@ jobs:
       - uses: actions/checkout@v4
       - uses: actions/setup-java@v4
         with: { distribution: temurin, java-version: '21' }
-      - name: Fetch OpenSysML nightly
-        run: curl -fsSL https://raw.githubusercontent.com/Open-MBEE/OpenSysML/develop/install.sh | sh -s -- --version nightly --tools sysml --prefix "$PWD/build/opensysml"
-      - name: Fetch the pinned pilot validators and the OpenSysML library sources
-        run: |
-          sudo apt-get install -y --no-install-recommends graphviz
-          git clone --depth 1 https://github.com/Open-MBEE/OpenSysML build/opensysml-src
-          (cd build/opensysml-src && ./scripts/download-pilot-sysml-validator.sh)
-          cp -r build/opensysml-src/build/pilot-validator build/opensysml-src/build/pilot-sysml-validator build/
+      - uses: actions/setup-go@v5
+        with: { go-version: '1.25' }
+      - run: sudo apt-get install -y --no-install-recommends graphviz z3
+      - name: Build OpenSysML at the pinned commit and fetch the pinned pilot validators
+        run: make tools
       - run: make tiers
       - run: make check

README.md

@@ -31,7 +31,7 @@ The model is written in standard SysML v2 and exists for two purposes:
 ## Running it
 
 ```bash
-make tools      # fetch OpenSysML (nightly + sources) and the pinned OMG pilot validators into build/
+make tools      # build OpenSysML from source at the pinned commit (scripts/fetch-tools.sh) and fetch the pinned OMG pilot validators into build/
 make check      # every gate: validate (strict), pilot (mission tier standalone, all files batch), house rules, runs/ diff
 make runs       # re-record runs/ after an intentional model change
 ```

docs/coverage/WP-B.md

@@ -21,7 +21,7 @@ Result legend: ✓ satisfied · ◐ construct in the model, tool result wrong or
 | SE-076 must | 31 : every leaf function performed by exactly one subsystem (`perform functions.handleData` on `cdh`, …) | `make validate` | ✓ 13 of 13 |
 | SE-077 should | — | — | ○ no software components in WP-B |
 | SE-078 must | 31 : `metadata def Critical`, `metadata def SinglePointWaiver`; `#Critical` units carry `[2]`/`[3]`/`[4]` or `@SinglePointWaiver { rationale }` (`primaryStructure`, `highGainAntenna`, `bag`); `required` vs installed on every `Unit` | `make validate`; `wpb-reliability` (k-of-n over `required`) | ✓ |
-| SE-079 should | 32 : `smallTarget`, `nominalTarget`, `largeTarget : TargetCase`, `targetCases`; the `variation attribute def TargetCases` is in `model/probes/F-B02-variant-binding-chain.sysml` | `wpb-xenon-large`, `wpb-hydrazine-large` | ◐ cases evaluate as plain usages; chaining through a `variant` fails (F-B02) |
+| SE-079 should | 32 : `smallTarget`, `nominalTarget`, `largeTarget : TargetCase`, `targetCases`; the `variation attribute def TargetCases` is in `model/probes/F-B02-variant-binding-chain.sysml` | `wpb-xenon-large`, `wpb-hydrazine-large` | ✓ cases evaluate as plain usages and through the `variant` (F-B02 fixed in pin: `ProbeVariantChain::viaVariant` = 507 000 kg) |
 | SE-080 should | — | — | ○ |
 | SE-081 could | — | — | ○ |
 | SE-082 must | 31 : `flow of TethysInterfaces::ElectricalPower`, `flow of Telemetry`, `flow of Propellant`, `flow of Heat`, `flow of ThrustCommand`, `flow of AttitudeEstimate`, `flow of RelativeState` between subsystem ports | `make validate` | ✓ every flow typed |
@@ -30,14 +30,14 @@ Result legend: ✓ satisfied · ◐ construct in the model, tool result wrong or
 | SE-085 must | backbone `model/09-ground.sysml` | — | — WP-D |
 | SE-086 must | backbone `model/08-launch.sysml`; 32 : `MassBudget.launcherCapability = arcturus5H.performanceAtC3` | `wpb-mass-budget` | — WP-C; used here |
 | SE-087 should | — | — | ○ tool tier (`DocumentQueries`) |
-| SE-088 could | 30 : `enum def Maturity { heritage; modified; newDesign }`; 31 : `Unit::maturity` on every unit | `wpb-tug-dry-mass-allocated` (contingency by maturity) | ◐ maturity read right, the `==` on it is F-B01 |
+| SE-088 could | 30 : `enum def Maturity { heritage; modified; newDesign }`; 31 : `Unit::maturity` on every unit | `wpb-tug-dry-mass-allocated` (contingency by maturity) | ✓ maturity read right and the `==` on it evaluates (F-B01 fixed in pin: `wpb-margin-policy` = 0.1) |
 | SE-089 could | — | — | ○ |
 | SE-090 could | — | — | ○ |
 | SE-121 must | 32 : `MassBudget` (`dryEstimate`, `dryWithContingency`, `dryAllocation`, `launchMass`, `launcherCapability`, `dryCloses`, `launchCloses`), `requirement <'TS-121'>` | `wpb-tug-dry-mass` = 3725.5 kg; `wpb-tug-dry-mass-allocated` = 4300.9 kg; `wpb-mass-budget` = 12624 kg; `wpb-budgets-satisfy` | ✓ dry margin 30 %, launch margin 36 % |
 | SE-122 should | — | — | ○ |
-| SE-123 must | 31 : `Unit::operatingPower/standbyPower/operatingModes/standbyModes/poweredShare`, `PowerInMode`, `UnitsPowerInMode`; 32 : `TugPowerInMode`, `PowerBudget.demand<Mode>` for the eight flight modes, `<'TS-123'>` | `wpb-unit-power-safe` = 42 W, `wpb-unit-power-thrusting` = 24.75 kW (right); `wpb-power-budget-safe` = 0 W (wrong) | ◐ on the pinned build F-B01 zeroes the rollup so `powerBudgetCloses` "holds" vacuously; on the F-B01-fixed build `demandThrusting` = 35 518 W against `arrayAtAphelionEol` = 39 757 W is `thrustingMargin` = 0.119 < the 0.15 policy — **power while thrusting does not close**; which attribute closes it (array rating, string draw or margin policy) is the pending maintainer decision |
+| SE-123 must | 31 : `Unit::operatingPower/standbyPower/operatingModes/standbyModes/poweredShare`, `PowerInMode`, `UnitsPowerInMode`; 32 : `TugPowerInMode`, `PowerBudget.demand<Mode>` for the eight flight modes, `<'TS-123'>` | `wpb-unit-power-safe` = 42 W, `wpb-unit-power-thrusting` = 24.75 kW (right); `wpb-power-budget-safe` = 0 W (wrong) | ✗ with F-B01 fixed in pin the rollup reads real demand and `satisfy powerBudgetCloses by powerBudget fails` (`wpb-budgets-satisfy`): `demandThrusting` = 35 518 W against `arrayAtAphelionEol` = 39 757 W is `thrustingMargin` = 0.119 < the 0.15 policy — **power while thrusting does not close**; which attribute closes it (array rating, string draw or margin policy) is the pending maintainer decision |
 | SE-124 must | 32 : `calc def ArrayPower`, `PowerBudget.arrayAtAphelionEol` from `TethysEnvironment::SolarFlux(amaranth.orbit.aphelionAu)` and `arrayWings.endOfLifeFactor` | `wpb-budgets-satisfy` (`thrustingCloses`) | ◐ capability 39.76 kW right; the demand it is checked against closes in every mode but `thrust` (SE-123) |
-| SE-125 must | 32 : `EnergyBudget` (DRO eclipse 4 h, launch to arrays 1.5 h, `maximumDepthOfDischarge`), `<'TS-125'>` | `wpb-budgets-satisfy` | ◐ usable 8640 W·h right; on the F-B01-fixed build `eclipseEnergy` = 3 588 W·h closes; `droEclipse = 4 h` is asserted, not derived (SE-264 open); static budget, no state-machine SOC run |
+| SE-125 must | 32 : `EnergyBudget` (DRO eclipse 4 h, launch to arrays 1.5 h, `maximumDepthOfDischarge`), `<'TS-125'>` | `wpb-budgets-satisfy` | ◐ usable 8640 W·h right; `eclipseEnergy` = 3 588 W·h closes against it (F-B01 fixed in pin, `wpb-budgets-satisfy`); `droEclipse = 4 h` is asserted, not derived (SE-264 open); static budget, no state-machine SOC run |
 | SE-126 must | 32 : `InspectorEnergyBudget`, `<'TS-126'>` | `wpb-budgets-satisfy` | ✓ 55 W·h of 108 W·h usable |
 | SE-127 must | 32 : `DataBudget` (`generatingRate`, `dailyGenerated`, `dailyDownlink`, `storageDemand`), `<'TS-127'>` | `wpb-data-daily` = 70.6 Gbit; `wpb-budgets-satisfy` | ✓ against 90 Gbit/day and 4 TB |
 | SE-128 must | — | — | — link budget is WP-D's; its 60 × 10⁶ km maximum range is asserted, not derived from the trajectory (domain list O7) |
@@ -46,7 +46,7 @@ Result legend: ✓ satisfied · ◐ construct in the model, tool result wrong or
 | SE-131 must | 32 : `PropellantBudget` (xenon per case, residuals, `tankCapacity`, `throughputLife`), `HydrazineBudget` (`DespinPropellant` per case, proximity Δv, stack control), `<'TS-130'>`, `<'TS-131'>` | `wpb-xenon-large`, `wpb-hydrazine-large` = 290 kg of 388 kg usable; `wpb-budgets-satisfy` | ✓ |
 | SE-132 must | 32 : `RootSumSquareDegrees`, `PointingBudget.antennaPointingErrorDegrees` vs `antennaAllocation`, `<'TS-132'>` | `wpb-pointing-antenna` = 0.0232° (allocation 0.05°) | ✓ |
 | SE-133 should | 32 : `PointingBudget.thrustVectorErrorDegrees` (centre-of-mass knowledge, thruster alignment, gimbal) | `wpb-budgets-satisfy` | ✓ 0.229° of 0.5° |
-| SE-134 must | 31 : `min/maxOperatingTemperature`, `predictedHot/ColdTemperature` on every unit; 32 : `RadiatorRejection`, `ThermalBudget` (hot case, cold-case heaters, `forAll` limits), `<'TS-134'>` | `wpb-radiator-capacity` = 7480 W; `wpb-budgets-satisfy` | ◐ limits and capacity right; on the F-B01-fixed build `hotCaseHeat` = 5 737 W closes against 7 480 W; pinned run still vacuous (F-B01) |
+| SE-134 must | 31 : `min/maxOperatingTemperature`, `predictedHot/ColdTemperature` on every unit; 32 : `RadiatorRejection`, `ThermalBudget` (hot case, cold-case heaters, `forAll` limits), `<'TS-134'>` | `wpb-radiator-capacity` = 7480 W; `wpb-budgets-satisfy` | ◐ limits and capacity right; `hotCaseHeat` = 5 737 W closes against 7 480 W (F-B01 fixed in pin, `wpb-budgets-satisfy`) |
 | SE-135 must | 32 : `CaptureLoadBudget` (contact force of the heavy case, cinch preload, thrust load vs `bag.cinchLoadCapacity`), `<'TS-135'>` — the small-body reading of the entry-loads rows | `wpb-budgets-satisfy` | ✓ 14.4 kN of 20 kN |
 | SE-136 must | as SE-135 | | ✓ |
 | SE-137 should | 31 : `Unit::doseRating : AbsorbedDoseValue`; 32 : `RadiationBudget` (150 Gy × RDM 2, `forAll`), `<'TS-137'>` | `wpb-budgets-satisfy` | ✓ |
@@ -57,15 +57,15 @@ Result legend: ✓ satisfied · ◐ construct in the model, tool result wrong or
 | SE-142 should | 31 : `FlightComputer.processorCapacityMips/LoadMips/memoryCapacity/memoryAllocated`; 32 : `ProcessorBudget`, `<'TS-142'>` | `wpb-budgets-satisfy` | ✓ 50 % reserve |
 | SE-143 should | — | — | — WP-D |
 | SE-144 could | — | — | ○ |
-| SE-145 must | 30 : `attribute def MarginPolicyRow`, `srrPolicy`/`pdrPolicy`/`cdrPolicy`/`acceptancePolicy`, `activePolicy`, `ContingencyFor`, `WithContingency`, `MarginFraction`, `constraint def ClosesWithMargin`/`WithinLimit`/`ReserveNotNegative`; every `assert constraint … : ClosesWithMargin { … in policy = activePolicy; }` in 32 | `wpb-margin-policy-alone` = 0.1 (right, file alone); `wpb-margin-policy` = 0.2 (wrong, whole model), 120.0, 0.2, holds | ◐ policy complete and referenced by every budget; on the F-B01-fixed build mass, xenon, energy and thermal close under `pdrPolicy`, power while thrusting does not (SE-123); pinned run still vacuous (F-B01) |
+| SE-145 must | 30 : `attribute def MarginPolicyRow`, `srrPolicy`/`pdrPolicy`/`cdrPolicy`/`acceptancePolicy`, `activePolicy`, `ContingencyFor`, `WithContingency`, `MarginFraction`, `constraint def ClosesWithMargin`/`WithinLimit`/`ReserveNotNegative`; every `assert constraint … : ClosesWithMargin { … in policy = activePolicy; }` in 32 | `wpb-margin-policy-alone` = 0.1 (right, file alone); `wpb-margin-policy` = 0.2 (wrong, whole model), 120.0, 0.2, holds | ◐ policy complete and referenced by every budget; mass, xenon, energy and thermal close under `pdrPolicy`, power while thrusting does not (SE-123; F-B01 fixed in pin, `wpb-budgets-satisfy`) |
 | SE-146 should | — | — | ○ tool tier (`DocumentQueries`); candidate `model/33-budget-report-tooling.sysml` |
 
 ## LANG rows
 
 | Row | File : element | Proving command | Result |
 | --- | --- | --- | --- |
 | LANG-506–510 attributes | 31 : `attribute def` — ; `Unit` attributes `mass : MassValue`, `operatingPower : PowerValue`, …; 30 : `attribute def MarginPolicyRow`, 32 : `attribute def TargetCase` | `make validate`, `make pilot` | ✓ |
-| LANG-511–518 enumerations | 31 : `enum def TugMode` (sixteen literals, the one mode vocabulary); 30 : `enum def Maturity`, `enum def ReviewGate`; enum-valued attributes and sequences (`allFlightModes : TugMode[*]`) | `make validate`, `make pilot`; `wpb-margin-policy` | ✓ (membership evaluation: F-B01) |
+| LANG-511–518 enumerations | 31 : `enum def TugMode` (sixteen literals, the one mode vocabulary); 30 : `enum def Maturity`, `enum def ReviewGate`; enum-valued attributes and sequences (`allFlightModes : TugMode[*]`) | `make validate`, `make pilot`; `wpb-margin-policy` | ✓ (F-B01 fixed in pin) |
 | LANG-547–551 parts | 31 : 60 `part def`s (`Unit`, `PassiveUnit`, `ElectronicUnit`, `Assembly`, ten subsystems, every unit type), `part argentDesign : ArgentTug` with redefinitions `part :>> sep : ArgentPropulsion`, sequences `part :>> units = (…)` | `instantiate-system` run | ✓ |
 | LANG-742–751 calculations | 31 : `PowerInMode`, `HeatInMode`, `UnitsPowerInMode`, `UnitsHeatInMode`; 30 : `ContingencyFor`, `WithContingency`, `MarginFraction`; 32 : `ArrayPower`, `ExpNeg`, `PropellantFor`, `MassFlowRate`, `RootSumSquareDegrees`, `Survival`, `SetReliability` (body items + `return`), `XenonForMission`, `DespinPropellant`, `RadiatorRejection`, `TugPowerInMode`, `TugHeatInMode`, `UnitsDataRate` | `wpb-*` runs | ✓ |
 | quantities and units | every physical quantity ISQ-typed with an SI literal: `[kg]`, `[W]`, `[K]`, `[Gy]`, `['W⋅h']`, `['bit/s']`, `['A⋅m²']`, `['°']`, `[N]`, `[Pa]`, `[Hz]`, `['m²']`, `[d]`, `[h]`; `[GHz]`/`[MPa]`/`[GB]` are not SI library literals, so `32.0e9 [Hz]`, `12.0e6 [Pa]`, `4.0e12 [B]` | `make validate`, `make pilot` | ✓ |

docs/coverage/WP-C.md

@@ -23,7 +23,7 @@ and surface speed are computed per case (`runs/wpc-target-cases.txt`).
 | SE-152 mode × subsystem | `TethysTarget::SmallBody::spinState` and `CaptureTargetCase` (moved to the backbone at integration) feed `TethysModes` through `TethysProximityOps` | `make check` (both) | partial — WP-E carries the matrix; Wren's units per mode are not modelled here |
 | SE-153 subsystem machines with orthogonal regions | `42:ProximityOpsModes::circumnavigating parallel { imaging; sounding }` | as SE-151 | partial: Wren's payload regions only |
 | SE-154 mission sequence | `40:CircumnavigationCampaign` (checkoutComplete → release → linkAcquired → imagingPasses → radarSounding → closePasses → characterisationDelivered → retreatToHold) | `make check` (both) | done — WP-C's segment of the timeline; `TethysMission::flightTimeline` now carries the `inspectorRetirement` event the campaign ends at |
-| SE-155 critical sequences with timing and go/no-go | `42:CaptureSequence` (`decide; if commit.go … else retreat`, `accept contact : ContactLoad`), `41:CaptureEnvelope` over the five cases, `42:ProximityOpsModes` (`accept after 7200.0 [s]`) | `runs/wpc-envelope-cases.txt`, `runs/wpc-capture-sequence.txt` | go/no-go satisfied (constraint verdicts per case); the sequence itself validates (both) but does not execute — F-C04 |
+| SE-155 critical sequences with timing and go/no-go | `42:CaptureSequence` (`decide; if commit.go … else retreat`, `accept contact : ContactLoad`), `41:CaptureEnvelope` over the five cases, `42:ProximityOpsModes` (`accept after 7200.0 [s]`) | `runs/wpc-envelope-cases.txt`, `runs/wpc-capture-sequence.txt` | go/no-go satisfied (constraint verdicts per case); the sequence itself validates (both) and instantiates (F-C04 fixed in pin) but `commit.go` does not evaluate — F-C05 |
 | SE-156 (replaced by the thrust-arc campaign) | — | — | not WP-C |
 | SE-157 capture sequence P10–P12 | `42:CaptureSequence` approach → contact → cinch → despin; `41:ContactForce`, `DespinDuration`, `DespinPropellant`, `MinimumRotationPeriod`; `TR-041`, `TR-042` | `runs/wpc-capture-calcs.txt`, `runs/wpc-requirements.txt` | satisfied: 10 kN at 0.10 m/s on 1 000 t over 0.5 m; 348 s and 6.44 kg for 4.17 × 10⁴ N·m·s at 120 N·m; 1 047 s minimum period for the largest body |
 | SE-158 Wren release and tug retreat | `42:proxStackFM` snapshots `beforeRelease`/`afterRelease` (12 624 → 12 600 kg), `40:wrenFM` snapshots `atRelease`/`atEndOfCampaign`, `40:WrenCampaignOutcome` variants `nominal`/`linkLost`/`notReleased` (F18, F19), `42:Retreat`, `TR-043` | `runs/wpc-individuals.txt`, `runs/wpc-requirements.txt` | satisfied |
@@ -55,5 +55,5 @@ and surface speed are computed per case (`runs/wpc-target-cases.txt`).
 
 F-C01 (`individual #Tag def` rejected by OpenSysML), F-C02 (metadata before `individual` accepted
 by OpenSysML, rejected by the pilot), F-C03 (redefinition direction not checked by OpenSysML),
-F-C04 (action output default evaluated before its input is bound — blocks `-action` on
+F-C04 (fixed in pin — action output default evaluated before its input is bound — blocks `-action` on
 `CaptureSequence`). Rows in `docs/findings/WP-C.md`, probes in `model/probes/`.