feat(stressmodel): generate the satellite network as a fleet of occurrences

changes/unreleased/stress-model-fleet-mode.added.md

@@ -0,0 +1,13 @@
+- **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,
+  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, 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
+  measurements. `BenchmarkFleetInstantiate` and `BenchmarkFleetSatisfy` in `tests/stressmodel`
+  time the runtime over the fleet form.

docs/guide/README.md

@@ -14,6 +14,11 @@ Read the chapters in order the first time through; each one builds on the ones b
 10. [Troubleshooting](10-troubleshooting.md) — diagnosing a run that stops early
 11. [Migrating a SysML v1 model](11-migrating-from-sysml-v1.md) — `-convert` from XMI, reading the report, finishing by hand
 
+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.

docs/guide/modeling-fleets.md

@@ -0,0 +1,317 @@
+# 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 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
+
+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
+
+`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
+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 — 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
+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 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 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 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 {
+    attribute plane : Integer;
+    part sats : Spacecraft[400] ordered;
+    interface ring : RFLink connect [1] sats.comms.crosslinkTx to [1] 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 [1] plane0.sats.comms.crosslinkTx to [1] plane1.sats.comms.crosslinkRx;
+    interface downlink0To0 : RFLink connect [1] plane0.sats.comms.rf to [1] 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 -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 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 assertions=324 elements=3203 bytes=192698
+```
+
+| 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 | 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 | 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
+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 | 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.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
+
+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.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.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
+  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: 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, 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
+  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
+  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 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.

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
+(`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 | 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.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
+[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