Repository navigation
Executable flight and ground software generated from the architecture, with its conformance harness (software/) - #29
Merged
Merged
Conversation
Add software/gen/generate.py, which reads the model through the pinned OpenSysML (-convert api-json, streamed per package) and writes deterministic C11 headers and Python NamedTuple modules under software/generated/: enums, command/telemetry/event dictionaries, packet layouts, parameter and limit tables, the mode table, twelve state-machine transition tables, the partition/rate-group/AABP-1 schedule and the inter-application interfaces. A hand-written C self-test compiles every header under -std=c11 -Wall -Wextra -Werror -pedantic and checks the table invariants; pytest cross-checks the Python tables against the pinned runs/. make software-generate, software-selftest, software-test and software-check (regenerate into a scratch dir, fail on drift) join the Makefile; the software-check job joins the workflow beside the unchanged model-only check. Coverage and findings (F-SW1001-F-SW1009) are under docs/. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…rator Co-Authored-By: jason.han <hanhuijun@gmail.com>
Add emit_go.py, writing software/generated/go/argenttables/*.go (and the go.mod beside it) in gofmt's canonical form, with the same header and MANIFEST conventions as the C and Python tables. Add a ground table (ground.py, ground.go) carrying the FR-001 to FR-004 flight rules and their constraint definitions, the on-board sequence definitions, the sequence checker's constants, the suite's twelve components, the archive retention rules, the proximity-operations products and the pass-planning data, so the ground software reads them from the model rather than from literals. Keep the requirements' short names in the api-json index for that, and read negative quantity literals (-0.1 [rad/s]) that the extractor previously left unbound, which binds 56 telemetry low limits in argent_telemetry.h and telemetry.py. Co-Authored-By: jason.han <hanhuijun@gmail.com>
The twelve components of TethysGroundSoftware as table-driven Python under software/ground/meridian: Forge (ValidateCommand over the dictionary), Warden (the FR- rules from the generated ground table), Lantern (CCSDS decommutation from the packet tables, limits, AlarmLifecycle, LinearTrend), Almanac, Vault, Ledger (with the programme's open gates as the model states them), Compass, Sextant (every calculation through the pinned OpenSysML client against a pinned sysml-grpc), the four simulators and the suite. Co-Authored-By: jason.han <hanhuijun@gmail.com>
pytest under software/ground/tests reproduces every verdict of runs/sw-ground-structure.txt and runs/sw-ground-sequencer-check.txt, names the TM-/TF-/SA- rows it checks, cross-checks the table-driven components against the model's calc definitions through the pinned client, and pins the golden packet fixtures (software/ground/fixtures/packets.json) the flight side can decode. Co-Authored-By: jason.han <hanhuijun@gmail.com>
software/ground/go: Meridian Lantern as an always-on Go service (CCSDS packet ingestion, decommutation by the generated packet tables, dictionary limits, alarms, archive, MLS-2 frame synchronisation) and the command uplink service (accepts Forge/Warden products, enforces the two-step hazardous flow server-side, frames for MLS-2 from the ICD parameter table); tests on the golden fixtures. Co-Authored-By: jason.han <hanhuijun@gmail.com>
software/ground/ground.mk builds sysml-grpc from the pinned checkout, runs the meridian pytest suite over it and gofmt/vet/test on the Go module and the generated Go package; one Makefile include, one CI job, one software README paragraph; software/ground/README.md documents the packet fixture format. Co-Authored-By: jason.han <hanhuijun@gmail.com>
docs/coverage/WP-SW-11.md maps every component, simulator, table and interface of the ground model to its artefact with the oracle of each test; docs/findings/WP-SW-11.md records F-SW1101 … F-SW1109 with the client probe under software/ground/probes/. Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
…erator The inspector's mode vocabulary is now an enum def of TethysModes (one literal per leaf state of InspectorModes, documented), as TugMode is for TugModes. The generator reads it like every other enum def instead of synthesising it from the state machine's leaf states; argent_enums.h, enums.py and the manifest are regenerated with the same seven literals. - software/README.md: the 961 x 16 per-mode telemetry-rate matrix is recoverable from the mode rate sets; every enumeration is model-declared - docs/findings: F-SW1009 resolved by model edit; coverage row updated - runs/house-rules.txt re-recorded (self-model census +9 elements) - stop tracking software/gen/__pycache__ Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
… it in the generator
…ost harness Kestrel-style time/space-partitioned cyclic executive over the generated schedule, host HAL (simulated clock, RIU registers, AABP-1 bus, MLS-2 link, image store), AABP-1 software bus with the per-mode reserve check, command/ telemetry/event/parameter/image services, the twelve applications on one table-driven state-machine runner, the JSONL trace, the argent_host scenario harness and the pinned-run comparison that reproduces the fourteen mode-manager, FDIR, SEP, capture, boot and failover runs. Co-Authored-By: jason.han <hanhuijun@gmail.com>
InspectorMode is now the model's enum def (TethysModes::InspectorMode); the Go tables are regenerated from it, byte-identical under make software-check. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…-flight-check gate Seven self-contained suites (state-machine runner, bus, command, telemetry, services, executive, integrated system) covering every stream, command, hazardous inhibit, packet, event, parameter row, limit, task, guard/effect id and the reachability of all 100 states / 161 transitions; the fourteen pinned runs are shipped as scenarios and re-derived byte-identically by the gate. Telemetry resolves packet fields once at initialisation and owns the sequence count; the root Makefile includes software/flight/flight.mk. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…indings, CI job Adds the software-flight-check job, the stage-2 paragraph in software/README.md, the trace/stimulus/exit-code contract in software/flight/README.md and the coverage and findings documents for the flight package. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…-flight Co-Authored-By: jason.han <hanhuijun@gmail.com> # Conflicts: # .github/workflows/check.yml # Makefile
…oss-check Packet fields sit at their table offset from the packet start (the first at header_bits), not header_bits further; the encoder rounds to the nearest count so raw -> engineering -> raw round-trips. argent_host --golden rebuilds the ground package's fixtures from their engineering values and tests/golden_packets.py checks all 51 byte for byte as part of the gate. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…forwards to exact deadlines A dispatched item that no active state takes is held (up to 16 per machine) and offered again when a state that names it becomes active, which is how the pinned model routes a transfer to a port: the run keeps it until an accepter takes it. The attitude-control region of TugModes now ends every scenario in the model's state (F-SW1201). The fast-forward deadline search skipped a timer expiring exactly on the frame it was computed in; it now includes it. Co-Authored-By: jason.han <hanhuijun@gmail.com>
… this host's uplink only The sequence render prints six significant digits, so campaign times such as 19880640 reached the host as 19880600; derived times are snapped to the gcd of the driver script's delays. Messages the operations centre sends to the inspector's own uplink are no longer stimuli of the tug host. The attitude-control wildcard is gone: the host agrees with the pinned run. Co-Authored-By: jason.han <hanhuijun@gmail.com>
software/conformance compares, per machine and scenario, the host's --trace state sequences with the model's ExecuteState(trace=true) trace at the pinned OpenSysML: every configuration change with its time, the transitions and accepts, with wall-clock, peak RSS and output size per step. make software-conformance-check compares the outputs byte for byte with software/conformance/expected/. Co-Authored-By: jason.han <hanhuijun@gmail.com>
Every calc def the software uses is evaluated by the model (Model.eval at the pin) and, where the pin compiles it, by its compiled C and Go programs over a deterministic grid of the model's own values and boundary points, with an explicit tolerance per calc (1e-9 relative for Reals, exact for Integer, Boolean and enumeration results). Each calc lands in one bucket: agree, disagree, does-not-compile-at-pin with the pin's reason, or not-driveable with what covers it instead. The power margin (11.9 % against 15 %) and the bus slots by mode (36 of 64 against the 32 reserve) come out of the model and the generated tables identical and failing. The compile steps run in parallel; the pin has no Python target. Co-Authored-By: jason.han <hanhuijun@gmail.com>
The five planned flightSoftwareInTheLoop cases of the software VCRM run on the flight host, the model through sysml-grpc and the ground suite, each with an evidence file under software/conformance/evidence/ (inputs, both sides' outputs, the case's own pass criterion, tool pin): final targeting (Earth-impact exclusion abort), thrust arc (string restart and the relay rule), capture sequence (fire when armed, hold when inhibited), fault detection (latency and the safe configuration) and the ground two-step (second approval and the flight-rule refusal). Two conformance scenarios drive the host for them; the trace rebuild prefers the run's own machine instance when a scenario traces two. Co-Authored-By: jason.han <hanhuijun@gmail.com>
next_deadline() polled only the state machines' timers, so a --fast-forward skip jumped over an on-board sequence step and the step items fired on the first frame after the skip (the inspector release steps hours late). The sequence engine's next step is a deadline too. CI job software-conformance-check runs make software-conformance-check after the flight job. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…cation cases pass The five flightSoftwareInTheLoop cases of TethysSoftwareAssurance that the conformance harness ran move from planned to pass with their evidence paths; the VCRM and test-plan documents and the assurance counts are re-recorded. software/conformance/README.md, docs/coverage/WP-SW-13.md, docs/findings/WP-SW-13.md (F-SW1301 to F-SW1310, with the F-SW1305 probe) and one paragraph in software/README.md. Co-Authored-By: jason.han <hanhuijun@gmail.com>
Contributor
Author
|
I'll fix CI failures and address comments from users with write access. I'll skip comments containing "(aside)".
|
HuiJun
marked this pull request as ready for review
October 23, 2026 22:52
…s: largest-case period, xenon trend from the propellant book) Co-Authored-By: jason.han <hanhuijun@gmail.com> # Conflicts: # runs/house-rules.txt
…owance on the flown arcs)
devin-ai-integration
Bot
changed the base branch from
integration/phase-6
to
develop
October 28, 2026 22:50
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
The
software/tree: everything executable that the software architecture tier (models 63–69, 88, 94) describes, derived from the pinned model (OpenSysML5cd37f288) rather than written beside it. Stacked on the architecture PR (#23); carries #24, #26, #25, #27 and #28 as merge commits, each landed at its CI-green head.software/gen/— deterministic generator: model (api-json +-compile -source) → C/Python/Go tables (software/generated/): 344 commands (51 hazardous), 961 telemetry points, 181 events, 51 packets, 48 parameters, 16 mode rows, 12 state machines / 100 states / 161 transitions, 22 tasks, 13 AABP-1 streams on 64 slots, plus the ground table (flight rules, sequences, stations, retention). Byte-identical regeneration is a gate (software-check).software/flight/— Argent flight software in C11 on those tables only: Kestrel-style partitioned cyclic executive, AABP-1 bus, command/telemetry/event/parameter services, one table-driven state-machine runner for the twelve applications, host HAL, JSONL trace whosemachinesstrings equal OpenSysML'sCurrent state:lines (software-flight-check: strict + sanitised builds, 9 277 unit checks, 14 pinned runs reproduced, 51 golden packets).software/ground/— Meridian Operations Suite: Python components evaluating the model's calcs through the pinned client (Model.evaloversysml-grpc), Go telemetry and uplink services, four simulators, golden packet fixtures (software-ground-check).software/conformance/— the harness: C-host trace vs gRPCExecuteState(trace)per machine and scenario (149 machine-runs, 146 agree, 3 adjudicated), compiled vs interpreted calc grids (47 calcs: 10 agree, 0 disagree, 15 do not compile at the pin, 22 not driveable), and the five flight-software-in-the-loop verification cases run as as-run evidence (software-conformance-check).Model edits:
enum def InspectorModedeclared in model 60 (the generator had synthesised it); the five run cases in model 88 movedplanned → passwith their evidence paths. Everything else about the model is read, not written.Behaviour that stays visible on purpose
TF-011 bus reserve fails (36 of 64 slots vs the 32-slot reserve in proximity operations/capture/despin) in the model, the host's
bus_reserve_check()and the harness alike; the power margin is 11.9 % against the 15 % policy on both sides; SA-001/SA-002 stay open (independent V&VinProgress); 26 verification cases stayplanned(no unit/integration/HIL/flatsat bench in this repository). Recorded, not edited: FR-003's 25° vs the sequencer's 30°,BatteryDepthOfDischargeusing the literal 0.4, the host's sequence-3 step items with no model source. The pinned run's retention of routed transfers was adjudicated for the model (SysML v2 §7.17.8/§7.18.3) and the host corrected.Findings
docs/findings/WP-SW-10.md…WP-SW-13.md(coverage indocs/coverage/): tool-side defects each have a probe; the ones already fixed upstream of the pin are marked for the next pin bump (graph export nil-deref, multi-file Python generator, duplicate performer instance over gRPC).Link to Devin session: https://nasa-jpl-demo.devinenterprise.com/sessions/bd8333c05232470c8601104d484dcc58
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/bd8333c05232470c8601104d484dcc58?variant=devin
Requested by: @HuiJun