[devin-ai-integration]

Summary

Closes three confirmed model defects from the review triage of PR #1 (WP-C) and PR #2 (WP-I), gated on the pinned OpenSysML 5cd37f288 (runs/tool-version.txt, unchanged). Base is develop; the maintainer decisions 1-1, 1-2, 1-4, 2-1 and 2-2 are untouched (no change to model/41-capture-system.sysml or model/95-as-built.sysml).

1-5 — the despin step had no duration or propellant (model/42-proximity-ops.sysml)

CaptureSequence.despin : Despin bound only torque; TethysCaptureSystem::DespinDuration/DespinPropellant were never invoked.

Probe: sysml -e TethysProximityOps::captureOperation.capture.despin.{angularMomentum,duration,propellant} model/*

	before	after
despin.angularMomentum	— (no such attribute)	41735.51 kg·m²·s⁻¹
despin.duration	<undetermined>	347.80 s
despin.propellant	<undetermined>	5.9109 kg (= TethysBudgets::hydrazineBudget.despinNominal)

Fix: Despin takes in characterisation : TargetCharacterisation, in momentArm : LengthValue, in specificImpulse : DurationValue and derives angularMomentum (SphereMomentOfInertia, AngularMomentum), duration (DespinDuration) and propellant (DespinPropellant) through the existing WP-C calcs, dividing the units out inside the def as model/32-budgets.sysml does. The sequence binds characterise.characterisation, hydrazineBudget.momentArm (3.2 m) and hydrazineBudget.isp (225 s), so the values follow the characterised target case rather than a literal. torque stays the explicit 120 N·m: binding it to system.maximumDespinTorque through the sequence's in system evaluates to no value on the pin (same nested-parameter gap as F-C05), and the sequence itself still stops at ContactLoad for the pre-existing F-C05 commit.go error, so the step's values are shown by the new runs/wpc-despin-step.txt rather than by runs/wpc-capture-sequence.txt (unchanged). Not covered by the closed #37.

2-3 — late passivation passed the deadline check (model/97-disposal.sysml, TS-292)

passivation declared deadline = 30 d but its constraint had no time term, so any delay satisfied it.

Probe: sysml -e "TethysDisposal::closeout.passivationCompleteTime - TethysDisposal::closeout.disposalBurnTime" -e TethysDisposal::passivation.deadline -requirement TethysDisposal::passivation model/*

	before	after
delay / deadline	23.0 d / 30.0 d (not compared)	passivationDelay 23.0 d ≤ 30.0 d
TS-292 verdict	satisfied (vacuously on time)	satisfied (23 d ≤ 30 d)

Fix, as in the closed #31: attribute passivationDelay : DurationValue = closeout.passivationCompleteTime - closeout.disposalBurnTime; and … and passivationDelay >= 0.0 [d] and passivationDelay <= deadline in the constraint. The lower bound follows a review finding: with the passivation recorded before the burn (delay −11 d) the upper bound alone still reported satisfied; it now fails on that case.

2-4 — disposal calculations discarded units and bypassed targetCases (model/97-disposal.sysml, TS-293)

SeparationDeltaV and separationSafety used bare Reals, and the body masses were literals 150/362/620/438.8 t while TethysTarget::targetCases defines small/nominal/large as 213 327 / 362 000 / 505 664 kg.

Probe: sysml -e TethysDisposal::separationSafety.{small,nominal,large,asCharacterised}BodyDeltaV -requirement TethysDisposal::separationSafety model/*

	before	after
smallBodyDeltaV	1.6667e-4 (unitless, 150 t)	1.1719e-4 m/s (targetCases.small.mass)
nominalBodyDeltaV	6.9061e-5	1/14480 m/s (targetCases.nominal.mass)
largeBodyDeltaV	4.0323e-5 (620 t)	4.9440e-5 m/s (targetCases.large.mass)
asCharacterisedDeltaV	5.6974e-5	1/17552 m/s (amaranthFM.postCapture.mass, 438.8 t)
TS-293 verdict	satisfied	satisfied (both terms ≤ 1.0e-3 m/s)

Fix: SeparationDeltaV takes in impulse : ImpulseValue, in bodyMass : MassValue and returns SpeedValue = (impulse / (1 ['N⋅s'])) / (bodyMass / (1 [kg])) * (1 ['m/s']) (units divided out only inside the calc, as model/32-budgets.sysml); separationImpulse : ImpulseValue = 25.0 ['N⋅s']; the four Δv attributes are SpeedValues read from targetCases.{small,nominal,large}.mass and TethysAsBuilt::amaranthFM.postCapture.mass; the constraint compares against 1.0e-3 ['m/s']. The ISQ typing is as in the closed #31; the targetCases/amaranthFM reads replace the literals it kept. Answer to the triage's open question: the real masses move the small-body Δv from 1.67e-4 to 1.17e-4 m/s and the large-body Δv from 4.03e-5 to 4.94e-5 m/s — TS-293 does not flip; both verdicts remain satisfied.

Model files

• model/42-proximity-ops.sysml — Despin def and despin usage, TethysBudgets::hydrazineBudget import.
• model/97-disposal.sysml — passivation (TS-292), SeparationDeltaV, separationSafety (TS-293), TethysTarget::targetCases import.
• docs/coverage/WP-C.md, docs/coverage/WP-I.md — coverage lines updated to the derived values.

Runs moved

• New: runs/wpc-despin-step.txt, runs/disposal-quantities.txt (probes above, added to scripts/runs.sh).
• runs/house-rules.txt: self-model check 80 537 → 80 550 elements, 703 451 → 703 578 checks, 0 violations, 0 unevaluated.
• runs/as-built-satisfy.txt, runs/requirements-satisfy.txt, runs/wpb-budgets-satisfy.txt: one ID shift (separationSafety by argentFM.captureSystem ID 4677 → 4678), same verdicts.
• All other runs reproduce byte-identical at the pin.

Behaviour changes

• No verdict flips. TS-292 now genuinely tests the 23 d delay against 0 d … 30 d; TS-293 now evaluates the model's target-case masses; both stay satisfied.
• separationSafety.*DeltaV and separationImpulse are quantities (SpeedValue, ImpulseValue) instead of unitless Reals; the small/large Δv values change as listed above.
• Despin gains angularMomentum and three in parameters; despin.duration/despin.propellant evaluate (347.8 s, 5.91 kg) where they were undetermined.

Gate (pinned 5cd37f288, Go 1.25.11, JDK 21)

• make check (validate → pilot → house-rules → runs-check): green, 30 min 32 s. sysml -validate -strict -warnings-as-errors over the 64 model files: no errors. make house-rules: 80 550 elements, 703 578 checks, 0 violations, 0 unevaluated. make pilot-mission + make pilot-all: green, 128 pilot warnings, none in the files this PR touches (the set is develop's). make runs-check: 0 differences across the 270 recorded runs.
• Re-gated after the review fix (1dc9644): strict validate clean, house-rules 80 550 / 703 578 / 0 unchanged, scripts/runs.sh reproduces all 270 runs byte-identical (the extra constraint term moves no recorded run), pilot-mission + pilot-all green, software-check green.
• After merging develop d49d64b (fix(model): station downlinks, light-time envelopes and the operations-day endpoint #46) as 74109ba: runs/house-rules.txt re-recorded from the combined tree (80 555 elements, 703 630 checks, 0 violations — the only conflict); make check + make software-check green again (35 min 47 s), 0 run differences.
• make software-check: green — selftest ok (344 commands, 961 telemetry points, 181 events, 51 packets, 48 parameters, 16 mode rows, 12 state machines), generated tables do not drift, 11 Python tests passed.
• git ls-remote --heads origin before pushing: the only other branches touching models 41/42/95/97 are wp/c-review-fixes and wp/as-built-review-fixes (the closed WP-C: envelope bounds angular momentum, commit uses upper-bound mass, link rates fit the transceiver #37 / fix(as-built): bind disposal requirements to gauged data and type the quantities #31).

Link to Devin session: https://nasa-jpl-demo.devinenterprise.com/sessions/6752b07e631249a29b882e1dd917bf85
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/6752b07e631249a29b882e1dd917bf85?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

[devin-ai-integration]

Devin Review found 1 new potential issue.

1 flag not posted on this PR by your GitHub settings — view it in Devin Review. (Configure)