From b3649c00e7dd633f36792a1e040d3b5c23e5c62d Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Tue, 15 Sep 2026 06:33:39 +0000 Subject: [PATCH 01/11] feat(stressmodel): generate the satellite network as a fleet of occurrences Add a fleet form to the stress-model generator (cmd/stress-model -fleet): four spacecraft blocks carry the as-built values as defaults, each orbital plane is 'part sats : Block[N] ordered', and only every sixteenth unit states values of its own, as a member subsetting the plane's fleet. The spacecraft, ground segment, requirements, mode machine, ring, inter-plane and downlink connectors are those of the single-definition form, whose output is unchanged. Stats gains Definitions and Units so the forms compare. At 12 800 satellites the fleet declares 11 667 elements against 2 354 827 and validates in 0.57 s and 185 MB rather than 301 s and 20.1 GB. The guide chapter on modeling fleets shows both forms, the stress-test record and the performance notes carry the measurements, including what the current runtime pays to instantiate, check and read the occurrences, and BenchmarkFleetInstantiate and BenchmarkFleetSatisfy time it. Co-Authored-By: jason.han --- README.md | 2 +- .../stress-model-fleet-mode.added.md | 12 + cmd/stress-model/main.go | 11 +- docs/guide/README.md | 5 + docs/guide/modeling-fleets.md | 293 ++++++++++++++++++ docs/internals/performance.md | 22 ++ docs/project/satellite-network-stress-test.md | 114 ++++++- docs/project/spec-compliance.md | 2 +- internal/stressmodel/bench_test.go | 69 +++++ internal/stressmodel/satnet.go | 182 ++++++++++- internal/stressmodel/satnet_test.go | 80 +++++ mkdocs.yml | 1 + 12 files changed, 771 insertions(+), 22 deletions(-) create mode 100644 changes/unreleased/stress-model-fleet-mode.added.md create mode 100644 docs/guide/modeling-fleets.md diff --git a/README.md b/README.md index 6510b47f17..fd73e1043b 100644 --- a/README.md +++ b/README.md @@ -326,7 +326,7 @@ What these numbers cannot show: the OMG corpora are demonstrations rather than a **Current commit:** All tests pass (`go test -race ./...`), builds clean (`go build ./...`). -**Test coverage:** 8,369 top-level `Test` functions (counted from the `_test.go` files, as `go test ./...` runs them) covering parsers, semantics, runtime (actions, states, instances, operators, validation). Behavioral robustness: 206 golden ASTs, 252 negatives, 917 conformance cases, 235 golden traces, 459 runtime robustness cases, 21 gRPC conformance cases and 8 gRPC robustness cases. These figures are generated by `make docs-counts` from the tree and gated. A test skips only for want of something the run did not provide, and says what: the held-image round trip declines a conformance case that creates no instance, a few gate on a PDF or Mermaid toolchain, a pinned pilot artifact, the PSSM suite, a locale, a case-insensitive filesystem or a live Flexo stack, and the OMG corpus gates skip until the corpora are downloaded unless asked to fail. +**Test coverage:** 8,371 top-level `Test` functions (counted from the `_test.go` files, as `go test ./...` runs them) covering parsers, semantics, runtime (actions, states, instances, operators, validation). Behavioral robustness: 206 golden ASTs, 252 negatives, 917 conformance cases, 235 golden traces, 459 runtime robustness cases, 21 gRPC conformance cases and 8 gRPC robustness cases. These figures are generated by `make docs-counts` from the tree and gated. A test skips only for want of something the run did not provide, and says what: the held-image round trip declines a conformance case that creates no instance, a few gate on a PDF or Mermaid toolchain, a pinned pilot artifact, the PSSM suite, a locale, a case-insensitive filesystem or a live Flexo stack, and the OMG corpus gates skip until the corpora are downloaded unless asked to fail. **Parser coverage:** 101/101 bundled library files parse cleanly — the 94 official SysML v2 standard library files and the non-normative `OpenSysML Libraries/OpenSysMLMathFunctions.kerml`, `OpenSysML Libraries/DocumentQueries.sysml`, `OpenSysML Libraries/IdentityMetadata.sysml`, `OpenSysML Libraries/DiagramLayout.sysml`, `OpenSysML Libraries/OOSEM.sysml`, `OpenSysML Libraries/MOSA.sysml` and `OpenSysML Libraries/StateSpaceIntegration.sysml` extensions. Conformance verified by [stdlib_conformance_test.go](internal/core/libs/stdlib_conformance_test.go). Grammar reference: [OMG Xtext grammar](https://github.com/Systems-Modeling/SysML-v2-Pilot-Implementation/tree/master/org.omg.kerml.xtext/src/org/omg/kerml/xtext). **Behavioral execution:** Calc/constraint/requirement/satisfy functional. Action/state executors handle nested invocation, control flow keywords, loop and conditional statements and the send statement (917/917 conformance cases passing). Coverage is self-assessed against the specification text and the normative library: the pinned OMG pilot implementation evaluates expressions but does not execute actions or state machines headlessly, so no external implementation currently adjudicates these rows. See [spec compliance](docs/project/spec-compliance.md). **Reference differential:** 377 files compared diagnostic-by-diagnostic against the pinned OMG pilot implementation (`2026-08`), 346 in full agreement; every divergence is enumerated and adjudicated in [the differential](docs/project/pilot-differential.md), reproducible with `go run ./cmd/pilot-diff`. diff --git a/changes/unreleased/stress-model-fleet-mode.added.md b/changes/unreleased/stress-model-fleet-mode.added.md new file mode 100644 index 0000000000..cf6f3b5b0f --- /dev/null +++ b/changes/unreleased/stress-model-fleet-mode.added.md @@ -0,0 +1,12 @@ +- **The satellite-network stress model can be generated as a fleet.** `cmd/stress-model -fleet` + declares each orbital plane as occurrences of one of four spacecraft blocks — `part sats : + BlockA[400] ordered` — with the as-built values as the block's defaults and stated only on the + units that diverge, instead of one `part def` per satellite; the spacecraft, ground segment, + requirements, state machine, ring, inter-plane and downlink connectors are unchanged. `-stats` + now reports the spacecraft definitions and the units carrying values of their own in both forms, + so the two can be compared: at 12 800 satellites the fleet declares 11 667 elements against + 2 354 827, and validates in 0.57 s and 185 MB rather than 301 s and 20.1 GB. A guide chapter, + `docs/guide/modeling-fleets.md`, shows the constellation both ways and what the + runtime does with 12 800 occurrences, and the stress-test record and performance notes carry the + measurements. `BenchmarkFleetInstantiate` and `BenchmarkFleetSatisfy` in `internal/stressmodel` + time the runtime over the fleet form. diff --git a/cmd/stress-model/main.go b/cmd/stress-model/main.go index ce3618c283..ccab08e5c5 100644 --- a/cmd/stress-model/main.go +++ b/cmd/stress-model/main.go @@ -1,7 +1,9 @@ // Command stress-model writes a large generated SysML v2 model of a stated shape // and size to stdout, for measuring how the toolchain scales. The one shape today // is a satellite network — a constellation of fully modeled spacecraft and the -// ground stations they downlink to. See docs/project/satellite-network-stress-test.md. +// ground stations they downlink to — written either with one definition per +// satellite or, with -fleet, as occurrences of a few spacecraft blocks. See +// docs/project/satellite-network-stress-test.md and docs/guide/modeling-fleets.md. package main import ( @@ -16,6 +18,7 @@ func main() { planes := flag.Int("planes", 4, "orbital planes in the constellation") perPlane := flag.Int("satellites", 8, "satellites in each orbital plane") stations := flag.Int("ground-stations", 3, "ground stations the constellation downlinks to") + fleet := flag.Bool("fleet", false, "declare each plane as occurrences of one spacecraft block rather than one definition per satellite") stats := flag.Bool("stats", false, "report on stderr what the model declares") flag.Parse() if flag.NArg() != 0 { @@ -26,14 +29,14 @@ func main() { fmt.Fprintln(os.Stderr, "stress-model: -planes and -satellites must be at least 1 and -ground-stations at least 0") os.Exit(2) } - n := stressmodel.SatelliteNetwork{Planes: *planes, Satellites: *perPlane, GroundStations: *stations} + n := stressmodel.SatelliteNetwork{Planes: *planes, Satellites: *perPlane, GroundStations: *stations, Fleet: *fleet} s, err := n.Generate(os.Stdout) if err != nil { fmt.Fprintf(os.Stderr, "stress-model: %v\n", err) os.Exit(1) } if *stats { - fmt.Fprintf(os.Stderr, "satellites=%d ground-stations=%d components=%d connections=%d requirements=%d elements=%d bytes=%d\n", - s.Satellites, s.GroundStations, s.Components, s.Connections, s.Requirements, s.Elements, s.Bytes) + fmt.Fprintf(os.Stderr, "satellites=%d definitions=%d units=%d ground-stations=%d components=%d connections=%d requirements=%d elements=%d bytes=%d\n", + s.Satellites, s.Definitions, s.Units, s.GroundStations, s.Components, s.Connections, s.Requirements, s.Elements, s.Bytes) } } diff --git a/docs/guide/README.md b/docs/guide/README.md index 28cf81f527..efee439128 100644 --- a/docs/guide/README.md +++ b/docs/guide/README.md @@ -13,6 +13,11 @@ Read the chapters in order the first time through; each one builds on the ones b 9. [From your own program](09-clients.md) — the Go, Python, Node, Java and Rust clients 10. [Troubleshooting](10-troubleshooting.md) — diagnosing a run that stops early +One topic stands on its own once the chapters are read: +[Modeling fleets and repeated structure](modeling-fleets.md) — one definition with a +multiplicity, variants with occurrence counts, per-occurrence values, and what a fleet of +12 800 occurrences costs to validate and to check. + Chapter 9 does one task in all five clients side by side — Go, Python, Node/TypeScript, Java and Rust, in tabs — and then has a section per client for what only that one has. [Client libraries](../reference/clients.md) explains which to choose and what each covers. diff --git a/docs/guide/modeling-fleets.md b/docs/guide/modeling-fleets.md new file mode 100644 index 0000000000..bb7f1e4049 --- /dev/null +++ b/docs/guide/modeling-fleets.md @@ -0,0 +1,293 @@ +# Modeling fleets and repeated structure + +A fleet — a constellation of satellites, a production run of vehicles, a rack of +identical servers — is one design, or a few, built many times with values that +differ per unit. This chapter shows how to write that in SysML v2 so the model +declares the design once and the units as *occurrences* of it, what the choice +costs in declared elements against writing every unit out, and what the +runtime does with a fleet of 12 800 occurrences today. + +## One definition, a multiplicity + +The unit of a fleet is a `part def`. The fleet is a usage of it with a +multiplicity: + +```sysml +part def Spacecraft { + attribute catalogId : Integer; + part comms : CommsSubsystem; + attribute dryMass : Real = eps.mass + adcs.mass + comms.mass; +} + +part def OrbitalPlane { + part sats : Spacecraft[400] ordered; +} +``` + +`sats` is one declared element whatever the number in the brackets. Every +occurrence has the shape `Spacecraft` gives it — the same features, the same +computed `dryMass`, the same mode machine — and the runtime creates the 400 +objects when the plane is instantiated, not when the model is read. + +Occurrences are addressed by position in an ordered collection and as a +whole for anything that applies to all of them: + +```sysml +sysml> %eval network.plane1.sats#(3).catalogId +sysml> %eval network.plane0.sats.dryMass // one value per occurrence +``` + +A connector whose ends are collection paths connects the occurrences, so +`connect sats.comms.crosslinkTx to sats.comms.crosslinkRx` links the fleet's +crosslink ports, and `connect plane0.sats.comms.rf to gs0.uplink` gives every +satellite in a plane a downlink to one station. + +## Variants as specializations + +A fleet is rarely one design. Write each variant as a specialization that +sets what differs — as *defaults*, so an occurrence that says nothing inherits +the variant's values and one that diverges can still redefine them: + +```sysml +part def BlockA :> Spacecraft { + attribute :>> catalogId default = 40000; + part :>> comms { + part :>> crosslinkTerminal { + attribute :>> mass default = 3.1 [kg]; + attribute :>> serialNumber default = "CROSSLINKTERMINAL-00000-1"; + } + } +} + +part def BlockB :> Spacecraft { /* … */ } +``` + +A plane of block-A spacecraft redefines its fleet to the variant, and the +occurrence count travels with the plane: + +```sysml +part plane0 : OrbitalPlane { + part :>> sats : BlockA { attribute :>> plane = 0; } +} +part plane1 : OrbitalPlane { + part :>> sats : BlockB { attribute :>> plane = 1; } +} +``` + +A value written with `=` on the variant is fixed for every occurrence and +cannot be redefined beneath it; write `default =` for anything a unit may +state for itself, and `=` for what is genuinely a property of the design. + +## Per-occurrence values + +A unit whose as-built values differ from its variant's — a heavier terminal, +a serial number — is a member of the fleet that subsets it and redefines the +values it owns: + +```sysml +part plane0 : OrbitalPlane { + part :>> sats : BlockA { attribute :>> plane = 0; } + part unit16 :> sats { + attribute :>> catalogId = 40016; + attribute :>> slot = 16; + part :>> comms { + part :>> crosslinkTerminal { + attribute :>> mass = 19.9 [kg]; + attribute :>> serialNumber = "CROSSLINKTERMINAL-00016-1"; + } + } + } +} +``` + +`unit16` is one of the occurrences of `sats` — the collection still has 400 +members, and the units that subset it are its leading members, so with +`unit0` and `unit16` declared, `sats#(1)` is `unit0`, `sats#(2)` is `unit16` +and `sats#(3)` onward read the block's defaults. A diverging unit inherits +everything it does not state, and it is checked by whatever checks the +fleet. The cost of the model is now proportional to how many units +*diverge*, not to how many there are. + +What the language also allows, and this implementation does not yet, is to +carry the per-unit values as one table the fleet binds to — a sequence of +serial numbers bound to `sats.comms.crosslinkTerminal.serialNumber` so that +the *n*th occurrence reads the *n*th entry. A binding to a collection path is +accepted, but a target feature that already carries a default is a binding +conflict, and a sequence of 12 800 literals written in the source is as long +as the fleet it describes. Until the runtime can bind a table over defaults, +write diverging units as above and keep the variant's values as defaults. + +## The stress-test constellation, both ways + +`internal/stressmodel` (`cmd/stress-model`) generates the +[satellite-network stress test](../project/satellite-network-stress-test.md) +in both forms: `-fleet` selects the fleet form. Both state the same +spacecraft — seven subsystems, twenty components with mass, power draw and +serial number, the power and data connections between them, a mass and a +power budget, three requirements with `satisfy` assertions, a mode machine +every spacecraft exhibits — the same ground stations, the same ring and +inter-plane crosslinks and the same downlinks. + +**One definition per satellite.** Every satellite is its own `part def` +specializing `Spacecraft` and redefines the whole tree beneath it to state +its serial numbers and as-built masses; the network is a usage of each: + +```sysml +part def Sat0 :> Spacecraft { + attribute :>> catalogId = 40000; + part :>> eps { + part :>> solarArray { + attribute :>> mass = 2.0 [kg]; + attribute :>> serialNumber = "SOLARARRAY-00000-0"; + // … + } + // … + } + // … about 180 declared elements per satellite, its links and requirements included +} +part def Sat1 :> Spacecraft { /* … */ } +part def Network { + part sat0 : Sat0; + part sat1 : Sat1; + interface link0To1 : RFLink connect sat0.comms.crosslinkTx to sat1.comms.crosslinkRx; + // … +} +``` + +**Fleet.** Four spacecraft blocks carry the as-built values as defaults; each +orbital plane is `part sats : Block[N] ordered` with a ring link over the +collection; every sixteenth unit states a catalog number, a slot and a +crosslink terminal of its own; the requirements are declared once per block +and asserted on the block's configuration and on every diverging unit: + +```sysml +part def OrbitalPlane { + attribute plane : Integer; + part sats : Spacecraft[400] ordered; + interface ring : RFLink connect sats.comms.crosslinkTx to sats.comms.crosslinkRx; +} +part def Network { + part plane0 : OrbitalPlane { + part :>> sats : BlockA { attribute :>> plane = 0; } + part unit0 :> sats { /* as-built values */ } + part unit16 :> sats { /* … */ } + } + // … + interface plane0To1 : RFLink connect plane0.sats.comms.crosslinkTx to plane1.sats.comms.crosslinkRx; + interface downlink0To0 : RFLink connect plane0.sats.comms.rf to gs0.uplink; +} +satisfy blockAMass by blockAConfig; +satisfy blockAMass by network.plane0.unit16; +``` + +`-stats` reports the element count of either form — the number of +declarations the source makes: + +```bash +go run ./cmd/stress-model -planes 8 -satellites 200 -ground-stations 20 -stats > legacy.sysml +# satellites=1600 definitions=1600 units=1600 ground-stations=20 components=32080 connections=25400 requirements=4800 elements=294627 bytes=18135413 +go run ./cmd/stress-model -planes 8 -satellites 200 -ground-stations 20 -fleet -stats > fleet.sysml +# satellites=1600 definitions=4 units=104 ground-stations=20 components=264 connections=220 requirements=12 elements=3099 bytes=183994 +``` + +| satellites | planes × per plane | form | definitions | units stating values | elements | source | +| ---------- | ------------------ | ---- | ----------- | -------------------- | -------- | ------ | +| 1 600 | 8 × 200 | one definition per satellite | 1 600 | 1 600 | 294 627 | 18.1 MB | +| 1 600 | 8 × 200 | fleet | 4 | 104 | 3 099 | 184 KB | +| 12 800 | 32 × 400 | one definition per satellite | 12 800 | 12 800 | 2 354 827 | 145 MB | +| 12 800 | 32 × 400 | fleet | 4 | 800 | 11 667 | 716 KB | + +The fleet form of the 12 800-satellite constellation is **11 667 declared +elements against 2 354 827** — a factor of 200 — and what remains grows with +the number of planes (links, downlinks) and of diverging units, not with the +number of satellites. (The +[stress-test record](../project/satellite-network-stress-test.md)'s +single-definition counts, 299 137 and 2 392 417, are the same constellation +split differently into planes and stations; the counts here are the same +layout in both forms.) + +## What it costs to validate + +All figures below were taken on one machine — `Intel Xeon Platinum 8559C`, +8 CPUs, 31 GiB of memory, no swap, Go 1.25, Linux — from the binary +`make build` produces, as single runs; peak RSS is measured from outside with +`/usr/bin/time`. + +`sysml -validate -memstats`, both forms over the layouts above: + +| satellites | form | elements | wall | allocated | peak RSS | +| ---------- | ---- | -------- | ---- | --------- | -------- | +| 1 600 | one definition per satellite | 294 627 | 17.5 s | 5.5 GiB | 2.6 GB | +| 1 600 | fleet, 8 × 200 | 3 099 | 0.16 s | 92 MiB | 106 MB | +| 12 800 | one definition per satellite | 2 354 827 | 301 s | 43.5 GiB | 20.1 GB | +| 12 800 | fleet, 32 × 400 | 11 667 | 0.57 s | 249 MiB | 185 MB | + +Validation is a function of what the source declares, so the fleet form +validates the 12 800-satellite constellation in **0.57 s and 185 MB** where +the single-definition form takes 301 s and 20.1 GB. That is the whole +payoff of writing the model this way, and it is available today. + +## What the runtime does with 12 800 occurrences today + +Declaring the fleet does not make the satellites free; it moves their cost +from the source to the runtime, which pays it when something asks for the +occurrences. Today the runtime materializes an object per occurrence with a +value slot per feature — the same objects the single-definition form would +create — and shares only the *shape* of the type (its effective feature list) +between them. Measured on the same machine, same layouts as above: + +| satellites | operation | wall | allocated | peak RSS | +| ---------- | --------- | ---- | --------- | -------- | +| 1 600 | `-instantiate` the network | 0.42 s | 219 MiB | 169 MB | +| 1 600 | `-satisfy`, 324 assertions | 0.91 s | 508 MiB | 269 MB | +| 12 800 | `-instantiate` the network | 2.55 s | 1.0 GiB | 650 MB | +| 12 800 | `-satisfy`, 2 412 assertions | 22.6 s | 14.4 GiB | 1.34 GB | +| 12 800 | `%eval` of `sats.dryMass` in every plane | 252 s | 73.8 GiB | 4.9 GB | + +What the rows say about the current runtime: + +- **Instantiating** the network (`sysml -instantiate + SatelliteNetwork::Constellation::network`) creates the object per + occurrence in every plane, 2.55 s and 650 MB — about 50 KB per + occurrence, linear from 1 600 to 12 800. The run then warns that + materialization is bounded: the walk that reads the created object's + feature values stops at the runtime's materialization budget, so the + component trees beneath the occurrences are unread, not checked clean. +- **Checking** an assertion on a unit — `satisfy blockAMass by + network.plane0.unit16` — reads the unit through the network object and + evaluates its summed mass and power, which materializes the unit's + subsystems and components and starts their behaviors. Every check then + drains the behaviors the network's objects run, so a check costs more the + more of the fleet earlier checks have touched: 0.9 MiB allocated per + assertion in a network of one plane of 400, 6 MiB in one of 32 planes. A + CPU profile of the 16-plane check spends 57% evaluating the requirements' + expressions (41% of the total in starting the behaviors of the parts that + evaluation materializes) and 31% polling running state machines for due + events. The 2 412 assertions of the 12 800-satellite fleet cost 22.6 s and + 14.4 GiB allocated, against 83 s and 28.9 GiB for the 9 600 assertions of + a 3 200-satellite single-definition constellation; each assertion still + pays for the fleet around it. +- **Reading a value over every occurrence** — the dry mass of all 12 800 + satellites — evaluates the summed expression over the full component tree + of every occurrence, 252 s and 73.8 GiB allocated. This is the cost the + single-definition form paid at validation; the fleet form pays it at the + first read instead. +- A `satisfy` whose subject is the fleet itself (`satisfy blockAMass by + plane0.sats`) is rejected: the subject must denote one object. Assertions + are therefore made on the block's configuration — one check for every + occurrence that inherits the block's values — and on each diverging unit. +- A collection whose lower bound exceeds 1 000 is not materialized: a plane + written `Spacecraft[1600]` validates but its assertions report + `multiplicity violation: lower bound too large or infinite` when checked. + Keep a fleet under that bound per usage — 32 planes of 400 rather than 8 + of 1 600 — until the runtime holds occurrences sparsely. + +What would make these cheap is described in +[scaling to very large models](../project/large-model-scaling-design.md), +one definition, many occurrences: an occurrence whose feature holds its +block's default storing nothing for it, and a check over N occurrences that +read only block-level values evaluating once. Until that lands, model the +fleet as this chapter shows — the declared model is two hundred times +smaller and validates in under a second — and expect instantiation and +checking to cost what they cost for the same number of fully written +satellites. diff --git a/docs/internals/performance.md b/docs/internals/performance.md index c863234e2b..fbcbb19e9f 100644 --- a/docs/internals/performance.md +++ b/docs/internals/performance.md @@ -176,6 +176,28 @@ which report nothing: Both time and memory grow linearly with the model. Loading was quadratic once — doubling the model roughly quadrupled the time — for the reasons below. +Because the cost is per declared element, the largest lever a model has is to +declare less: one definition with a multiplicity rather than a definition per +unit. The satellite-network generator writes its constellation both ways +(`cmd/stress-model -fleet`), and on the machine named above — 8 CPUs, 31 GiB, +no swap — `sysml -validate -memstats` of the 12 800-satellite constellation +costs: + +| form | elements | source | wall | allocated | peak RSS | +| ---- | -------- | ------ | ---- | --------- | -------- | +| one `part def` per satellite, 32 planes of 400 | 2 354 827 | 145 MB | 301 s | 43.5 GiB | 20.1 GB | +| four blocks, `part sats : Block[400]` in 32 planes | 11 667 | 716 KB | 0.57 s | 249 MiB | 185 MB | + +The runtime then pays for the occurrences when something asks for them: the +same network instantiates in 2.55 s and 650 MB, its 2 412 `satisfy` +assertions check in 22.6 s and 14.4 GiB allocated, and reading one summed +attribute over every occurrence costs 252 s and 73.8 GiB, because each +occurrence is still an object with a value slot per feature whose component +tree is materialized to evaluate it. Both forms, their element counts and +what the runtime does with 12 800 occurrences are in the +[stress-test record](../project/satellite-network-stress-test.md) and the +guide chapter on [modeling fleets](../guide/modeling-fleets.md). + ### What made it quadratic The load path had several costs, including three scans over a namespace's diff --git a/docs/project/satellite-network-stress-test.md b/docs/project/satellite-network-stress-test.md index 66ef84232f..f9708f6dbf 100644 --- a/docs/project/satellite-network-stress-test.md +++ b/docs/project/satellite-network-stress-test.md @@ -173,6 +173,111 @@ That is under 0.1 ms per assertion warm, against 3.2 ms cold: the first check pays for building the runtime's view of every type, and a session that keeps the model loaded — the REPL, the gRPC service — amortizes it. +## The same constellation as a fleet + +Everything above declares a `part def` per satellite. The generator's +`-fleet` form states the same constellation the way a fleet is engineered +— a few spacecraft blocks carrying the as-built values as defaults, each +orbital plane as `part sats : Block[N] ordered`, as-built values only on the +units that diverge from their block (every sixteenth), the ring link as one +connector over the collection, one inter-plane link per adjacent pair of +planes and one downlink per plane and station, and the three requirements +declared once per block and asserted on the block's configuration and on +every diverging unit. `-stats` reports both forms alike; the two new fields +are the spacecraft definitions and the units that state values of their own. +The guide chapter [modeling fleets](../guide/modeling-fleets.md) shows the +source of both forms. + +```bash +go run ./cmd/stress-model -planes 32 -satellites 400 -ground-stations 20 -stats > legacy.sysml +# satellites=12800 definitions=12800 units=12800 ground-stations=20 components=256080 connections=204400 requirements=38400 elements=2354827 bytes=145364954 +go run ./cmd/stress-model -planes 32 -satellites 400 -ground-stations 20 -fleet -stats > fleet.sysml +# satellites=12800 definitions=4 units=800 ground-stations=20 components=960 connections=724 requirements=12 elements=11667 bytes=716125 +``` + +| satellites | planes × per plane | form | definitions | units | elements | source | `-validate` wall | allocated | peak RSS | +| ---------- | ------------------ | ---- | ----------- | ----- | -------- | ------ | ---------------- | --------- | -------- | +| 1 600 | 8 × 200 | one definition per satellite | 1 600 | 1 600 | 294 627 | 18.1 MB | 17.5 s | 5.5 GiB | 2.6 GB | +| 1 600 | 8 × 200 | fleet | 4 | 104 | 3 099 | 184 KB | 0.16 s | 92 MiB | 106 MB | +| 12 800 | 32 × 400 | one definition per satellite | 12 800 | 12 800 | 2 354 827 | 145 MB | 301 s | 43.5 GiB | 20.1 GB | +| 12 800 | 32 × 400 | fleet | 4 | 800 | 11 667 | 716 KB | 0.57 s | 249 MiB | 185 MB | + +The single-definition rows here are the plane and station layout the fleet +uses, so the two forms declare the same links; the validation table above +(299 137 and 2 392 417 elements, 19.0 s and 318 s) was taken over a layout +with a different split into planes and stations, and so slightly more links +and station components. The fleet form +declares **200 times fewer elements** at 12 800 satellites and validates in +0.57 s and 185 MB rather than 301 s and 20.1 GB: validation is a function of +what the source declares, and the fleet source is the size of four +spacecraft, twenty stations and the links between thirty-two planes. + +What the current runtime does with the 12 800 occurrences, on the same +machine: + +| satellites | operation | wall | allocated | peak RSS | +| ---------- | --------- | ---- | --------- | -------- | +| 1 600 | `-instantiate` the network | 0.42 s | 219 MiB | 169 MB | +| 1 600 | `-satisfy`, 324 assertions | 0.91 s | 508 MiB | 269 MB | +| 12 800 | `-instantiate` the network | 2.55 s | 1.0 GiB | 650 MB | +| 12 800 | `-satisfy`, 2 412 assertions | 22.6 s | 14.4 GiB | 1.34 GB | +| 12 800 | `%eval` of `plane.sats.dryMass`, all 32 planes | 252 s | 73.8 GiB | 4.9 GB | + +The runtime shares one shape — the effective feature list `FeaturesOf` +caches per type — between the occurrences of a block, and nothing else: each +occurrence is an object with a value slot per feature, materialized lazily. +Instantiating the network is therefore linear and cheap (about 50 KB per +occurrence; the walk of the created object's feature values stops at the +materialization budget and says so). Checking is not: a `satisfy` on a unit +reads the unit through the network object, evaluates its summed mass and +power — materializing its subsystems and components and starting their +behaviors — and then drains the behaviors every object of the network runs, +so each check costs more the more of the fleet earlier checks have touched +(0.9 MiB allocated per assertion in a network of one plane of 400, 6 MiB in +one of 32 planes). A CPU profile of the 16-plane `-satisfy` spends 57% of +its samples evaluating the requirements' expressions, 41% of the total under +`startClassifierBehaviors` for the parts that evaluation materializes, and +31% in `ObjectBehavior.hasPendingWork` / `StateExecutor.hasDueEvent` +polling the running mode machines. Reading one summed attribute over every +occurrence evaluates it over the full tree of each — the cost the +single-definition form paid at validation, paid here at the first read. + +Two limits of the current runtime shape the fleet form: + +- A `satisfy` whose subject is a collection (`satisfy blockAMass by + plane0.sats`) is rejected — the subject must denote one object — so the + fleet asserts each requirement on the block's configuration, which stands + for every occurrence inheriting the block's values, and on each diverging + unit. +- A collection whose lower bound exceeds 1 000 (`maxMaterializedLowerBound`) + is not materialized: a plane of `Spacecraft[1600]` validates, but checking + a unit of it reports `multiplicity violation: lower bound too large or + infinite`. The 12 800-satellite fleet is therefore 32 planes of 400. + +`BenchmarkFleetInstantiate` and `BenchmarkFleetSatisfy` in +`internal/stressmodel` measure, warm, instantiating the fleet network and +reading `sats.dryMass` over four planes, and re-checking every assertion: + +```bash +go test ./internal/stressmodel -run '^$' -bench Fleet -benchmem -benchtime 3x +``` + +| satellites | elements | instantiate + read four planes | per satellite | allocated | assertions | warm re-check | allocated | +| ---------- | -------- | ------------------------------ | ------------- | --------- | ---------- | ------------- | --------- | +| 32 | 1 175 | 64 ms | 2.0 ms | 19.2 MiB | 24 | 0.9 ms | 0.5 MiB | +| 128 | 1 707 | 234 ms | 1.8 ms | 78.9 MiB | 36 | 1.3 ms | 1.1 MiB | +| 512 | 3 915 | 1.33 s | 2.6 ms | 563 MiB | 108 | 7.1 ms | 7.4 MiB | + +Warm, instantiating a fleet and reading a summed attribute over its +occurrences costs **about 2 ms and 1 MiB per satellite** — the per-satellite +cost of a cold `-satisfy` over the single-definition form — because every +occurrence's component tree is still materialized to evaluate the sum. What +would change that is sparse per-occurrence values and verification over +distinct shapes ([scaling to very large models](large-model-scaling-design.md), +one definition, many occurrences): an occurrence whose feature holds its +block's default storing nothing for it, and a check over N occurrences that +read only block-level values evaluating once. + ## Editing: what an editor pays per keystroke An editor does not validate once; it re-validates the open file after every @@ -281,9 +386,12 @@ the interactive band at every operation measured. things: the CLI submits files one at a time and reindexes after each, which is quadratic in the file count (`docs/internals/performance.md`, notes for further work), and an editor pays the per-file analysis once per open file. -- `-satisfy` instantiates each satellite's tree on its own; it does not - instantiate the whole `Network` as one object with 12 800 satellites and - their links, and no figure here says what that would cost. +- `-satisfy` over the single-definition form instantiates each satellite's + tree on its own; it does not instantiate the whole `Network` as one object + with 12 800 satellites and their links. Only the fleet section + instantiates the network whole, and its occurrences are lazily materialized + objects whose component trees are read only where a check or an + evaluation reaches them. - Runtime execution is a mode machine driven to its initial state per instantiation, not a long simulation with events. Event throughput is measured separately in `docs/project/execution-performance-2026-09.md`. diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md index 874b447d20..dba54e00dc 100644 --- a/docs/project/spec-compliance.md +++ b/docs/project/spec-compliance.md @@ -133,7 +133,7 @@ what cannot be checked by anything is in - Golden traces: 235 golden execution traces under the default schedule (state×86, action×74, calc×32, clock×6, extent×6, constraint×4, string×4, three each of accept and analysis, two each of exhibited, f63 and verification, and one each of assign, f62, function, meta, object, occurrence, performed, send, two, w6e and w7d), and 48 more `.trace.golden` files pinning a case under a named policy, `.declared` or `.seed-` — entry/do/exit ordering of inline action bodies and a do body run to its end inside one round, the standard loop `until` with `then done`, a decision's guarded and `else` branches, a named flow carrying a value between action nodes, an accept with a `when` trigger, an accept subsetting an event, a send invocation through a port, a transition accepting through a port, loop and conditional bodies, one calc usage body run feeding several output reads, a usage whose outputs are read either side of an assignment to what its input named, a usage nested in a calc read for two of its outputs, calc statement bodies and their loop iterations, fork/join branch ordering, region entry/exit ordering, do behavior interleaving across orthogonal regions, send/accept, an accept parked until its message arrives, a payload read by a node declared before the accept that binds it, calc and constraint evaluation, library function invocation, the dotted-target transition, control-node and merge-body traces, and the merge loops re-entered on every pass) - Negative parser tests: 252 negative parser subtests (first-level subtests of `TestNegative`; 396 across the `TestNegative*` functions, 60 of them KerML, and 454 across every `*Negative*` parser test) - gRPC: 21 gRPC conformance cases and 8 gRPC robustness cases (`internal/grpc/testdata/conformance/`, `internal/grpc/robustness_test.go`) -- Test functions: 8,369 top-level `Test` functions across the module (`go test -count=1 ./...` runs them all, with the OMG corpora downloaded, `OPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 OPENSYSML_REQUIRE_SMT=1` and z3 installed). The figures on this list are generated by `make docs-counts` from the tree and gated; the test and subtest total of a run is not, since it moves with every fixture and only a run can state it. A test skips only where it says why: TestHeldImageRoundTrip declines a conformance case that creates no instance, so there is no held image to round-trip. Three skip themselves: TestSubsettingTargetIsTheInheritedFeature and TestRequirementEvaluation_SubjectNotFound against a limitation they record, and TestHelperSolverProcess, which is a solver child process the parent invokes. The others skip for want of something the run did not provide, and each names it: the `weasyprint`, `pandoc` and `prince` subtests of TestRenderWithInstalledEngines and TestRenderInlineRunsWithInstalledEngines and TestRenderDiagramsWithInstalledMermaid want the PDF and Mermaid toolchain, TestExtractionMatchesBaseline and TestUpdateIsIdempotentAcrossDays the pinned pilot validator jar, TestEmitSuite, TestRefereeRowsAreWellFormed, TestSuiteRead and TestSuiteClassification the downloaded PSSM test suite, TestCRealNotationIsLocaleIndependent a non-C locale, TestRenderDocumentsRejectsCaseAliasedTargets a case-insensitive filesystem, and TestFlexoInterop and TestFlexoInteropApply a live Flexo stack. +- Test functions: 8,371 top-level `Test` functions across the module (`go test -count=1 ./...` runs them all, with the OMG corpora downloaded, `OPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 OPENSYSML_REQUIRE_SMT=1` and z3 installed). The figures on this list are generated by `make docs-counts` from the tree and gated; the test and subtest total of a run is not, since it moves with every fixture and only a run can state it. A test skips only where it says why: TestHeldImageRoundTrip declines a conformance case that creates no instance, so there is no held image to round-trip. Three skip themselves: TestSubsettingTargetIsTheInheritedFeature and TestRequirementEvaluation_SubjectNotFound against a limitation they record, and TestHelperSolverProcess, which is a solver child process the parent invokes. The others skip for want of something the run did not provide, and each names it: the `weasyprint`, `pandoc` and `prince` subtests of TestRenderWithInstalledEngines and TestRenderInlineRunsWithInstalledEngines and TestRenderDiagramsWithInstalledMermaid want the PDF and Mermaid toolchain, TestExtractionMatchesBaseline and TestUpdateIsIdempotentAcrossDays the pinned pilot validator jar, TestEmitSuite, TestRefereeRowsAreWellFormed, TestSuiteRead and TestSuiteClassification the downloaded PSSM test suite, TestCRealNotationIsLocaleIndependent a non-C locale, TestRenderDocumentsRejectsCaseAliasedTargets a case-insensitive filesystem, and TestFlexoInterop and TestFlexoInteropApply a live Flexo stack. --- diff --git a/internal/stressmodel/bench_test.go b/internal/stressmodel/bench_test.go index 44dacd05e5..40b57a7836 100644 --- a/internal/stressmodel/bench_test.go +++ b/internal/stressmodel/bench_test.go @@ -89,6 +89,75 @@ func BenchmarkSatisfy(b *testing.B) { } } +func fleet(satellitesPerPlane int) SatelliteNetwork { + n := network(satellitesPerPlane) + n.Fleet = true + return n +} + +const fleetNetwork = "SatelliteNetwork::Constellation::network" + +// BenchmarkFleetInstantiate measures creating the fleet-form network and reading +// the dry mass of every occurrence in every plane: what it costs to materialize +// N spacecraft declared as `Spacecraft[N]` and evaluate a summed attribute over +// each one's component tree. +func BenchmarkFleetInstantiate(b *testing.B) { + for _, n := range networkSizes { + src, stats := fleet(n).Source() + b.Run(fmt.Sprintf("satellites=%d/elements=%d", stats.Satellites, stats.Elements), func(b *testing.B) { + sess := loadNetwork(b, src) + read := func() { + if _, err := sess.InstantiateNamed(fleetNetwork); err != nil { + b.Fatal(err) + } + for p := 0; p < 4; p++ { + if _, err := sess.EvalExpr(fmt.Sprintf("%s.plane%d.sats.dryMass", fleetNetwork, p)); err != nil { + b.Fatal(err) + } + } + } + read() + b.ReportAllocs() + b.ResetTimer() + for i := 0; i < b.N; i++ { + read() + } + b.StopTimer() + b.ReportMetric(float64(b.Elapsed().Nanoseconds())/float64(b.N)/float64(stats.Satellites), "ns/satellite") + }) + } +} + +// BenchmarkFleetSatisfy measures the warm re-check of every satisfy assertion of +// a fleet-form network: three per block and three per unit stating values of its +// own, each unit checked as one occurrence of its plane's fleet. +func BenchmarkFleetSatisfy(b *testing.B) { + for _, n := range networkSizes { + src, stats := fleet(n).Source() + assertions := 3 * (stats.Definitions + stats.Units) + b.Run(fmt.Sprintf("satellites=%d/assertions=%d", stats.Satellites, assertions), func(b *testing.B) { + sess := loadNetwork(b, src) + check := func() { + verdicts := sess.CheckSatisfy("") + if len(verdicts) != assertions { + b.Fatalf("got %d verdicts, want %d", len(verdicts), assertions) + } + for _, v := range verdicts { + if !v.Holds() { + b.Fatalf("%s: %v", v.Subject, v.Lines) + } + } + } + check() + b.ReportAllocs() + b.ResetTimer() + for i := 0; i < b.N; i++ { + check() + } + }) + } +} + // BenchmarkEditBeside measures what an editor pays per keystroke in a small file // open beside a network: reparse of the small file, reindex, and diagnostics. func BenchmarkEditBeside(b *testing.B) { diff --git a/internal/stressmodel/satnet.go b/internal/stressmodel/satnet.go index dad0df147f..dd91d72655 100644 --- a/internal/stressmodel/satnet.go +++ b/internal/stressmodel/satnet.go @@ -8,6 +8,9 @@ // power budget, the requirements it satisfies and the mode machine it exhibits. // Satellites are cross-linked to their neighbours in the same orbital plane and // in the adjacent plane, and every satellite has a downlink to a ground station. +// +// The network is written either as a `part def` per satellite or, in the fleet +// form, as `part sats : Block[N]` over a few blocks whose as-built values are defaults. package stressmodel import ( @@ -22,12 +25,32 @@ type SatelliteNetwork struct { Planes, Satellites int // GroundStations is the number of ground stations the constellation downlinks to. GroundStations int + // Fleet declares each plane as occurrences of one spacecraft block rather + // than one definition per satellite; see the package documentation. + Fleet bool } +// fleetBlocks is how many spacecraft blocks the fleet form declares; plane p is +// built from block p mod fleetBlocks. +const fleetBlocks = 4 + +// fleetUnitStride is how many satellites of a plane share their block's +// defaults for each one the fleet form declares as-built values for. +const fleetUnitStride = 16 + // Stats counts what a generated network declares. type Stats struct { + // Satellites is the number of spacecraft in the constellation, whichever + // form declares them; GroundStations the number of ground stations. Satellites, GroundStations int - // Components is the number of leaf components across every satellite and station. + // Definitions is the number of spacecraft definitions declared: one per + // satellite in the single-definition form, one per block in the fleet form. + Definitions int + // Units is the number of satellites stating as-built values of their own: + // every satellite in the single-definition form, the diverging units in the fleet form. + Units int + // Components is the number of leaf components declared across the spacecraft + // definitions, the diverging units and the stations. Components int // Connections is the number of interface usages, inside satellites and between them. Connections int @@ -71,7 +94,11 @@ func (n SatelliteNetwork) Generate(w io.Writer) (Stats, error) { var b strings.Builder g := &generator{b: &b} g.library() - g.constellation(n) + if n.Fleet { + g.fleet(n) + } else { + g.constellation(n) + } g.stats.Bytes = b.Len() _, err := io.WriteString(w, b.String()) return g.stats, err @@ -404,10 +431,22 @@ func (g *generator) link(kind string, a, b int) { // satellite writes one fully configured spacecraft definition and its requirements. func (g *generator) satellite(id, plane, slot int) { g.stats.Satellites++ + g.stats.Units++ g.decl(2, "part def Sat%d :> Spacecraft {", id) g.decl(3, "attribute :>> catalogId = %d;", 40000+id) g.decl(3, "attribute :>> plane = %d;", plane) g.decl(3, "attribute :>> slot = %d;", slot) + g.spacecraftBody(id, "") + g.line(2, "}") + g.decl(2, "part sat%dConfig : Sat%d;", id, id) + g.requirements(fmt.Sprintf("sat%d", id), fmt.Sprintf("sat%dConfig", id), id) + g.line(0, "") +} + +// spacecraftBody writes the subsystems, budgets and connections of spacecraft id; +// valued (`=` or `default =`) writes the values a unit may state its own for. +func (g *generator) spacecraftBody(id int, valued string) { + g.stats.Definitions++ var massTerms, powerTerms []string for _, s := range subsystems { massTerms = append(massTerms, s.name+".mass") @@ -419,9 +458,9 @@ func (g *generator) satellite(id, plane, slot int) { subMass = append(subMass, c.name+".mass") subPower = append(subPower, c.name+".powerDraw") g.decl(4, "part :>> %s {", c.name) - g.decl(5, "attribute :>> mass = %d.%d [kg];", 2+(id+j)%40, (id*3+j)%10) - g.decl(5, "attribute :>> powerDraw = %d.0 [W];", 5+(id*5+j*7)%50) - g.decl(5, "attribute :>> serialNumber = \"%s-%05d-%d\";", strings.ToUpper(c.name), id, j) + g.decl(5, "attribute :>> mass %s= %d.%d [kg];", valued, 2+(id+j)%40, (id*3+j)%10) + g.decl(5, "attribute :>> powerDraw %s= %d.0 [W];", valued, 5+(id*5+j*7)%50) + g.decl(5, "attribute :>> serialNumber %s= \"%s-%05d-%d\";", valued, strings.ToUpper(c.name), id, j) g.componentDetail(c.def, id, j) g.line(4, "}") } @@ -451,19 +490,136 @@ func (g *generator) satellite(id, plane, slot int) { g.stats.Connections++ g.decl(3, "interface payloadToCdh : DataFeed connect payload.dataOut to cdh.dataIn;") g.decl(3, "constraint massMargin { dryMass <= %d [kg] }", 500+id%100) - g.line(2, "}") - g.decl(2, "part sat%dConfig : Sat%d;", id, id) +} + +// requirements writes the three requirements of the spacecraft configuration +// named config, with their satisfy assertions, under names prefixed by name. +func (g *generator) requirements(name, config string, id int) { g.stats.Requirements += 3 - g.decl(2, "requirement sat%dMass : MassBudget { subject :>> sc = sat%dConfig; attribute :>> limit = %d [kg]; }", id, id, 900+id%100) + g.decl(2, "requirement %sMass : MassBudget { subject :>> sc = %s; attribute :>> limit = %d [kg]; }", name, config, 900+id%100) g.stats.Elements += 2 - g.decl(2, "satisfy sat%dMass by sat%dConfig;", id, id) - g.decl(2, "requirement sat%dPower : PowerBudget { subject :>> sc = sat%dConfig; }", id, id) + g.decl(2, "satisfy %sMass by %s;", name, config) + g.decl(2, "requirement %sPower : PowerBudget { subject :>> sc = %s; }", name, config) g.stats.Elements++ - g.decl(2, "satisfy sat%dPower by sat%dConfig;", id, id) - g.decl(2, "requirement sat%dCrosslink : CrosslinkCapacity { subject :>> sc = sat%dConfig; attribute :>> minimumRate = %d.0; }", id, id, 50+id%50) + g.decl(2, "satisfy %sPower by %s;", name, config) + g.decl(2, "requirement %sCrosslink : CrosslinkCapacity { subject :>> sc = %s; attribute :>> minimumRate = %d.0; }", name, config, 50+id%50) g.stats.Elements += 2 - g.decl(2, "satisfy sat%dCrosslink by sat%dConfig;", id, id) + g.decl(2, "satisfy %sCrosslink by %s;", name, config) +} + +// fleet writes the constellation as a few spacecraft blocks, each plane as +// occurrences of one of them, the ground stations and the links between them. +func (g *generator) fleet(n SatelliteNetwork) { + g.decl(1, "package Constellation {") + g.line(2, "private import Interfaces::*;") + g.line(2, "private import Platform::*;") + g.line(2, "private import Requirements::*;") + g.line(2, "private import Behavior::*;") + blocks := min(fleetBlocks, n.Planes) + for b := 0; b < blocks; b++ { + g.block(b) + } + for k := 0; k < n.GroundStations; k++ { + g.groundStation(k) + } + g.decl(2, "part def OrbitalPlane {") + g.decl(3, "attribute plane : Integer;") + g.decl(3, "part sats : Spacecraft[%d] ordered;", n.Satellites) + if n.Satellites > 1 { + g.stats.Connections++ + g.decl(3, "interface ring : RFLink connect sats.comms.crosslinkTx to sats.comms.crosslinkRx {") + g.decl(4, "attribute :>> dataRate = 100.0;") + g.decl(4, "attribute :>> slantRange = 2000 [km];") + g.line(3, "}") + } + g.decl(3, "attribute satelliteCount : Integer = %d;", n.Satellites) + g.line(2, "}") g.line(0, "") + g.decl(2, "part def Network {") + for p := 0; p < n.Planes; p++ { + g.plane(n, p, p%blocks) + } + for k := 0; k < n.GroundStations; k++ { + g.decl(3, "part gs%d : Station%d;", k, k) + } + for p := 0; p+1 < n.Planes; p++ { + g.stats.Connections++ + g.decl(3, "interface plane%dTo%d : RFLink connect plane%d.sats.comms.crosslinkTx to plane%d.sats.comms.crosslinkRx {", p, p+1, p, p+1) + g.decl(4, "attribute :>> dataRate = %d.0;", 100+(2*p+1)%400) + g.decl(4, "attribute :>> slantRange = %d [km];", 2000+(p*10+3)%3000) + g.line(3, "}") + } + for p := 0; p < n.Planes; p++ { + for k := 0; k < n.GroundStations; k++ { + g.stats.Connections++ + g.decl(3, "interface downlink%dTo%d : RFLink connect plane%d.sats.comms.rf to gs%d.uplink {", k, p, p, k) + g.decl(4, "attribute :>> dataRate = %d.0;", 50+p%200) + g.decl(4, "attribute :>> slantRange = %d [km];", 900+p%1500) + g.line(3, "}") + } + } + g.decl(3, "attribute satelliteCount : Integer = %d;", n.Planes*n.Satellites) + g.line(2, "}") + g.decl(2, "part network : Network;") + g.line(0, "") + for b := 0; b < blocks; b++ { + g.decl(2, "part block%sConfig : Block%s;", blockName(b), blockName(b)) + g.requirements("block"+blockName(b), "block"+blockName(b)+"Config", b) + } + for p := 0; p < n.Planes; p++ { + for s := 0; s < n.Satellites; s += fleetUnitStride { + for _, req := range []string{"Mass", "Power", "Crosslink"} { + g.decl(2, "satisfy block%s%s by network.plane%d.unit%d;", blockName(p%blocks), req, p, s) + } + } + } + g.line(1, "}") + g.line(0, "}") +} + +// block writes one spacecraft block: a definition whose as-built values are +// defaults, so a unit built from it states only the values it diverges in. +func (g *generator) block(b int) { + g.decl(2, "part def Block%s :> Spacecraft {", blockName(b)) + g.decl(3, "attribute :>> catalogId default = %d;", 40000+b*10000) + g.decl(3, "attribute :>> slot default = 0;") + g.spacecraftBody(b, "default ") + g.line(2, "}") + g.line(0, "") +} + +// plane writes orbital plane p as occurrences of block b, the units diverging +// from the block stating their catalog identity, slot and as-built terminal. +func (g *generator) plane(n SatelliteNetwork, p, b int) { + g.decl(3, "part plane%d : OrbitalPlane {", p) + g.decl(4, "attribute :>> plane = %d;", p) + g.decl(4, "part :>> sats : Block%s { attribute :>> plane = %d; }", blockName(b), p) + g.stats.Elements++ + for s := 0; s < n.Satellites; s++ { + g.stats.Satellites++ + if s%fleetUnitStride != 0 { + continue + } + id := p*n.Satellites + s + g.stats.Units++ + g.stats.Components++ + g.decl(4, "part unit%d :> sats {", s) + g.decl(5, "attribute :>> catalogId = %d;", 40000+id) + g.decl(5, "attribute :>> slot = %d;", s) + g.decl(5, "part :>> comms {") + g.decl(6, "part :>> crosslinkTerminal {") + g.decl(7, "attribute :>> mass = %d.%d [kg];", 2+(id+1)%40, (id*3+1)%10) + g.decl(7, "attribute :>> serialNumber = \"CROSSLINKTERMINAL-%05d-1\";", id) + g.line(6, "}") + g.line(5, "}") + g.line(4, "}") + } + g.line(3, "}") +} + +// blockName letters the spacecraft blocks A, B, C, ... +func blockName(b int) string { + return string(rune('A' + b)) } // componentDetail writes the as-built values of the attributes a component kind adds. diff --git a/internal/stressmodel/satnet_test.go b/internal/stressmodel/satnet_test.go index c6e39bb86f..12555098ca 100644 --- a/internal/stressmodel/satnet_test.go +++ b/internal/stressmodel/satnet_test.go @@ -59,3 +59,83 @@ func TestSatelliteNetworkScales(t *testing.T) { t.Errorf("first satellite definition missing from:\n%s", one) } } + +// TestFleetValidates keeps the fleet form in step with the grammar and the +// runtime: a constellation of a few blocks with occurrence counts loads under +// strict conformance without a diagnostic, its satisfy assertions hold, and the +// occurrences read the block's defaults where a unit states nothing of its own. +func TestFleetValidates(t *testing.T) { + n := SatelliteNetwork{Planes: 2, Satellites: 2 * fleetUnitStride, GroundStations: 1, Fleet: true} + src, stats := n.Source() + if stats.Satellites != 4*fleetUnitStride || stats.GroundStations != 1 { + t.Fatalf("stats = %+v, want %d satellites and 1 station", stats, 4*fleetUnitStride) + } + if stats.Definitions != 2 || stats.Units != 4 { + t.Errorf("stats = %+v, want 2 blocks and 4 diverging units", stats) + } + if stats.Requirements != 3*stats.Definitions { + t.Errorf("Requirements = %d, want three per block", stats.Requirements) + } + if stats.Bytes != len(src) { + t.Errorf("Bytes = %d, want %d", stats.Bytes, len(src)) + } + + s := repl.NewSession() + s.SetConformanceMode(conformance.ModeOf(true)) + for _, d := range s.Submit(src).Diagnostics { + t.Errorf("diagnostic: %s", d.Message) + } + verdicts := s.CheckSatisfy("") + if want := 3 * (stats.Definitions + stats.Units); len(verdicts) != want { + t.Fatalf("got %d satisfy verdicts, want %d", len(verdicts), want) + } + for _, v := range verdicts { + if !v.Holds() { + t.Errorf("%s: %v", v.Subject, v.Lines) + } + } + + const network = "SatelliteNetwork::Constellation::network" + for expr, want := range map[string]string{ + network + ".plane1.sats#(1).catalogId": "= 40032", + network + ".plane1.sats#(2).slot": "= 16", + network + ".plane1.sats#(3).catalogId": "= 50000", + network + ".plane1.unit0.catalogId": "= 40032", + network + ".plane1.unit16.comms.crosslinkTerminal.serialNumber": `= "CROSSLINKTERMINAL-00048-1"`, + network + ".plane0.sats#(3).plane": "= 0", + network + ".satelliteCount": "= 64", + } { + lines, err := s.EvalExpr(expr) + if err != nil { + t.Errorf("%s: %v", expr, err) + continue + } + if got := strings.TrimSpace(lines[len(lines)-1]); got != want { + t.Errorf("%s = %q, want %q", expr, got, want) + } + } +} + +// TestFleetScales checks the fleet form declares the blocks, the planes and the +// links but not the satellites: the element count grows with the planes and the +// diverging units, not with the occurrences. +func TestFleetScales(t *testing.T) { + _, small := SatelliteNetwork{Planes: 2, Satellites: fleetUnitStride, GroundStations: 1, Fleet: true}.Source() + _, wide := SatelliteNetwork{Planes: 2, Satellites: 2 * fleetUnitStride, GroundStations: 1, Fleet: true}.Source() + _, wider := SatelliteNetwork{Planes: 2, Satellites: 8 * fleetUnitStride, GroundStations: 1, Fleet: true}.Source() + _, tall := SatelliteNetwork{Planes: 4, Satellites: fleetUnitStride, GroundStations: 1, Fleet: true}.Source() + _, legacy := SatelliteNetwork{Planes: 2, Satellites: fleetUnitStride, GroundStations: 1}.Source() + if wider.Satellites != 8*small.Satellites || wider.Definitions != small.Definitions { + t.Errorf("more satellites per plane changed the blocks: %+v vs %+v", wider, small) + } + perUnit := wide.Elements - small.Elements + if wide.Units-small.Units != 2 || wider.Units != 8*small.Units || wider.Elements-small.Elements != (wider.Units-small.Units)*perUnit/2 { + t.Errorf("elements do not grow only with the diverging units: %+v, %+v vs %+v", wider, wide, small) + } + if tall.Definitions != 4 || tall.Connections <= small.Connections { + t.Errorf("more planes add no blocks or links: %+v vs %+v", tall, small) + } + if legacy.Satellites != small.Satellites || legacy.Elements <= 4*small.Elements { + t.Errorf("the fleet form is not much smaller than one definition per satellite: %+v vs %+v", small, legacy) + } +} diff --git a/mkdocs.yml b/mkdocs.yml index bf627cbfbc..32c007e798 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -167,6 +167,7 @@ nav: - guide/08-editors.md - guide/09-clients.md - guide/10-troubleshooting.md + - guide/modeling-fleets.md - Document generation: - manual/README.md - Introduction and concepts: manual/introduction.md From 1c49ec075c4325de402025c4e2b0998f2b55613c Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Tue, 15 Sep 2026 07:40:50 +0000 Subject: [PATCH 02/11] fix(stressmodel): let fleet units diverge in every as-built value and state link cardinality MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Block component details (array area, battery capacity, terminal data rate, …) are now defaults like the masses and serial numbers, so a diverging unit can redefine them; the crosslink terminal of every diverging unit states its data rate. The ring and inter-plane collection connectors declare [1] ends, and the guide, stress-test record and changelog say what a collection connector does and does not state about the per-pair topology. Fleet figures re-measured. Co-Authored-By: jason.han --- .../stress-model-fleet-mode.added.md | 7 +- docs/guide/modeling-fleets.md | 80 ++++++++++++------- docs/internals/performance.md | 6 +- docs/project/satellite-network-stress-test.md | 43 ++++++---- internal/stressmodel/satnet.go | 78 ++++++++++-------- internal/stressmodel/satnet_test.go | 13 +++ 6 files changed, 143 insertions(+), 84 deletions(-) diff --git a/changes/unreleased/stress-model-fleet-mode.added.md b/changes/unreleased/stress-model-fleet-mode.added.md index cf6f3b5b0f..7834417376 100644 --- a/changes/unreleased/stress-model-fleet-mode.added.md +++ b/changes/unreleased/stress-model-fleet-mode.added.md @@ -2,10 +2,11 @@ declares each orbital plane as occurrences of one of four spacecraft blocks — `part sats : BlockA[400] ordered` — with the as-built values as the block's defaults and stated only on the units that diverge, instead of one `part def` per satellite; the spacecraft, ground segment, - requirements, state machine, ring, inter-plane and downlink connectors are unchanged. `-stats` + requirements and state machine are unchanged, and the ring, inter-plane and downlink connectors + are declared once over each collection with `[1]` ends rather than once per satellite pair. `-stats` now reports the spacecraft definitions and the units carrying values of their own in both forms, - so the two can be compared: at 12 800 satellites the fleet declares 11 667 elements against - 2 354 827, and validates in 0.57 s and 185 MB rather than 301 s and 20.1 GB. A guide chapter, + so the two can be compared: at 12 800 satellites the fleet declares 12 467 elements against + 2 354 827, and validates in 0.57 s and 175 MB rather than 301 s and 20.1 GB. A guide chapter, `docs/guide/modeling-fleets.md`, shows the constellation both ways and what the runtime does with 12 800 occurrences, and the stress-test record and performance notes carry the measurements. `BenchmarkFleetInstantiate` and `BenchmarkFleetSatisfy` in `internal/stressmodel` diff --git a/docs/guide/modeling-fleets.md b/docs/guide/modeling-fleets.md index bb7f1e4049..3cfd033d2d 100644 --- a/docs/guide/modeling-fleets.md +++ b/docs/guide/modeling-fleets.md @@ -37,10 +37,19 @@ sysml> %eval network.plane1.sats#(3).catalogId sysml> %eval network.plane0.sats.dryMass // one value per occurrence ``` -A connector whose ends are collection paths connects the occurrences, so -`connect sats.comms.crosslinkTx to sats.comms.crosslinkRx` links the fleet's -crosslink ports, and `connect plane0.sats.comms.rf to gs0.uplink` gives every -satellite in a plane a downlink to one station. +A connector whose ends are collection paths connects the occurrences as a +whole, and an end multiplicity says how many of them each link joins: +`connect [1] sats.comms.crosslinkTx to [1] sats.comms.crosslinkRx` declares +links that each join one transmitter to one receiver over the fleet's ports, +and `connect plane0.sats.comms.rf to gs0.uplink` gives every satellite in a +plane a downlink to one station. What such a connector cannot say is *which* +occurrence pairs with which: a connector end is a feature chain, not an +expression, so `sats#(1).comms.crosslinkTx` is not an end, and the pairing a +per-unit model writes out — unit `i` to unit `i + 1`, unit `i` to the same +slot of the next plane — has no compact form. When the pairing matters, +name the occurrences it involves (`part unit0 :> sats`, below) and connect +those; the runtime realizes a collection connector as one link whose ends +hold the collections, not as a link per pair. ## Variants as specializations @@ -125,8 +134,14 @@ in both forms: `-fleet` selects the fleet form. Both state the same spacecraft — seven subsystems, twenty components with mass, power draw and serial number, the power and data connections between them, a mass and a power budget, three requirements with `satisfy` assertions, a mode machine -every spacecraft exhibits — the same ground stations, the same ring and -inter-plane crosslinks and the same downlinks. +every spacecraft exhibits — and the same ground stations. The links differ +in what they can state: the per-unit form writes every ring link (satellite +`i` to `i + 1`, closing the ring), every inter-plane link (slot `i` to slot +`i` of the next plane) and every downlink (satellite `i` to station `i mod +G`) as its own connector, and the fleet form declares one connector per +collection with `[1]` ends — each link joins one satellite to one satellite +or station, but the connector does not say which pairs, and the runtime +realizes it as one link over the collections. **One definition per satellite.** Every satellite is its own `part def` specializing `Spacecraft` and redefines the whole tree beneath it to state @@ -149,22 +164,25 @@ part def Sat1 :> Spacecraft { /* … */ } part def Network { part sat0 : Sat0; part sat1 : Sat1; - interface link0To1 : RFLink connect sat0.comms.crosslinkTx to sat1.comms.crosslinkRx; + interface ring0To1 : RFLink connect sat0.comms.crosslinkTx to sat1.comms.crosslinkRx; // … } ``` **Fleet.** Four spacecraft blocks carry the as-built values as defaults; each -orbital plane is `part sats : Block[N] ordered` with a ring link over the -collection; every sixteenth unit states a catalog number, a slot and a -crosslink terminal of its own; the requirements are declared once per block -and asserted on the block's configuration and on every diverging unit: +orbital plane is `part sats : Block[N] ordered` with one ring connector over +the collection, one connector between adjacent planes and one downlink +connector per plane and station, their ends declared `[1]` so that each link +joins one satellite to one satellite or station; every sixteenth unit states +a catalog number, a slot and a crosslink terminal of its own; the +requirements are declared once per block and asserted on the block's +configuration and on every diverging unit: ```sysml part def OrbitalPlane { attribute plane : Integer; part sats : Spacecraft[400] ordered; - interface ring : RFLink connect sats.comms.crosslinkTx to sats.comms.crosslinkRx; + interface ring : RFLink connect [1] sats.comms.crosslinkTx to [1] sats.comms.crosslinkRx; } part def Network { part plane0 : OrbitalPlane { @@ -173,7 +191,7 @@ part def Network { part unit16 :> sats { /* … */ } } // … - interface plane0To1 : RFLink connect plane0.sats.comms.crosslinkTx to plane1.sats.comms.crosslinkRx; + interface plane0To1 : RFLink connect [1] plane0.sats.comms.crosslinkTx to [1] plane1.sats.comms.crosslinkRx; interface downlink0To0 : RFLink connect plane0.sats.comms.rf to gs0.uplink; } satisfy blockAMass by blockAConfig; @@ -187,18 +205,18 @@ declarations the source makes: go run ./cmd/stress-model -planes 8 -satellites 200 -ground-stations 20 -stats > legacy.sysml # satellites=1600 definitions=1600 units=1600 ground-stations=20 components=32080 connections=25400 requirements=4800 elements=294627 bytes=18135413 go run ./cmd/stress-model -planes 8 -satellites 200 -ground-stations 20 -fleet -stats > fleet.sysml -# satellites=1600 definitions=4 units=104 ground-stations=20 components=264 connections=220 requirements=12 elements=3099 bytes=183994 +# satellites=1600 definitions=4 units=104 ground-stations=20 components=264 connections=220 requirements=12 elements=3203 bytes=191418 ``` | satellites | planes × per plane | form | definitions | units stating values | elements | source | | ---------- | ------------------ | ---- | ----------- | -------------------- | -------- | ------ | | 1 600 | 8 × 200 | one definition per satellite | 1 600 | 1 600 | 294 627 | 18.1 MB | -| 1 600 | 8 × 200 | fleet | 4 | 104 | 3 099 | 184 KB | +| 1 600 | 8 × 200 | fleet | 4 | 104 | 3 203 | 191 KB | | 12 800 | 32 × 400 | one definition per satellite | 12 800 | 12 800 | 2 354 827 | 145 MB | -| 12 800 | 32 × 400 | fleet | 4 | 800 | 11 667 | 716 KB | +| 12 800 | 32 × 400 | fleet | 4 | 800 | 12 467 | 766 KB | -The fleet form of the 12 800-satellite constellation is **11 667 declared -elements against 2 354 827** — a factor of 200 — and what remains grows with +The fleet form of the 12 800-satellite constellation is **12 467 declared +elements against 2 354 827** — a factor of 190 — and what remains grows with the number of planes (links, downlinks) and of diverging units, not with the number of satellites. (The [stress-test record](../project/satellite-network-stress-test.md)'s @@ -218,12 +236,12 @@ All figures below were taken on one machine — `Intel Xeon Platinum 8559C`, | satellites | form | elements | wall | allocated | peak RSS | | ---------- | ---- | -------- | ---- | --------- | -------- | | 1 600 | one definition per satellite | 294 627 | 17.5 s | 5.5 GiB | 2.6 GB | -| 1 600 | fleet, 8 × 200 | 3 099 | 0.16 s | 92 MiB | 106 MB | +| 1 600 | fleet, 8 × 200 | 3 203 | 0.17 s | 93 MiB | 106 MB | | 12 800 | one definition per satellite | 2 354 827 | 301 s | 43.5 GiB | 20.1 GB | -| 12 800 | fleet, 32 × 400 | 11 667 | 0.57 s | 249 MiB | 185 MB | +| 12 800 | fleet, 32 × 400 | 12 467 | 0.57 s | 254 MiB | 175 MB | Validation is a function of what the source declares, so the fleet form -validates the 12 800-satellite constellation in **0.57 s and 185 MB** where +validates the 12 800-satellite constellation in **0.57 s and 175 MB** where the single-definition form takes 301 s and 20.1 GB. That is the whole payoff of writing the model this way, and it is available today. @@ -238,17 +256,17 @@ between them. Measured on the same machine, same layouts as above: | satellites | operation | wall | allocated | peak RSS | | ---------- | --------- | ---- | --------- | -------- | -| 1 600 | `-instantiate` the network | 0.42 s | 219 MiB | 169 MB | -| 1 600 | `-satisfy`, 324 assertions | 0.91 s | 508 MiB | 269 MB | -| 12 800 | `-instantiate` the network | 2.55 s | 1.0 GiB | 650 MB | -| 12 800 | `-satisfy`, 2 412 assertions | 22.6 s | 14.4 GiB | 1.34 GB | +| 1 600 | `-instantiate` the network | 0.47 s | 220 MiB | 168 MB | +| 1 600 | `-satisfy`, 324 assertions | 0.95 s | 513 MiB | 269 MB | +| 12 800 | `-instantiate` the network | 2.34 s | 1.0 GiB | 692 MB | +| 12 800 | `-satisfy`, 2 412 assertions | 23.4 s | 14.4 GiB | 1.36 GB | | 12 800 | `%eval` of `sats.dryMass` in every plane | 252 s | 73.8 GiB | 4.9 GB | What the rows say about the current runtime: - **Instantiating** the network (`sysml -instantiate SatelliteNetwork::Constellation::network`) creates the object per - occurrence in every plane, 2.55 s and 650 MB — about 50 KB per + occurrence in every plane, 2.34 s and 692 MB — about 50 KB per occurrence, linear from 1 600 to 12 800. The run then warns that materialization is bounded: the walk that reads the created object's feature values stops at the runtime's materialization budget, so the @@ -263,7 +281,7 @@ What the rows say about the current runtime: CPU profile of the 16-plane check spends 57% evaluating the requirements' expressions (41% of the total in starting the behaviors of the parts that evaluation materializes) and 31% polling running state machines for due - events. The 2 412 assertions of the 12 800-satellite fleet cost 22.6 s and + events. The 2 412 assertions of the 12 800-satellite fleet cost 23.4 s and 14.4 GiB allocated, against 83 s and 28.9 GiB for the 9 600 assertions of a 3 200-satellite single-definition constellation; each assertion still pays for the fleet around it. @@ -272,6 +290,12 @@ What the rows say about the current runtime: of every occurrence, 252 s and 73.8 GiB allocated. This is the cost the single-definition form paid at validation; the fleet form pays it at the first read instead. +- A connector over the collection is realized as **one link whose ends hold + the collections** (`%eval network.plane0.ring.a` is the sequence of every + transmitter in the plane), whatever its end multiplicities declare. The + per-pair topology of the single-definition form — `ring0To1`, `ring1To2`, + …, `downlink5To0` — is not recovered from it; only what the connector + states about the collections as a whole is. - A `satisfy` whose subject is the fleet itself (`satisfy blockAMass by plane0.sats`) is rejected: the subject must denote one object. Assertions are therefore made on the block's configuration — one check for every @@ -287,7 +311,7 @@ What would make these cheap is described in one definition, many occurrences: an occurrence whose feature holds its block's default storing nothing for it, and a check over N occurrences that read only block-level values evaluating once. Until that lands, model the -fleet as this chapter shows — the declared model is two hundred times +fleet as this chapter shows — the declared model is nearly two hundred times smaller and validates in under a second — and expect instantiation and checking to cost what they cost for the same number of fully written satellites. diff --git a/docs/internals/performance.md b/docs/internals/performance.md index fbcbb19e9f..dd1ffb40fe 100644 --- a/docs/internals/performance.md +++ b/docs/internals/performance.md @@ -186,11 +186,11 @@ costs: | form | elements | source | wall | allocated | peak RSS | | ---- | -------- | ------ | ---- | --------- | -------- | | one `part def` per satellite, 32 planes of 400 | 2 354 827 | 145 MB | 301 s | 43.5 GiB | 20.1 GB | -| four blocks, `part sats : Block[400]` in 32 planes | 11 667 | 716 KB | 0.57 s | 249 MiB | 185 MB | +| four blocks, `part sats : Block[400]` in 32 planes | 12 467 | 766 KB | 0.57 s | 254 MiB | 175 MB | The runtime then pays for the occurrences when something asks for them: the -same network instantiates in 2.55 s and 650 MB, its 2 412 `satisfy` -assertions check in 22.6 s and 14.4 GiB allocated, and reading one summed +same network instantiates in 2.34 s and 692 MB, its 2 412 `satisfy` +assertions check in 23.4 s and 14.4 GiB allocated, and reading one summed attribute over every occurrence costs 252 s and 73.8 GiB, because each occurrence is still an object with a value slot per feature whose component tree is materialized to evaluate it. Both forms, their element counts and diff --git a/docs/project/satellite-network-stress-test.md b/docs/project/satellite-network-stress-test.md index f9708f6dbf..e9f53f959f 100644 --- a/docs/project/satellite-network-stress-test.md +++ b/docs/project/satellite-network-stress-test.md @@ -181,7 +181,9 @@ Everything above declares a `part def` per satellite. The generator's orbital plane as `part sats : Block[N] ordered`, as-built values only on the units that diverge from their block (every sixteenth), the ring link as one connector over the collection, one inter-plane link per adjacent pair of -planes and one downlink per plane and station, and the three requirements +planes and one downlink per plane and station — the collection connectors +with `[1]` ends, so each link joins one satellite to one satellite or +station, though not which to which — and the three requirements declared once per block and asserted on the block's configuration and on every diverging unit. `-stats` reports both forms alike; the two new fields are the spacecraft definitions and the units that state values of their own. @@ -192,23 +194,23 @@ source of both forms. go run ./cmd/stress-model -planes 32 -satellites 400 -ground-stations 20 -stats > legacy.sysml # satellites=12800 definitions=12800 units=12800 ground-stations=20 components=256080 connections=204400 requirements=38400 elements=2354827 bytes=145364954 go run ./cmd/stress-model -planes 32 -satellites 400 -ground-stations 20 -fleet -stats > fleet.sysml -# satellites=12800 definitions=4 units=800 ground-stations=20 components=960 connections=724 requirements=12 elements=11667 bytes=716125 +# satellites=12800 definitions=4 units=800 ground-stations=20 components=960 connections=724 requirements=12 elements=12467 bytes=765501 ``` | satellites | planes × per plane | form | definitions | units | elements | source | `-validate` wall | allocated | peak RSS | | ---------- | ------------------ | ---- | ----------- | ----- | -------- | ------ | ---------------- | --------- | -------- | | 1 600 | 8 × 200 | one definition per satellite | 1 600 | 1 600 | 294 627 | 18.1 MB | 17.5 s | 5.5 GiB | 2.6 GB | -| 1 600 | 8 × 200 | fleet | 4 | 104 | 3 099 | 184 KB | 0.16 s | 92 MiB | 106 MB | +| 1 600 | 8 × 200 | fleet | 4 | 104 | 3 203 | 191 KB | 0.17 s | 93 MiB | 106 MB | | 12 800 | 32 × 400 | one definition per satellite | 12 800 | 12 800 | 2 354 827 | 145 MB | 301 s | 43.5 GiB | 20.1 GB | -| 12 800 | 32 × 400 | fleet | 4 | 800 | 11 667 | 716 KB | 0.57 s | 249 MiB | 185 MB | +| 12 800 | 32 × 400 | fleet | 4 | 800 | 12 467 | 766 KB | 0.57 s | 254 MiB | 175 MB | The single-definition rows here are the plane and station layout the fleet -uses, so the two forms declare the same links; the validation table above +uses, so the two forms describe the same planes and stations; the validation table above (299 137 and 2 392 417 elements, 19.0 s and 318 s) was taken over a layout with a different split into planes and stations, and so slightly more links and station components. The fleet form -declares **200 times fewer elements** at 12 800 satellites and validates in -0.57 s and 185 MB rather than 301 s and 20.1 GB: validation is a function of +declares **190 times fewer elements** at 12 800 satellites and validates in +0.57 s and 175 MB rather than 301 s and 20.1 GB: validation is a function of what the source declares, and the fleet source is the size of four spacecraft, twenty stations and the links between thirty-two planes. @@ -217,10 +219,10 @@ machine: | satellites | operation | wall | allocated | peak RSS | | ---------- | --------- | ---- | --------- | -------- | -| 1 600 | `-instantiate` the network | 0.42 s | 219 MiB | 169 MB | -| 1 600 | `-satisfy`, 324 assertions | 0.91 s | 508 MiB | 269 MB | -| 12 800 | `-instantiate` the network | 2.55 s | 1.0 GiB | 650 MB | -| 12 800 | `-satisfy`, 2 412 assertions | 22.6 s | 14.4 GiB | 1.34 GB | +| 1 600 | `-instantiate` the network | 0.47 s | 220 MiB | 168 MB | +| 1 600 | `-satisfy`, 324 assertions | 0.95 s | 513 MiB | 269 MB | +| 12 800 | `-instantiate` the network | 2.34 s | 1.0 GiB | 692 MB | +| 12 800 | `-satisfy`, 2 412 assertions | 23.4 s | 14.4 GiB | 1.36 GB | | 12 800 | `%eval` of `plane.sats.dryMass`, all 32 planes | 252 s | 73.8 GiB | 4.9 GB | The runtime shares one shape — the effective feature list `FeaturesOf` @@ -242,7 +244,18 @@ polling the running mode machines. Reading one summed attribute over every occurrence evaluates it over the full tree of each — the cost the single-definition form paid at validation, paid here at the first read. -Two limits of the current runtime shape the fleet form: +Three limits of the current language and runtime shape the fleet form: + +- A connector end is a feature chain, so the fleet form cannot write the + single-definition form's pairing — `ringTo` closing each plane, + `planeTo` between the same slots of adjacent planes, `downlinkTo` + to station `i mod G` — without naming every occurrence. It declares one + connector over each collection instead, and the runtime realizes that as + one link whose ends hold the collections (`%eval network.plane0.ring.a` + is every transmitter of the plane), whatever the `[1]` ends declare. The + topology the two forms state is therefore not the same: the fleet says + each satellite is linked within its plane, to the next plane and to the + stations, not to which neighbour or station. - A `satisfy` whose subject is a collection (`satisfy blockAMass by plane0.sats`) is rejected — the subject must denote one object — so the @@ -264,9 +277,9 @@ go test ./internal/stressmodel -run '^$' -bench Fleet -benchmem -benchtime 3x | satellites | elements | instantiate + read four planes | per satellite | allocated | assertions | warm re-check | allocated | | ---------- | -------- | ------------------------------ | ------------- | --------- | ---------- | ------------- | --------- | -| 32 | 1 175 | 64 ms | 2.0 ms | 19.2 MiB | 24 | 0.9 ms | 0.5 MiB | -| 128 | 1 707 | 234 ms | 1.8 ms | 78.9 MiB | 36 | 1.3 ms | 1.1 MiB | -| 512 | 3 915 | 1.33 s | 2.6 ms | 563 MiB | 108 | 7.1 ms | 7.4 MiB | +| 32 | 1 179 | 74 ms | 2.3 ms | 20.3 MiB | 24 | 0.8 ms | 0.5 MiB | +| 128 | 1 715 | 268 ms | 2.1 ms | 83.0 MiB | 36 | 1.4 ms | 1.1 MiB | +| 512 | 3 947 | 1.43 s | 2.8 ms | 579 MiB | 108 | 6.4 ms | 7.4 MiB | Warm, instantiating a fleet and reading a summed attribute over its occurrences costs **about 2 ms and 1 MiB per satellite** — the per-satellite diff --git a/internal/stressmodel/satnet.go b/internal/stressmodel/satnet.go index dd91d72655..3e2ef1b671 100644 --- a/internal/stressmodel/satnet.go +++ b/internal/stressmodel/satnet.go @@ -461,7 +461,7 @@ func (g *generator) spacecraftBody(id int, valued string) { g.decl(5, "attribute :>> mass %s= %d.%d [kg];", valued, 2+(id+j)%40, (id*3+j)%10) g.decl(5, "attribute :>> powerDraw %s= %d.0 [W];", valued, 5+(id*5+j*7)%50) g.decl(5, "attribute :>> serialNumber %s= \"%s-%05d-%d\";", valued, strings.ToUpper(c.name), id, j) - g.componentDetail(c.def, id, j) + g.componentDetail(c.def, id, j, valued) g.line(4, "}") } g.decl(4, "attribute :>> mass = %s;", strings.Join(subMass, " + ")) @@ -527,7 +527,7 @@ func (g *generator) fleet(n SatelliteNetwork) { g.decl(3, "part sats : Spacecraft[%d] ordered;", n.Satellites) if n.Satellites > 1 { g.stats.Connections++ - g.decl(3, "interface ring : RFLink connect sats.comms.crosslinkTx to sats.comms.crosslinkRx {") + g.decl(3, "interface ring : RFLink connect [1] sats.comms.crosslinkTx to [1] sats.comms.crosslinkRx {") g.decl(4, "attribute :>> dataRate = 100.0;") g.decl(4, "attribute :>> slantRange = 2000 [km];") g.line(3, "}") @@ -544,7 +544,7 @@ func (g *generator) fleet(n SatelliteNetwork) { } for p := 0; p+1 < n.Planes; p++ { g.stats.Connections++ - g.decl(3, "interface plane%dTo%d : RFLink connect plane%d.sats.comms.crosslinkTx to plane%d.sats.comms.crosslinkRx {", p, p+1, p, p+1) + g.decl(3, "interface plane%dTo%d : RFLink connect [1] plane%d.sats.comms.crosslinkTx to [1] plane%d.sats.comms.crosslinkRx {", p, p+1, p, p+1) g.decl(4, "attribute :>> dataRate = %d.0;", 100+(2*p+1)%400) g.decl(4, "attribute :>> slantRange = %d [km];", 2000+(p*10+3)%3000) g.line(3, "}") @@ -610,6 +610,7 @@ func (g *generator) plane(n SatelliteNetwork, p, b int) { g.decl(6, "part :>> crosslinkTerminal {") g.decl(7, "attribute :>> mass = %d.%d [kg];", 2+(id+1)%40, (id*3+1)%10) g.decl(7, "attribute :>> serialNumber = \"CROSSLINKTERMINAL-%05d-1\";", id) + g.decl(7, "attribute :>> dataRate = %s;", crosslinkDataRate(id)) g.line(6, "}") g.line(5, "}") g.line(4, "}") @@ -622,55 +623,62 @@ func blockName(b int) string { return string(rune('A' + b)) } -// componentDetail writes the as-built values of the attributes a component kind adds. -func (g *generator) componentDetail(def string, id, j int) { +// crosslinkDataRate is the as-built data rate of the crosslink terminal of the +// spacecraft or block numbered id. +func crosslinkDataRate(id int) string { + return fmt.Sprintf("%d.0", 100+(id*3)%400) +} + +// componentDetail writes the as-built values of the attributes a component kind +// adds, each valued with the given keyword ("default " or none). +func (g *generator) componentDetail(def string, id, j int, valued string) { switch def { case "SolarArray": - g.decl(5, "attribute :>> area = %d.%d ['m²'];", 4+id%6, id%10) - g.decl(5, "attribute :>> generated = %d.0 [W];", 1200+(id*13)%700) + g.decl(5, "attribute :>> area %s= %d.%d ['m²'];", valued, 4+id%6, id%10) + g.decl(5, "attribute :>> generated %s= %d.0 [W];", valued, 1200+(id*13)%700) case "Battery": - g.decl(5, "attribute :>> capacity = %d.0 [J];", 3600000+(id*17)%7200000) - g.decl(5, "attribute :>> depthOfDischarge = 0.%d;", 2+id%5) + g.decl(5, "attribute :>> capacity %s= %d.0 [J];", valued, 3600000+(id*17)%7200000) + g.decl(5, "attribute :>> depthOfDischarge %s= 0.%d;", valued, 2+id%5) case "PowerConditioner": - g.decl(5, "attribute :>> efficiency = 0.9%d;", id%10) + g.decl(5, "attribute :>> efficiency %s= 0.9%d;", valued, id%10) case "StarTracker": - g.decl(5, "attribute :>> accuracy = %d.0 [arcsec];", 1+id%5) - g.decl(5, "attribute :>> updateRate = %d.0 [Hz];", 2+id%8) + g.decl(5, "attribute :>> accuracy %s= %d.0 [arcsec];", valued, 1+id%5) + g.decl(5, "attribute :>> updateRate %s= %d.0 [Hz];", valued, 2+id%8) case "InertialMeasurementUnit": - g.decl(5, "attribute :>> driftRate = 0.0%d;", 1+id%9) + g.decl(5, "attribute :>> driftRate %s= 0.0%d;", valued, 1+id%9) case "ReactionWheel": - g.decl(5, "attribute :>> maxTorque = 0.%d ['N⋅m'];", 1+(id+j)%9) - g.decl(5, "attribute :>> momentumCapacity = %d.0;", 10+(id+j)%40) + g.decl(5, "attribute :>> maxTorque %s= 0.%d ['N⋅m'];", valued, 1+(id+j)%9) + g.decl(5, "attribute :>> momentumCapacity %s= %d.0;", valued, 10+(id+j)%40) case "OnboardComputer": - g.decl(5, "attribute :>> clockRate = %d.0 [Hz];", 200000000+(id*11)%600000000) - g.decl(5, "attribute :>> memoryBytes = %d;", (1+id%8)*1073741824) + g.decl(5, "attribute :>> clockRate %s= %d.0 [Hz];", valued, 200000000+(id*11)%600000000) + g.decl(5, "attribute :>> memoryBytes %s= %d;", valued, (1+id%8)*1073741824) case "MassMemory": - g.decl(5, "attribute :>> capacityBytes = %d;", (16+id%48)*1073741824) + g.decl(5, "attribute :>> capacityBytes %s= %d;", valued, (16+id%48)*1073741824) case "Transponder": - g.decl(5, "attribute :>> frequency = %d.0 [Hz];", 8000000000+(id*7)%400000000) - g.decl(5, "attribute :>> transmitPower = %d.0 [W];", 10+id%40) + g.decl(5, "attribute :>> frequency %s= %d.0 [Hz];", valued, 8000000000+(id*7)%400000000) + g.decl(5, "attribute :>> transmitPower %s= %d.0 [W];", valued, 10+id%40) case "CrosslinkTerminal": - g.decl(5, "attribute :>> wavelength = 1550 [nm];") - g.decl(5, "attribute :>> dataRate = %d.0;", 100+(id*3)%400) + g.decl(5, "attribute :>> wavelength %s= 1550 [nm];", valued) + g.decl(5, "attribute :>> dataRate %s= %s;", valued, crosslinkDataRate(id)) case "Antenna": - g.decl(5, "attribute :>> gain = %d.%d;", 20+id%20, id%10) - g.decl(5, "attribute :>> diameter = 0.%d [m];", 3+id%6) + g.decl(5, "attribute :>> gain %s= %d.%d;", valued, 20+id%20, id%10) + g.decl(5, "attribute :>> diameter %s= 0.%d [m];", valued, 3+id%6) case "PropellantTank": - g.decl(5, "attribute :>> propellantMass = %d.0 [kg];", 30+(id*5)%100) - g.decl(5, "attribute :>> volume = 0.%d ['m³'];", 1+id%5) + g.decl(5, "attribute :>> propellantMass %s= %d.0 [kg];", valued, 30+(id*5)%100) + g.decl(5, "attribute :>> volume %s= 0.%d ['m³'];", valued, 1+id%5) case "Thruster": - g.decl(5, "attribute :>> thrust = %d.0 [mN];", 20+id%200) - g.decl(5, "attribute :>> specificImpulse = %d.0 [s];", 1200+(id*19)%800) + g.decl(5, "attribute :>> thrust %s= %d.0 [mN];", valued, 20+id%200) + g.decl(5, "attribute :>> specificImpulse %s= %d.0 [s];", valued, 1200+(id*19)%800) case "Radiator": - g.decl(5, "attribute :>> area = 1.%d ['m²'];", id%10) - g.decl(5, "attribute :>> emissivity = 0.8%d;", id%10) + g.decl(5, "attribute :>> area %s= 1.%d ['m²'];", valued, id%10) + g.decl(5, "attribute :>> emissivity %s= 0.8%d;", valued, id%10) case "Heater": - g.decl(5, "attribute :>> setpoint = %d.0 [K];", 283+id%20) + g.decl(5, "attribute :>> setpoint %s= %d.0 [K];", valued, 283+id%20) case "ImagingSensor": - g.decl(5, "attribute :>> groundSampleDistance = 0.%d [m];", 3+id%7) - g.decl(5, "attribute :>> swath = %d.0 [km];", 10+id%30) + g.decl(5, "attribute :>> groundSampleDistance %s= 0.%d [m];", valued, 3+id%7) + g.decl(5, "attribute :>> swath %s= %d.0 [km];", valued, 10+id%30) case "PayloadProcessor": - g.decl(5, "attribute :>> throughput = %d.0;", 100+(id*23)%900) + g.decl(5, "attribute :>> throughput %s= %d.0;", valued, 100+(id*23)%900) } } @@ -687,7 +695,7 @@ func (g *generator) groundStation(k int) { g.decl(4, "attribute :>> mass = %d.0 [kg];", 50+(k*7+j*11)%900) g.decl(4, "attribute :>> powerDraw = %d.0 [W];", 100+(k*13+j*17)%2000) g.decl(4, "attribute :>> serialNumber = \"GS-%s-%03d\";", strings.ToUpper(c.name), k) - g.componentDetail(c.def, k, j) + g.componentDetail(c.def, k, j, "") g.line(3, "}") } g.line(2, "}") diff --git a/internal/stressmodel/satnet_test.go b/internal/stressmodel/satnet_test.go index 12555098ca..39e0e15c9a 100644 --- a/internal/stressmodel/satnet_test.go +++ b/internal/stressmodel/satnet_test.go @@ -79,6 +79,16 @@ func TestFleetValidates(t *testing.T) { if stats.Bytes != len(src) { t.Errorf("Bytes = %d, want %d", stats.Bytes, len(src)) } + for _, want := range []string{ + "attribute :>> dataRate default = ", + "attribute :>> area default = ", + "connect [1] sats.comms.crosslinkTx to [1] sats.comms.crosslinkRx", + "connect [1] plane0.sats.comms.crosslinkTx to [1] plane1.sats.comms.crosslinkRx", + } { + if !strings.Contains(src, want) { + t.Errorf("source lacks %q", want) + } + } s := repl.NewSession() s.SetConformanceMode(conformance.ModeOf(true)) @@ -102,6 +112,9 @@ func TestFleetValidates(t *testing.T) { network + ".plane1.sats#(3).catalogId": "= 50000", network + ".plane1.unit0.catalogId": "= 40032", network + ".plane1.unit16.comms.crosslinkTerminal.serialNumber": `= "CROSSLINKTERMINAL-00048-1"`, + network + ".plane1.unit16.comms.crosslinkTerminal.dataRate": "= 244.0", + network + ".plane1.sats#(3).comms.crosslinkTerminal.dataRate": "= 103.0", + network + ".plane1.sats#(3).eps.solarArray.area": "= 5.1 ['m²']", network + ".plane0.sats#(3).plane": "= 0", network + ".satelliteCount": "= 64", } { From b1b30b01c048929b33663f3fd7bf961849705ce3 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Tue, 15 Sep 2026 16:55:09 +0000 Subject: [PATCH 03/11] chore(docs): regenerate documentation counts Co-Authored-By: jason.han --- README.md | 2 +- docs/project/spec-compliance.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 3146243268..c913a7de1d 100644 --- a/README.md +++ b/README.md @@ -326,7 +326,7 @@ What these numbers cannot show: the OMG corpora are demonstrations rather than a **Current commit:** All tests pass (`go test -race ./...`), builds clean (`go build ./...`). -**Test coverage:** 8,391 top-level `Test` functions (counted from the `_test.go` files, as `go test ./...` runs them) covering parsers, semantics, runtime (actions, states, instances, operators, validation). Behavioral robustness: 206 golden ASTs, 252 negatives, 939 conformance cases, 256 golden traces, 464 runtime robustness cases, 21 gRPC conformance cases and 8 gRPC robustness cases. These figures are generated by `make docs-counts` from the tree and gated. A test skips only for want of something the run did not provide, and says what: the held-image round trip declines a conformance case that creates no instance, a few gate on a PDF or Mermaid toolchain, a pinned pilot artifact, the PSSM suite, a locale, a case-insensitive filesystem or a live Flexo stack, and the OMG corpus gates skip until the corpora are downloaded unless asked to fail. +**Test coverage:** 8,393 top-level `Test` functions (counted from the `_test.go` files, as `go test ./...` runs them) covering parsers, semantics, runtime (actions, states, instances, operators, validation). Behavioral robustness: 206 golden ASTs, 252 negatives, 939 conformance cases, 256 golden traces, 464 runtime robustness cases, 21 gRPC conformance cases and 8 gRPC robustness cases. These figures are generated by `make docs-counts` from the tree and gated. A test skips only for want of something the run did not provide, and says what: the held-image round trip declines a conformance case that creates no instance, a few gate on a PDF or Mermaid toolchain, a pinned pilot artifact, the PSSM suite, a locale, a case-insensitive filesystem or a live Flexo stack, and the OMG corpus gates skip until the corpora are downloaded unless asked to fail. **Parser coverage:** 101/101 bundled library files parse cleanly — the 94 official SysML v2 standard library files and the non-normative `OpenSysML Libraries/OpenSysMLMathFunctions.kerml`, `OpenSysML Libraries/DocumentQueries.sysml`, `OpenSysML Libraries/IdentityMetadata.sysml`, `OpenSysML Libraries/DiagramLayout.sysml`, `OpenSysML Libraries/OOSEM.sysml`, `OpenSysML Libraries/MOSA.sysml` and `OpenSysML Libraries/StateSpaceIntegration.sysml` extensions. Conformance verified by [stdlib_conformance_test.go](internal/core/libs/stdlib_conformance_test.go). Grammar reference: [OMG Xtext grammar](https://github.com/Systems-Modeling/SysML-v2-Pilot-Implementation/tree/master/org.omg.kerml.xtext/src/org/omg/kerml/xtext). **Behavioral execution:** Calc/constraint/requirement/satisfy functional. Action/state executors handle nested invocation, control flow keywords, loop and conditional statements and the send statement (939/939 conformance cases passing). Coverage is self-assessed against the specification text and the normative library: the pinned OMG pilot implementation evaluates expressions but does not execute actions or state machines headlessly, so no external implementation currently adjudicates these rows. See [spec compliance](docs/project/spec-compliance.md). **Reference differential:** 377 files compared diagnostic-by-diagnostic against the pinned OMG pilot implementation (`2026-08`), 346 in full agreement; every divergence is enumerated and adjudicated in [the differential](docs/project/pilot-differential.md), reproducible with `go run ./cmd/pilot-diff`. diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md index 90fb5b692e..d3a7ef8202 100644 --- a/docs/project/spec-compliance.md +++ b/docs/project/spec-compliance.md @@ -133,7 +133,7 @@ what cannot be checked by anything is in - Golden traces: 256 golden execution traces under the default schedule (state×107, action×74, calc×32, clock×6, extent×6, constraint×4, string×4, three each of accept and analysis, two each of exhibited, f63 and verification, and one each of assign, f62, function, meta, object, occurrence, performed, send, two, w6e and w7d), and 50 more `.trace.golden` files pinning a case under a named policy, `.declared` or `.seed-` — entry/do/exit ordering of inline action bodies and a do body run to its end inside one round, the standard loop `until` with `then done`, a decision's guarded and `else` branches, a named flow carrying a value between action nodes, an accept with a `when` trigger, an accept subsetting an event, a send invocation through a port, a transition accepting through a port, loop and conditional bodies, one calc usage body run feeding several output reads, a usage whose outputs are read either side of an assignment to what its input named, a usage nested in a calc read for two of its outputs, calc statement bodies and their loop iterations, fork/join branch ordering, region entry/exit ordering, do behavior interleaving across orthogonal regions, send/accept, an accept parked until its message arrives, a payload read by a node declared before the accept that binds it, calc and constraint evaluation, library function invocation, the dotted-target transition, control-node and merge-body traces, and the merge loops re-entered on every pass) - Negative parser tests: 252 negative parser subtests (first-level subtests of `TestNegative`; 396 across the `TestNegative*` functions, 60 of them KerML, and 454 across every `*Negative*` parser test) - gRPC: 21 gRPC conformance cases and 8 gRPC robustness cases (`internal/grpc/testdata/conformance/`, `internal/grpc/robustness_test.go`) -- Test functions: 8,391 top-level `Test` functions across the module (`go test -count=1 ./...` runs them all, with the OMG corpora downloaded, `OPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 OPENSYSML_REQUIRE_SMT=1` and z3 installed). The figures on this list are generated by `make docs-counts` from the tree and gated; the test and subtest total of a run is not, since it moves with every fixture and only a run can state it. A test skips only where it says why: TestHeldImageRoundTrip declines a conformance case that creates no instance, so there is no held image to round-trip. Three skip themselves: TestSubsettingTargetIsTheInheritedFeature and TestRequirementEvaluation_SubjectNotFound against a limitation they record, and TestHelperSolverProcess, which is a solver child process the parent invokes. The others skip for want of something the run did not provide, and each names it: the `weasyprint`, `pandoc` and `prince` subtests of TestRenderWithInstalledEngines and TestRenderInlineRunsWithInstalledEngines and TestRenderDiagramsWithInstalledMermaid want the PDF and Mermaid toolchain, TestExtractionMatchesBaseline and TestUpdateIsIdempotentAcrossDays the pinned pilot validator jar, TestEmitSuite, TestRefereeRowsAreWellFormed, TestSuiteRead and TestSuiteClassification the downloaded PSSM test suite, TestCRealNotationIsLocaleIndependent a non-C locale, TestRenderDocumentsRejectsCaseAliasedTargets a case-insensitive filesystem, and TestFlexoInterop and TestFlexoInteropApply a live Flexo stack. +- Test functions: 8,393 top-level `Test` functions across the module (`go test -count=1 ./...` runs them all, with the OMG corpora downloaded, `OPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 OPENSYSML_REQUIRE_SMT=1` and z3 installed). The figures on this list are generated by `make docs-counts` from the tree and gated; the test and subtest total of a run is not, since it moves with every fixture and only a run can state it. A test skips only where it says why: TestHeldImageRoundTrip declines a conformance case that creates no instance, so there is no held image to round-trip. Three skip themselves: TestSubsettingTargetIsTheInheritedFeature and TestRequirementEvaluation_SubjectNotFound against a limitation they record, and TestHelperSolverProcess, which is a solver child process the parent invokes. The others skip for want of something the run did not provide, and each names it: the `weasyprint`, `pandoc` and `prince` subtests of TestRenderWithInstalledEngines and TestRenderInlineRunsWithInstalledEngines and TestRenderDiagramsWithInstalledMermaid want the PDF and Mermaid toolchain, TestExtractionMatchesBaseline and TestUpdateIsIdempotentAcrossDays the pinned pilot validator jar, TestEmitSuite, TestRefereeRowsAreWellFormed, TestSuiteRead and TestSuiteClassification the downloaded PSSM test suite, TestCRealNotationIsLocaleIndependent a non-C locale, TestRenderDocumentsRejectsCaseAliasedTargets a case-insensitive filesystem, and TestFlexoInterop and TestFlexoInteropApply a live Flexo stack. --- From 893e0befc1adcc9d435996a4026430b09965fa86 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Tue, 15 Sep 2026 16:58:59 +0000 Subject: [PATCH 04/11] fix(stressmodel): declare [1] ends on fleet downlink connectors Co-Authored-By: jason.han --- docs/guide/modeling-fleets.md | 2 +- internal/stressmodel/satnet.go | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/guide/modeling-fleets.md b/docs/guide/modeling-fleets.md index 3cfd033d2d..e779b80a95 100644 --- a/docs/guide/modeling-fleets.md +++ b/docs/guide/modeling-fleets.md @@ -192,7 +192,7 @@ part def Network { } // … interface plane0To1 : RFLink connect [1] plane0.sats.comms.crosslinkTx to [1] plane1.sats.comms.crosslinkRx; - interface downlink0To0 : RFLink connect plane0.sats.comms.rf to gs0.uplink; + interface downlink0To0 : RFLink connect [1] plane0.sats.comms.rf to [1] gs0.uplink; } satisfy blockAMass by blockAConfig; satisfy blockAMass by network.plane0.unit16; diff --git a/internal/stressmodel/satnet.go b/internal/stressmodel/satnet.go index 3e2ef1b671..3772ff9fba 100644 --- a/internal/stressmodel/satnet.go +++ b/internal/stressmodel/satnet.go @@ -552,7 +552,7 @@ func (g *generator) fleet(n SatelliteNetwork) { for p := 0; p < n.Planes; p++ { for k := 0; k < n.GroundStations; k++ { g.stats.Connections++ - g.decl(3, "interface downlink%dTo%d : RFLink connect plane%d.sats.comms.rf to gs%d.uplink {", k, p, p, k) + g.decl(3, "interface downlink%dTo%d : RFLink connect [1] plane%d.sats.comms.rf to [1] gs%d.uplink {", k, p, p, k) g.decl(4, "attribute :>> dataRate = %d.0;", 50+p%200) g.decl(4, "attribute :>> slantRange = %d [km];", 900+p%1500) g.line(3, "}") From 3bff111344fd2cc5e159c869eff3c8f0bcd001c6 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Tue, 15 Sep 2026 17:54:09 +0000 Subject: [PATCH 05/11] docs(stressmodel): restate the fleet source sizes after the connector-end fix Co-Authored-By: jason.han --- docs/guide/modeling-fleets.md | 4 ++-- docs/internals/performance.md | 2 +- docs/project/satellite-network-stress-test.md | 6 +++--- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/docs/guide/modeling-fleets.md b/docs/guide/modeling-fleets.md index e779b80a95..792bf0b08d 100644 --- a/docs/guide/modeling-fleets.md +++ b/docs/guide/modeling-fleets.md @@ -211,9 +211,9 @@ go run ./cmd/stress-model -planes 8 -satellites 200 -ground-stations 20 -fleet - | satellites | planes × per plane | form | definitions | units stating values | elements | source | | ---------- | ------------------ | ---- | ----------- | -------------------- | -------- | ------ | | 1 600 | 8 × 200 | one definition per satellite | 1 600 | 1 600 | 294 627 | 18.1 MB | -| 1 600 | 8 × 200 | fleet | 4 | 104 | 3 203 | 191 KB | +| 1 600 | 8 × 200 | fleet | 4 | 104 | 3 203 | 193 KB | | 12 800 | 32 × 400 | one definition per satellite | 12 800 | 12 800 | 2 354 827 | 145 MB | -| 12 800 | 32 × 400 | fleet | 4 | 800 | 12 467 | 766 KB | +| 12 800 | 32 × 400 | fleet | 4 | 800 | 12 467 | 771 KB | The fleet form of the 12 800-satellite constellation is **12 467 declared elements against 2 354 827** — a factor of 190 — and what remains grows with diff --git a/docs/internals/performance.md b/docs/internals/performance.md index dd1ffb40fe..0482cc5ef3 100644 --- a/docs/internals/performance.md +++ b/docs/internals/performance.md @@ -186,7 +186,7 @@ costs: | form | elements | source | wall | allocated | peak RSS | | ---- | -------- | ------ | ---- | --------- | -------- | | one `part def` per satellite, 32 planes of 400 | 2 354 827 | 145 MB | 301 s | 43.5 GiB | 20.1 GB | -| four blocks, `part sats : Block[400]` in 32 planes | 12 467 | 766 KB | 0.57 s | 254 MiB | 175 MB | +| four blocks, `part sats : Block[400]` in 32 planes | 12 467 | 771 KB | 0.57 s | 254 MiB | 175 MB | The runtime then pays for the occurrences when something asks for them: the same network instantiates in 2.34 s and 692 MB, its 2 412 `satisfy` diff --git a/docs/project/satellite-network-stress-test.md b/docs/project/satellite-network-stress-test.md index e9f53f959f..a5f7c29957 100644 --- a/docs/project/satellite-network-stress-test.md +++ b/docs/project/satellite-network-stress-test.md @@ -194,15 +194,15 @@ source of both forms. go run ./cmd/stress-model -planes 32 -satellites 400 -ground-stations 20 -stats > legacy.sysml # satellites=12800 definitions=12800 units=12800 ground-stations=20 components=256080 connections=204400 requirements=38400 elements=2354827 bytes=145364954 go run ./cmd/stress-model -planes 32 -satellites 400 -ground-stations 20 -fleet -stats > fleet.sysml -# satellites=12800 definitions=4 units=800 ground-stations=20 components=960 connections=724 requirements=12 elements=12467 bytes=765501 +# satellites=12800 definitions=4 units=800 ground-stations=20 components=960 connections=724 requirements=12 elements=12467 bytes=770621 ``` | satellites | planes × per plane | form | definitions | units | elements | source | `-validate` wall | allocated | peak RSS | | ---------- | ------------------ | ---- | ----------- | ----- | -------- | ------ | ---------------- | --------- | -------- | | 1 600 | 8 × 200 | one definition per satellite | 1 600 | 1 600 | 294 627 | 18.1 MB | 17.5 s | 5.5 GiB | 2.6 GB | -| 1 600 | 8 × 200 | fleet | 4 | 104 | 3 203 | 191 KB | 0.17 s | 93 MiB | 106 MB | +| 1 600 | 8 × 200 | fleet | 4 | 104 | 3 203 | 193 KB | 0.17 s | 93 MiB | 106 MB | | 12 800 | 32 × 400 | one definition per satellite | 12 800 | 12 800 | 2 354 827 | 145 MB | 301 s | 43.5 GiB | 20.1 GB | -| 12 800 | 32 × 400 | fleet | 4 | 800 | 12 467 | 766 KB | 0.57 s | 254 MiB | 175 MB | +| 12 800 | 32 × 400 | fleet | 4 | 800 | 12 467 | 771 KB | 0.57 s | 254 MiB | 175 MB | The single-definition rows here are the plane and station layout the fleet uses, so the two forms describe the same planes and stations; the validation table above From e9f8b2acb2b67c83383740ff144a6d5380fdca81 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Tue, 15 Sep 2026 18:17:11 +0000 Subject: [PATCH 06/11] feat(stressmodel): split the fleet form into the library and the constellation Co-Authored-By: jason.han --- docs/project/satellite-network-stress-test.md | 4 ++- internal/stressmodel/satnet.go | 9 ++++-- internal/stressmodel/satnet_test.go | 28 +++++++++++++++++-- internal/stressmodel/split.go | 11 ++++++++ 4 files changed, 47 insertions(+), 5 deletions(-) diff --git a/docs/project/satellite-network-stress-test.md b/docs/project/satellite-network-stress-test.md index 523b25301f..d14fad4117 100644 --- a/docs/project/satellite-network-stress-test.md +++ b/docs/project/satellite-network-stress-test.md @@ -336,7 +336,9 @@ frame in the resolver, its memoized semantics and its gathered facts stay. The worst edit is to a document everything else depends on. `Split` writes the same network as one document per plane beside the library they build on and -the constellation joining them (six files at these sizes); `BenchmarkLoadFiles` +the constellation joining them (six files at these sizes; the fleet form, whose +planes are members of the network, splits into the library and the +constellation alone); `BenchmarkLoadFiles` opens and analyzes every file through one workspace, and `BenchmarkEditImported` edits the library and then asks every file for its diagnostics, as the editor's refresh sweep does: diff --git a/internal/stressmodel/satnet.go b/internal/stressmodel/satnet.go index dfe6c9387a..49bd81f050 100644 --- a/internal/stressmodel/satnet.go +++ b/internal/stressmodel/satnet.go @@ -521,6 +521,13 @@ func (g *generator) fleet(n SatelliteNetwork) { g.line(2, "private import Platform::*;") g.line(2, "private import Requirements::*;") g.line(2, "private import Behavior::*;") + g.fleetBody(n) + g.line(1, "}") + g.line(0, "}") +} + +// fleetBody writes the members of the fleet-form constellation package. +func (g *generator) fleetBody(n SatelliteNetwork) { blocks := min(fleetBlocks, n.Planes) for b := 0; b < blocks; b++ { g.block(b) @@ -579,8 +586,6 @@ func (g *generator) fleet(n SatelliteNetwork) { } } } - g.line(1, "}") - g.line(0, "}") } // block writes one spacecraft block: a definition whose as-built values are diff --git a/internal/stressmodel/satnet_test.go b/internal/stressmodel/satnet_test.go index 6bd510fd4e..c0cb6d93c1 100644 --- a/internal/stressmodel/satnet_test.go +++ b/internal/stressmodel/satnet_test.go @@ -167,6 +167,30 @@ func TestSatelliteNetworkFilesValidate(t *testing.T) { if stats.Satellites != whole.Satellites || stats.Requirements != whole.Requirements || stats.Connections != whole.Connections { t.Fatalf("split stats %+v, single-file stats %+v", stats, whole) } + validateFiles(t, files, stats.Requirements) +} + +// TestFleetFilesValidate keeps the split fleet form in step with the whole one: +// the library and the constellation as two documents declare the same network, +// load clean under strict conformance, and hold every satisfy assertion. +func TestFleetFilesValidate(t *testing.T) { + n := SatelliteNetwork{Planes: 2, Satellites: 2 * fleetUnitStride, GroundStations: 1, Fleet: true} + files, stats := n.Split() + if len(files) != 2 { + t.Fatalf("got %d files, want the library and the constellation", len(files)) + } + _, whole := n.Source() + if stats.Elements != whole.Elements || stats.Definitions != whole.Definitions || stats.Units != whole.Units || + stats.Satellites != whole.Satellites || stats.Requirements != whole.Requirements || stats.Connections != whole.Connections { + t.Fatalf("split stats %+v, single-file stats %+v", stats, whole) + } + validateFiles(t, files, 3*(stats.Definitions+stats.Units)) +} + +// validateFiles opens files as one workspace and one session, wanting no +// diagnostic and the given number of satisfy assertions, all holding. +func validateFiles(t *testing.T, files []File, assertions int) { + t.Helper() ws := model.NewWorkspace(model.WithConformanceMode(conformance.ModeOf(true))) for _, f := range files { ws.Open(f.Name, []byte(f.Source), 1) @@ -187,8 +211,8 @@ func TestSatelliteNetworkFilesValidate(t *testing.T) { t.Errorf("diagnostic: %s", d.Message) } verdicts := s.CheckSatisfy("") - if len(verdicts) != stats.Requirements { - t.Fatalf("got %d satisfy verdicts, want %d", len(verdicts), stats.Requirements) + if len(verdicts) != assertions { + t.Fatalf("got %d satisfy verdicts, want %d", len(verdicts), assertions) } for _, v := range verdicts { if !v.Holds() { diff --git a/internal/stressmodel/split.go b/internal/stressmodel/split.go index 658341eae4..51add371ef 100644 --- a/internal/stressmodel/split.go +++ b/internal/stressmodel/split.go @@ -13,6 +13,8 @@ type File struct { // Split generates the network Generate writes as one document per orbital plane // beside the shared library and the constellation joining the planes. Each plane // imports the library by qualified name, so a file resolves against the others. +// The fleet form declares its planes inside the network, so it splits into the +// library and the constellation alone. func (n SatelliteNetwork) Split() ([]File, Stats) { var b strings.Builder g := &generator{b: &b} @@ -28,6 +30,15 @@ func (n SatelliteNetwork) Split() ([]File, Stats) { g.line(0, "}") files = append(files, take("library.sysml")) + if n.Fleet { + g.decl(0, "package Constellation {") + g.planeImports() + g.line(0, "") + g.fleetBody(n) + g.line(0, "}") + return append(files, take("constellation.sysml")), g.stats + } + id := 0 for p := 0; p < n.Planes; p++ { g.decl(0, "package Plane%d {", p) From d3f1c8db6da3478bfa1652c59a53ed9a019ddfba Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Tue, 15 Sep 2026 18:43:28 +0000 Subject: [PATCH 07/11] docs: refresh generated test-function counts Co-Authored-By: jason.han --- README.md | 2 +- docs/project/spec-compliance.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index a7bef5e2a4..105a5205c8 100644 --- a/README.md +++ b/README.md @@ -326,7 +326,7 @@ What these numbers cannot show: the OMG corpora are demonstrations rather than a **Current commit:** All tests pass (`go test -race ./...`), builds clean (`go build ./...`). -**Test coverage:** 8,421 top-level `Test` functions (counted from the `_test.go` files, as `go test ./...` runs them) covering parsers, semantics, runtime (actions, states, instances, operators, validation). Behavioral robustness: 206 golden ASTs, 252 negatives, 940 conformance cases, 257 golden traces, 465 runtime robustness cases, 21 gRPC conformance cases and 8 gRPC robustness cases. These figures are generated by `make docs-counts` from the tree and gated. A test skips only for want of something the run did not provide, and says what: the held-image round trip declines a conformance case that creates no instance, a few gate on a PDF or Mermaid toolchain, a pinned pilot artifact, the PSSM suite, a locale, a case-insensitive filesystem or a live Flexo stack, and the OMG corpus gates skip until the corpora are downloaded unless asked to fail. +**Test coverage:** 8,422 top-level `Test` functions (counted from the `_test.go` files, as `go test ./...` runs them) covering parsers, semantics, runtime (actions, states, instances, operators, validation). Behavioral robustness: 206 golden ASTs, 252 negatives, 940 conformance cases, 257 golden traces, 465 runtime robustness cases, 21 gRPC conformance cases and 8 gRPC robustness cases. These figures are generated by `make docs-counts` from the tree and gated. A test skips only for want of something the run did not provide, and says what: the held-image round trip declines a conformance case that creates no instance, a few gate on a PDF or Mermaid toolchain, a pinned pilot artifact, the PSSM suite, a locale, a case-insensitive filesystem or a live Flexo stack, and the OMG corpus gates skip until the corpora are downloaded unless asked to fail. **Parser coverage:** 101/101 bundled library files parse cleanly — the 94 official SysML v2 standard library files and the non-normative `OpenSysML Libraries/OpenSysMLMathFunctions.kerml`, `OpenSysML Libraries/DocumentQueries.sysml`, `OpenSysML Libraries/IdentityMetadata.sysml`, `OpenSysML Libraries/DiagramLayout.sysml`, `OpenSysML Libraries/OOSEM.sysml`, `OpenSysML Libraries/MOSA.sysml` and `OpenSysML Libraries/StateSpaceIntegration.sysml` extensions. Conformance verified by [stdlib_conformance_test.go](internal/core/libs/stdlib_conformance_test.go). Grammar reference: [OMG Xtext grammar](https://github.com/Systems-Modeling/SysML-v2-Pilot-Implementation/tree/master/org.omg.kerml.xtext/src/org/omg/kerml/xtext). **Behavioral execution:** Calc/constraint/requirement/satisfy functional. Action/state executors handle nested invocation, control flow keywords, loop and conditional statements and the send statement (940/940 conformance cases passing). Coverage is self-assessed against the specification text and the normative library: the pinned OMG pilot implementation evaluates expressions but does not execute actions or state machines headlessly, so no external implementation currently adjudicates these rows. See [spec compliance](docs/project/spec-compliance.md). **Reference differential:** 377 files compared diagnostic-by-diagnostic against the pinned OMG pilot implementation (`2026-08`), 346 in full agreement; every divergence is enumerated and adjudicated in [the differential](docs/project/pilot-differential.md), reproducible with `go run ./cmd/pilot-diff`. diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md index 03c23775c9..6b0ab33477 100644 --- a/docs/project/spec-compliance.md +++ b/docs/project/spec-compliance.md @@ -133,7 +133,7 @@ what cannot be checked by anything is in - Golden traces: 257 golden execution traces under the default schedule (state×108, action×74, calc×32, clock×6, extent×6, constraint×4, string×4, three each of accept and analysis, two each of exhibited, f63 and verification, and one each of assign, f62, function, meta, object, occurrence, performed, send, two, w6e and w7d), and 54 more `.trace.golden` files pinning a case under a named policy, `.declared` or `.seed-` — entry/do/exit ordering of inline action bodies and a do body run to its end inside one round, the standard loop `until` with `then done`, a decision's guarded and `else` branches, a named flow carrying a value between action nodes, an accept with a `when` trigger, an accept subsetting an event, a send invocation through a port, a transition accepting through a port, loop and conditional bodies, one calc usage body run feeding several output reads, a usage whose outputs are read either side of an assignment to what its input named, a usage nested in a calc read for two of its outputs, calc statement bodies and their loop iterations, fork/join branch ordering, region entry/exit ordering, do behavior interleaving across orthogonal regions, send/accept, an accept parked until its message arrives, a payload read by a node declared before the accept that binds it, calc and constraint evaluation, library function invocation, the dotted-target transition, control-node and merge-body traces, and the merge loops re-entered on every pass) - Negative parser tests: 252 negative parser subtests (first-level subtests of `TestNegative`; 396 across the `TestNegative*` functions, 60 of them KerML, and 454 across every `*Negative*` parser test) - gRPC: 21 gRPC conformance cases and 8 gRPC robustness cases (`internal/grpc/testdata/conformance/`, `internal/grpc/robustness_test.go`) -- Test functions: 8,421 top-level `Test` functions across the module (`go test -count=1 ./...` runs them all, with the OMG corpora downloaded, `OPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 OPENSYSML_REQUIRE_SMT=1` and z3 installed). The figures on this list are generated by `make docs-counts` from the tree and gated; the test and subtest total of a run is not, since it moves with every fixture and only a run can state it. A test skips only where it says why: TestHeldImageRoundTrip declines a conformance case that creates no instance, so there is no held image to round-trip. Three skip themselves: TestSubsettingTargetIsTheInheritedFeature and TestRequirementEvaluation_SubjectNotFound against a limitation they record, and TestHelperSolverProcess, which is a solver child process the parent invokes. The others skip for want of something the run did not provide, and each names it: the `weasyprint`, `pandoc` and `prince` subtests of TestRenderWithInstalledEngines and TestRenderInlineRunsWithInstalledEngines and TestRenderDiagramsWithInstalledMermaid want the PDF and Mermaid toolchain, TestExtractionMatchesBaseline and TestUpdateIsIdempotentAcrossDays the pinned pilot validator jar, TestEmitSuite, TestRefereeRowsAreWellFormed, TestSuiteRead and TestSuiteClassification the downloaded PSSM test suite, TestCRealNotationIsLocaleIndependent a non-C locale, TestRenderDocumentsRejectsCaseAliasedTargets a case-insensitive filesystem, and TestFlexoInterop and TestFlexoInteropApply a live Flexo stack. +- Test functions: 8,422 top-level `Test` functions across the module (`go test -count=1 ./...` runs them all, with the OMG corpora downloaded, `OPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 OPENSYSML_REQUIRE_SMT=1` and z3 installed). The figures on this list are generated by `make docs-counts` from the tree and gated; the test and subtest total of a run is not, since it moves with every fixture and only a run can state it. A test skips only where it says why: TestHeldImageRoundTrip declines a conformance case that creates no instance, so there is no held image to round-trip. Three skip themselves: TestSubsettingTargetIsTheInheritedFeature and TestRequirementEvaluation_SubjectNotFound against a limitation they record, and TestHelperSolverProcess, which is a solver child process the parent invokes. The others skip for want of something the run did not provide, and each names it: the `weasyprint`, `pandoc` and `prince` subtests of TestRenderWithInstalledEngines and TestRenderInlineRunsWithInstalledEngines and TestRenderDiagramsWithInstalledMermaid want the PDF and Mermaid toolchain, TestExtractionMatchesBaseline and TestUpdateIsIdempotentAcrossDays the pinned pilot validator jar, TestEmitSuite, TestRefereeRowsAreWellFormed, TestSuiteRead and TestSuiteClassification the downloaded PSSM test suite, TestCRealNotationIsLocaleIndependent a non-C locale, TestRenderDocumentsRejectsCaseAliasedTargets a case-insensitive filesystem, and TestFlexoInterop and TestFlexoInteropApply a live Flexo stack. --- From 1065f40c75fc6179efc99ad5de7f27093e2e6934 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Tue, 15 Sep 2026 19:59:11 +0000 Subject: [PATCH 08/11] docs(guide): state the fidelity trade-off of the diverging-unit stride Co-Authored-By: jason.han --- docs/guide/modeling-fleets.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/docs/guide/modeling-fleets.md b/docs/guide/modeling-fleets.md index 792bf0b08d..d8caee881b 100644 --- a/docs/guide/modeling-fleets.md +++ b/docs/guide/modeling-fleets.md @@ -174,9 +174,11 @@ orbital plane is `part sats : Block[N] ordered` with one ring connector over the collection, one connector between adjacent planes and one downlink connector per plane and station, their ends declared `[1]` so that each link joins one satellite to one satellite or station; every sixteenth unit states -a catalog number, a slot and a crosslink terminal of its own; the -requirements are declared once per block and asserted on the block's -configuration and on every diverging unit: +a catalog number, a slot and a crosslink terminal of its own — the fifteen +units between read the block's values, so the fleet carries fewer distinct +per-unit values than the per-satellite form, the trade-off a bound value +table would remove; the requirements are declared once per block and +asserted on the block's configuration and on every diverging unit: ```sysml part def OrbitalPlane { From 85797ffaa444326658bdb2c87d8189dc7a4ac7d9 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Wed, 16 Sep 2026 03:28:37 +0000 Subject: [PATCH 09/11] docs: regenerate test-count figures Co-Authored-By: jason.han --- README.md | 2 +- docs/project/spec-compliance.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index aa24da08f3..1ede4adc61 100644 --- a/README.md +++ b/README.md @@ -326,7 +326,7 @@ What these numbers cannot show: the OMG corpora are demonstrations rather than a **Current commit:** All tests pass (`go test -race ./...`), builds clean (`go build ./...`). -**Test coverage:** 8,507 top-level `Test` functions (counted from the `_test.go` files, as `go test ./...` runs them) covering parsers, semantics, runtime (actions, states, instances, operators, validation). Behavioral robustness: 206 golden ASTs, 252 negatives, 961 conformance cases, 270 golden traces, 470 runtime robustness cases, 21 gRPC conformance cases and 8 gRPC robustness cases. These figures are generated by `make docs-counts` from the tree and gated. A test skips only for want of something the run did not provide, and says what: the held-image round trip declines a conformance case that creates no instance, a few gate on a PDF or Mermaid toolchain, a pinned pilot artifact, the PSSM suite, a locale, a case-insensitive filesystem or a live Flexo stack, and the OMG corpus gates skip until the corpora are downloaded unless asked to fail. +**Test coverage:** 8,533 top-level `Test` functions (counted from the `_test.go` files, as `go test ./...` runs them) covering parsers, semantics, runtime (actions, states, instances, operators, validation). Behavioral robustness: 206 golden ASTs, 252 negatives, 961 conformance cases, 270 golden traces, 470 runtime robustness cases, 21 gRPC conformance cases and 8 gRPC robustness cases. These figures are generated by `make docs-counts` from the tree and gated. A test skips only for want of something the run did not provide, and says what: the held-image round trip declines a conformance case that creates no instance, a few gate on a PDF or Mermaid toolchain, a pinned pilot artifact, the PSSM suite, a locale, a case-insensitive filesystem or a live Flexo stack, and the OMG corpus gates skip until the corpora are downloaded unless asked to fail. **Parser coverage:** 101/101 bundled library files parse cleanly — the 94 official SysML v2 standard library files and the non-normative `OpenSysML Libraries/OpenSysMLMathFunctions.kerml`, `OpenSysML Libraries/DocumentQueries.sysml`, `OpenSysML Libraries/IdentityMetadata.sysml`, `OpenSysML Libraries/DiagramLayout.sysml`, `OpenSysML Libraries/OOSEM.sysml`, `OpenSysML Libraries/MOSA.sysml` and `OpenSysML Libraries/StateSpaceIntegration.sysml` extensions. Conformance verified by [stdlib_conformance_test.go](internal/core/libs/stdlib_conformance_test.go). Grammar reference: [OMG Xtext grammar](https://github.com/Systems-Modeling/SysML-v2-Pilot-Implementation/tree/master/org.omg.kerml.xtext/src/org/omg/kerml/xtext). **Behavioral execution:** Calc/constraint/requirement/satisfy functional. Action/state executors handle nested invocation, control flow keywords, loop and conditional statements and the send statement (961/961 conformance cases passing). Coverage is self-assessed against the specification text and the normative library: the pinned OMG pilot implementation evaluates expressions but does not execute actions or state machines headlessly, so no external implementation currently adjudicates these rows. See [spec compliance](docs/project/spec-compliance.md). **Reference differential:** 379 files compared diagnostic-by-diagnostic against the pinned OMG pilot implementation (`2026-08`), 347 in full agreement; every divergence is enumerated and adjudicated in [the differential](docs/project/pilot-differential.md), reproducible with `go run ./cmd/pilot-diff`. diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md index 7ae7143bfb..33f1c4f5b8 100644 --- a/docs/project/spec-compliance.md +++ b/docs/project/spec-compliance.md @@ -133,7 +133,7 @@ what cannot be checked by anything is in - Golden traces: 270 golden execution traces under the default schedule (state×121, action×74, calc×32, clock×6, extent×6, constraint×4, string×4, three each of accept and analysis, two each of exhibited, f63 and verification, and one each of assign, f62, function, meta, object, occurrence, performed, send, two, w6e and w7d), and 80 more `.trace.golden` files pinning a case under a named policy, `.declared` or `.seed-` — entry/do/exit ordering of inline action bodies and a do body run to its end inside one round, the standard loop `until` with `then done`, a decision's guarded and `else` branches, a named flow carrying a value between action nodes, an accept with a `when` trigger, an accept subsetting an event, a send invocation through a port, a transition accepting through a port, loop and conditional bodies, one calc usage body run feeding several output reads, a usage whose outputs are read either side of an assignment to what its input named, a usage nested in a calc read for two of its outputs, calc statement bodies and their loop iterations, fork/join branch ordering, region entry/exit ordering, do behavior interleaving across orthogonal regions, send/accept, an accept parked until its message arrives, a payload read by a node declared before the accept that binds it, calc and constraint evaluation, library function invocation, the dotted-target transition, control-node and merge-body traces, and the merge loops re-entered on every pass) - Negative parser tests: 252 negative parser subtests (first-level subtests of `TestNegative`; 396 across the `TestNegative*` functions, 60 of them KerML, and 454 across every `*Negative*` parser test) - gRPC: 21 gRPC conformance cases and 8 gRPC robustness cases (`internal/grpc/testdata/conformance/`, `internal/grpc/robustness_test.go`) -- Test functions: 8,507 top-level `Test` functions across the module (`go test -count=1 ./...` runs them all, with the OMG corpora downloaded, `OPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 OPENSYSML_REQUIRE_SMT=1` and z3 installed). The figures on this list are generated by `make docs-counts` from the tree and gated; the test and subtest total of a run is not, since it moves with every fixture and only a run can state it. A test skips only where it says why: TestHeldImageRoundTrip declines a conformance case that creates no instance, so there is no held image to round-trip. Three skip themselves: TestSubsettingTargetIsTheInheritedFeature and TestRequirementEvaluation_SubjectNotFound against a limitation they record, and TestHelperSolverProcess, which is a solver child process the parent invokes. The others skip for want of something the run did not provide, and each names it: the `weasyprint`, `pandoc` and `prince` subtests of TestRenderWithInstalledEngines and TestRenderInlineRunsWithInstalledEngines and TestRenderDiagramsWithInstalledMermaid want the PDF and Mermaid toolchain, TestExtractionMatchesBaseline and TestUpdateIsIdempotentAcrossDays the pinned pilot validator jar, TestEmitSuite, TestRefereeRowsAreWellFormed, TestSuiteRead and TestSuiteClassification the downloaded PSSM test suite, TestCRealNotationIsLocaleIndependent a non-C locale, TestRenderDocumentsRejectsCaseAliasedTargets a case-insensitive filesystem, and TestFlexoInterop and TestFlexoInteropApply a live Flexo stack. +- Test functions: 8,533 top-level `Test` functions across the module (`go test -count=1 ./...` runs them all, with the OMG corpora downloaded, `OPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 OPENSYSML_REQUIRE_SMT=1` and z3 installed). The figures on this list are generated by `make docs-counts` from the tree and gated; the test and subtest total of a run is not, since it moves with every fixture and only a run can state it. A test skips only where it says why: TestHeldImageRoundTrip declines a conformance case that creates no instance, so there is no held image to round-trip. Three skip themselves: TestSubsettingTargetIsTheInheritedFeature and TestRequirementEvaluation_SubjectNotFound against a limitation they record, and TestHelperSolverProcess, which is a solver child process the parent invokes. The others skip for want of something the run did not provide, and each names it: the `weasyprint`, `pandoc` and `prince` subtests of TestRenderWithInstalledEngines and TestRenderInlineRunsWithInstalledEngines and TestRenderDiagramsWithInstalledMermaid want the PDF and Mermaid toolchain, TestExtractionMatchesBaseline and TestUpdateIsIdempotentAcrossDays the pinned pilot validator jar, TestEmitSuite, TestRefereeRowsAreWellFormed, TestSuiteRead and TestSuiteClassification the downloaded PSSM test suite, TestCRealNotationIsLocaleIndependent a non-C locale, TestRenderDocumentsRejectsCaseAliasedTargets a case-insensitive filesystem, and TestFlexoInterop and TestFlexoInteropApply a live Flexo stack. --- From aca58864096eafc53226be95c6b2b54463d02dc7 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Fri, 25 Sep 2026 21:06:41 +0000 Subject: [PATCH 10/11] docs(stressmodel): re-measure the fleet and single-definition forms on the current tree Co-Authored-By: jason.han --- .../stress-model-fleet-mode.added.md | 6 +-- docs/guide/modeling-fleets.md | 48 +++++++++--------- docs/internals/performance.md | 12 ++--- docs/project/satellite-network-stress-test.md | 50 +++++++++---------- 4 files changed, 57 insertions(+), 59 deletions(-) diff --git a/changes/unreleased/stress-model-fleet-mode.added.md b/changes/unreleased/stress-model-fleet-mode.added.md index 7834417376..489f49ba5e 100644 --- a/changes/unreleased/stress-model-fleet-mode.added.md +++ b/changes/unreleased/stress-model-fleet-mode.added.md @@ -1,4 +1,4 @@ -- **The satellite-network stress model can be generated as a fleet.** `cmd/stress-model -fleet` +- **The satellite-network stress model can be generated as a fleet.** `tools/cmd/stress-model -fleet` declares each orbital plane as occurrences of one of four spacecraft blocks — `part sats : BlockA[400] ordered` — with the as-built values as the block's defaults and stated only on the units that diverge, instead of one `part def` per satellite; the spacecraft, ground segment, @@ -6,8 +6,8 @@ are declared once over each collection with `[1]` ends rather than once per satellite pair. `-stats` now reports the spacecraft definitions and the units carrying values of their own in both forms, so the two can be compared: at 12 800 satellites the fleet declares 12 467 elements against - 2 354 827, and validates in 0.57 s and 175 MB rather than 301 s and 20.1 GB. A guide chapter, + 2 354 827, and validates in 0.70 s and 184 MB rather than 331 s and 20.3 GB. A guide chapter, `docs/guide/modeling-fleets.md`, shows the constellation both ways and what the runtime does with 12 800 occurrences, and the stress-test record and performance notes carry the - measurements. `BenchmarkFleetInstantiate` and `BenchmarkFleetSatisfy` in `internal/stressmodel` + measurements. `BenchmarkFleetInstantiate` and `BenchmarkFleetSatisfy` in `tests/stressmodel` time the runtime over the fleet form. diff --git a/docs/guide/modeling-fleets.md b/docs/guide/modeling-fleets.md index d8caee881b..b02cde5c6c 100644 --- a/docs/guide/modeling-fleets.md +++ b/docs/guide/modeling-fleets.md @@ -128,7 +128,7 @@ write diverging units as above and keep the variant's values as defaults. ## The stress-test constellation, both ways -`internal/stressmodel` (`cmd/stress-model`) generates the +`tests/stressmodel` (`tools/cmd/stress-model`) generates the [satellite-network stress test](../project/satellite-network-stress-test.md) in both forms: `-fleet` selects the fleet form. Both state the same spacecraft — seven subsystems, twenty components with mass, power draw and @@ -204,10 +204,10 @@ satisfy blockAMass by network.plane0.unit16; declarations the source makes: ```bash -go run ./cmd/stress-model -planes 8 -satellites 200 -ground-stations 20 -stats > legacy.sysml +go run -C tools ./cmd/stress-model -planes 8 -satellites 200 -ground-stations 20 -stats > legacy.sysml # satellites=1600 definitions=1600 units=1600 ground-stations=20 components=32080 connections=25400 requirements=4800 elements=294627 bytes=18135413 -go run ./cmd/stress-model -planes 8 -satellites 200 -ground-stations 20 -fleet -stats > fleet.sysml -# satellites=1600 definitions=4 units=104 ground-stations=20 components=264 connections=220 requirements=12 elements=3203 bytes=191418 +go run -C tools ./cmd/stress-model -planes 8 -satellites 200 -ground-stations 20 -fleet -stats > fleet.sysml +# satellites=1600 definitions=4 units=104 ground-stations=20 components=264 connections=220 requirements=12 elements=3203 bytes=192698 ``` | satellites | planes × per plane | form | definitions | units stating values | elements | source | @@ -237,14 +237,14 @@ All figures below were taken on one machine — `Intel Xeon Platinum 8559C`, | satellites | form | elements | wall | allocated | peak RSS | | ---------- | ---- | -------- | ---- | --------- | -------- | -| 1 600 | one definition per satellite | 294 627 | 17.5 s | 5.5 GiB | 2.6 GB | -| 1 600 | fleet, 8 × 200 | 3 203 | 0.17 s | 93 MiB | 106 MB | -| 12 800 | one definition per satellite | 2 354 827 | 301 s | 43.5 GiB | 20.1 GB | -| 12 800 | fleet, 32 × 400 | 12 467 | 0.57 s | 254 MiB | 175 MB | +| 1 600 | one definition per satellite | 294 627 | 22.7 s | 6.2 GiB | 2.5 GB | +| 1 600 | fleet, 8 × 200 | 3 203 | 0.22 s | 102 MiB | 108 MB | +| 12 800 | one definition per satellite | 2 354 827 | 331 s | 49.8 GiB | 20.3 GB | +| 12 800 | fleet, 32 × 400 | 12 467 | 0.70 s | 289 MiB | 184 MB | Validation is a function of what the source declares, so the fleet form -validates the 12 800-satellite constellation in **0.57 s and 175 MB** where -the single-definition form takes 301 s and 20.1 GB. That is the whole +validates the 12 800-satellite constellation in **0.70 s and 184 MB** where +the single-definition form takes 331 s and 20.3 GB. That is the whole payoff of writing the model this way, and it is available today. ## What the runtime does with 12 800 occurrences today @@ -258,17 +258,18 @@ between them. Measured on the same machine, same layouts as above: | satellites | operation | wall | allocated | peak RSS | | ---------- | --------- | ---- | --------- | -------- | -| 1 600 | `-instantiate` the network | 0.47 s | 220 MiB | 168 MB | -| 1 600 | `-satisfy`, 324 assertions | 0.95 s | 513 MiB | 269 MB | -| 12 800 | `-instantiate` the network | 2.34 s | 1.0 GiB | 692 MB | -| 12 800 | `-satisfy`, 2 412 assertions | 23.4 s | 14.4 GiB | 1.36 GB | -| 12 800 | `%eval` of `sats.dryMass` in every plane | 252 s | 73.8 GiB | 4.9 GB | +| 1 600 | `-instantiate` the network | 0.44 s | 238 MiB | 195 MB | +| 1 600 | `-satisfy`, 324 assertions | 0.71 s | 666 MiB | 306 MB | +| 1 600 | `%eval` of `sats.dryMass` in every plane | 1.85 s | 2.9 GiB | 737 MB | +| 12 800 | `-instantiate` the network | 2.06 s | 1.1 GiB | 801 MB | +| 12 800 | `-satisfy`, 2 412 assertions | 8.84 s | 23.4 GiB | 1.49 GB | +| 12 800 | `%eval` of `sats.dryMass` in every plane | 42.7 s | 141.3 GiB | 5.2 GB | What the rows say about the current runtime: - **Instantiating** the network (`sysml -instantiate SatelliteNetwork::Constellation::network`) creates the object per - occurrence in every plane, 2.34 s and 692 MB — about 50 KB per + occurrence in every plane, 2.06 s and 801 MB — about 60 KB per occurrence, linear from 1 600 to 12 800. The run then warns that materialization is bounded: the walk that reads the created object's feature values stops at the runtime's materialization budget, so the @@ -278,18 +279,15 @@ What the rows say about the current runtime: evaluates its summed mass and power, which materializes the unit's subsystems and components and starts their behaviors. Every check then drains the behaviors the network's objects run, so a check costs more the - more of the fleet earlier checks have touched: 0.9 MiB allocated per - assertion in a network of one plane of 400, 6 MiB in one of 32 planes. A - CPU profile of the 16-plane check spends 57% evaluating the requirements' - expressions (41% of the total in starting the behaviors of the parts that - evaluation materializes) and 31% polling running state machines for due - events. The 2 412 assertions of the 12 800-satellite fleet cost 23.4 s and - 14.4 GiB allocated, against 83 s and 28.9 GiB for the 9 600 assertions of - a 3 200-satellite single-definition constellation; each assertion still + more of the fleet earlier checks have touched: 2 MiB allocated per + assertion in a network of 8 planes, 10 MiB in one of 32 planes. The 2 412 + assertions of the 12 800-satellite fleet cost 8.84 s and 23.4 GiB + allocated, against 83 s and 28.9 GiB for the 9 600 assertions of a + 3 200-satellite single-definition constellation; each assertion still pays for the fleet around it. - **Reading a value over every occurrence** — the dry mass of all 12 800 satellites — evaluates the summed expression over the full component tree - of every occurrence, 252 s and 73.8 GiB allocated. This is the cost the + of every occurrence, 42.7 s and 141.3 GiB allocated. This is the cost the single-definition form paid at validation; the fleet form pays it at the first read instead. - A connector over the collection is realized as **one link whose ends hold diff --git a/docs/internals/performance.md b/docs/internals/performance.md index 829ac576b5..c9b3072252 100644 --- a/docs/internals/performance.md +++ b/docs/internals/performance.md @@ -179,19 +179,19 @@ doubling the model roughly quadrupled the time — for the reasons below. Because the cost is per declared element, the largest lever a model has is to declare less: one definition with a multiplicity rather than a definition per unit. The satellite-network generator writes its constellation both ways -(`cmd/stress-model -fleet`), and on the machine named above — 8 CPUs, 31 GiB, +(`tools/cmd/stress-model -fleet`), and on the machine named above — 8 CPUs, 31 GiB, no swap — `sysml -validate -memstats` of the 12 800-satellite constellation costs: | form | elements | source | wall | allocated | peak RSS | | ---- | -------- | ------ | ---- | --------- | -------- | -| one `part def` per satellite, 32 planes of 400 | 2 354 827 | 145 MB | 301 s | 43.5 GiB | 20.1 GB | -| four blocks, `part sats : Block[400]` in 32 planes | 12 467 | 771 KB | 0.57 s | 254 MiB | 175 MB | +| one `part def` per satellite, 32 planes of 400 | 2 354 827 | 145 MB | 331 s | 49.8 GiB | 20.3 GB | +| four blocks, `part sats : Block[400]` in 32 planes | 12 467 | 771 KB | 0.70 s | 289 MiB | 184 MB | The runtime then pays for the occurrences when something asks for them: the -same network instantiates in 2.34 s and 692 MB, its 2 412 `satisfy` -assertions check in 23.4 s and 14.4 GiB allocated, and reading one summed -attribute over every occurrence costs 252 s and 73.8 GiB, because each +same network instantiates in 2.06 s and 801 MB, its 2 412 `satisfy` +assertions check in 8.84 s and 23.4 GiB allocated, and reading one summed +attribute over every occurrence costs 42.7 s and 141.3 GiB, because each occurrence is still an object with a value slot per feature whose component tree is materialized to evaluate it. Both forms, their element counts and what the runtime does with 12 800 occurrences are in the diff --git a/docs/project/satellite-network-stress-test.md b/docs/project/satellite-network-stress-test.md index b8a147aff7..9c9ff08fb5 100644 --- a/docs/project/satellite-network-stress-test.md +++ b/docs/project/satellite-network-stress-test.md @@ -198,18 +198,18 @@ The guide chapter [modeling fleets](../guide/modeling-fleets.md) shows the source of both forms. ```bash -go run ./cmd/stress-model -planes 32 -satellites 400 -ground-stations 20 -stats > legacy.sysml +go run -C tools ./cmd/stress-model -planes 32 -satellites 400 -ground-stations 20 -stats > legacy.sysml # satellites=12800 definitions=12800 units=12800 ground-stations=20 components=256080 connections=204400 requirements=38400 elements=2354827 bytes=145364954 -go run ./cmd/stress-model -planes 32 -satellites 400 -ground-stations 20 -fleet -stats > fleet.sysml +go run -C tools ./cmd/stress-model -planes 32 -satellites 400 -ground-stations 20 -fleet -stats > fleet.sysml # satellites=12800 definitions=4 units=800 ground-stations=20 components=960 connections=724 requirements=12 elements=12467 bytes=770621 ``` | satellites | planes × per plane | form | definitions | units | elements | source | `-validate` wall | allocated | peak RSS | | ---------- | ------------------ | ---- | ----------- | ----- | -------- | ------ | ---------------- | --------- | -------- | -| 1 600 | 8 × 200 | one definition per satellite | 1 600 | 1 600 | 294 627 | 18.1 MB | 17.5 s | 5.5 GiB | 2.6 GB | -| 1 600 | 8 × 200 | fleet | 4 | 104 | 3 203 | 193 KB | 0.17 s | 93 MiB | 106 MB | -| 12 800 | 32 × 400 | one definition per satellite | 12 800 | 12 800 | 2 354 827 | 145 MB | 301 s | 43.5 GiB | 20.1 GB | -| 12 800 | 32 × 400 | fleet | 4 | 800 | 12 467 | 771 KB | 0.57 s | 254 MiB | 175 MB | +| 1 600 | 8 × 200 | one definition per satellite | 1 600 | 1 600 | 294 627 | 18.1 MB | 22.7 s | 6.2 GiB | 2.5 GB | +| 1 600 | 8 × 200 | fleet | 4 | 104 | 3 203 | 193 KB | 0.22 s | 102 MiB | 108 MB | +| 12 800 | 32 × 400 | one definition per satellite | 12 800 | 12 800 | 2 354 827 | 145 MB | 331 s | 49.8 GiB | 20.3 GB | +| 12 800 | 32 × 400 | fleet | 4 | 800 | 12 467 | 771 KB | 0.70 s | 289 MiB | 184 MB | The single-definition rows here are the plane and station layout the fleet uses, so the two forms describe the same planes and stations; the validation table above @@ -217,7 +217,7 @@ uses, so the two forms describe the same planes and stations; the validation tab with a different split into planes and stations, and so slightly more links and station components. The fleet form declares **190 times fewer elements** at 12 800 satellites and validates in -0.57 s and 175 MB rather than 301 s and 20.1 GB: validation is a function of +0.70 s and 184 MB rather than 331 s and 20.3 GB: validation is a function of what the source declares, and the fleet source is the size of four spacecraft, twenty stations and the links between thirty-two planes. @@ -226,27 +226,26 @@ machine: | satellites | operation | wall | allocated | peak RSS | | ---------- | --------- | ---- | --------- | -------- | -| 1 600 | `-instantiate` the network | 0.47 s | 220 MiB | 168 MB | -| 1 600 | `-satisfy`, 324 assertions | 0.95 s | 513 MiB | 269 MB | -| 12 800 | `-instantiate` the network | 2.34 s | 1.0 GiB | 692 MB | -| 12 800 | `-satisfy`, 2 412 assertions | 23.4 s | 14.4 GiB | 1.36 GB | -| 12 800 | `%eval` of `plane.sats.dryMass`, all 32 planes | 252 s | 73.8 GiB | 4.9 GB | +| 1 600 | `-instantiate` the network | 0.44 s | 238 MiB | 195 MB | +| 1 600 | `-satisfy`, 324 assertions | 0.71 s | 666 MiB | 306 MB | +| 1 600 | `%eval` of `plane.sats.dryMass`, all 8 planes | 1.85 s | 2.9 GiB | 737 MB | +| 12 800 | `-instantiate` the network | 2.06 s | 1.1 GiB | 801 MB | +| 12 800 | `-satisfy`, 2 412 assertions | 8.84 s | 23.4 GiB | 1.49 GB | +| 12 800 | `%eval` of `plane.sats.dryMass`, all 32 planes | 42.7 s | 141.3 GiB | 5.2 GB | The runtime shares one shape — the effective feature list `FeaturesOf` caches per type — between the occurrences of a block, and nothing else: each occurrence is an object with a value slot per feature, materialized lazily. -Instantiating the network is therefore linear and cheap (about 50 KB per +Instantiating the network is therefore linear and cheap (about 60 KB per occurrence; the walk of the created object's feature values stops at the materialization budget and says so). Checking is not: a `satisfy` on a unit reads the unit through the network object, evaluates its summed mass and power — materializing its subsystems and components and starting their behaviors — and then drains the behaviors every object of the network runs, so each check costs more the more of the fleet earlier checks have touched -(0.9 MiB allocated per assertion in a network of one plane of 400, 6 MiB in -one of 32 planes). A CPU profile of the 16-plane `-satisfy` spends 57% of -its samples evaluating the requirements' expressions, 41% of the total under -`startClassifierBehaviors` for the parts that evaluation materializes, and -31% in `ObjectBehavior.hasPendingWork` / `StateExecutor.hasDueEvent` +(2 MiB allocated per assertion in a network of 8 planes, 10 MiB in one of +32 planes): the cost is in evaluating the requirements' expressions, in +starting the behaviors of the parts that evaluation materializes, and in polling the running mode machines. Reading one summed attribute over every occurrence evaluates it over the full tree of each — the cost the single-definition form paid at validation, paid here at the first read. @@ -275,22 +274,23 @@ Three limits of the current language and runtime shape the fleet form: infinite`. The 12 800-satellite fleet is therefore 32 planes of 400. `BenchmarkFleetInstantiate` and `BenchmarkFleetSatisfy` in -`internal/stressmodel` measure, warm, instantiating the fleet network and +`tests/stressmodel` measure, warm, instantiating the fleet network and reading `sats.dryMass` over four planes, and re-checking every assertion: ```bash -go test ./internal/stressmodel -run '^$' -bench Fleet -benchmem -benchtime 3x +go test ./tests/stressmodel -run '^$' -bench Fleet -benchmem -benchtime 3x ``` | satellites | elements | instantiate + read four planes | per satellite | allocated | assertions | warm re-check | allocated | | ---------- | -------- | ------------------------------ | ------------- | --------- | ---------- | ------------- | --------- | -| 32 | 1 179 | 74 ms | 2.3 ms | 20.3 MiB | 24 | 0.8 ms | 0.5 MiB | -| 128 | 1 715 | 268 ms | 2.1 ms | 83.0 MiB | 36 | 1.4 ms | 1.1 MiB | -| 512 | 3 947 | 1.43 s | 2.8 ms | 579 MiB | 108 | 6.4 ms | 7.4 MiB | +| 32 | 1 179 | 29 ms | 0.9 ms | 18.4 MiB | 24 | 0.9 ms | 0.5 MiB | +| 128 | 1 715 | 87 ms | 0.7 ms | 93.1 MiB | 36 | 1.2 ms | 1.0 MiB | +| 512 | 3 947 | 460 ms | 0.9 ms | 882 MiB | 108 | 8.5 ms | 7.3 MiB | Warm, instantiating a fleet and reading a summed attribute over its -occurrences costs **about 2 ms and 1 MiB per satellite** — the per-satellite -cost of a cold `-satisfy` over the single-definition form — because every +occurrences costs **about 1 ms and 1.7 MiB per satellite** — of the order +of the per-satellite cost of a cold `-satisfy` over the single-definition +form — because every occurrence's component tree is still materialized to evaluate the sum. What would change that is sparse per-occurrence values and verification over distinct shapes ([scaling to very large models](large-model-scaling-design.md), From 48951ff807963638c3451d4cce3ce22c6c7bd190 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Fri, 25 Sep 2026 21:12:32 +0000 Subject: [PATCH 11/11] feat(stressmodel): count satisfy assertions apart from requirement usages Co-Authored-By: jason.han --- .../stress-model-fleet-mode.added.md | 4 ++-- docs/guide/modeling-fleets.md | 4 ++-- docs/project/satellite-network-stress-test.md | 12 +++++----- tests/stressmodel/bench_test.go | 4 ++-- tests/stressmodel/satnet.go | 6 ++++- tests/stressmodel/satnet_test.go | 22 +++++++++---------- tools/cmd/stress-model/main.go | 4 ++-- 7 files changed, 31 insertions(+), 25 deletions(-) diff --git a/changes/unreleased/stress-model-fleet-mode.added.md b/changes/unreleased/stress-model-fleet-mode.added.md index 489f49ba5e..b2a051eb09 100644 --- a/changes/unreleased/stress-model-fleet-mode.added.md +++ b/changes/unreleased/stress-model-fleet-mode.added.md @@ -4,8 +4,8 @@ units that diverge, instead of one `part def` per satellite; the spacecraft, ground segment, requirements and state machine are unchanged, and the ring, inter-plane and downlink connectors are declared once over each collection with `[1]` ends rather than once per satellite pair. `-stats` - now reports the spacecraft definitions and the units carrying values of their own in both forms, - so the two can be compared: at 12 800 satellites the fleet declares 12 467 elements against + now reports the spacecraft definitions, the units carrying values of their own and the satisfy + assertions in both forms, so the two can be compared: at 12 800 satellites the fleet declares 12 467 elements against 2 354 827, and validates in 0.70 s and 184 MB rather than 331 s and 20.3 GB. A guide chapter, `docs/guide/modeling-fleets.md`, shows the constellation both ways and what the runtime does with 12 800 occurrences, and the stress-test record and performance notes carry the diff --git a/docs/guide/modeling-fleets.md b/docs/guide/modeling-fleets.md index b02cde5c6c..cbf939aa9b 100644 --- a/docs/guide/modeling-fleets.md +++ b/docs/guide/modeling-fleets.md @@ -205,9 +205,9 @@ declarations the source makes: ```bash go run -C tools ./cmd/stress-model -planes 8 -satellites 200 -ground-stations 20 -stats > legacy.sysml -# satellites=1600 definitions=1600 units=1600 ground-stations=20 components=32080 connections=25400 requirements=4800 elements=294627 bytes=18135413 +# satellites=1600 definitions=1600 units=1600 ground-stations=20 components=32080 connections=25400 requirements=4800 assertions=4800 elements=294627 bytes=18135413 go run -C tools ./cmd/stress-model -planes 8 -satellites 200 -ground-stations 20 -fleet -stats > fleet.sysml -# satellites=1600 definitions=4 units=104 ground-stations=20 components=264 connections=220 requirements=12 elements=3203 bytes=192698 +# satellites=1600 definitions=4 units=104 ground-stations=20 components=264 connections=220 requirements=12 assertions=324 elements=3203 bytes=192698 ``` | satellites | planes × per plane | form | definitions | units stating values | elements | source | diff --git a/docs/project/satellite-network-stress-test.md b/docs/project/satellite-network-stress-test.md index 9c9ff08fb5..7c1733c2e1 100644 --- a/docs/project/satellite-network-stress-test.md +++ b/docs/project/satellite-network-stress-test.md @@ -19,7 +19,7 @@ smallest models carry ±30% of noise from the machine, which the trend does not. ```bash go run -C tools ./cmd/stress-model -planes 8 -satellites 25 -ground-stations 20 -stats > constellation.sysml -# satellites=200 ground-stations=20 components=4080 connections=3175 requirements=600 elements=37552 bytes=2297852 +# satellites=200 definitions=200 units=200 ground-stations=20 components=4080 connections=3175 requirements=600 assertions=600 elements=37552 bytes=2297852 sysml -validate -memstats constellation.sysml sysml -satisfy -memstats constellation.sysml ``` @@ -192,16 +192,18 @@ planes and one downlink per plane and station — the collection connectors with `[1]` ends, so each link joins one satellite to one satellite or station, though not which to which — and the three requirements declared once per block and asserted on the block's configuration and on -every diverging unit. `-stats` reports both forms alike; the two new fields -are the spacecraft definitions and the units that state values of their own. +every diverging unit. `-stats` reports both forms alike; the new fields are +the spacecraft definitions, the units that state values of their own, and the +satisfy assertions, which in the fleet form outnumber the requirements by +three per unit. The guide chapter [modeling fleets](../guide/modeling-fleets.md) shows the source of both forms. ```bash go run -C tools ./cmd/stress-model -planes 32 -satellites 400 -ground-stations 20 -stats > legacy.sysml -# satellites=12800 definitions=12800 units=12800 ground-stations=20 components=256080 connections=204400 requirements=38400 elements=2354827 bytes=145364954 +# satellites=12800 definitions=12800 units=12800 ground-stations=20 components=256080 connections=204400 requirements=38400 assertions=38400 elements=2354827 bytes=145364954 go run -C tools ./cmd/stress-model -planes 32 -satellites 400 -ground-stations 20 -fleet -stats > fleet.sysml -# satellites=12800 definitions=4 units=800 ground-stations=20 components=960 connections=724 requirements=12 elements=12467 bytes=770621 +# satellites=12800 definitions=4 units=800 ground-stations=20 components=960 connections=724 requirements=12 assertions=2412 elements=12467 bytes=770621 ``` | satellites | planes × per plane | form | definitions | units | elements | source | `-validate` wall | allocated | peak RSS | diff --git a/tests/stressmodel/bench_test.go b/tests/stressmodel/bench_test.go index 1e9975213a..24c39af2f7 100644 --- a/tests/stressmodel/bench_test.go +++ b/tests/stressmodel/bench_test.go @@ -70,7 +70,7 @@ func BenchmarkLoad(b *testing.B) { func BenchmarkSatisfy(b *testing.B) { for _, n := range networkSizes { src, stats := network(n).Source() - b.Run(fmt.Sprintf("satellites=%d/assertions=%d", stats.Satellites, stats.Requirements), func(b *testing.B) { + b.Run(fmt.Sprintf("satellites=%d/assertions=%d", stats.Satellites, stats.Assertions), func(b *testing.B) { sess := loadNetwork(b, src) check := func() { for _, v := range sess.CheckSatisfy("") { @@ -134,7 +134,7 @@ func BenchmarkFleetInstantiate(b *testing.B) { func BenchmarkFleetSatisfy(b *testing.B) { for _, n := range networkSizes { src, stats := fleet(n).Source() - assertions := 3 * (stats.Definitions + stats.Units) + assertions := stats.Assertions b.Run(fmt.Sprintf("satellites=%d/assertions=%d", stats.Satellites, assertions), func(b *testing.B) { sess := loadNetwork(b, src) check := func() { diff --git a/tests/stressmodel/satnet.go b/tests/stressmodel/satnet.go index a7375789bd..7d53b6e9ed 100644 --- a/tests/stressmodel/satnet.go +++ b/tests/stressmodel/satnet.go @@ -54,8 +54,10 @@ type Stats struct { Components int // Connections is the number of interface usages, inside satellites and between them. Connections int - // Requirements is the number of requirement usages, each with a satisfy assertion. + // Requirements is the number of requirement usages; Assertions the number of + // satisfy assertions, one per requirement plus one per diverging unit in fleet form. Requirements int + Assertions int // Elements is the number of declarations the model makes, library included. Elements int // Bytes is the length of the generated source. @@ -514,6 +516,7 @@ func (g *generator) spacecraftBody(id int, valued string) { // named config, with their satisfy assertions, under names prefixed by name. func (g *generator) requirements(name, config string, id int) { g.stats.Requirements += 3 + g.stats.Assertions += 3 g.decl(2, "requirement %sMass : MassBudget { subject :>> sc = %s; attribute :>> limit = %d [kg]; }", name, config, 900+id%100) g.stats.Elements += 2 g.decl(2, "satisfy %sMass by %s;", name, config) @@ -594,6 +597,7 @@ func (g *generator) fleetBody(n SatelliteNetwork) { for p := 0; p < n.Planes; p++ { for s := 0; s < n.Satellites; s += fleetUnitStride { for _, req := range []string{"Mass", "Power", "Crosslink"} { + g.stats.Assertions++ g.decl(2, "satisfy block%s%s by network.plane%d.unit%d;", blockName(p%blocks), req, p, s) } } diff --git a/tests/stressmodel/satnet_test.go b/tests/stressmodel/satnet_test.go index 010bd3a783..f766b81871 100644 --- a/tests/stressmodel/satnet_test.go +++ b/tests/stressmodel/satnet_test.go @@ -18,8 +18,8 @@ func TestSatelliteNetworkValidates(t *testing.T) { if stats.Satellites != 4 || stats.GroundStations != 1 { t.Fatalf("stats = %+v, want 4 satellites and 1 station", stats) } - if stats.Requirements != 3*stats.Satellites { - t.Errorf("Requirements = %d, want three per satellite", stats.Requirements) + if stats.Requirements != 3*stats.Satellites || stats.Assertions != stats.Requirements { + t.Errorf("Requirements = %d, Assertions = %d, want three per satellite", stats.Requirements, stats.Assertions) } if stats.Bytes != len(src) { t.Errorf("Bytes = %d, want %d", stats.Bytes, len(src)) @@ -31,8 +31,8 @@ func TestSatelliteNetworkValidates(t *testing.T) { t.Errorf("diagnostic: %s", d.Message) } verdicts := s.CheckSatisfy("") - if len(verdicts) != stats.Requirements { - t.Fatalf("got %d satisfy verdicts, want %d", len(verdicts), stats.Requirements) + if len(verdicts) != stats.Assertions { + t.Fatalf("got %d satisfy verdicts, want %d", len(verdicts), stats.Assertions) } for _, v := range verdicts { if !v.Holds() { @@ -74,8 +74,8 @@ func TestFleetValidates(t *testing.T) { if stats.Definitions != 2 || stats.Units != 4 { t.Errorf("stats = %+v, want 2 blocks and 4 diverging units", stats) } - if stats.Requirements != 3*stats.Definitions { - t.Errorf("Requirements = %d, want three per block", stats.Requirements) + if stats.Requirements != 3*stats.Definitions || stats.Assertions != 3*(stats.Definitions+stats.Units) { + t.Errorf("Requirements = %d, Assertions = %d, want three per block and three more per unit", stats.Requirements, stats.Assertions) } if stats.Bytes != len(src) { t.Errorf("Bytes = %d, want %d", stats.Bytes, len(src)) @@ -97,7 +97,7 @@ func TestFleetValidates(t *testing.T) { t.Errorf("diagnostic: %s", d.Message) } verdicts := s.CheckSatisfy("") - if want := 3 * (stats.Definitions + stats.Units); len(verdicts) != want { + if want := stats.Assertions; len(verdicts) != want { t.Fatalf("got %d satisfy verdicts, want %d", len(verdicts), want) } for _, v := range verdicts { @@ -164,10 +164,10 @@ func TestSatelliteNetworkFilesValidate(t *testing.T) { t.Fatalf("got %d files, want the library, %d planes and the network", len(files), n.Planes) } _, whole := n.Source() - if stats.Satellites != whole.Satellites || stats.Requirements != whole.Requirements || stats.Connections != whole.Connections { + if stats.Satellites != whole.Satellites || stats.Assertions != whole.Assertions || stats.Connections != whole.Connections { t.Fatalf("split stats %+v, single-file stats %+v", stats, whole) } - validateFiles(t, files, stats.Requirements) + validateFiles(t, files, stats.Assertions) } // TestFleetFilesValidate keeps the split fleet form in step with the whole one: @@ -181,10 +181,10 @@ func TestFleetFilesValidate(t *testing.T) { } _, whole := n.Source() if stats.Elements != whole.Elements || stats.Definitions != whole.Definitions || stats.Units != whole.Units || - stats.Satellites != whole.Satellites || stats.Requirements != whole.Requirements || stats.Connections != whole.Connections { + stats.Satellites != whole.Satellites || stats.Assertions != whole.Assertions || stats.Connections != whole.Connections { t.Fatalf("split stats %+v, single-file stats %+v", stats, whole) } - validateFiles(t, files, 3*(stats.Definitions+stats.Units)) + validateFiles(t, files, stats.Assertions) } // validateFiles opens files as one workspace and one session, wanting no diff --git a/tools/cmd/stress-model/main.go b/tools/cmd/stress-model/main.go index f84be049d3..6daf778bad 100644 --- a/tools/cmd/stress-model/main.go +++ b/tools/cmd/stress-model/main.go @@ -36,7 +36,7 @@ func main() { os.Exit(1) } if *stats { - fmt.Fprintf(os.Stderr, "satellites=%d definitions=%d units=%d ground-stations=%d components=%d connections=%d requirements=%d elements=%d bytes=%d\n", - s.Satellites, s.Definitions, s.Units, s.GroundStations, s.Components, s.Connections, s.Requirements, s.Elements, s.Bytes) + fmt.Fprintf(os.Stderr, "satellites=%d definitions=%d units=%d ground-stations=%d components=%d connections=%d requirements=%d assertions=%d elements=%d bytes=%d\n", + s.Satellites, s.Definitions, s.Units, s.GroundStations, s.Components, s.Connections, s.Requirements, s.Assertions, s.Elements, s.Bytes) } }