From 2f8e723be9b5ae8e147b143ee1bf010ab8d67f1e Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Wed, 9 Sep 2026 17:33:52 +0000 Subject: [PATCH 01/33] docs(examples): add expression feature walkthrough Add examples/expressions-demo.sysml and its walkthrough EXPRESSIONS-DEMO.md, taking casts, the unbounded value, .metadata, function values, sets, rank-three tensors and typed collection bodies through one payload model, and give each a section with REPL transcripts in the guide's expressions chapter. Pin the new example as stable in the RDF round-trip ratchet and re-record the examples count and digest in the differential baseline. Co-Authored-By: jason.han --- .../expression-features-guide.added.md | 1 + docs/guide/05-checking.md | 226 +++++++++++- docs/project/pilot-differential-baseline.json | 4 +- docs/project/rdf-corpus-roundtrip.md | 8 +- examples/EXPRESSIONS-DEMO.md | 331 ++++++++++++++++++ examples/README.md | 1 + examples/expressions-demo.sysml | 153 ++++++++ .../testdata/corpus_roundtrip_expected.txt | 3 +- 8 files changed, 719 insertions(+), 8 deletions(-) create mode 100644 changes/unreleased/expression-features-guide.added.md create mode 100644 examples/EXPRESSIONS-DEMO.md create mode 100644 examples/expressions-demo.sysml diff --git a/changes/unreleased/expression-features-guide.added.md b/changes/unreleased/expression-features-guide.added.md new file mode 100644 index 000000000..2d9f25cfc --- /dev/null +++ b/changes/unreleased/expression-features-guide.added.md @@ -0,0 +1 @@ +- **A worked example of the expression forms.** `examples/expressions-demo.sysml` and its walkthrough `examples/EXPRESSIONS-DEMO.md` take `as` casts, the unbounded value `*`, `.metadata`, function values, `Collections::Set`, rank-three tensor quantities and typed collection bodies through one payload model, and the guide's expressions chapter (`docs/guide/05-checking.md`) gains sections on each with REPL transcripts. diff --git a/docs/guide/05-checking.md b/docs/guide/05-checking.md index 42d7d7487..6d979d90c 100644 --- a/docs/guide/05-checking.md +++ b/docs/guide/05-checking.md @@ -93,6 +93,166 @@ part System { } ``` +## Casts, the unbounded value and metadata + +**Casts:** `x as T` selects rather than converts. It yields `x` where `T` classifies the value `x` +is, and the empty sequence where it does not; a sequence is cast element by element, keeping the +elements `T` classifies in their order. A whole Real *is* an Integer in the `ScalarValues` +hierarchy, so `4.0 as Integer` keeps `4.0` (the conversions, `ToInteger` and its kin, are library +functions). An object is kept by every classifier it is an instance of, its type's generalizations +included. + +```sysml +sysml> package Payload { + ...> private import ScalarValues::*; + ...> part def Instrument; + ...> part def Camera :> Instrument; + ...> part navCam : Camera; + ...> part probe : Instrument; + ...> ref part cameras : Camera[0..*] = (navCam, probe) as Camera; + ...> attribute whole : Integer[0..*] = (1.0, 2.5, 3.0) as Integer; + ...> } +✓ package Payload + +sysml> %eval Payload::whole +✓ Payload::whole + = [1.0, 3.0] + +sysml> %eval Payload::cameras +✓ Payload::cameras + = [Instance(ID: 1)] + +sysml> %eval 2.5 as ScalarValues::Integer +✓ 2.5 as ScalarValues::Integer + = [] +``` + +Declare a feature that holds a cast result `[0..1]` or `[0..*]`: a cast that selects nothing is +empty, which a feature of multiplicity `[1]` cannot hold. The checker warns where a cast can only +be empty because the operand's type and the target are unrelated. + +**The unbounded value:** `*` is a value of its own, not a large number. It exceeds every finite +number, equals itself and prints as `*`; arithmetic over it is refused with an error naming the +operator. + +```sysml +sysml> package Budget { + ...> private import ScalarValues::*; + ...> attribute passLimit : Natural = *; + ...> attribute withinLimit : Boolean = 40 < passLimit; + ...> } +✓ package Budget + +sysml> %eval Budget::withinLimit +✓ Budget::withinLimit + = true + +sysml> %eval * + 1 +error: evaluation failed: type mismatch: operator '+' is not defined for the unbounded value '*': * + 1 +``` + +**Metadata:** `elem.metadata` is the sequence of metadata annotating `elem`, one object per +annotation in the order written, each carrying the values its body binds over the defaults its +`metadata def` declares. An element with no annotation answers the empty sequence. + +```sysml +sysml> package Provenance { + ...> private import ScalarValues::*; + ...> metadata def Heritage { attribute mission : String; attribute flown : Boolean = true; } + ...> part def Camera; + ...> part navCam : Camera { @Heritage { mission = "Cassini"; } } + ...> part sciCam : Camera; + ...> } +✓ package Provenance + +sysml> %eval Provenance::navCam.metadata#(1).mission +✓ Provenance::navCam.metadata#(1).mission + = "Cassini" + +sysml> %eval Provenance::navCam.metadata#(1).flown +✓ Provenance::navCam.metadata#(1).flown + = true + +sysml> %eval Provenance::sciCam.metadata +✓ Provenance::sciCam.metadata + = [] +``` + +## Sets and tensors + +**Sets:** the library declares the elements of a `Collections::Set` unique and unordered, so a +`Set` holds a set: the elements it was given with every repeat dropped and no order of its own. +Two sets holding the same elements are equal however they were written, and a set prints as +`Set{…}` in a canonical order. `Bag` and `OrderedSet` keep their repeats or their order, and are +sequences. + +```sysml +sysml> package Bands { + ...> private import ScalarValues::*; + ...> private import Collections::*; + ...> private import CollectionFunctions::*; + ...> attribute requested : Set { :>> elements = ("X", "Ka", "X", "S"); } + ...> attribute licensed : Set { :>> elements = ("S", "X", "Ka"); } + ...> attribute same : Boolean = requested == licensed; + ...> } +✓ package Bands + +sysml> %instantiate Bands::requested +✓ Created instance of Bands::requested + ID: 1 + Use %features Bands::requested to inspect + +sysml> %features Bands::requested +Instance: Bands::requested (ID: 1) +Features: + elements = Set{"Ka", "S", "X"} + +sysml> %eval Bands::same +✓ Bands::same + = true + +sysml> %eval CollectionFunctions::size(Bands::requested) +✓ CollectionFunctions::size(Bands::requested) + = 3 +``` + +**Tensors:** a `TensorQuantityValue` of any rank is built by `TensorCalculations::'['` from a flat +sequence of numbers and a `TensorMeasurementReference` whose `dimensions` give the shape, in +row-major order with the last index varying fastest. `#` takes one index per dimension, counted +from 1, and refuses an index outside the shape or the wrong number of them; `+`, `-` and the +scalar multiplications keep the shape component by component. + +```sysml +sysml> package Stress { + ...> private import ScalarValues::*; + ...> private import ISQ::*; + ...> private import SI::*; + ...> private import Quantities::*; + ...> private import MeasurementReferences::*; + ...> private import TensorCalculations::*; + ...> attribute ref3 : TensorMeasurementReference { + ...> :>> dimensions = (2, 2, 2); + ...> :>> mRefs = (Pa, Pa, Pa, Pa, Pa, Pa, Pa, Pa); + ...> } + ...> attribute field : TensorQuantityValue = '['((1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0), ref3); + ...> attribute cell = field#(2, 1, 1); + ...> attribute rank = field.order; + ...> } +✓ package Stress + +sysml> %eval Stress::field +✓ Stress::field + = Tensor(2, 2, 2)[1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0] [Pa] + +sysml> %eval Stress::cell +✓ Stress::cell + = 5.0 [Pa] + +sysml> %eval Stress::rank +✓ Stress::rank + = 3 +``` + ## Calculations, constraints and requirements **Calculations:** @@ -152,6 +312,68 @@ A `calc` the model declares under a library function's name is what a call resol the library is also imported. `%builtins` lists every function the build evaluates, each with the package an `import` must name for its bare name to resolve. +**Calculations as values:** + +A `calc def`, a `calc` usage or an `in calc` parameter named where a value is expected is a +*function value*: the calculation, together with whatever it closes over. It is passed as an +argument, held in a feature, compared with `==`, and invoked by the parameter that receives it; +reading it on its own answers the function, named by its declaration. + +```sysml +sysml> package Gains { + ...> private import ScalarValues::*; + ...> calc def Square { in v : Real; return : Real = v * v; } + ...> calc def Apply { in calc f { in v : Real; return : Real; } in a : Real; return : Real = f(a); } + ...> } +✓ package Gains + +sysml> %calc Gains::Apply(Gains::Square, 3.0) +✓ Gains::Apply(Gains::Square, 3.0) + = 9.0 + +sysml> %eval Gains::Square +✓ Gains::Square + = Gains::Square +``` + +A `calc def` is a definition, not a feature, so it is passed as an argument or referenced through +a `calc` usage rather than bound directly as a feature's value. A nested `calc` closes over the +features around it, and `SampledFunctions::Sample` from the analysis library takes a function value +and tabulates it over a domain. + +**Collection bodies:** + +`collect`, `select` and `reduce` (`ControlFunctions`) take a body whose parameter is bound to each +element in turn. A `collect` is typed by what its body returns, not by the element type of the +collection it ran over, so its result can be declared with the body's type and a mismatch is +reported before anything runs. + +```sysml +sysml> package Rollup { + ...> private import ScalarValues::*; + ...> private import ISQ::*; + ...> private import SI::*; + ...> private import ControlFunctions::*; + ...> part def Instrument { attribute mass : MassValue; } + ...> part navCam : Instrument { :>> mass = 4.0 [kg]; } + ...> part spectrometer : Instrument { :>> mass = 12.0 [kg]; } + ...> attribute masses : MassValue[0..*] = (navCam, spectrometer)->collect { in i : Instrument; i.mass }; + ...> attribute total : MassValue = masses->reduce { in a : MassValue; in b : MassValue; a + b }; + ...> } +✓ package Rollup + +sysml> %eval Rollup::total +✓ Rollup::total + = 16.0 [kg] + +sysml> package Rollup { + ...> attribute names : String[0..*] = (navCam, spectrometer)->collect { in i : Instrument; i.mass }; + ...> } +1:35: error: cannot bind a value of type MassValue to a feature typed by String + attribute names : String[0..*] = (navCam, spectrometer)->collect { in i : Instrument; i.mass }; + ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +``` + **Constraints:** ```sysml sysml> constraint ValidSpeed { @@ -176,7 +398,9 @@ sysml> %requirement SafetyReq ``` For more examples, see -[examples/repl-behavioral-demo.sysml](../../examples/repl-behavioral-demo.sysml). +[examples/repl-behavioral-demo.sysml](../../examples/repl-behavioral-demo.sysml), and the +[expressions demo](../../examples/EXPRESSIONS-DEMO.md) for casts, `*`, `.metadata`, function +values, sets, tensors and collection bodies worked through one model. --- diff --git a/docs/project/pilot-differential-baseline.json b/docs/project/pilot-differential-baseline.json index b5b6f91bc..cb90aaeaa 100644 --- a/docs/project/pilot-differential-baseline.json +++ b/docs/project/pilot-differential-baseline.json @@ -60,8 +60,8 @@ "name": "examples", "dir": "examples", "origin": "ours", - "files": 33, - "digest": "sha256:6d94418e64c9b40adaeeb4575a17c77c55a4ca17a74a17ef42420a651fa9e993" + "files": 34, + "digest": "sha256:c2e816860b279abd662c6f411719b05147ee9a749a711d02fe01f892bbdfe0ef" }, { "name": "probes", diff --git a/docs/project/rdf-corpus-roundtrip.md b/docs/project/rdf-corpus-roundtrip.md index 2adeb359a..6235adbd0 100644 --- a/docs/project/rdf-corpus-roundtrip.md +++ b/docs/project/rdf-corpus-roundtrip.md @@ -9,7 +9,7 @@ pin in `scripts/pilot-pin.sh`. | Root | Files | |---|---| -| `committed` (everything under `examples/` outside the downloaded roots) | 33 | +| `committed` (everything under `examples/` outside the downloaded roots) | 34 | | `sysml-v2-training` | 100 | | `pilot-corpora/kerml-examples` | 58 | | `pilot-corpora/sysml-examples` | 99 | @@ -59,15 +59,15 @@ Recorded against the corpus above, reproduced byte-identically on a second run: | Verdict | Files | |---|---| -| `stable` | 346 | +| `stable` | 347 | | `whitespace-only` | 0 | | `graph-diff` | 0 | | `unwritable` | 0 | | `unparseable` | 0 | | `refused` | 0 | -| **total** | **346** | +| **total** | **347** | -So every one of the 346 files converts to Turtle, and every one comes back as the same Turtle byte +So every one of the 347 files converts to Turtle, and every one comes back as the same Turtle byte for byte. That is the source text at work: the decoder writes each file back from the `sysx:sourceText` it carries (see [What the gate does not do](#what-the-gate-does-not-do)), so the files that came back up to whitespace, as a different graph, or that could not be written back or diff --git a/examples/EXPRESSIONS-DEMO.md b/examples/EXPRESSIONS-DEMO.md new file mode 100644 index 000000000..cf754d532 --- /dev/null +++ b/examples/EXPRESSIONS-DEMO.md @@ -0,0 +1,331 @@ +# Expressions demo + +[`expressions-demo.sysml`](expressions-demo.sysml) is a small instrument +payload — two cameras and a spectrometer with masses, heritage annotations, a +downlink budget, radio bands and a stress field on the mount — written so that +each of the expression forms below has something concrete to answer: + +| Form | Where it appears | What it answers | +| --- | --- | --- | +| `x as T` | `WholeReadings`, `CamerasOf`, `PayloadCasts` | the values `T` classifies, and nothing else | +| `*` | `DownlinkBudget` | a bound with no upper limit, compared but never added | +| `.metadata` | `HeritageReport` | the annotations on an element and the values they bind | +| a calc as a value | `Apply`, `Squared`, `SquaresOf`, `Amplifier` | passing, holding, comparing and invoking a calculation | +| `Set` | `RadioBands` | a collection with no order and no repeats | +| `TensorQuantityValue` | `MountStress` | a rank-three tensor indexed by three positions | +| collection bodies | `MassRollup` | `collect`/`select`/`reduce` results typed by their bodies | + +Everything below runs with no external tools. Load the model at the prompt: + +```bash +./bin/sysml examples/expressions-demo.sysml +``` + +Each section instantiates one `part def` and reads its features; `%features` +also lists the inherited `Part` features (`ownedPorts`, `subparts`, …), which +are left out of the transcripts here. + +## `x as T` — a cast selects, it does not convert + +A cast keeps the values its target classifies and drops the rest; it never +changes a value. `4.0 as Integer` is `4.0`, because a whole Real *is* an +Integer in the `ScalarValues` hierarchy, and `2.5 as Integer` is the empty +sequence. The functions that convert — `ToInteger`, `ToString` and their kin +— are in the library, and are not what `as` does. + +``` +%instantiate PayloadCasts +%features PayloadCasts +``` + +``` +Instance: ExpressionsDemo::PayloadCasts (ID: 1) +Features: + wholeOnly = [1.0, 3.0] + cameras = [Instance(ID: 2), Instance(ID: 4)] + mass = 4.0 [kg] + mass = 6.5 [kg] + cameraCount = 2 + asInstrument = Instance(ID: 2) + mass = 4.0 [kg] + notACamera = [] +``` + +- `wholeOnly` is `WholeReadings((1.0, 2.5, 3.0, 4.75))`: a sequence casts + element by element, in order, keeping only the whole numbers. +- `cameras` is `CamerasOf((navCam, spectrometer, sciCam))`: an object is kept + by every classifier it is an instance of, so the two cameras pass and the + spectrometer does not. +- `asInstrument` widens `navCam` to its general type and keeps it; + `notACamera` asks whether the spectrometer is a `Camera`, and it is not. + +A feature holding a cast result should be declared `[0..1]` or `[0..*]`: a +cast that selects nothing yields the empty sequence, which a feature of +multiplicity `[1]` cannot hold. + +The same expressions work at the prompt, where the cast's target is written +with its qualified name: + +``` +(1, 2.5, 3) as ScalarValues::Integer +2.5 as ScalarValues::Integer +ExpressionsDemo::navCam as ExpressionsDemo::Spectrometer +``` + +``` +✓ (1, 2.5, 3) as ScalarValues::Integer + = [1, 3] +✓ 2.5 as ScalarValues::Integer + = [] +✓ ExpressionsDemo::navCam as ExpressionsDemo::Spectrometer + = [] +``` + +The checker warns ahead of time when a cast can select nothing because the +operand's type and the target are unrelated — `navCam as Spectrometer` draws +"cast argument is typed by Camera, unrelated to the target Spectrometer" — so +a cast that always comes back empty does not have to be found at run time. + +## `*` — the unbounded value + +`*` is a value of its own, not a large number: it exceeds every finite number, +equals itself, and prints as `*`. + +``` +%instantiate DownlinkBudget +%features DownlinkBudget +``` + +``` +Instance: ExpressionsDemo::DownlinkBudget (ID: 5) +Features: + passLimit = * + plannedPasses = 40 + withinLimit = true + limitIsUnbounded = true +``` + +Comparisons work at the prompt too, and arithmetic over `*` is refused with an +error naming the operator rather than answered with a finite result: + +``` +3 < * +* == * +* + 1 +``` + +``` +✓ 3 < * + = true +✓ * == * + = true +error: evaluation failed: type mismatch: operator '+' is not defined for the unbounded value '*': * + 1 +``` + +## `.metadata` — what annotates an element + +`elem.metadata` is the sequence of metadata annotating `elem`, one object per +annotation in the order they are written, each carrying the values its body +binds over the defaults its `metadata def` declares. `navCam` is annotated +`@Heritage { mission = "Cassini"; }`, the spectrometer sets `flown = false`, +and `sciCam` carries no annotation at all. + +``` +%instantiate HeritageReport +%features HeritageReport +``` + +``` +Instance: ExpressionsDemo::HeritageReport (ID: 6) +Features: + navCamAnnotations = [Instance(ID: 7)] + mission = "Cassini" + flown = true + navCamMission = "Cassini" + navCamFlown = true + spectrometerFlown = false + sciCamAnnotations = [] +``` + +`navCamFlown` is `true` without `navCam` saying so: the annotation did not bind +`flown`, so the object carries the default from `Heritage`. Indexing is +one-based, as everywhere in SysML: `navCam.metadata#(1)` is the first +annotation. + +## A calculation as a value + +A `calc def`, a `calc` usage or an `in calc` parameter named where a value is +expected is a *function value*: the calculation itself, together with whatever +it closes over. `Apply` takes one as its `in calc f` parameter and invokes it +as `f(a)`: + +``` +%calc Squared(3.0) +%calc Halved(3.0) +%calc Apply(Halve, 9.0) +``` + +``` +✓ Squared(3.0) + = 9.0 +✓ Halved(3.0) + = 1.5 +✓ Apply(Halve, 9.0) + = 4.5 +``` + +Reading a calculation on its own answers the function, named by its +declaration; the analysis library's `SampledFunctions::Sample` takes one and +tabulates it over a domain: + +``` +ExpressionsDemo::Square +%calc SquaresOf((1.0, 2.0, 3.0)) +``` + +``` +✓ ExpressionsDemo::Square + = ExpressionsDemo::Square +✓ SquaresOf((1.0, 2.0, 3.0)) + = [1.0, 4.0, 9.0] +``` + +A nested calc closes over the features around it. `Amplifier::amplify` +multiplies by the part's `gain`, so the function held in `transfer` carries +that `gain` with it, and two reads of the same calc in one object are the same +function: + +``` +%instantiate Amplifier +%features Amplifier +``` + +``` +Instance: ExpressionsDemo::Amplifier (ID: 9) +Features: + gain = 1.5 + transfer = ExpressionsDemo::Amplifier::amplify + sameTransfer = true + atThree = 4.5 + squaredAtThree = 9.0 +``` + +A definition is not a feature, so `attribute transfer = Square;` is refused by +the checker ("Must be a valid feature") where `attribute transfer = amplify;` +— a calc usage — is fine; a `calc def` is passed as an argument, as +`Apply(Square, 3.0)` does, or held through a usage of it. + +## `Set` — no order, no repeats + +The library declares a `Collections::Set`'s elements unique and unordered, so +a `Set` holds a set: the elements it was given with every repeat dropped, and +no order of its own. Two sets given the same elements in different orders are +equal, and so are their `elements`. + +``` +%instantiate RadioBands +%features RadioBands +``` + +``` +Instance: ExpressionsDemo::RadioBands (ID: 10) +Features: + requested = Instance(ID: 11) + elements = Set{"Ka", "S", "X"} + licensed = Instance(ID: 12) + elements = Set{"Ka", "S", "X"} + distinctBands = 3 + sameBands = true + hasKa = true + asList = ["Ka", "S", "X"] +``` + +A set prints as `Set{…}` in a canonical order, which is not the order it was +written in. Flowing its elements into an ordered feature (`asList`) gives a +sequence in that same canonical order. `Bag` and `OrderedSet` are not sets: +the library keeps their order or their repeats, and so does the runtime. + +## A rank-three tensor + +`TensorCalculations::'['` pairs a flat sequence of numbers with a +`TensorMeasurementReference` whose `dimensions` give the shape, in row-major +order with the last index varying fastest. `#` then takes one index per +dimension, and the arithmetic keeps the shape component by component: + +``` +%instantiate MountStress +%features MountStress +``` + +``` +Instance: ExpressionsDemo::MountStress (ID: 13) +Features: + field = Tensor(2, 2, 2)[1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0] [Pa] + rank = 3 + dims = [2, 2, 2] + corner = 1.0 [Pa] + opposite = 8.0 [Pa] + doubled = Tensor(2, 2, 2)[2.0, 4.0, 6.0, 8.0, 10.0, 12.0, 14.0, 16.0] [Pa] + doubledCorner = 10.0 [Pa] +``` + +`doubledCorner` is `doubled#(2, 1, 1)`: the first index selects the second +2×2 slab, whose first component is `2 * 5.0`. An index outside the shape, or +the wrong number of indices for the rank, is an error rather than a wrapped +or truncated read. + +## Collection bodies — the result has the body's type + +`collect`, `select` and `reduce` take a body whose parameter is bound to each +element in turn. The checker types a `collect` by what its body returns, not +by the element type of the collection it ran over, so `instruments->collect { +in i : Instrument; i.mass }` is a `MassValue[0..*]` and can be declared as one +— and can be reduced, compared and aggregated as masses: + +``` +%instantiate MassRollup +%features MassRollup +``` + +``` +Instance: ExpressionsDemo::MassRollup (ID: 15) +Features: + instruments = [Instance(ID: 2), Instance(ID: 4), Instance(ID: 3)] + mass = 4.0 [kg] + mass = 6.5 [kg] + mass = 12.0 [kg] + masses = [4.0 [kg], 6.5 [kg], 12.0 [kg]] + total = 22.5 [kg] + heaviest = 12.0 [kg] + heavy = [Instance(ID: 4), Instance(ID: 3)] + mass = 6.5 [kg] + mass = 12.0 [kg] + heavyCount = 2 +``` + +Because the result type is the body's, a mismatch is caught before anything +runs. Declaring the same `collect` as `String[0..*]` is refused when the model +is loaded: + +``` +error: cannot bind a value of type MassValue to a feature typed by String + attribute names : String[0..*] = instruments->collect { in i : Instrument; i.mass }; +``` + +The body's parameter is declared with its type, `in i : Instrument`, so that +`i.mass` resolves to a feature of `Instrument` and the body's result is typed +by it. + +## Where these are specified + +- Casts: KerML 1.1 §8.3.4.9, *CastExpression*. +- `*`: KerML 1.1 §8.3.3.1, *LiteralInfinity*. +- `.metadata`: KerML 1.1 §8.3.3.1, *MetadataAccessExpression*. +- Sets: `Collections::Set` in the SysML v2 Systems Library, whose `elements` + redefine `UniqueCollection::elements` as unordered. +- Tensors: `Quantities::TensorQuantityValue` and `TensorCalculations` in the + Quantities and Units Domain Library. + +The guide chapter on [expressions, calculations, constraints and +requirements](../docs/guide/05-checking.md) introduces each of these forms; +this demo is its worked example. diff --git a/examples/README.md b/examples/README.md index 7b00ffd76..1e68acb68 100644 --- a/examples/README.md +++ b/examples/README.md @@ -32,6 +32,7 @@ Each of these is a model and a walkthrough of the commands that exercise it. | [solver-demo.sysml](solver-demo.sysml) | [SOLVER-DEMO.md](SOLVER-DEMO.md) | `%check`, `%explain`, `%solve`, `%configure` and `%optimize` — what conditions *can* hold, which conflict, what satisfies them, which variants are permitted, what is best (needs z3 or cvc5) | | [oosem-demo/oosem-demo.sysml](oosem-demo/oosem-demo.sysml) | [oosem-demo/README.md](oosem-demo/README.md) | the `OOSEM` library on a small Earth-observation mission: as-is and to-be enterprise, causal analysis, stakeholder needs derived down to component requirements with `#moe`/`#mop`, the black-box system context and its use case, the logical scenario and components, and the physical architecture distributed over nodes | | [views-demo.sysml](views-demo.sysml) | [VIEWS-DEMO.md](VIEWS-DEMO.md) | `%view` and `%render` — the five rendering kinds, the text/Mermaid/Markdown forms, viewpoint conformance and filtered exposure | +| [expressions-demo.sysml](expressions-demo.sysml) | [EXPRESSIONS-DEMO.md](EXPRESSIONS-DEMO.md) | the expression forms worked through one payload: `as` casts that select rather than convert, `*` as the unbounded value, `.metadata` on an annotated part, calculations passed and invoked as function values, a `Set` with no order and no repeats, a rank-three tensor quantity indexed and scaled, and `collect`/`select`/`reduce` bodies typed by what they return | | [action-executor-demo.sysml](action-executor-demo.sysml) | [ACTION-EXECUTOR-DEMO.md](ACTION-EXECUTOR-DEMO.md) | executing actions, and stepping one in the REPL | | [self-model/](self-model/) | [self-model/README.md](self-model/README.md) | OpenSysML's own architecture in SysML v2: the analysis pipeline as parts, ports and item flows onto the Go packages that implement it, the validation tiers and the two execution engines as state machines, the [AGENTS.md](../AGENTS.md) architecture invariants as requirements the tool evaluates, and the views `make self-model` renders the architecture diagrams from | | `parser_features_demo_*.sysml`/`.kerml` | [PARSER_FEATURES_DEMOS.md](PARSER_FEATURES_DEMOS.md) | the notation the parser accepts, feature by feature | diff --git a/examples/expressions-demo.sysml b/examples/expressions-demo.sysml new file mode 100644 index 000000000..eb48561e1 --- /dev/null +++ b/examples/expressions-demo.sysml @@ -0,0 +1,153 @@ +// An instrument payload written so that each expression form — casts, `*`, +// `.metadata`, function values, sets, tensors, collection bodies — has +// something concrete to answer: see EXPRESSIONS-DEMO.md for the walkthrough. +package ExpressionsDemo { + private import ScalarValues::*; + private import ISQ::*; + private import SI::*; + private import Quantities::*; + private import MeasurementReferences::*; + private import TensorCalculations::*; + private import ControlFunctions::*; + private import SequenceFunctions::*; + private import CollectionFunctions::*; + private import Collections::*; + private import SampledFunctions::*; + + // --- The payload ------------------------------------------------------- + + metadata def Heritage { + attribute mission : String; + attribute flown : Boolean = true; + } + + part def Instrument { + attribute mass : MassValue; + } + part def Camera :> Instrument; + part def Spectrometer :> Instrument; + + part navCam : Camera { + :>> mass = 4.0 [kg]; + @Heritage { mission = "Cassini"; } + } + part sciCam : Camera { + :>> mass = 6.5 [kg]; + } + part spectrometer : Spectrometer { + :>> mass = 12.0 [kg]; + @Heritage { mission = "Rosetta"; flown = false; } + } + + // --- Casts: `x as T` selects, it does not convert ------------------------- + + calc def WholeReadings { + in readings : Real[0..*]; + return : Integer[0..*] = readings as Integer; + } + + calc def CamerasOf { + in candidates : Instrument[0..*]; + return : Camera[0..*] = candidates as Camera; + } + + part def PayloadCasts { + attribute wholeOnly : Integer[0..*] = WholeReadings((1.0, 2.5, 3.0, 4.75)); + ref part cameras : Camera[0..*] = CamerasOf((navCam, spectrometer, sciCam)); + attribute cameraCount : Natural = size(cameras); + ref part asInstrument : Instrument[0..1] = navCam as Instrument; + ref part notACamera : Camera[0..1] = CamerasOf(spectrometer); + } + + // --- `*`: the unbounded value --------------------------------------------- + + part def DownlinkBudget { + attribute passLimit : Natural = *; + attribute plannedPasses : Natural = 40; + attribute withinLimit : Boolean = plannedPasses < passLimit; + attribute limitIsUnbounded : Boolean = passLimit == *; + } + + // --- `.metadata`: what annotates an element ------------------------------- + + part def HeritageReport { + attribute navCamAnnotations [*] = navCam.metadata; + attribute navCamMission : String = navCam.metadata#(1).mission; + attribute navCamFlown : Boolean = navCam.metadata#(1).flown; + attribute spectrometerFlown : Boolean = spectrometer.metadata#(1).flown; + attribute sciCamAnnotations [*] = sciCam.metadata; + } + + // --- Calculations as values ----------------------------------------------- + + calc def Square { in v : Real; return : Real = v * v; } + calc def Halve { in v : Real; return : Real = v / 2.0; } + + calc def Apply { + in calc f { in v : Real; return : Real; } + in a : Real; + return : Real = f(a); + } + + calc def Squared { in a : Real; return : Real = Apply(Square, a); } + calc def Halved { in a : Real; return : Real = Apply(Halve, a); } + + calc def SquaresOf { + in xs : Real[0..*]; + attribute sampled : SampledFunction = Sample(Square, xs); + return : Real[0..*] = Range(sampled); + } + + part def Amplifier { + attribute gain : Real = 1.5; + calc amplify { in v : Real; return : Real = v * gain; } + attribute transfer = amplify; + attribute sameTransfer : Boolean = transfer == amplify; + attribute atThree : Real = Apply(transfer, 3.0); + attribute squaredAtThree : Real = Apply(Square, 3.0); + } + + // --- Sets: unordered, no repeats ------------------------------------------ + + part def RadioBands { + attribute requested : Set { :>> elements = ("X", "Ka", "X", "S", "Ka"); } + attribute licensed : Set { :>> elements = ("S", "X", "Ka"); } + attribute distinctBands : Natural = size(requested); + attribute sameBands : Boolean = requested == licensed; + attribute hasKa : Boolean = contains(requested, "Ka"); + attribute asList : String[*] ordered = requested.elements; + } + + // --- Tensors of rank three ------------------------------------------------ + + attribute stressRef : TensorMeasurementReference { + :>> dimensions = (2, 2, 2); + :>> mRefs = (Pa, Pa, Pa, Pa, Pa, Pa, Pa, Pa); + } + + part def MountStress { + attribute field : TensorQuantityValue = + TensorCalculations::'['((1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0), stressRef); + attribute rank = field.order; + attribute dims : Positive[*] ordered = field.dimensions; + attribute corner = field#(1, 1, 1); + attribute opposite = field#(2, 2, 2); + attribute doubled = 2 * field; + attribute doubledCorner = doubled#(2, 1, 1); + } + + // --- Collection bodies: the result has the body's type -------------------- + + part def MassRollup { + ref part instruments : Instrument[0..*] = (navCam, sciCam, spectrometer); + attribute masses : MassValue[0..*] = + instruments->collect { in i : Instrument; i.mass }; + attribute total : MassValue = + masses->reduce { in a : MassValue; in b : MassValue; a + b }; + attribute heaviest : MassValue = + masses->reduce { in a : MassValue; in b : MassValue; if a > b ? a else b }; + ref part heavy : Instrument[0..*] = + instruments->select { in i : Instrument; i.mass > 5.0 [kg] }; + attribute heavyCount : Natural = size(heavy); + } +} diff --git a/internal/core/export/testdata/corpus_roundtrip_expected.txt b/internal/core/export/testdata/corpus_roundtrip_expected.txt index 37ab11187..5223f2677 100644 --- a/internal/core/export/testdata/corpus_roundtrip_expected.txt +++ b/internal/core/export/testdata/corpus_roundtrip_expected.txt @@ -8,7 +8,7 @@ # is a per-file ratchet, not a claim that any verdict is right; see # docs/project/rdf-corpus-roundtrip.md. Regenerate with: # go test ./internal/core/export -run TestCorpusRoundTrip -update-corpus-roundtrip -# files: committed 33 +# files: committed 34 # files: sysml-v2-training 100 # files: pilot-corpora/kerml-examples 58 # files: pilot-corpora/sysml-examples 99 @@ -17,6 +17,7 @@ stable action-executor-demo.sysml stable combined-behavioral-demo.sysml stable disposal-robot-demo/robot.sysml stable disposal-team-demo/team.sysml +stable expressions-demo.sysml stable oosem-demo/oosem-demo.sysml stable orthogonal-regions-demo.sysml stable parser_features_demo_action_semantics.sysml From b85841013254e79e6b40b8becbecf7896414a6aa Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Wed, 9 Sep 2026 17:45:57 +0000 Subject: [PATCH 02/33] docs(examples): match walkthrough transcripts to a full session Instance ids in the walkthrough follow a session that also runs the intervening %calc commands, and the guide's redeclaration transcript shows the note the REPL prints after the error. Co-Authored-By: jason.han --- docs/guide/05-checking.md | 1 + examples/EXPRESSIONS-DEMO.md | 12 ++++++------ 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/docs/guide/05-checking.md b/docs/guide/05-checking.md index 6d979d90c..e282092ce 100644 --- a/docs/guide/05-checking.md +++ b/docs/guide/05-checking.md @@ -372,6 +372,7 @@ sysml> package Rollup { 1:35: error: cannot bind a value of type MassValue to a feature typed by String attribute names : String[0..*] = (navCam, spectrometer)->collect { in i : Instrument; i.mass }; ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +note: added to the existing package Rollup (its other members are kept) ``` **Constraints:** diff --git a/examples/EXPRESSIONS-DEMO.md b/examples/EXPRESSIONS-DEMO.md index cf754d532..cc65e997b 100644 --- a/examples/EXPRESSIONS-DEMO.md +++ b/examples/EXPRESSIONS-DEMO.md @@ -201,7 +201,7 @@ function: ``` ``` -Instance: ExpressionsDemo::Amplifier (ID: 9) +Instance: ExpressionsDemo::Amplifier (ID: 13) Features: gain = 1.5 transfer = ExpressionsDemo::Amplifier::amplify @@ -228,11 +228,11 @@ equal, and so are their `elements`. ``` ``` -Instance: ExpressionsDemo::RadioBands (ID: 10) +Instance: ExpressionsDemo::RadioBands (ID: 14) Features: - requested = Instance(ID: 11) + requested = Instance(ID: 15) elements = Set{"Ka", "S", "X"} - licensed = Instance(ID: 12) + licensed = Instance(ID: 16) elements = Set{"Ka", "S", "X"} distinctBands = 3 sameBands = true @@ -258,7 +258,7 @@ dimension, and the arithmetic keeps the shape component by component: ``` ``` -Instance: ExpressionsDemo::MountStress (ID: 13) +Instance: ExpressionsDemo::MountStress (ID: 17) Features: field = Tensor(2, 2, 2)[1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0] [Pa] rank = 3 @@ -288,7 +288,7 @@ in i : Instrument; i.mass }` is a `MassValue[0..*]` and can be declared as one ``` ``` -Instance: ExpressionsDemo::MassRollup (ID: 15) +Instance: ExpressionsDemo::MassRollup (ID: 19) Features: instruments = [Instance(ID: 2), Instance(ID: 4), Instance(ID: 3)] mass = 4.0 [kg] From 27ec2579df1f1de1afbe7636a3c72b7ed37d268a Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Wed, 9 Sep 2026 18:18:01 +0000 Subject: [PATCH 03/33] docs(runtime): document scheduling, choice points and exploration Add a design note on how a run resolves what the library leaves unordered: the six choice kinds and how each is recorded without altering the run, the reverse, declared, seed and explore policies, replay-based exploration from a fresh context per run, and the conformance contract of plural outcomes, .trace.order constraints, per-policy trace goldens and the declared/seed:1 sweep. Point the architecture, testing and orthogonal-regions notes at it, the last now describing scheduler-drawn region order for events and change triggers. List region order among the choice kinds the --trace, %trace and SchedulePolicy descriptions name, and add %schedule to the REPL guide's command table. Co-Authored-By: jason.han --- .../scheduling-internals-docs.changed.md | 1 + docs/guide/04-repl.md | 1 + docs/internals/architecture.md | 30 +++- docs/internals/design/README.md | 4 + .../design/bounded-model-checking.md | 24 ++- docs/internals/design/orthogonal-regions.md | 22 +++ docs/internals/design/scheduling.md | 161 ++++++++++++++++++ docs/internals/testing.md | 12 +- docs/reference/api.md | 3 +- docs/reference/cli.md | 4 +- docs/reference/repl-commands.md | 2 +- internal/core/runtime/scheduler.go | 9 +- 12 files changed, 247 insertions(+), 26 deletions(-) create mode 100644 changes/unreleased/scheduling-internals-docs.changed.md create mode 100644 docs/internals/design/scheduling.md diff --git a/changes/unreleased/scheduling-internals-docs.changed.md b/changes/unreleased/scheduling-internals-docs.changed.md new file mode 100644 index 000000000..14e8e7e69 --- /dev/null +++ b/changes/unreleased/scheduling-internals-docs.changed.md @@ -0,0 +1 @@ +- **The contributor documentation now covers how a run resolves what the library leaves unordered.** A new design note, `docs/internals/design/scheduling.md`, describes the six kinds of choice point and how each is recorded without altering the run, the `reverse`, `declared`, `seed:` and `explore[:runs=N,depth=D]` policies and what each draws, replay-based exploration from a fresh context per run with its witnesses, outcome grouping, budgets and `incomplete` verdict, and the conformance contract behind it — plural `outcomes` with their `admissible` citations, `.trace.order` partial-order constraints, per-policy trace goldens and the whole-suite sweep under `declared` and `seed:1`. The architecture and testing overviews and the orthogonal-regions note point to it, the latter now describing how sibling regions' reactions to one event or one change are dispatched through the scheduler and reported as a `region order` choice. The `--trace`, `%trace` and `SchedulePolicy` descriptions list region order among the choice kinds they report, and the REPL guide's command table gains a row for `%schedule`. diff --git a/docs/guide/04-repl.md b/docs/guide/04-repl.md index 412a1d8fd..b2baf0401 100644 --- a/docs/guide/04-repl.md +++ b/docs/guide/04-repl.md @@ -343,6 +343,7 @@ completes them: `#` offers the ids there are, `car.` the objects `car` holds. | which variants its conditions permit (experimental, needs [z3 or cvc5](01-install.md#installing-a-solver-optional)) | `%configure` | [reference](../reference/repl-commands.md) | | which values are best for an analysis case's objectives (experimental, needs [z3](01-install.md#installing-a-solver-optional)) | `%optimize` | [reference](../reference/repl-commands.md) | | what a behavior does, step by step | `%action`, `%state`, `%step`, `%tokens`, `%advance` | [6](06-behavior.md) | +| whether a result depends on the order the run happened to take, and how to replay another | `%schedule`, `%trace` | [6](06-behavior.md#when-a-model-has-more-than-one-valid-run) | | where a run stopped and why | `%trace`, `%budget`, `%verbosity` | [10](10-troubleshooting.md) | | whether what is typed is conforming SysML v2 | `%strict` | [3](03-command-line.md#strict-conformance) | diff --git a/docs/internals/architecture.md b/docs/internals/architecture.md index b2e9aade6..9c4ae338c 100644 --- a/docs/internals/architecture.md +++ b/docs/internals/architecture.md @@ -294,14 +294,21 @@ Parse + model all behavioral bodies with unified fallback grammar: - Guard evaluation for transitions - Transition effect actions - Hierarchical states with LCA-based entry/exit propagation - - Orthogonal regions with multi-region event broadcasting + - Orthogonal regions with multi-region event broadcasting; the order sibling regions react in is a scheduler choice, drawn per firing among the regions still active (`dispatchInOrder`), for change triggers as for queued events - Choice + Junction pseudostates - Golden trace recording for transitions/entry/exit - APIs: `ProcessNextEvent()`, `CurrentState()`, `EventQueue()`, `StateData()`, `SetTrace()` - Deferred events: an event no active transition handles is retained while a state deferring it is active, and delivered afterwards in arrival order - CallEvent matches the operation named by the trigger (`signal.go`, `state_executor.go`; `signal_test.go:TestCallEventMatchesOperationName`) -3. **Context Integration** — Public runtime APIs +3. **Scheduler and choice points** — one resolution rule for what the library leaves unordered ([design note](design/scheduling.md)) + - Six `ChoiceKind`s (`choice.go`): token order within a step, decision branch, same-step write order, transition, region order, due order; each site resolves through the run's `scheduler` and then records a `ChoicePoint`, an informational `RunNote` (diagnostic code `choice-point`) that never alters the run + - Every decision guard is evaluated so a second holding one is seen; a later guard that cannot be evaluated is an `UnevaluableGuard` note (`guard-unevaluable`), not a failure + - `SchedulePolicy` (`scheduler.go`): `reverse` (default and zero value — exactly what every run did before policies existed), `declared`, `seed:` (a PCG generator the run consumes, replayed by the seed), `explore[:runs=N,depth=D]` + - `Explore` (`explore.go`) replays whole runs from a fresh `Context` each, a recorded choice prefix then the first untried alternative, depth-first within `ExploreBudget` (default 1024 runs, 64 choice points); reports distinct outcomes by `Outcome.identity` with linearization counts and a witness, and `incomplete` when a bound stopped it + - The scheduler lives in the run's `runState` beside the budget and notes; a run driven call by call (`beginExecutorRun`) keeps its own across interleaved runs, and a probe (`beginProbe`) restores the scheduler's position and notes nothing + +4. **Context Integration** — Public runtime APIs - `InvokeCalc(symbol, args)` — Invoke calculation with arguments, return result - `EvaluateConstraint(symbol)` — Evaluate constraint, return satisfaction boolean (assert/assume) - `EvaluateRequirement(symbol)` — Evaluate requirement, return satisfaction boolean (require/subject/actor/assume/nested) @@ -309,12 +316,15 @@ Parse + model all behavioral bodies with unified fallback grammar: - `ExecuteState(symbol)` — Run state machine until final/suspended - `CreateActionExecutor(symbol)` — Create executor for debugging - `CreateStateExecutor(symbol)` — Create executor for debugging + - `SetSchedule(policy)`, `Schedule()` — the policy runs started from now on resolve their choice points under (`explore` is refused: `Explore` drives it) + - `Notes()`, `Choices()`, `UnevaluableGuards()` — what the last run recorded **Implementation:** - `context.go` (460 lines) — Public Execute/Invoke/Evaluate APIs, step budget enforcement - `action_executor.go` (729 lines) — Token-flow engine with nested actions, send statement - `state_executor.go` (1149 lines) — Event-driven state machine with do behaviors - `executor_common.go` — Token, Event, EventQueue, ExecutionState +- `scheduler.go`, `choice.go`, `action_choice.go`, `explore.go` — scheduling policies, choice-point notes, bounded exploration - `trace.go` (154 lines) — Deterministic execution trace recorder - `eval.go` — Expression evaluation (binary/unary operators, literals, feature references, qualified names, type coercion) - Lowering to execution IR lives in `internal/core/lower/` (`ToActionGraph`, `ToStateGraph`) @@ -323,8 +333,9 @@ Parse + model all behavioral bodies with unified fallback grammar: - **Golden ASTs**: `internal/core/parser/testdata/parse/` — count in [the measured counts](../project/spec-compliance.md) - **Negative tests**: `internal/core/parser/negative_test.go` — count in [the measured counts](../project/spec-compliance.md) - **Unit tests**: `action_executor_test.go`, `state_executor_test.go` (action, state) -- **Conformance gate**: `.sysml` + `.expected.json` pairs, all passing - `conformance_test.go` — counts and per-category breakdown in [the measured counts](../project/spec-compliance.md) -- **Golden traces**: `.trace.golden` files - `trace_test.go` — count in [the measured counts](../project/spec-compliance.md) +- **Conformance gate**: `.sysml` + `.expected.json` pairs, all passing - `conformance_test.go` — counts and per-category breakdown in [the measured counts](../project/spec-compliance.md); a case whose model admits several results lists them as `outcomes`, each cited to [the semantic oracle](../project/behavior-semantic-oracle.md), and is explored to prove every one reachable and nothing else; `TestExecutionConformanceUnderPolicies` re-runs the suite under `declared` and `seed:1` +- **Golden traces**: `.trace.golden` files - `trace_test.go` — count in [the measured counts](../project/spec-compliance.md); `.trace.order` files state the partial order a trace must respect (`a < b`), and a case with `outcomes` owns a `..trace.golden` per sweep policy +- **Exploration**: `explore_test.go` — every linearization reached once, determinism, each budget's incompleteness, an error as an outcome, transition, region and due order - **Robustness**: failure-mode cases (deadlock, unbound params, missing features, dangling transitions, sourceless accept, step budget, pseudostate dead ends and cycles, history and defer misuse, send/accept misrouting, calc arity/recursion, `perform` reference failures) - `robustness_test.go` - **Coverage**: All behavioral types fully functional. Action: 14/14 features ✅. State: 13/13 features ✅. Calc: 8/8 ✅. Constraint: 5/5 ✅. Requirement: 5/5 ✅. Evaluation: 7/7 ✅. @@ -482,6 +493,7 @@ See [the guide](../guide/) for VS Code configuration. - `%constraint ` — Evaluate constraint, check assert/assume satisfaction - `%requirement ` — Evaluate requirement, validate subject/require/actor conditions - `%satisfy [name]` — Evaluate satisfaction assertions, with the requirement's subject bound to the object `by` names +- `%schedule [policy]` — Show or set the policy the next run resolves its choice points under (`reverse`, `declared`, `seed:`); `explore` is refused, since a debugging session steps one run **Action debugging:** - `%action []` — Start debugging action execution, optionally performed by an instantiated object @@ -645,10 +657,10 @@ New behavioral features (actions, states, calc, constraints, requirements) requi #### 2. Execution Conformance Gate - **Purpose:** Verify behavioral execution produces expected outcomes - **Location:** `internal/core/runtime/conformance_test.go` -- **Test:** `TestExecutionConformance` runs `.sysml` + `.expected.json` pairs -- **Schema:** `internal/core/runtime/testdata/conformance/README.md` (outcome format for each behavioral type) +- **Test:** `TestExecutionConformance` runs `.sysml` + `.expected.json` pairs; `TestExecutionConformanceUnderPolicies` runs them again under `declared` and `seed:1` +- **Schema:** `internal/core/runtime/testdata/conformance/README.md` (outcome format for each behavioral type; `outcomes` with an `admissible` citation when the model admits several) - **Allowlist:** `known_failures.txt` (currently empty — all cases pass) -- **Acceptance:** Expected outputs/satisfaction match actual execution results +- **Acceptance:** Expected outputs/satisfaction match actual execution results under every policy; a case listing `outcomes` is explored, and every listed outcome must be reached and no other ([design note](design/scheduling.md#the-conformance-contract)) **Coverage (by fixture prefix, all passing; counts in [the measured counts](../project/spec-compliance.md)):** - Calc: parameter binding, return values, defaults, inherited parameters, unary operators, type coercion, qualified names, body-local usages, statement bodies, nested and from-constraint invocation @@ -668,8 +680,8 @@ go test -v -run TestExecutionConformance ./internal/core/runtime #### 3. Golden Execution Traces - **Purpose:** verify *how* execution proceeds (ordering, scheduling), not only the final result - **Location:** `internal/core/runtime/trace_test.go` -- **Test:** `TestExecutionTrace` compares executor traces against `.trace.golden` -- **Determinism:** Token sorting by ID, fixed event queue tie-breaking +- **Test:** `TestExecutionTrace` compares executor traces against `.trace.golden`, and against the partial order a `.trace.order` states (`a < b` per line) +- **Determinism:** Token sorting by ID, fixed event queue tie-breaking; each `choice` the run made is a trace line, so a golden pins one linearization and a case with `outcomes` owns one golden per sweep policy (`..trace.golden`) - **Acceptance:** Trace output matches golden file - **Update flag:** `go test -run TestExecutionTrace -update-traces` - **Coverage:** `.trace.golden` files for action, calc, state, constraint, accept and string execution diff --git a/docs/internals/design/README.md b/docs/internals/design/README.md index 91274bab1..03dd19c30 100644 --- a/docs/internals/design/README.md +++ b/docs/internals/design/README.md @@ -8,6 +8,10 @@ maintainers; the behavior a user sees is [the guide](../../guide/). - **[Bounded model checking of behaviors](bounded-model-checking.md)** — a proposal: explore every admissible interleaving up to a bound with partial-order reduction, and report the requirement violations, deadlocks and schedule-dependent outcomes it finds +- **[Scheduling policies, choice points and exploration](scheduling.md)** — how a run + resolves what the library leaves unordered, reports each such choice without changing the + run, takes another linearization under `declared` or `seed:`, and enumerates every one + within a budget under `explore` - **[Orthogonal regions](orthogonal-regions.md)** — concurrent substates, an OpenSysML extension against UML 2.5.1 semantics - **[Pseudostates](pseudostates.md)** — choice, junction, fork, join, entry/exit points diff --git a/docs/internals/design/bounded-model-checking.md b/docs/internals/design/bounded-model-checking.md index 1fbadd138..bbaf2294a 100644 --- a/docs/internals/design/bounded-model-checking.md +++ b/docs/internals/design/bounded-model-checking.md @@ -2,9 +2,17 @@ A design for exploring every admissible interleaving of an action or state machine, up to a bound, and reporting the outcomes the specification leaves open, the deadlocks a run can reach, -and the requirements an interleaving can violate. Nothing here is implemented; this note fixes -the data shapes, the reduction rule, the bounds and the user surface so the work can be reviewed -before code is written, and so each stage can be judged complete on its own. +and the requirements an interleaving can violate. This note fixes the data shapes, the reduction +rule, the bounds and the user surface so the work can be reviewed before code is written, and so +each stage can be judged complete on its own. + +What is implemented of it is the `explore` scheduling policy +([scheduling](scheduling.md#exploration-explorego)): every linearization within a budget of runs +and choice points, each replayed from a fresh context, with the distinct outcomes, their +linearization counts and one witness per outcome reported, and an honest `incomplete` when the +budget stopped it. It runs every linearization rather than one per equivalence class, and it +reports outcomes, not deadlocks or requirement violations; the snapshots, the partial-order +reduction and those analyses remain this proposal's. ## The problem this answers @@ -21,10 +29,12 @@ descending index order within a step, a fork appends its branch tokens in succes order, a state machine fires transitions and exits regions in region declaration order — and [the semantic oracle](../../project/behavior-semantic-oracle.md) separates what the library fixes from what that scheduling chose. The compliance map marks the rows where the runtime picks an -order the specification does not as approximate. What no surface offers today is the question a -safety case asks: *does any admissible execution violate this requirement, deadlock, or end in a -state the model did not intend?* A single run cannot answer it, and a race the scheduling happens -to resolve the intended way is invisible. +order the specification does not as approximate. The `explore` policy answers which outcomes the +admissible executions reach, by running each of them within a budget; what no surface offers is +the question a safety case asks at scale: *does any admissible execution violate this +requirement, deadlock, or end in a state the model did not intend?* Enumerating every +linearization answers it only for behaviors small enough to enumerate, and a race the scheduling +happens to resolve the intended way is invisible to a single run. The pinned OMG pilot evaluates expressions and executes neither actions nor state machines ([pilot execution referee](../../project/pilot-execution-referee.md)), so there is no reference diff --git a/docs/internals/design/orthogonal-regions.md b/docs/internals/design/orthogonal-regions.md index 75f7fbb80..e5a68fdf3 100644 --- a/docs/internals/design/orthogonal-regions.md +++ b/docs/internals/design/orthogonal-regions.md @@ -138,6 +138,28 @@ func (e *StateExecutor) ProcessNextEvent() error { **Key insight:** Events broadcast to all regions. Each region processes event independently (run-to-completion per region). +**As implemented (`state_executor.go`):** the order the regions react in is not the map's +iteration order above, nor declaration order by rule. `broadcastEvent` first selects one +candidate per active leaf against the configuration the event was dequeued for +(`selectTransitions`: the innermost state on the leaf's parent chain with an enabled transition, +so a state the event enters never reacts to it), drops the candidates a nested transition +outranks, then hands the survivors to `dispatchInOrder`. That loop fires them one at a time: before +each firing it discards the candidates whose leaf is no longer active — a reaction may have left +a sibling's leaf — and draws which of the rest fires next through `chooseRegion`, which asks the +run's scheduling policy and, when two or more remain, records a `ChoicePoint` of kind +`ChoiceRegionOrder` ahead of the firing's own notes (in a trace, +`choice on go: states left, right react (unordered; took right first)`). Each +`StateTransitionPerformance` is ordered against its own source and target only +(`StatePerformances.kerml`), and UML 2.5.1 §14.2.3.9.4 leaves the firing order of the transitions +selected for one event undefined, so the order is a genuine opening the run reports rather than a +rule: under `reverse` and `declared` the draw is declaration order and is still reported, +`seed:` varies and replays it, and `explore` enumerates every order. The choice is labelled by +the occurrence dispatched (`on go`, `on change`), not by the trigger of whichever region was +drawn first, so the label reads the same under every policy. Change triggers +(`state_change_trigger.go`, `pollChangeEvents`) select their candidates by the guards that came to +hold and dispatch through the same loop. See +[scheduling policies, choice points and exploration](scheduling.md). + ### 4. State Entry/Exit with Regions **Entering composite state with regions:** diff --git a/docs/internals/design/scheduling.md b/docs/internals/design/scheduling.md new file mode 100644 index 000000000..8ac1c97aa --- /dev/null +++ b/docs/internals/design/scheduling.md @@ -0,0 +1,161 @@ +# Scheduling policies, choice points and exploration + +How the runtime resolves what the Kernel Semantic Library leaves unordered, how it reports each +such resolution without changing the run, how a driver asks for another one, and how every one +within a bound is enumerated. The behavior a user sees is in +[the guide](../../guide/06-behavior.md#when-a-model-has-more-than-one-valid-run); which openings +are the library's and which are the tool's is derived case by case in +[the semantic oracle](../../project/behavior-semantic-oracle.md). + +## The problem this answers + +A succession is a `HappensBefore` link between whole occurrences (`Occurrences.kerml`); the +library orders nothing two such chains do not connect. Fork branches, the reactions of sibling +regions to one event, two enabled transitions out of one state, several holding guards of one +decision, and two performances due at one instant of the clock are all unordered, so one model +admits several complete outcomes and every one of them conforms. The executor runs exactly one +linearization. Until that linearization is named and reported, a conformance case can only pin it, +and a test that pins it cannot tell an admissible alternative from an executor bug. + +The design separates four things that were one: the set of outcomes a case admits, the +linearization a run took, the points at which it had a choice, and the rule it chose by. + +## Choice points (`choice.go`, `action_choice.go`) + +A `ChoicePoint` is one point where an executor had several enabled alternatives the library leaves +unordered and took one by its scheduling rule. `ChoiceKind` names the six: + +| Kind | Where it is noted | Alternatives, canonically | +|------|-------------------|---------------------------| +| `ChoiceTokenOrder` | `ActionExecutor.noteTokenOrder` | the tokens that could act in the step, by ID; the one stepped first is taken | +| `ChoiceDecisionBranch` | `ActionExecutor.noteDecisionBranches` | the successions whose guards hold, by declaration position | +| `ChoiceWriteOrder` | `stepWriteLedger.noteChoices` | the tokens that wrote one feature in one step; the write that stood is taken | +| `ChoiceTransition` | `StateExecutor.chooseTransition` | the transitions one event enables out of one state, by declaration position | +| `ChoiceRegionOrder` | `StateExecutor.chooseRegion`, drawn by `dispatchInOrder` | the states whose transitions one occurrence selected, by name in declaration order; the one fired first is taken | +| `ChoiceDueOrder` | `Context.runDue` (`advance.go`) | the executors due at one instant, in creation order; the one run first is taken | + +Two rules hold at every site: + +- **Recording a choice never alters the run.** The executor resolves the point exactly as the + policy says and then describes what it resolved. To *know* a decision had a second holding + guard, every guard is evaluated, not just up to the first that holds; a later guard that cannot + be evaluated is recorded as an `UnevaluableGuard`, not a failure — a guard with no result is not + true, so its succession is simply not selected, which is the library's reading. A first guard + that errors still fails the run as it always did. +- **A choice is a fact about the run, not a fault in the model.** `ChoicePoint.Diagnostic()` is + informational with code `choice-point`; `UnevaluableGuard.Diagnostic()` is informational with + code `guard-unevaluable`. Both are `RunNote`s. + +`Context.note` appends a note to the run's `runState.notes` and, when tracing, writes its +`String()` to the trace at the point it was made (`choice …`, `unevaluable guard …`). A probe — +a preview of what a run would do, bracketed by `beginProbe` — notes nothing, since it is not a +run. `Context.Notes`, `Choices` and `UnevaluableGuards` read them back; the executors' `Notes` and +`NoteCount` let a caller driving a run call by call see what one call noted, which is how the REPL +ends `%step`, `%continue` and `%advance` with a count. + +Region order is drawn per dispatch, not per event: `dispatchInOrder` draws among the candidates +still active before each firing, since a reaction may leave a sibling's leaf, and both the +broadcast of a queued event and the polling of change triggers (`state_change_trigger.go`) go +through it. The choice is labelled by the occurrence dispatched, not by the trigger of whichever +region was drawn first, so the label is the same under every policy. + +## Policies (`scheduler.go`) + +A `SchedulePolicy` is parsed from one spelling and printed back to it: + +| Spelling | Token order in a step | `pick` (branch, transition, region) | `pickDue` | +|----------|----------------------|--------------------------------------|-----------| +| `reverse` (default, zero value) | reverse spawn order | first in declaration order | last created | +| `declared` | spawn order | first in declaration order | first created | +| `seed:` | shuffle of the tokens not parked | uniform draw | uniform draw | +| `explore[:runs=N,depth=D]` | the exploration's plan | the exploration's plan | the exploration's plan | + +`reverse` is exactly what every run did before policies existed, so every `.expected.json` and +`.trace.golden` recorded before them still holds unchanged; that is the invariant the whole design +is built to keep. Under `reverse` and `declared` a region-order pick is declaration order and is +still reported — a fixed policy resolves the choice, it does not remove it. + +`SchedulePolicy.start` begins the resolutions of one run as a `scheduler`. A seeded one carries a +`math/rand/v2` PCG the run consumes draw by draw, so the same seed replays the same run on every +platform; `scheduler.mark` saves and restores that state around a probe, so previewing does not +move the generator. `Context.SetSchedule` sets the policy runs started from then on draw under; a +run already under way keeps the one it started with, and `explore` is refused with +`ErrExploreUndriven` because it is not a policy one context runs under (below). + +The scheduler lives in the run's `runState` beside the budget and the notes. A run driven call by +call — a REPL `%action` or `%state` session — owns its `executorRun.state`, installed for each +call by `beginExecutorRun` whatever ran in between, so a seeded debugging session draws from its +own generator and an interleaved run neither consumes its draws nor inherits its notes. + +## Exploration (`explore.go`) + +`explore` enumerates every linearization within a budget by replaying whole runs, each from a +fresh `Context`: + +1. The first run records each choice point it reaches as an `exploreSlot` (a `pick` among `n` + alternatives, or which of the tokens able to act a step tries next) and takes the first + alternative at each. +2. `nextPrefix` walks the record backwards to the last slot with an untried alternative, keeps + the record up to it with that alternative advanced, and the next run replays that prefix and + takes first alternatives past it. This is a depth-first walk of the choice tree. +3. A replay that does not meet the choice points its prefix planned — a different number of + alternatives, or tokens able to act the plan did not find so — is `ErrExplorationDiverged`, + and no outcome set is reported, since one could not be trusted. +4. Runs stop when every alternative within depth is tried, or when the `runs` budget is reached; + a slot resolved past the `depth` budget takes its first alternative and is not the + exploration's to vary. Either bound reached makes the `Exploration` incomplete, and + `Exploration.Status` says which; nothing is silently truncated. The default budget is + `DefaultExploreBudget`, 1024 runs and 64 choice points per run. + +A fresh context per run is what makes replay sound: instances, identities, the message bus, the +clock, object behaviors, calc memoization and the notes of one run cannot leak into the next. +`Context.beginExploration` installs the exploration's run as the scheduler every choice draws +from; `scheduler.describe` attaches the `ChoicePoint` the run reports to the slot it just resolved, +so a witness names alternatives exactly as the trace does. + +Outcomes are keyed by `Outcome.identity` — outputs, `finalState`, state visits, or the error — +and grouped: each distinct outcome reports how many linearizations reached it and the choices of +the first run that did, its witness. A step's pick among tokens that then did not act is no +alternative (the slot is narrowed, and a run that repeats one already made is not counted twice). +`Explore` is the one driver of this policy; the CLI's `-schedule explore`, the wire `schedule` +field and the Python client all reach it, and a REPL debugging session refuses it because it steps +one run and cannot replay from the start. + +## The conformance contract + +Every element above has a test surface, documented for authors in +`internal/core/runtime/testdata/conformance/README.md` and summarised in +[testing](../testing.md): + +- A case whose model admits several results lists them under `outcomes` with an `admissible` + citation into the semantic oracle; a case with one result states it as before. The observed run + must match exactly one listed outcome. +- `TestExecutionConformance` runs every case under the default policy. + `TestExecutionConformanceUnderPolicies` runs the whole suite under `declared` and `seed:1`: a + case with no `schedule` pin was recorded under the default and must hold under any policy, so + one that differs has been pinning a scheduling artefact and fails rather than being skipped. +- A case with `outcomes` is also explored (`exploreConformanceCase`): exploration must reach every + listed outcome, reach nothing unlisted, and complete within the case's `exploreBudget`. A case + without `outcomes` is not explored, on the expectation that it has one reachable outcome; when + exploring it shows more, the fix is to derive its admissible set in the oracle and list it, not + to pin the policy. A `schedule` pin of `reverse` says the case's result is one linearization, + kept only until its admissible set is derived or the bug it pins is fixed. +- `TestExecutionTrace` checks a case's `.trace.golden` under the default policy and, for a case + with `outcomes`, a `..trace.golden` under each sweep policy; a `.trace.order` + states the partial order — `a < b` per line — a trace must respect, checked beside the golden + or instead of one, and `TestTraceOrderViolationFails` proves a violated constraint fails. +- `explore_test.go` covers the enumeration itself: every outcome reached once, determinism, + the one-run case with no choice points, each budget's incompleteness, an error as an outcome, + a decision in a loop, transition conflict, sibling region order under every policy, and due + order. + +## What this is not + +This is bounded enumeration of linearizations, not model checking: +[bounded model checking](bounded-model-checking.md) proposes snapshots at choice points and +partial-order reduction so that only one representative of each equivalence class of +interleavings is run. Exploration runs every linearization within budget and reports the +distinct outcomes it reached; it answers "which outcomes can this model produce, and by what +choices" and reports honestly when the budget stopped it, which is the question the conformance +harness asks. The reduction, the deadlock and requirement analyses across schedules, and the +exploration of value domains remain that proposal's. diff --git a/docs/internals/testing.md b/docs/internals/testing.md index a08a2108c..201574ee4 100644 --- a/docs/internals/testing.md +++ b/docs/internals/testing.md @@ -11,8 +11,9 @@ internal/core/ │ ├── negative_test.go # Malformed input handling │ └── testdata/parse/ # Test fixtures + goldens ├── runtime/ -│ ├── conformance_test.go # Execution outcome verification +│ ├── conformance_test.go # Execution outcome verification, under every policy │ ├── trace_test.go # Execution ordering/scheduling +│ ├── explore_test.go # Every linearization within a budget │ ├── robustness_test.go # Failure mode handling │ └── testdata/conformance/ # Behavioral test cases └── libs/ @@ -111,6 +112,9 @@ New behavioral features (actions, states, calc, constraints, requirements) requi - **Format:** `.sysml` + `.expected.json` pairs - **Schema:** `internal/core/runtime/testdata/conformance/README.md` - **Allowlist:** `known_failures.txt` (currently empty) +- **Admissible outcomes:** a case whose model admits several complete results lists them under `outcomes`, each with an `admissible` citation into [the semantic oracle](../project/behavior-semantic-oracle.md) deriving why the library leaves the order open; the observed run must match exactly one. The case is also explored (`explore` policy): every listed outcome must be reached, nothing unlisted may be, and the exploration must complete within the case's `exploreBudget` +- **Policy sweep:** `TestExecutionConformanceUnderPolicies` runs the whole suite under `declared` and `seed:1`. A case with no `schedule` pin was recorded under the default and must hold under any policy; one that differs was pinning a scheduling artefact and fails rather than being skipped. Pinning `schedule: "reverse"` declares the result one linearization, kept only until its admissible set is derived or the bug it pins is fixed +- **Design:** [scheduling policies, choice points and exploration](design/scheduling.md) **Coverage (all passing, by fixture prefix; counts in [the measured counts](../project/spec-compliance.md)):** - Calc: parameter binding, return values, defaults, inherited parameters, unary ops, qualified names, type coercion, body-local usages, statement bodies, nested and from-constraint invocation @@ -128,13 +132,15 @@ go test -v -run TestExecutionConformance ./internal/core/runtime **Purpose:** verify *how* execution proceeds (ordering, scheduling), not only the final result - **Test:** `TestExecutionTrace` (internal/core/runtime/) -- **Format:** `.trace.golden` files -- **Determinism:** Token sorting by ID, fixed event queue tie-breaking +- **Format:** `.trace.golden` files, one linearization each; a case with `outcomes` owns a `..trace.golden` per sweep policy beside the default one +- **Order constraints:** a `.trace.order` file states the partial order a trace must respect, one `a < b` per line — the first trace entry mentioning `a` before the first mentioning `b`; labels the same entry first mentions are unordered, and a label no entry mentions fails. It is checked beside a golden, or instead of one where every linearization is admissible; `TestTraceOrderViolationFails` proves a violated constraint fails +- **Determinism:** Token sorting by ID, fixed event queue tie-breaking; each `choice` the run made is a trace line naming the alternatives and the one taken - **Coverage:** `.trace.golden` files for action, calc, state, constraint, accept and string execution **Trace format examples:** - Action: `step 1: token T1@node1, token T2@node2` (sorted) - State: `entry: StateName [hasEntryAction]`, `transition: From -> To [event]`, `exit: StateName [hasExitAction]` +- Choice: `choice step 2: tokens 3@left, 4@right (unordered; took 4@right first)` **Generate traces:** ```bash diff --git a/docs/reference/api.md b/docs/reference/api.md index 37db52b0a..3040187dc 100644 --- a/docs/reference/api.md +++ b/docs/reference/api.md @@ -423,7 +423,8 @@ Execution runtime (Tiers 1-5: instances, expressions, behaviors). - **`SchedulePolicy`** — How the executors resolve a run's choice points (several steppable tokens in one step, several holding guards at a decision, several enabled transitions for one - event, several executors due at one instant of the clock; which same-step write to one feature + event, several regions reacting to one event, several executors due at one instant of the + clock; which same-step write to one feature stands follows from the token order). The zero value and `DefaultSchedulePolicy` are `reverse`, what every run did before policies were selectable; every `.expected.json` and `.trace.golden` recorded under it still holds diff --git a/docs/reference/cli.md b/docs/reference/cli.md index 00a9807a8..d681b6789 100644 --- a/docs/reference/cli.md +++ b/docs/reference/cli.md @@ -603,7 +603,9 @@ client through the [`RunSweep` RPC](api.md). Where a behavior has [choice points](../guide/06-behavior.md) — several steppable tokens in one step, several holding guards at a decision, several enabled transitions out of one state for one -event, two tokens writing one feature in one step — one run shows one linearization. +event, several regions of one parallel state reacting to one event, two tokens writing one +feature in one step, two executors due at one instant of the clock — one run shows one +linearization. `-schedule explore` runs them all: the first run records the alternative taken at each choice point, and every later run replays the recorded prefix and takes the next untried alternative at the frontier, depth-first, until no alternative is left untried or a budget is hit. Every run diff --git a/docs/reference/repl-commands.md b/docs/reference/repl-commands.md index e5373fa0e..0456b8228 100644 --- a/docs/reference/repl-commands.md +++ b/docs/reference/repl-commands.md @@ -23,7 +23,7 @@ into the parts it holds (`car.fl.hub`, `#3.fl`, `car.wheels[2]`). | `%save ` | Write the session model to a file: `.sysml` notation (comments preserved) or `.ttl` RDF, which is [experimental](rdf-mapping.md#status-experimental) and reported as such on each save | | `%query ` | Identify model elements using OSLC Query text | | `%verbosity [level]` | Show or set output level: `quiet` (errors only), `normal`, `debug` (every diagnostic over the whole buffer) | -| `%trace [on\|off]` | Show or set execution tracing: each evaluation, calc invocation, action step and state transition, and each `choice` the executor made among alternatives the library leaves unordered — several steppable tokens, several holding decision guards, several enabled transitions out of one state for one event, two tokens writing one feature in one step, two executors due at one instant of the clock — naming the alternatives and the one taken, and each `unevaluable guard` it read only to report one and could not evaluate ([Choice points](../guide/06-behavior.md)). `%step`, `%continue` and `%advance` end with a count of the choices they made and of the guards they could not evaluate (`1 choice point; 1 guard not evaluable`) whether or not tracing is on | +| `%trace [on\|off]` | Show or set execution tracing: each evaluation, calc invocation, action step and state transition, and each `choice` the executor made among alternatives the library leaves unordered — several steppable tokens, several holding decision guards, several enabled transitions out of one state for one event, several regions of one parallel state reacting to one event, two tokens writing one feature in one step, two executors due at one instant of the clock — naming the alternatives and the one taken, and each `unevaluable guard` it read only to report one and could not evaluate ([Choice points](../guide/06-behavior.md)). `%step`, `%continue` and `%advance` end with a count of the choices they made and of the guards they could not evaluate (`1 choice point; 1 guard not evaluable`) whether or not tracing is on | | `%schedule []` | Show or set the scheduling policy the executors resolve their [choice points](../guide/06-behavior.md) under: `reverse` (the default: reverse token order, first holding guard, first enabled transition), `declared` (spawn and declaration order) or `seed:` (a pseudo-random order the non-negative integer `n` fixes, so the same seed replays the same run). Applies to runs started from then on — `%action`, `%state`, `%analysis`; a calc's body performs nothing, so `%calc` has no choice to make — while a debugging session already under way keeps the policy it started with; every choice point a run reaches is reported and the `took …` of each `choice` line is what the policy took. A spelling naming no policy (an unknown name, `seed` or `seed:` without a number, `seed:-1`, `seed:abc`, a malformed `explore:` option) is refused and the policy is left as it was. `explore[:runs=N,depth=D]` is refused at the prompt too, as a typed error saying why: it replays a behavior from the start once per linearization, which `%action` and `%state`, stepping one run, cannot do — run `sysml -schedule explore -action ` (or `-state`, `-analysis`, `-calc`) for the outcome table ([Exploring every linearization](cli.md#exploring-every-linearization)), or send a request with that `schedule` over the wire | | `%strict [on\|off]` | Show or set strict conformance: report notation no SysML v2 production admits as an error, and reprint the session's diagnostics under the new mode ([Strict conformance](../guide/03-command-line.md#strict-conformance)) | | `%budget` | Show the five bounds one run may spend, each with the variable that raises it | diff --git a/internal/core/runtime/scheduler.go b/internal/core/runtime/scheduler.go index be1476a84..e54f88e14 100644 --- a/internal/core/runtime/scheduler.go +++ b/internal/core/runtime/scheduler.go @@ -10,10 +10,11 @@ import ( // A run's choice points — several steppable tokens in one step, several holding // guards at a decision, several enabled transitions for one event, several -// executors due at one instant of the clock — are resolved by a scheduling -// policy; which of two same-step writes to one feature stands follows from the -// token order it chose. The default is what the executors always did; the others -// let a driver ask for another linearization of the run. +// regions reacting to one event, several executors due at one instant of the +// clock — are resolved by a scheduling policy; which of two same-step writes to +// one feature stands follows from the token order it chose. The default is what +// the executors always did; the others let a driver ask for another +// linearization of the run. // ErrInvalidSchedulePolicy is the typed error every unparseable policy spelling wraps. var ErrInvalidSchedulePolicy = errors.New("invalid scheduling policy") From b50646758598ccda39824cd9be43c8ac1573e889 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Wed, 9 Sep 2026 18:46:19 +0000 Subject: [PATCH 04/33] docs(examples): measure the expressions demo in the pilot differential Re-record the pilot differential baseline over the 34-file examples root so the new example is in the measured census, not only in its provenance: 368 files, 600 pilot-only, 636 pilot diagnostics, with the generated counts in README, architecture, the differential record and the testing skills regenerated together. Write the example to what both implementations accept where the notation allows it: metadata reads cast the Metaobject to its metadata def, metadata sequences and the held function are ref features, and the Heritage default uses the default keyword. The four remaining pilot-only rows are a calc def passed as an argument, adjudicated as a deliberate extension. Co-Authored-By: jason.han --- .../testing-pilot-corpora-gate/SKILL.md | 4 +- .../testing-pilot-differential/SKILL.md | 8 +-- .../testing-pilot-execution-referee/SKILL.md | 4 +- .agents/skills/testing-pilot-xpect/SKILL.md | 4 +- README.md | 6 +-- docs/guide/05-checking.md | 14 ++--- docs/internals/architecture.md | 4 +- docs/project/pilot-differential-baseline.json | 54 +++++++++++++++---- docs/project/pilot-differential.md | 28 ++++++---- examples/EXPRESSIONS-DEMO.md | 19 +++++-- examples/expressions-demo.sysml | 17 +++--- 11 files changed, 109 insertions(+), 53 deletions(-) diff --git a/.agents/skills/testing-pilot-corpora-gate/SKILL.md b/.agents/skills/testing-pilot-corpora-gate/SKILL.md index f3e7425e7..42112de46 100644 --- a/.agents/skills/testing-pilot-corpora-gate/SKILL.md +++ b/.agents/skills/testing-pilot-corpora-gate/SKILL.md @@ -183,8 +183,8 @@ gate's own helpers are package-private but reusable (`pilotCorporaGate.files(t)` `actionlint`, `shellcheck`, `python3 scripts/check-doc-links.py`, `gofmt`, `go vet`, `go run ./cmd/pilot-diff` (validators pre-downloaded; ~4min, prints e.g. -the headline the committed baseline holds — `367 file(s), 337 fully agreeing; 34 agreed -diagnostic(s), 21 only ours, 596 only the pilot's` after the unbound-parameter round, so read it from +the headline the committed baseline holds — `368 file(s), 337 fully agreeing; 34 agreed +diagnostic(s), 21 only ours, 600 only the pilot's` after the expressions example joined `examples/`, so read it from `docs/project/pilot-differential-baseline.json` rather than from this line) and `make lint` (staticcheck+gosec, ~2min) all work. There is **no** `yamllint` and **no** `circleci` CLI, so `.circleci/config.yml` can only be parsed as YAML, not schema-validated — say so diff --git a/.agents/skills/testing-pilot-differential/SKILL.md b/.agents/skills/testing-pilot-differential/SKILL.md index 48ddb5841..271bf9c97 100644 --- a/.agents/skills/testing-pilot-differential/SKILL.md +++ b/.agents/skills/testing-pilot-differential/SKILL.md @@ -21,9 +21,9 @@ GNU-format diagnostics **relative to `--root`**. Consequences for testing: - The pin `cmd/pilot-diff` reports comes from `build/pilot-sysml-validator/pilot-pin.txt` (written by the new script), not from the DeciSym `pom.xml`. - `-validator /nonexistent` now says `run ./scripts/download-pilot-sysml-validator.sh`. -- Measured after the unbound-parameter round, with a fresh library cache: `367 file(s), 337 fully agreeing; 34 agreed, - 21 only ours, 596 only the pilot's`, JSON totals `openSysMLDiagnostics 57 / pilotDiagnostics - 632 / severityMismatch 2`; ~2 min wall, byte-identical across runs *and* after a from-scratch +- Measured after the expressions example joined `examples/`, with a fresh library cache: `368 file(s), 337 fully agreeing; 34 agreed, + 21 only ours, 600 only the pilot's`, JSON totals `openSysMLDiagnostics 57 / pilotDiagnostics + 636 / severityMismatch 2`; ~2 min wall, byte-identical across runs *and* after a from-scratch rebuild of `build/pilot-validator`. `kerml-examples` carries no `syntax` diagnostic on either side. Refresh this paragraph with every rebaseline, and treat a stale one as a finding. - **`cmd/pilot-diff` has no `-jobs` flag.** Its full flag set is @@ -135,7 +135,7 @@ The harness compares OpenSysML diagnostics against the OMG SysML v2 Pilot Implem `build/pilot-diff/pilot-diff.{txt,json}`. `docs/project/pilot-differential-baseline.json` is the committed result of the *last refreshed* run, so **the harness is testable by reproduction** — but only while the baseline is current. Check that first. As of the rebaseline that came with the unbound-parameter round it **is** -current: a live run gives `367 file(s), 337 fully agreeing; 34 agreed, 21 only ours, 596 only the +current: a live run gives `368 file(s), 337 fully agreeing; 34 agreed, 21 only ours, 600 only the pilot's`, byte-identical to the committed baseline, and `docs/project/pilot-differential.md`'s "Results" table matches. The rebaseline before it, at the architecture self-model's landing, covered two rounds, because the succession-shorthand removal before it landed without refreshing the baseline; a control run of its merge commit gives diff --git a/.agents/skills/testing-pilot-execution-referee/SKILL.md b/.agents/skills/testing-pilot-execution-referee/SKILL.md index 3710fae56..7b638d76d 100644 --- a/.agents/skills/testing-pilot-execution-referee/SKILL.md +++ b/.agents/skills/testing-pilot-execution-referee/SKILL.md @@ -108,8 +108,8 @@ subset it or none does (and folds a `default null` one to `0`). See `pilot-exec-diff: :: model no/such/model.sysml: stat : no such file or directory`. - **Additivity.** `go run ./cmd/pilot-diff` must still print the headline the - committed baseline holds (`367 file(s), 337 fully agreeing; 34 agreed - diagnostic(s), 21 only ours, 596 only the pilot's` after the unbound-parameter round — read it from the baseline JSON, not from this line, since each + committed baseline holds (`368 file(s), 337 fully agreeing; 34 agreed + diagnostic(s), 21 only ours, 600 only the pilot's` after the expressions example joined `examples/` — read it from the baseline JSON, not from this line, since each fix round moves it) and `jq -S` diff clean against `docs/project/pilot-differential-baseline.json`; `git status --porcelain` empty at the end. diff --git a/.agents/skills/testing-pilot-xpect/SKILL.md b/.agents/skills/testing-pilot-xpect/SKILL.md index 4a0035d08..bc3b65e60 100644 --- a/.agents/skills/testing-pilot-xpect/SKILL.md +++ b/.agents/skills/testing-pilot-xpect/SKILL.md @@ -416,8 +416,8 @@ census in `w5c_census_test.go` is live two ways: perturb one pinned triple (e.g. ## Regression neighbour `go run ./cmd/pilot-diff` (~1m12s) must still print the headline the *committed* baseline holds — -after the unbound-parameter round that is `367 file(s), 337 fully agreeing; 34 agreed diagnostic(s), 21 -only ours, 596 only the pilot's`. Read the number out of +after the expressions example joined `examples/` that is `368 file(s), 337 fully agreeing; 34 agreed diagnostic(s), 21 +only ours, 600 only the pilot's`. Read the number out of `docs/project/pilot-differential-baseline.json` rather than trusting this line, since a landing fix round moves it. When the baseline is itself stale (it was at `19a3ce03`, holding 273 / 281 / 317), a failing `cmp` against it is *not* evidence of an Xpect regression — compare the summary line, and see diff --git a/README.md b/README.md index b8f6267e5..fdc0166c0 100644 --- a/README.md +++ b/README.md @@ -233,11 +233,11 @@ The project is under active development, with the core infrastructure operationa **Measured against the pinned reference** (`PILOT_TAG=2026-07`, artifact `0.61.0`). Every number below is generated by `make docs-counts` from the committed baselines and gated; none of them is typed in by hand. -- **Corpus agreement:** 337 of 367 files agree diagnostic-by-diagnostic; 21 diagnostics are ours alone and 596 the reference's alone, and the first number must be read by root: our diagnostics against the reference's own corpora fell while our non-standard-notation warnings on our own example models rose ([differential](docs/project/pilot-differential.md), `go run ./cmd/pilot-diff`). +- **Corpus agreement:** 337 of 368 files agree diagnostic-by-diagnostic; 21 diagnostics are ours alone and 600 the reference's alone, and the first number must be read by root: our diagnostics against the reference's own corpora fell while our non-standard-notation warnings on our own example models rose ([differential](docs/project/pilot-differential.md), `go run ./cmd/pilot-diff`). - **Declared-diagnostic silence:** of the 511 declared `errors` rows in the reference's own Xpect suites, we report nothing for 0. 244 we report word-for-word; 248 wording-only and 7 location-only differences are agreement in substance and are not counted as gaps; 0 more we report as a warning and 2 elsewhere in the file ([Xpect oracle](docs/project/pilot-xpect.md), `go run ./cmd/pilot-xpect`). - **Scope agreement:** 230 of 230 declared scope assertions match exactly (same source). - **Permissiveness gaps:** of 285 invalid models we wrote ourselves, the reference rejects 3 that we accept by default, and 273 both reject; 3 further cases agree only when we are asked strictly. We authored every one of these cases ourselves, so the denominator measures the reach of our own corpus and not our conformance; agreement reached only under an opt-in strict mode is weaker evidence than agreement by default ([rejection oracle](docs/project/pilot-rejection.md), `go run ./cmd/pilot-reject`). -- **Declared errata:** the registry declares 3 defect(s) in the published reference material — 1 with a specification-derived correction, 2 documented without one, since no intended reading can be inferred ([OMG issues](docs/project/omg-issues.md), `internal/errata`). Every figure above is as published and stays the conformance statement; running the same oracles over the corrected text instead reports 338 of 367 files agreeing, 20 diagnostics ours alone and 596 the reference's alone, 0 declared rows we are silent on, and 0 of 285 authored cases the reference alone rejects. The corrected figures are diagnostic only: an erratum never reclassifies a divergence category, and the published corpus is never edited. +- **Declared errata:** the registry declares 3 defect(s) in the published reference material — 1 with a specification-derived correction, 2 documented without one, since no intended reading can be inferred ([OMG issues](docs/project/omg-issues.md), `internal/errata`). Every figure above is as published and stays the conformance statement; running the same oracles over the corrected text instead reports 338 of 368 files agreeing, 20 diagnostics ours alone and 600 the reference's alone, 0 declared rows we are silent on, and 0 of 285 authored cases the reference alone rejects. The corrected figures are diagnostic only: an erratum never reclassifies a divergence category, and the published corpus is never edited. - **Self-assessed surface:** the action, state-machine and classifier-behavior rows have no external referee at all — the four refereed figures above cannot see them, because the pinned artifact evaluates expressions but executes neither actions nor state machines. [Spec compliance](docs/project/spec-compliance.md) counts them. What these numbers cannot show: the OMG corpora are demonstrations rather than an official conformance suite; the differential is one-directional, comparing the diagnostics the two implementations report on the same files; the Xpect suites are the pilot authors' test intent rather than a certification oracle; and none of these is a percentage of the specification — no global compliance figure is claimed anywhere. @@ -249,7 +249,7 @@ What these numbers cannot show: the OMG corpora are demonstrations rather than a **Test coverage:** 15,139 tests and subtests (15,122 pass, 17 skip — 3 skip themselves, 14 gate on a PDF toolchain, a pinned pilot artifact, a locale, a case-insensitive filesystem or a live Flexo stack; 6,570 top-level `Test` functions; counted with the OMG corpora downloaded and an SMT solver installed, without which 80 more skip) covering parsers, semantics, runtime (actions, states, instances, operators, validation). Behavioral robustness: 195 golden ASTs, 249 negatives, 671 conformance cases, 140 golden traces, 336 runtime robustness cases, 15 gRPC conformance cases and 8 gRPC robustness cases. **Parser coverage:** 98/98 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` and `OpenSysML Libraries/OOSEM.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 (671/671 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:** 367 files compared diagnostic-by-diagnostic against the pinned OMG pilot implementation (`2026-07`), 337 in full agreement; every divergence is enumerated and adjudicated in [the differential](docs/project/pilot-differential.md), reproducible with `go run ./cmd/pilot-diff`. +**Reference differential:** 368 files compared diagnostic-by-diagnostic against the pinned OMG pilot implementation (`2026-07`), 337 in full agreement; every divergence is enumerated and adjudicated in [the differential](docs/project/pilot-differential.md), reproducible with `go run ./cmd/pilot-diff`. **Rejection oracle:** the reverse direction — do we reject what the reference rejects? 285 hand-written invalid models validated by both implementations, 276 rejected by both, 0 the pinned pilot rejects and we accept; the remainder only we reject — the control-node succession rules the pinned pilot leaves unimplemented and a non-Boolean succession guard it accepts once the standard library types it — and every permissiveness gap is enumerated with a reproducer and likely root cause in [the rejection oracle](docs/project/pilot-rejection.md), reproducible with `go run ./cmd/pilot-reject`. We wrote every case, so the count measures our coverage of the rejection surface, not our conformance — a sample, not a proof. **Training examples:** 100/100 files clean, gated by `internal/core/model/testdata/training_examples_expected.txt`. Download with `./scripts/download-training-examples.sh` (from the [OMG training directory](https://github.com/Systems-Modeling/SysML-v2-Pilot-Implementation/tree/master/sysml/src/training)). See [training examples](docs/project/training-examples.md) for analysis. **Semantic layer:** a complete implementation of runtime operators, feature chains and validation rules. See [examples/semantic-layer/](examples/semantic-layer/) for a full demonstration. diff --git a/docs/guide/05-checking.md b/docs/guide/05-checking.md index e282092ce..d57790145 100644 --- a/docs/guide/05-checking.md +++ b/docs/guide/05-checking.md @@ -153,24 +153,26 @@ error: evaluation failed: type mismatch: operator '+' is not defined for the unb **Metadata:** `elem.metadata` is the sequence of metadata annotating `elem`, one object per annotation in the order written, each carrying the values its body binds over the defaults its -`metadata def` declares. An element with no annotation answers the empty sequence. +`metadata def` declares. An element with no annotation answers the empty sequence. The library +types the sequence as `Metaobject`, so cast an annotation to its `metadata def` before reading +the values it binds. ```sysml sysml> package Provenance { ...> private import ScalarValues::*; - ...> metadata def Heritage { attribute mission : String; attribute flown : Boolean = true; } + ...> metadata def Heritage { attribute mission : String; attribute flown : Boolean default true; } ...> part def Camera; ...> part navCam : Camera { @Heritage { mission = "Cassini"; } } ...> part sciCam : Camera; ...> } ✓ package Provenance -sysml> %eval Provenance::navCam.metadata#(1).mission -✓ Provenance::navCam.metadata#(1).mission +sysml> %eval (Provenance::navCam.metadata#(1) as Provenance::Heritage).mission +✓ (Provenance::navCam.metadata#(1) as Provenance::Heritage).mission = "Cassini" -sysml> %eval Provenance::navCam.metadata#(1).flown -✓ Provenance::navCam.metadata#(1).flown +sysml> %eval (Provenance::navCam.metadata#(1) as Provenance::Heritage).flown +✓ (Provenance::navCam.metadata#(1) as Provenance::Heritage).flown = true sysml> %eval Provenance::sciCam.metadata diff --git a/docs/internals/architecture.md b/docs/internals/architecture.md index b2e9aade6..f31595cef 100644 --- a/docs/internals/architecture.md +++ b/docs/internals/architecture.md @@ -734,11 +734,11 @@ Every behavioral feature must have: **Measured against the pinned reference** (`PILOT_TAG=2026-07`, artifact `0.61.0`). Every number below is generated by `make docs-counts` from the committed baselines and gated; none of them is typed in by hand. -- **Corpus agreement:** 337 of 367 files agree diagnostic-by-diagnostic; 21 diagnostics are ours alone and 596 the reference's alone, and the first number must be read by root: our diagnostics against the reference's own corpora fell while our non-standard-notation warnings on our own example models rose ([differential](../project/pilot-differential.md), `go run ./cmd/pilot-diff`). +- **Corpus agreement:** 337 of 368 files agree diagnostic-by-diagnostic; 21 diagnostics are ours alone and 600 the reference's alone, and the first number must be read by root: our diagnostics against the reference's own corpora fell while our non-standard-notation warnings on our own example models rose ([differential](../project/pilot-differential.md), `go run ./cmd/pilot-diff`). - **Declared-diagnostic silence:** of the 511 declared `errors` rows in the reference's own Xpect suites, we report nothing for 0. 244 we report word-for-word; 248 wording-only and 7 location-only differences are agreement in substance and are not counted as gaps; 0 more we report as a warning and 2 elsewhere in the file ([Xpect oracle](../project/pilot-xpect.md), `go run ./cmd/pilot-xpect`). - **Scope agreement:** 230 of 230 declared scope assertions match exactly (same source). - **Permissiveness gaps:** of 285 invalid models we wrote ourselves, the reference rejects 3 that we accept by default, and 273 both reject; 3 further cases agree only when we are asked strictly. We authored every one of these cases ourselves, so the denominator measures the reach of our own corpus and not our conformance; agreement reached only under an opt-in strict mode is weaker evidence than agreement by default ([rejection oracle](../project/pilot-rejection.md), `go run ./cmd/pilot-reject`). -- **Declared errata:** the registry declares 3 defect(s) in the published reference material — 1 with a specification-derived correction, 2 documented without one, since no intended reading can be inferred ([OMG issues](../project/omg-issues.md), `internal/errata`). Every figure above is as published and stays the conformance statement; running the same oracles over the corrected text instead reports 338 of 367 files agreeing, 20 diagnostics ours alone and 596 the reference's alone, 0 declared rows we are silent on, and 0 of 285 authored cases the reference alone rejects. The corrected figures are diagnostic only: an erratum never reclassifies a divergence category, and the published corpus is never edited. +- **Declared errata:** the registry declares 3 defect(s) in the published reference material — 1 with a specification-derived correction, 2 documented without one, since no intended reading can be inferred ([OMG issues](../project/omg-issues.md), `internal/errata`). Every figure above is as published and stays the conformance statement; running the same oracles over the corrected text instead reports 338 of 368 files agreeing, 20 diagnostics ours alone and 600 the reference's alone, 0 declared rows we are silent on, and 0 of 285 authored cases the reference alone rejects. The corrected figures are diagnostic only: an erratum never reclassifies a divergence category, and the published corpus is never edited. - **Self-assessed surface:** the action, state-machine and classifier-behavior rows have no external referee at all — the four refereed figures above cannot see them, because the pinned artifact evaluates expressions but executes neither actions nor state machines. [Spec compliance](../project/spec-compliance.md) counts them. What these numbers cannot show: the OMG corpora are demonstrations rather than an official conformance suite; the differential is one-directional, comparing the diagnostics the two implementations report on the same files; the Xpect suites are the pilot authors' test intent rather than a certification oracle; and none of these is a percentage of the specification — no global compliance figure is claimed anywhere. diff --git a/docs/project/pilot-differential-baseline.json b/docs/project/pilot-differential-baseline.json index cb90aaeaa..82e57f2b6 100644 --- a/docs/project/pilot-differential-baseline.json +++ b/docs/project/pilot-differential-baseline.json @@ -61,7 +61,7 @@ "dir": "examples", "origin": "ours", "files": 34, - "digest": "sha256:c2e816860b279abd662c6f411719b05147ee9a749a711d02fe01f892bbdfe0ef" + "digest": "sha256:b4e18def4b6e2cc375578908bd2fe11f52895a48dcabc8427b911193d2015307" }, { "name": "probes", @@ -71,17 +71,17 @@ "digest": "sha256:b0153c55bbfcdacabab911725dc44e0e7f4d3a501a281b1f3f2a13cda19737c6" } ], - "recorded": "2026-09-08" + "recorded": "2026-09-09" }, "totals": { - "files": 367, + "files": 368, "filesFullyAgreeing": 337, "agreement": 34, "severityMismatch": 2, "openSysMLOnly": 21, - "pilotOnly": 596, + "pilotOnly": 600, "openSysMLDiagnostics": 57, - "pilotDiagnostics": 632 + "pilotDiagnostics": 636 }, "roots": [ { @@ -748,14 +748,14 @@ "name": "examples", "dir": "examples", "totals": { - "files": 33, + "files": 34, "filesFullyAgreeing": 25, "agreement": 0, "severityMismatch": 1, "openSysMLOnly": 1, - "pilotOnly": 570, + "pilotOnly": 574, "openSysMLDiagnostics": 2, - "pilotDiagnostics": 571 + "pilotDiagnostics": 575 }, "files": [ { @@ -810,6 +810,38 @@ } ] }, + { + "path": "expressions-demo.sysml", + "agreement": [], + "severityMismatch": [], + "openSysMLOnly": [], + "pilotOnly": [ + { + "line": 95, + "severity": "error", + "category": "kind-mismatch", + "count": 1 + }, + { + "line": 96, + "severity": "error", + "category": "kind-mismatch", + "count": 1 + }, + { + "line": 100, + "severity": "error", + "category": "kind-mismatch", + "count": 1 + }, + { + "line": 110, + "severity": "error", + "category": "kind-mismatch", + "count": 1 + } + ] + }, { "path": "oosem-demo/oosem-demo.sysml", "agreement": [], @@ -3730,14 +3762,14 @@ } ], "totals": { - "files": 367, + "files": 368, "filesFullyAgreeing": 338, "agreement": 34, "severityMismatch": 2, "openSysMLOnly": 20, - "pilotOnly": 596, + "pilotOnly": 600, "openSysMLDiagnostics": 56, - "pilotDiagnostics": 632 + "pilotDiagnostics": 636 }, "findings": [ { diff --git a/docs/project/pilot-differential.md b/docs/project/pilot-differential.md index 0f19232f4..3c4eda353 100644 --- a/docs/project/pilot-differential.md +++ b/docs/project/pilot-differential.md @@ -208,7 +208,7 @@ nor double-counted as two independent disagreements. --- -## Results (pilot `2026-07`, 367 files) +## Results (pilot `2026-07`, 368 files) | Root | Files | Fully agreeing | Ours | Pilot | Agreed | Severity-only | Only ours | Only pilot | |---|---:|---:|---:|---:|---:|---:|---:|---:| @@ -217,9 +217,9 @@ nor double-counted as two independent disagreements. | `examples/pilot-corpora/sysml-validation` | 56 | 56 | 0 | 0 | 0 | 0 | 0 | 0 | | `examples/pilot-corpora/kerml-examples` | 58 | 50 | 4 | 6 | 0 | 0 | 4 | 6 | | `testdata` | 17 | 10 | 38 | 55 | 34 | 1 | 3 | 20 | -| `examples` | 33 | 25 | 2 | 571 | 0 | 1 | 1 | 570 | +| `examples` | 34 | 25 | 2 | 575 | 0 | 1 | 1 | 574 | | `cmd/pilot-diff/testdata` (probes) | 4 | 1 | 6 | 0 | 0 | 0 | 6 | 0 | -| **Total** | **367** | **337** | **57** | **632** | **34** | **2** | **21** | **596** | +| **Total** | **368** | **337** | **57** | **636** | **34** | **2** | **21** | **600** | **Read the `only ours` total by root, never as one number.** Step 2 removes nine resolver false positives from the reference's **own** corpora: `pilot-examples` 16 → **7** and @@ -381,8 +381,8 @@ cascades through the rest of the file. The movement is entirely one file, | Count | Before the initializer rewrite | Now | |---|---:|---:| -| only pilot | 82 | **596** | -| pilot diagnostics | 123 | **632** | +| only pilot | 82 | **600** | +| pilot diagnostics | 123 | **636** | | severity-only | 9 | **2** | The rewrite itself took only-pilot to 61 and pilot diagnostics to 101; the `Now` column states @@ -513,7 +513,7 @@ Per category, the only-ours totals are: `pilot-examples` 4 `unmapped`, 2 [unbound-parameter advisory](#the-unbound-parameter-advisory)); `examples` 1 syntax; `testdata` 2 `unmapped`, 1 `multiplicity`; `probes` 6 `unmapped`. Only-pilot: `testdata` 12 `kind-mismatch`, 3 `unmapped`, 3 syntax, 2 `unresolved-reference`; -`examples` 10 syntax, 15 `unmapped`, 258 `kind-mismatch`, 287 `unresolved-reference` — of which +`examples` 10 syntax, 15 `unmapped`, 262 `kind-mismatch`, 287 `unresolved-reference` — of which `relay-probe-demo/mission.sysml` carries none: it carried a `kind-mismatch` on its send of a `Telemetry` invocation until the send-argument round above, and the demo now writes the constructor, `send new Telemetry(…) via antenna`, which both implementations accept, so the row @@ -556,6 +556,16 @@ cousins, 7 of them warnings). The `examples` only-pilot column moves 302 → 572 stays at 20 and our diagnostics at 65: two files the reference has no library for, plus the 48 rows the other files carry. +**`expressions-demo.sysml` adds 4 pilot-only `kind-mismatch` rows, all one shape: a `calc def` +passed as an argument.** The example passes `Square` and `Halve` to an `in calc` parameter +(`Apply(Square, a)`, `Sample(Square, xs)`), and the reference reports each argument as `Must be a +valid feature`: it has no function values, so a definition can appear only where a type is +expected. Here a calculation named as an operand is a function value, so the argument is accepted +and invoked. The example's other forms were written to what both accept — its metadata reads cast +the `Metaobject` to its `metadata def` before reading a value, its metadata sequences are `ref` +features rather than attributes, and the function held in a part is a `ref` to a calc usage — so +these four rows are the whole of the disagreement, and each is a deliberate extension, not a gap. + **`pilot-examples` is the row to read carefully: its total falls 68 → 63 and its mix barely resembles the old one.** All 31 syntax rows are gone, and `pilot-validation`'s 7 with them — the parser now parses notation we used to reject. But `unresolved-reference` rises 27 → 36, `unmapped` 5 → 17 and @@ -588,13 +598,13 @@ page's history. | Count | Now | |---|---:| | overall: fully agreeing / only ours / our diagnostics | **337 / 21 / 57** | -| only pilot | **596** | -| pilot diagnostics | **632** | +| only pilot | **600** | +| pilot diagnostics | **636** | | severity-only | **2** | | unmapped, our side | **19** | | kerml-examples: only ours | **4** | | pilot-examples: only ours | **7** | -| examples: only pilot | **570** | +| examples: only pilot | **574** | The KerML root is now the *cleanest* of the three OMG roots in proportion: **4** only-ours against 6 only-pilot — the only root where the reference reports more than we do — with 50 of 58 files fully diff --git a/examples/EXPRESSIONS-DEMO.md b/examples/EXPRESSIONS-DEMO.md index cc65e997b..cba38358a 100644 --- a/examples/EXPRESSIONS-DEMO.md +++ b/examples/EXPRESSIONS-DEMO.md @@ -150,7 +150,12 @@ Features: `navCamFlown` is `true` without `navCam` saying so: the annotation did not bind `flown`, so the object carries the default from `Heritage`. Indexing is one-based, as everywhere in SysML: `navCam.metadata#(1)` is the first -annotation. +annotation. The library types `.metadata` as `Metaobject`, which has no +`mission` of its own, so the report casts the annotation to `Heritage` before +reading it — `(navCam.metadata#(1) as Heritage).mission` — the same cast as +the first section, selecting the object because it conforms. A sequence of +metadata objects is held by a `ref`, not an `attribute`: an attribute holds +data values, and an annotation is an object. ## A calculation as a value @@ -210,10 +215,14 @@ Features: squaredAtThree = 9.0 ``` -A definition is not a feature, so `attribute transfer = Square;` is refused by -the checker ("Must be a valid feature") where `attribute transfer = amplify;` -— a calc usage — is fine; a `calc def` is passed as an argument, as -`Apply(Square, 3.0)` does, or held through a usage of it. +A definition is not a feature, so `ref transfer = Square;` is refused by the +checker ("Must be a valid feature") where `ref transfer = amplify;` — a calc +usage — is fine; a `calc def` is passed as an argument, as `Apply(Square, 3.0)` +does, or held through a usage of it. Passing a definition is the one place the +reference implementation disagrees with this file: it reports `Apply(Square, +3.0)` as "Must be a valid feature" too, because it has no function values to +receive a `calc def`. To stay within what both accept, name a usage — +`Apply(transfer, 3.0)` — instead. ## `Set` — no order, no repeats diff --git a/examples/expressions-demo.sysml b/examples/expressions-demo.sysml index eb48561e1..16c8affe2 100644 --- a/examples/expressions-demo.sysml +++ b/examples/expressions-demo.sysml @@ -18,7 +18,7 @@ package ExpressionsDemo { metadata def Heritage { attribute mission : String; - attribute flown : Boolean = true; + attribute flown : Boolean default true; } part def Instrument { @@ -71,11 +71,14 @@ package ExpressionsDemo { // --- `.metadata`: what annotates an element ------------------------------- part def HeritageReport { - attribute navCamAnnotations [*] = navCam.metadata; - attribute navCamMission : String = navCam.metadata#(1).mission; - attribute navCamFlown : Boolean = navCam.metadata#(1).flown; - attribute spectrometerFlown : Boolean = spectrometer.metadata#(1).flown; - attribute sciCamAnnotations [*] = sciCam.metadata; + ref navCamAnnotations [*] = navCam.metadata; + attribute navCamMission : String = + (navCam.metadata#(1) as Heritage).mission; + attribute navCamFlown : Boolean = + (navCam.metadata#(1) as Heritage).flown; + attribute spectrometerFlown : Boolean = + (spectrometer.metadata#(1) as Heritage).flown; + ref sciCamAnnotations [*] = sciCam.metadata; } // --- Calculations as values ----------------------------------------------- @@ -101,7 +104,7 @@ package ExpressionsDemo { part def Amplifier { attribute gain : Real = 1.5; calc amplify { in v : Real; return : Real = v * gain; } - attribute transfer = amplify; + ref transfer = amplify; attribute sameTransfer : Boolean = transfer == amplify; attribute atThree : Real = Apply(transfer, 3.0); attribute squaredAtThree : Real = Apply(Square, 3.0); From a52275ff3470c875c68f97e92d52f1608d5986b4 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Wed, 9 Sep 2026 18:55:18 +0000 Subject: [PATCH 05/33] docs(examples): re-measure the examples root with the analysis walkthrough beside the expressions demo Both walkthroughs now sit in the examples root, so the differential baseline and the RDF round-trip ratchet are re-recorded over the 35-file root: 369 files, 338 fully agreeing, 600 pilot-only, 636 pilot diagnostics; 348 stable round trips. The generated counts and the testing skills' figures follow. Co-Authored-By: jason.han --- .../testing-pilot-corpora-gate/SKILL.md | 4 +- .../testing-pilot-differential/SKILL.md | 10 ++-- .../testing-pilot-execution-referee/SKILL.md | 4 +- .agents/skills/testing-pilot-xpect/SKILL.md | 4 +- README.md | 6 +-- docs/internals/architecture.md | 4 +- docs/project/pilot-differential-baseline.json | 54 +++++++++++++++---- docs/project/pilot-differential.md | 26 +++++---- docs/project/rdf-corpus-roundtrip.md | 8 +-- .../testdata/corpus_roundtrip_expected.txt | 2 +- 10 files changed, 81 insertions(+), 41 deletions(-) diff --git a/.agents/skills/testing-pilot-corpora-gate/SKILL.md b/.agents/skills/testing-pilot-corpora-gate/SKILL.md index 2abb78d38..254336760 100644 --- a/.agents/skills/testing-pilot-corpora-gate/SKILL.md +++ b/.agents/skills/testing-pilot-corpora-gate/SKILL.md @@ -183,8 +183,8 @@ gate's own helpers are package-private but reusable (`pilotCorporaGate.files(t)` `actionlint`, `shellcheck`, `python3 scripts/check-doc-links.py`, `gofmt`, `go vet`, `go run ./cmd/pilot-diff` (validators pre-downloaded; ~4min, prints e.g. -the headline the committed baseline holds — `368 file(s), 338 fully agreeing; 34 agreed -diagnostic(s), 21 only ours, 596 only the pilot's` after the unbound-parameter round, so read it from +the headline the committed baseline holds — `369 file(s), 338 fully agreeing; 34 agreed +diagnostic(s), 21 only ours, 600 only the pilot's` after the expressions example joined `examples/`, so read it from `docs/project/pilot-differential-baseline.json` rather than from this line) and `make lint` (staticcheck+gosec, ~2min) all work. There is **no** `yamllint` and **no** `circleci` CLI, so `.circleci/config.yml` can only be parsed as YAML, not schema-validated — say so diff --git a/.agents/skills/testing-pilot-differential/SKILL.md b/.agents/skills/testing-pilot-differential/SKILL.md index 76f5d01d1..df659a05d 100644 --- a/.agents/skills/testing-pilot-differential/SKILL.md +++ b/.agents/skills/testing-pilot-differential/SKILL.md @@ -21,9 +21,9 @@ GNU-format diagnostics **relative to `--root`**. Consequences for testing: - The pin `cmd/pilot-diff` reports comes from `build/pilot-sysml-validator/pilot-pin.txt` (written by the new script), not from the DeciSym `pom.xml`. - `-validator /nonexistent` now says `run ./scripts/download-pilot-sysml-validator.sh`. -- Measured after the unbound-parameter round, with a fresh library cache: `368 file(s), 338 fully agreeing; 34 agreed, - 21 only ours, 596 only the pilot's`, JSON totals `openSysMLDiagnostics 57 / pilotDiagnostics - 632 / severityMismatch 2`; ~2 min wall, byte-identical across runs *and* after a from-scratch +- Measured after the expressions example joined `examples/`, with a fresh library cache: `369 file(s), 338 fully agreeing; 34 agreed, + 21 only ours, 600 only the pilot's`, JSON totals `openSysMLDiagnostics 57 / pilotDiagnostics + 636 / severityMismatch 2`; ~2 min wall, byte-identical across runs *and* after a from-scratch rebuild of `build/pilot-validator`. `kerml-examples` carries no `syntax` diagnostic on either side. Refresh this paragraph with every rebaseline, and treat a stale one as a finding. - **`cmd/pilot-diff` has no `-jobs` flag.** Its full flag set is @@ -134,8 +134,8 @@ The harness compares OpenSysML diagnostics against the OMG SysML v2 Pilot Implem (via two pinned plain-Java bridges over the pilot's own validators) over four corpus roots and writes `build/pilot-diff/pilot-diff.{txt,json}`. `docs/project/pilot-differential-baseline.json` is the committed result of the *last refreshed* run, so **the harness is testable by reproduction** — -but only while the baseline is current. Check that first. As of the rebaseline that came with the unbound-parameter round it **is** -current: a live run gives `368 file(s), 338 fully agreeing; 34 agreed, 21 only ours, 596 only the +but only while the baseline is current. Check that first. As of the rebaseline that came with the expressions walkthrough round it **is** +current: a live run gives `369 file(s), 338 fully agreeing; 34 agreed, 21 only ours, 600 only the pilot's`, byte-identical to the committed baseline, and `docs/project/pilot-differential.md`'s "Results" table matches. The rebaseline before it, at the architecture self-model's landing, covered two rounds, because the succession-shorthand removal before it landed without refreshing the baseline; a control run of its merge commit gives diff --git a/.agents/skills/testing-pilot-execution-referee/SKILL.md b/.agents/skills/testing-pilot-execution-referee/SKILL.md index d0492355c..1322c1c68 100644 --- a/.agents/skills/testing-pilot-execution-referee/SKILL.md +++ b/.agents/skills/testing-pilot-execution-referee/SKILL.md @@ -108,8 +108,8 @@ subset it or none does (and folds a `default null` one to `0`). See `pilot-exec-diff: :: model no/such/model.sysml: stat : no such file or directory`. - **Additivity.** `go run ./cmd/pilot-diff` must still print the headline the - committed baseline holds (`368 file(s), 338 fully agreeing; 34 agreed - diagnostic(s), 21 only ours, 596 only the pilot's` after the unbound-parameter round — read it from the baseline JSON, not from this line, since each + committed baseline holds (`369 file(s), 338 fully agreeing; 34 agreed + diagnostic(s), 21 only ours, 600 only the pilot's` after the expressions example joined `examples/` — read it from the baseline JSON, not from this line, since each fix round moves it) and `jq -S` diff clean against `docs/project/pilot-differential-baseline.json`; `git status --porcelain` empty at the end. diff --git a/.agents/skills/testing-pilot-xpect/SKILL.md b/.agents/skills/testing-pilot-xpect/SKILL.md index 200d11834..79c041693 100644 --- a/.agents/skills/testing-pilot-xpect/SKILL.md +++ b/.agents/skills/testing-pilot-xpect/SKILL.md @@ -416,8 +416,8 @@ census in `w5c_census_test.go` is live two ways: perturb one pinned triple (e.g. ## Regression neighbour `go run ./cmd/pilot-diff` (~1m12s) must still print the headline the *committed* baseline holds — -after the unbound-parameter round that is `368 file(s), 338 fully agreeing; 34 agreed diagnostic(s), 21 -only ours, 596 only the pilot's`. Read the number out of +after the expressions walkthrough round that is `369 file(s), 338 fully agreeing; 34 agreed diagnostic(s), 21 +only ours, 600 only the pilot's`. Read the number out of `docs/project/pilot-differential-baseline.json` rather than trusting this line, since a landing fix round moves it. When the baseline is itself stale (it was at `19a3ce03`, holding 273 / 281 / 317), a failing `cmp` against it is *not* evidence of an Xpect regression — compare the summary line, and see diff --git a/README.md b/README.md index 23e10a862..d1b48c424 100644 --- a/README.md +++ b/README.md @@ -253,11 +253,11 @@ The project is under active development, with the core infrastructure operationa **Measured against the pinned reference** (`PILOT_TAG=2026-07`, artifact `0.61.0`). Every number below is generated by `make docs-counts` from the committed baselines and gated; none of them is typed in by hand. -- **Corpus agreement:** 338 of 368 files agree diagnostic-by-diagnostic; 21 diagnostics are ours alone and 596 the reference's alone, and the first number must be read by root: our diagnostics against the reference's own corpora fell while our non-standard-notation warnings on our own example models rose ([differential](docs/project/pilot-differential.md), `go run ./cmd/pilot-diff`). +- **Corpus agreement:** 338 of 369 files agree diagnostic-by-diagnostic; 21 diagnostics are ours alone and 600 the reference's alone, and the first number must be read by root: our diagnostics against the reference's own corpora fell while our non-standard-notation warnings on our own example models rose ([differential](docs/project/pilot-differential.md), `go run ./cmd/pilot-diff`). - **Declared-diagnostic silence:** of the 511 declared `errors` rows in the reference's own Xpect suites, we report nothing for 0. 244 we report word-for-word; 248 wording-only and 7 location-only differences are agreement in substance and are not counted as gaps; 0 more we report as a warning and 2 elsewhere in the file ([Xpect oracle](docs/project/pilot-xpect.md), `go run ./cmd/pilot-xpect`). - **Scope agreement:** 230 of 230 declared scope assertions match exactly (same source). - **Permissiveness gaps:** of 285 invalid models we wrote ourselves, the reference rejects 3 that we accept by default, and 273 both reject; 3 further cases agree only when we are asked strictly. We authored every one of these cases ourselves, so the denominator measures the reach of our own corpus and not our conformance; agreement reached only under an opt-in strict mode is weaker evidence than agreement by default ([rejection oracle](docs/project/pilot-rejection.md), `go run ./cmd/pilot-reject`). -- **Declared errata:** the registry declares 3 defect(s) in the published reference material — 1 with a specification-derived correction, 2 documented without one, since no intended reading can be inferred ([OMG issues](docs/project/omg-issues.md), `internal/errata`). Every figure above is as published and stays the conformance statement; running the same oracles over the corrected text instead reports 339 of 368 files agreeing, 20 diagnostics ours alone and 596 the reference's alone, 0 declared rows we are silent on, and 0 of 285 authored cases the reference alone rejects. The corrected figures are diagnostic only: an erratum never reclassifies a divergence category, and the published corpus is never edited. +- **Declared errata:** the registry declares 3 defect(s) in the published reference material — 1 with a specification-derived correction, 2 documented without one, since no intended reading can be inferred ([OMG issues](docs/project/omg-issues.md), `internal/errata`). Every figure above is as published and stays the conformance statement; running the same oracles over the corrected text instead reports 339 of 369 files agreeing, 20 diagnostics ours alone and 600 the reference's alone, 0 declared rows we are silent on, and 0 of 285 authored cases the reference alone rejects. The corrected figures are diagnostic only: an erratum never reclassifies a divergence category, and the published corpus is never edited. - **Self-assessed surface:** the action, state-machine and classifier-behavior rows have no external referee at all — the four refereed figures above cannot see them, because the pinned artifact evaluates expressions but executes neither actions nor state machines. [Spec compliance](docs/project/spec-compliance.md) counts them. What these numbers cannot show: the OMG corpora are demonstrations rather than an official conformance suite; the differential is one-directional, comparing the diagnostics the two implementations report on the same files; the Xpect suites are the pilot authors' test intent rather than a certification oracle; and none of these is a percentage of the specification — no global compliance figure is claimed anywhere. @@ -269,7 +269,7 @@ What these numbers cannot show: the OMG corpora are demonstrations rather than a **Test coverage:** 15,139 tests and subtests (15,122 pass, 17 skip — 3 skip themselves, 14 gate on a PDF toolchain, a pinned pilot artifact, a locale, a case-insensitive filesystem or a live Flexo stack; 6,570 top-level `Test` functions; counted with the OMG corpora downloaded and an SMT solver installed, without which 80 more skip) covering parsers, semantics, runtime (actions, states, instances, operators, validation). Behavioral robustness: 195 golden ASTs, 249 negatives, 671 conformance cases, 140 golden traces, 336 runtime robustness cases, 15 gRPC conformance cases and 8 gRPC robustness cases. **Parser coverage:** 98/98 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` and `OpenSysML Libraries/OOSEM.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 (671/671 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:** 368 files compared diagnostic-by-diagnostic against the pinned OMG pilot implementation (`2026-07`), 338 in full agreement; every divergence is enumerated and adjudicated in [the differential](docs/project/pilot-differential.md), reproducible with `go run ./cmd/pilot-diff`. +**Reference differential:** 369 files compared diagnostic-by-diagnostic against the pinned OMG pilot implementation (`2026-07`), 338 in full agreement; every divergence is enumerated and adjudicated in [the differential](docs/project/pilot-differential.md), reproducible with `go run ./cmd/pilot-diff`. **Rejection oracle:** the reverse direction — do we reject what the reference rejects? 285 hand-written invalid models validated by both implementations, 276 rejected by both, 0 the pinned pilot rejects and we accept; the remainder only we reject — the control-node succession rules the pinned pilot leaves unimplemented and a non-Boolean succession guard it accepts once the standard library types it — and every permissiveness gap is enumerated with a reproducer and likely root cause in [the rejection oracle](docs/project/pilot-rejection.md), reproducible with `go run ./cmd/pilot-reject`. We wrote every case, so the count measures our coverage of the rejection surface, not our conformance — a sample, not a proof. **Training examples:** 100/100 files clean, gated by `internal/core/model/testdata/training_examples_expected.txt`. Download with `./scripts/download-training-examples.sh` (from the [OMG training directory](https://github.com/Systems-Modeling/SysML-v2-Pilot-Implementation/tree/master/sysml/src/training)). See [training examples](docs/project/training-examples.md) for analysis. **Semantic layer:** a complete implementation of runtime operators, feature chains and validation rules. See [examples/semantic-layer/](examples/semantic-layer/) for a full demonstration. diff --git a/docs/internals/architecture.md b/docs/internals/architecture.md index 4c43fbb7c..650b0796f 100644 --- a/docs/internals/architecture.md +++ b/docs/internals/architecture.md @@ -734,11 +734,11 @@ Every behavioral feature must have: **Measured against the pinned reference** (`PILOT_TAG=2026-07`, artifact `0.61.0`). Every number below is generated by `make docs-counts` from the committed baselines and gated; none of them is typed in by hand. -- **Corpus agreement:** 338 of 368 files agree diagnostic-by-diagnostic; 21 diagnostics are ours alone and 596 the reference's alone, and the first number must be read by root: our diagnostics against the reference's own corpora fell while our non-standard-notation warnings on our own example models rose ([differential](../project/pilot-differential.md), `go run ./cmd/pilot-diff`). +- **Corpus agreement:** 338 of 369 files agree diagnostic-by-diagnostic; 21 diagnostics are ours alone and 600 the reference's alone, and the first number must be read by root: our diagnostics against the reference's own corpora fell while our non-standard-notation warnings on our own example models rose ([differential](../project/pilot-differential.md), `go run ./cmd/pilot-diff`). - **Declared-diagnostic silence:** of the 511 declared `errors` rows in the reference's own Xpect suites, we report nothing for 0. 244 we report word-for-word; 248 wording-only and 7 location-only differences are agreement in substance and are not counted as gaps; 0 more we report as a warning and 2 elsewhere in the file ([Xpect oracle](../project/pilot-xpect.md), `go run ./cmd/pilot-xpect`). - **Scope agreement:** 230 of 230 declared scope assertions match exactly (same source). - **Permissiveness gaps:** of 285 invalid models we wrote ourselves, the reference rejects 3 that we accept by default, and 273 both reject; 3 further cases agree only when we are asked strictly. We authored every one of these cases ourselves, so the denominator measures the reach of our own corpus and not our conformance; agreement reached only under an opt-in strict mode is weaker evidence than agreement by default ([rejection oracle](../project/pilot-rejection.md), `go run ./cmd/pilot-reject`). -- **Declared errata:** the registry declares 3 defect(s) in the published reference material — 1 with a specification-derived correction, 2 documented without one, since no intended reading can be inferred ([OMG issues](../project/omg-issues.md), `internal/errata`). Every figure above is as published and stays the conformance statement; running the same oracles over the corrected text instead reports 339 of 368 files agreeing, 20 diagnostics ours alone and 596 the reference's alone, 0 declared rows we are silent on, and 0 of 285 authored cases the reference alone rejects. The corrected figures are diagnostic only: an erratum never reclassifies a divergence category, and the published corpus is never edited. +- **Declared errata:** the registry declares 3 defect(s) in the published reference material — 1 with a specification-derived correction, 2 documented without one, since no intended reading can be inferred ([OMG issues](../project/omg-issues.md), `internal/errata`). Every figure above is as published and stays the conformance statement; running the same oracles over the corrected text instead reports 339 of 369 files agreeing, 20 diagnostics ours alone and 600 the reference's alone, 0 declared rows we are silent on, and 0 of 285 authored cases the reference alone rejects. The corrected figures are diagnostic only: an erratum never reclassifies a divergence category, and the published corpus is never edited. - **Self-assessed surface:** the action, state-machine and classifier-behavior rows have no external referee at all — the four refereed figures above cannot see them, because the pinned artifact evaluates expressions but executes neither actions nor state machines. [Spec compliance](../project/spec-compliance.md) counts them. What these numbers cannot show: the OMG corpora are demonstrations rather than an official conformance suite; the differential is one-directional, comparing the diagnostics the two implementations report on the same files; the Xpect suites are the pilot authors' test intent rather than a certification oracle; and none of these is a percentage of the specification — no global compliance figure is claimed anywhere. diff --git a/docs/project/pilot-differential-baseline.json b/docs/project/pilot-differential-baseline.json index 65f55ca79..d5de83846 100644 --- a/docs/project/pilot-differential-baseline.json +++ b/docs/project/pilot-differential-baseline.json @@ -60,8 +60,8 @@ "name": "examples", "dir": "examples", "origin": "ours", - "files": 34, - "digest": "sha256:cb438013cc511395df7d9b5cd97a9d693d1d0bfe79abe5cd2176fe453a5508d4" + "files": 35, + "digest": "sha256:897a4cf143bd6b3b949b70f1119c89d438f1e150b905ab30f603ced69bb5c35a" }, { "name": "probes", @@ -74,14 +74,14 @@ "recorded": "2026-09-09" }, "totals": { - "files": 368, + "files": 369, "filesFullyAgreeing": 338, "agreement": 34, "severityMismatch": 2, "openSysMLOnly": 21, - "pilotOnly": 596, + "pilotOnly": 600, "openSysMLDiagnostics": 57, - "pilotDiagnostics": 632 + "pilotDiagnostics": 636 }, "roots": [ { @@ -748,14 +748,14 @@ "name": "examples", "dir": "examples", "totals": { - "files": 34, + "files": 35, "filesFullyAgreeing": 26, "agreement": 0, "severityMismatch": 1, "openSysMLOnly": 1, - "pilotOnly": 570, + "pilotOnly": 574, "openSysMLDiagnostics": 2, - "pilotDiagnostics": 571 + "pilotDiagnostics": 575 }, "files": [ { @@ -810,6 +810,38 @@ } ] }, + { + "path": "expressions-demo.sysml", + "agreement": [], + "severityMismatch": [], + "openSysMLOnly": [], + "pilotOnly": [ + { + "line": 95, + "severity": "error", + "category": "kind-mismatch", + "count": 1 + }, + { + "line": 96, + "severity": "error", + "category": "kind-mismatch", + "count": 1 + }, + { + "line": 100, + "severity": "error", + "category": "kind-mismatch", + "count": 1 + }, + { + "line": 110, + "severity": "error", + "category": "kind-mismatch", + "count": 1 + } + ] + }, { "path": "oosem-demo/oosem-demo.sysml", "agreement": [], @@ -3730,14 +3762,14 @@ } ], "totals": { - "files": 368, + "files": 369, "filesFullyAgreeing": 339, "agreement": 34, "severityMismatch": 2, "openSysMLOnly": 20, - "pilotOnly": 596, + "pilotOnly": 600, "openSysMLDiagnostics": 56, - "pilotDiagnostics": 632 + "pilotDiagnostics": 636 }, "findings": [ { diff --git a/docs/project/pilot-differential.md b/docs/project/pilot-differential.md index 6a8547bc1..5114c93e9 100644 --- a/docs/project/pilot-differential.md +++ b/docs/project/pilot-differential.md @@ -208,7 +208,7 @@ nor double-counted as two independent disagreements. --- -## Results (pilot `2026-07`, 368 files) +## Results (pilot `2026-07`, 369 files) | Root | Files | Fully agreeing | Ours | Pilot | Agreed | Severity-only | Only ours | Only pilot | |---|---:|---:|---:|---:|---:|---:|---:|---:| @@ -217,9 +217,9 @@ nor double-counted as two independent disagreements. | `examples/pilot-corpora/sysml-validation` | 56 | 56 | 0 | 0 | 0 | 0 | 0 | 0 | | `examples/pilot-corpora/kerml-examples` | 58 | 50 | 4 | 6 | 0 | 0 | 4 | 6 | | `testdata` | 17 | 10 | 38 | 55 | 34 | 1 | 3 | 20 | -| `examples` | 34 | 26 | 2 | 571 | 0 | 1 | 1 | 570 | +| `examples` | 35 | 26 | 2 | 575 | 0 | 1 | 1 | 574 | | `cmd/pilot-diff/testdata` (probes) | 4 | 1 | 6 | 0 | 0 | 0 | 6 | 0 | -| **Total** | **368** | **338** | **57** | **632** | **34** | **2** | **21** | **596** | +| **Total** | **369** | **338** | **57** | **636** | **34** | **2** | **21** | **600** | **Read the `only ours` total by root, never as one number.** Step 2 removes nine resolver false positives from the reference's **own** corpora: `pilot-examples` 16 → **7** and @@ -381,8 +381,8 @@ cascades through the rest of the file. The movement is entirely one file, | Count | Before the initializer rewrite | Now | |---|---:|---:| -| only pilot | 82 | **596** | -| pilot diagnostics | 123 | **632** | +| only pilot | 82 | **600** | +| pilot diagnostics | 123 | **636** | | severity-only | 9 | **2** | The rewrite itself took only-pilot to 61 and pilot diagnostics to 101; the `Now` column states @@ -513,7 +513,7 @@ Per category, the only-ours totals are: `pilot-examples` 4 `unmapped`, 2 [unbound-parameter advisory](#the-unbound-parameter-advisory)); `examples` 1 syntax; `testdata` 2 `unmapped`, 1 `multiplicity`; `probes` 6 `unmapped`. Only-pilot: `testdata` 12 `kind-mismatch`, 3 `unmapped`, 3 syntax, 2 `unresolved-reference`; -`examples` 10 syntax, 15 `unmapped`, 258 `kind-mismatch`, 287 `unresolved-reference` — of which +`examples` 10 syntax, 15 `unmapped`, 262 `kind-mismatch`, 287 `unresolved-reference` — of which `relay-probe-demo/mission.sysml` carries none: it carried a `kind-mismatch` on its send of a `Telemetry` invocation until the send-argument round above, and the demo now writes the constructor, `send new Telemetry(…) via antenna`, which both implementations accept, so the row @@ -588,13 +588,13 @@ page's history. | Count | Now | |---|---:| | overall: fully agreeing / only ours / our diagnostics | **338 / 21 / 57** | -| only pilot | **596** | -| pilot diagnostics | **632** | +| only pilot | **600** | +| pilot diagnostics | **636** | | severity-only | **2** | | unmapped, our side | **19** | | kerml-examples: only ours | **4** | | pilot-examples: only ours | **7** | -| examples: only pilot | **570** | +| examples: only pilot | **574** | The KerML root is now the *cleanest* of the three OMG roots in proportion: **4** only-ours against 6 only-pilot — the only root where the reference reports more than we do — with 50 of 58 files fully @@ -695,6 +695,14 @@ timed transition in the full form (`transition first coasting accept after 5 [SI because the pinned reference does not parse a target transition inside the body of its source state, and this implementation does not lower a sourceless target transition at the state machine's top level. +### Expressions walkthrough round + +`examples/expressions-demo.sysml` is one file added to the `examples` root: files 34 → **35** on the +root, 368 → **369** overall, and pilot diagnostics 632 → **636** / only pilot 596 → **600**, all four +of them the `kind-mismatch` rows adjudicated below where a `calc def` is passed as an argument. +Nothing else moves: the file draws no diagnostic from this implementation, so `fully agreeing`, +`only ours` and `agreed` stay where the analysis walkthrough left them. + ## Adjudications ### Only ours — candidate false positives (3, SysML side) diff --git a/docs/project/rdf-corpus-roundtrip.md b/docs/project/rdf-corpus-roundtrip.md index 6235adbd0..b315023ec 100644 --- a/docs/project/rdf-corpus-roundtrip.md +++ b/docs/project/rdf-corpus-roundtrip.md @@ -9,7 +9,7 @@ pin in `scripts/pilot-pin.sh`. | Root | Files | |---|---| -| `committed` (everything under `examples/` outside the downloaded roots) | 34 | +| `committed` (everything under `examples/` outside the downloaded roots) | 35 | | `sysml-v2-training` | 100 | | `pilot-corpora/kerml-examples` | 58 | | `pilot-corpora/sysml-examples` | 99 | @@ -59,15 +59,15 @@ Recorded against the corpus above, reproduced byte-identically on a second run: | Verdict | Files | |---|---| -| `stable` | 347 | +| `stable` | 348 | | `whitespace-only` | 0 | | `graph-diff` | 0 | | `unwritable` | 0 | | `unparseable` | 0 | | `refused` | 0 | -| **total** | **347** | +| **total** | **348** | -So every one of the 347 files converts to Turtle, and every one comes back as the same Turtle byte +So every one of the 348 files converts to Turtle, and every one comes back as the same Turtle byte for byte. That is the source text at work: the decoder writes each file back from the `sysx:sourceText` it carries (see [What the gate does not do](#what-the-gate-does-not-do)), so the files that came back up to whitespace, as a different graph, or that could not be written back or diff --git a/internal/core/export/testdata/corpus_roundtrip_expected.txt b/internal/core/export/testdata/corpus_roundtrip_expected.txt index 63788d1a6..b4b095544 100644 --- a/internal/core/export/testdata/corpus_roundtrip_expected.txt +++ b/internal/core/export/testdata/corpus_roundtrip_expected.txt @@ -8,7 +8,7 @@ # is a per-file ratchet, not a claim that any verdict is right; see # docs/project/rdf-corpus-roundtrip.md. Regenerate with: # go test ./internal/core/export -run TestCorpusRoundTrip -update-corpus-roundtrip -# files: committed 34 +# files: committed 35 # files: sysml-v2-training 100 # files: pilot-corpora/kerml-examples 58 # files: pilot-corpora/sysml-examples 99 From a8c12b7b3b1a1d369f17a0afc61b7f17c63f3e93 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Wed, 9 Sep 2026 19:14:05 +0000 Subject: [PATCH 06/33] fix(runtime): explore advances one token per step Exploration permuted the tokens of one lockstep step, in which every steppable token moved once, so a branch of two nodes could never both run before a concurrent branch's one node and `complete` under-reported the admissible outcomes. Under `explore` a step is now one token advancing one node; the tokens able to act are picked among afresh after each move and each pick is its own choice point. Fixed policies keep their sweep. Adds `action_explore_write_between_branch_nodes`, re-derives the oracle's run counts at the new granularity, and updates the guide, CLI, wire and compliance prose. Co-Authored-By: jason.han --- .../explore-single-token-steps.fixed.md | 10 +++ docs/guide/06-behavior.md | 19 +++-- .../design/bounded-model-checking.md | 7 +- docs/project/behavior-semantic-oracle.md | 79 ++++++++++++++++--- docs/project/roadmap.md | 10 ++- docs/project/spec-compliance.md | 2 +- docs/reference/cli.md | 14 ++-- docs/reference/wire-contract.md | 2 +- internal/core/runtime/action_choice.go | 34 ++++---- internal/core/runtime/action_executor.go | 13 +-- internal/core/runtime/action_subflow.go | 2 +- internal/core/runtime/explore.go | 30 ++++--- internal/core/runtime/scheduler.go | 15 ++++ ...between_branch_nodes.declared.trace.golden | 14 ++++ ...e_write_between_branch_nodes.expected.json | 25 ++++++ ...e_between_branch_nodes.seed-1.trace.golden | 14 ++++ ...n_explore_write_between_branch_nodes.sysml | 29 +++++++ ...re_write_between_branch_nodes.trace.golden | 14 ++++ ...ore_write_between_branch_nodes.trace.order | 9 +++ internal/repl/explore_test.go | 20 +++-- 20 files changed, 292 insertions(+), 70 deletions(-) create mode 100644 changes/unreleased/explore-single-token-steps.fixed.md create mode 100644 internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.declared.trace.golden create mode 100644 internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.expected.json create mode 100644 internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.seed-1.trace.golden create mode 100644 internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.sysml create mode 100644 internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.trace.golden create mode 100644 internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.trace.order diff --git a/changes/unreleased/explore-single-token-steps.fixed.md b/changes/unreleased/explore-single-token-steps.fixed.md new file mode 100644 index 000000000..ae771b297 --- /dev/null +++ b/changes/unreleased/explore-single-token-steps.fixed.md @@ -0,0 +1,10 @@ +- **`explore` advances one token per step, so `complete` covers every interleaving.** Exploration + used to permute the tokens of one lockstep step, in which every steppable token moved once, so a + branch of two nodes could never both run before a concurrent branch's one node: a fork of + `left1 { x := 1 } → left2 { y := x }` against `right { x := 2 }` reported `complete` with two + outcomes and missed `x = 2, y = 1`. Under `explore` a step is now one token advancing one node, + the tokens able to act are picked among afresh after each move, and each pick is its own + `step N:` choice point in the witness; the fixed policies (`reverse`, `declared`, `seed:`) + keep their sweep, so no default trace changed. Run counts grow with the finer granularity + (`action_merge_fork_branch_and_loop` needs `explore:runs=10000` to complete) and the semantic + oracle's figures are re-derived; `action_explore_write_between_branch_nodes` pins the case. diff --git a/docs/guide/06-behavior.md b/docs/guide/06-behavior.md index ceff03313..c7222cfe0 100644 --- a/docs/guide/06-behavior.md +++ b/docs/guide/06-behavior.md @@ -467,9 +467,9 @@ $ sysml -schedule explore -action test::race action_explore_three_writers.sysml ✓ explored test::race: 3 outcomes outcome | linearizations | witness ---------------------------------------------+----------------+------------------------------------------------------------------ -aRan = true; bRan = true; cRan = true; x = 1 | 2 | step 3: 3@b first of 2@a, 3@b, 4@c; step 3: 4@c first of 2@a, 4@c -aRan = true; bRan = true; cRan = true; x = 2 | 2 | step 3: 2@a first of 2@a, 3@b, 4@c; step 3: 4@c first of 3@b, 4@c -aRan = true; bRan = true; cRan = true; x = 3 | 2 | step 3: 2@a first of 2@a, 3@b, 4@c; step 3: 3@b first of 3@b, 4@c +aRan = true; bRan = true; cRan = true; x = 1 | 2 | step 3: 3@b first of 2@a, 3@b, 4@c; step 4: 4@c first of 2@a, 4@c +aRan = true; bRan = true; cRan = true; x = 2 | 2 | step 3: 2@a first of 2@a, 3@b, 4@c; step 4: 4@c first of 3@b, 4@c +aRan = true; bRan = true; cRan = true; x = 3 | 2 | step 3: 2@a first of 2@a, 3@b, 4@c; step 4: 3@b first of 3@b, 4@c complete (6 runs) ``` @@ -479,8 +479,13 @@ final state, states visited and values; an analysis case's outputs and verdicts linearizations reached it, and the choice sequence of one *witness* run (`3@b first of 2@a, 3@b, 4@c` is the first pick, then `4@c first of 2@a, 4@c` among the two that remained). Six linearizations, three outcomes, two each; `complete (6 runs)` says every choice sequence was -tried. A run that fails under some order is an outcome of its own (`error: …`), not the end of -the exploration; a behavior with no choice point explores in exactly one run (`no choice points` +tried. Under `explore` an action step is one token advancing one node — not, as under the fixed +policies, every steppable token moving once — so the picks fall in consecutive steps and a branch +of several nodes can run ahead of, or be overtaken by, a concurrent one at each of them. A +`complete` exploration therefore covers every interleaving of the nodes the library leaves +unordered, at body granularity: the statements of one body run without interruption. A run that +fails under some order is an outcome of its own (`error: …`), not the end of the exploration; a +behavior with no choice point explores in exactly one run (`no choice points` in the witness column); the same model explores to the same table every time. With `-trace`, the table is followed by the trace of each outcome's witness run (`trace of outcome 1's witness (run 4):`). With `-json`, each check carries `outcomes` (values, `linearizations`, `witness`) and @@ -502,8 +507,8 @@ $ sysml -schedule explore:runs=2 -action test::race action_explore_three_writers ? explored test::race: 2 outcomes outcome | linearizations | witness ---------------------------------------------+----------------+------------------------------------------------------------------ -aRan = true; bRan = true; cRan = true; x = 2 | 1 | step 3: 2@a first of 2@a, 3@b, 4@c; step 3: 4@c first of 3@b, 4@c -aRan = true; bRan = true; cRan = true; x = 3 | 1 | step 3: 2@a first of 2@a, 3@b, 4@c; step 3: 3@b first of 3@b, 4@c +aRan = true; bRan = true; cRan = true; x = 2 | 1 | step 3: 2@a first of 2@a, 3@b, 4@c; step 4: 4@c first of 3@b, 4@c +aRan = true; bRan = true; cRan = true; x = 3 | 1 | step 3: 2@a first of 2@a, 3@b, 4@c; step 4: 3@b first of 3@b, 4@c incomplete: runs budget 2 hit after 2 runs $ echo $? 2 diff --git a/docs/internals/design/bounded-model-checking.md b/docs/internals/design/bounded-model-checking.md index 1fbadd138..98756e3fd 100644 --- a/docs/internals/design/bounded-model-checking.md +++ b/docs/internals/design/bounded-model-checking.md @@ -97,11 +97,14 @@ move's writes — and avoids copying the object graph at every choice point. ### The atomic step -The executor's `Step()` is a tool artifact: it steps every token once, in a fixed order, and the +The executor's `Step()` under a fixed policy is a tool artifact: it steps every token once, in a +fixed order, and the [oracle](../../project/behavior-semantic-oracle.md#what-the-library-fixes-and-what-a-trace-adds) already warns that a `step N:` line is a boundary the library does not define. The checker must not explore interleavings *inside* that artifact, nor interleavings finer than the library -admits. +admits. The `explore` policy already takes the unit below for actions: one of its steps is one +token advancing one node, so a branch of several nodes can be overtaken between any two of them +(`action_explore_write_between_branch_nodes` is the case a lockstep step would have missed). The unit the library defines is a **performance**: a node's body runs "completely before" its successors start (`HappensBefore`), and two unordered performances may overlap arbitrarily in diff --git a/docs/project/behavior-semantic-oracle.md b/docs/project/behavior-semantic-oracle.md index 6023a9c32..93d0588da 100644 --- a/docs/project/behavior-semantic-oracle.md +++ b/docs/project/behavior-semantic-oracle.md @@ -47,6 +47,12 @@ scheduling detail the library says nothing about: to the token list once every succession has delivered, and the step that fired it may go on to step that token (and tokens the removal shifted) again; a `step N:` line is therefore the executor's step boundary, not a unit the library defines. +- Under the `explore` policy a step is one token advancing one node, so a `choice` line is one + pick among the tokens able to act at that moment and the next step picks again among those left + and any the move enabled; a linearization is the sequence of those picks, and a branch of + several nodes may be overtaken by a concurrent one between any two of them. The fixed policies + move every steppable token once per step, so their `step N:` lines group moves that `explore` + spreads over consecutive steps; a body's statements run without interruption under both. - A state machine records a transition's guard evaluation, exit, effect and entry as they run, and evaluates a guard once to select the transition and once again to fire it; the second evaluation is a tool detail with no observable effect, since a guard is an expression. @@ -123,9 +129,10 @@ Open: the relative order of `a`, `b2` and `c3` — and of every node on one bran node on another. The golden's order (the `c` branch stepped first within each step, `a` finishing first because its branch is shortest) is one admissible linearization. Nothing observable depends on it: every interleaving increments `arrived` three times before `after` reads it, so the fixture -pins the one outcome and has no `outcomes`. Under `explore` the interleavings are twelve -linearizations reaching that one outcome (12 runs, 1 outcome, complete), each a sequence of token -choices (`step 3: 2@a first of 2@a, 3@b1, 4@c1; …`). +pins the one outcome and has no `outcomes`. Under `explore` the interleavings of one, two and +three nodes on three branches are `6! / (1! 2! 3!) = 60` linearizations reaching that one outcome +(60 runs, 1 outcome, complete), each a sequence of token choices (`step 3: 2@a first of 2@a, 3@b1, +4@c1; step 4: 3@b1 first of 3@b1, 4@c1; …`). Fixed outcome: `arrived = 3`, `seen = 3`. The executor agrees; the golden shows `after` reading `arrived -> 3` and every branch's write preceding it. @@ -149,8 +156,9 @@ Derived constraints: - `right` writes `log := log * 10 + 1`; `after` follows `sync` and writes `log := log * 10 + 2`. Open: the order of `left` against any node of the `r` branch. Nothing observable depends on it, -so the fixture pins the one outcome without `outcomes`; under `explore` the twelve interleavings -all reach it (12 runs, 1 outcome, complete). +so the fixture pins the one outcome without `outcomes`; under `explore` the seventy +interleavings — `l1` and `l2` in either order then `left`, three events woven into the four of +the `r` branch, `2 × C(7, 3)` — all reach it (70 runs, 1 outcome, complete). Fixed outcome: `log = 12` — `right` writes before `after`, whatever the interleaving, because `after` cannot start before `sync`, and `sync` cannot start before `right` has ended. @@ -318,8 +326,44 @@ as `outcomes` citing this section; `.trace.order` states the partial order the l records the default schedule (`c` is declared last, so its token is stepped first and `a` writes last, giving `x = 1`). Exploration is what makes the set checkable: `explore` replays the run along every choice sequence and must reach each of the three outcomes and no other, in six runs. -The first pick among three tokens and the next among the two left are two choice points of one -step, so a linearization is a sequence of two choices, not one choice among six. +The first pick among three tokens and the next among the two left are two choice points in +consecutive steps, so a linearization is a sequence of two choices, not one choice among six. + +### A write between two nodes of a concurrent branch: three orders, three outcomes + +Fixture: `action_explore_write_between_branch_nodes` (golden, explored). + +``` +start → split ⇉ left1 { x := 1 } → left2 { y := x } ─┐ + ⇉ right { x := 2 } ────────────────────┤→ sync → done +``` + +Derived constraints: + +- `left1`, `left2` and `right` are each performed exactly once (ForkAction, and `left2` follows + `left1` by HappensBefore), and `sync` follows `left2` and `right` (JoinAction), so every write + has ended before the action ends. +- `left2` reads `x` after `left1`'s write has ended, so `y` is `1` or `2`, never `0`. + +Open: the order of `right` against `left1` and against `left2`. The library gives no `HappensBefore` +link from either to `right`, so `right` may end before `left1` starts, start after `left1` ends and +end before `left2` starts, or start after `left2` ends: three linearizations, no more, since +`left2` cannot precede `left1`. Each leaves a different pair of values: `right, left1, left2` +gives `x = 1, y = 1`; `left1, right, left2` gives `x = 2, y = 2`; `left1, left2, right` gives +`x = 2, y = 1`. + +Pinned outcome: that admissible set of three, stated as `outcomes` citing this section; +`.trace.order` states the partial order the library does fix (`split < left1`, `left1 < left2`, +`split < right`, `left2 < sync`, `right < sync`). The exact golden records the default schedule +(`right` is declared last, so its token is stepped first: `right, left1, left2`, giving `x = 1, +y = 1`). Exploration must reach each of the three outcomes and no other, in three runs (3 runs, +3 outcomes, complete). The case is what distinguishes exploring one move at a time from exploring +the order of one lockstep step: had every steppable token moved once per step, `left1` and `right` +would both have moved in the step after the fork whichever went first, `left2` could never have +run before `right`, and the exploration would have reported two outcomes complete, missing +`x = 2, y = 1`. No fixed policy takes it: each moves `left1` and `right` in the step after the fork, +in one order or the other, before `left2` can run, so `declared` (and `seed:1`) give `x = 2, y = 2` +and `reverse` gives `x = 1, y = 1`. ### A decision inside a loop: every pass is its own open choice @@ -383,7 +427,11 @@ re-reading the first. Under it either pairing is admissible: `left` takes `1` an the reverse. Pinned outcome: the admissible set `{a = 2 ∧ b = 1, a = 1 ∧ b = 2}`, stated as `outcomes` citing -this section; exploration reaches each once (2 runs, 2 outcomes, complete). The partial order the library fixes among the nodes is stated as `.trace.order` +this section; exploration reaches each twice (4 runs, 2 outcomes, complete): once the first +message is in flight, `sendTwo` and both accepts are able to act, and an accept picked first takes +the message while the other must wait for `sendTwo`, whereas `sendTwo` picked first leaves both +messages to the two accepts and the accept picked next takes the older. The partial order the +library fixes among the nodes is stated as `.trace.order` constraints (`split < sendOne`, `split < left`, `split < right`, `sendOne < sendTwo`, `sync < recorder`, `recorder < done`); the join's predecessors are not stated as constraints on `sync` because a token parks at a join before the join performs, so the entry first mentioning @@ -633,8 +681,11 @@ Derived constraints: Open: the interleaving of the two tokens at every node; which token takes which exit. The outcome does not depend on it, so the fixture pins the one outcome without `outcomes`; under `explore` -every interleaving — a choice between the two tokens at each of seven steps — reaches it -(128 runs, 1 outcome, complete). +every interleaving — a choice between the two tokens at each step until one of them is done, the +two threads dividing the four passes as `3 + 1`, `2 + 2` or `1 + 3` — reaches it. There are +8526 of them, more than the default budget of 1024 runs, so `explore` alone reports +`incomplete: runs budget 1024 hit after 1024 runs` with the one outcome tabled, and +`explore:runs=10000` completes (8526 runs, 1 outcome, complete). Fixed outcome: `passes = 4`, `merged = 4`, `worked = 4`. Whatever the interleaving, `passes` takes the values 1, 2, 3, 4 one `more` performance at a time, the two that read 1 and 2 select @@ -681,9 +732,11 @@ Derived constraints: Open: in the first model, the interleaving of the direct arrival with `slow → slower`; the outcome does not depend on it, since `ready` is written before the second arrival either way. -Both fixtures pin one outcome without `outcomes`; under `explore` the first reaches it by both -interleavings (2 runs, 1 outcome, complete) and the second, a chain, reaches no choice point -(1 run, 1 outcome, complete). +Both fixtures pin one outcome without `outcomes`; under `explore` the first reaches it by every +interleaving of the direct arrival with the `slow → slower` branch (22 runs, 1 outcome, complete) — +when `slower` runs before the direct arrival reaches `gate`, that arrival reads `ready = true` and +goes on to `tail` too, and the two tokens' moves through `gate`, `tail` and `done` interleave — and +the second, a chain, reaches no choice point (1 run, 1 outcome, complete). Fixed outcome, first model: `ready = true`, `mergeRuns = 2`, `passed = 2` — the direct arrival performs `gate` and reads `ready = false`, so no link to `tail` follows it; the second arrival diff --git a/docs/project/roadmap.md b/docs/project/roadmap.md index bae2afb57..76e2fba27 100644 --- a/docs/project/roadmap.md +++ b/docs/project/roadmap.md @@ -971,7 +971,15 @@ cases without `outcomes` are not explored; and the budget is the author's to rai (`"exploreBudget": {"runs": N, "depth": D}`), not the harness's to sample past. #138 wrote it up: every open ordering in the oracle names the `outcomes` or `.trace.order` that encodes it and the run and outcome counts `explore` reaches, and the behavior guide has a section on models with -more than one valid run. +more than one valid run. As landed, `explore` permuted the tokens of one lockstep step — every +steppable token moved once per step — so a branch of two nodes could never both run before a +concurrent branch's one, and a fork of `left1 { x := 1 } → left2 { y := x }` against +`right { x := 2 }` explored `complete` with two outcomes, missing `x = 2, y = 1`. An action step +under `explore` is now one token advancing one node, the tokens able to act are picked among +afresh after each move, and `complete` covers every interleaving at body granularity +(`action_explore_write_between_branch_nodes` pins the three); the fixed policies keep their +sweep, so no default trace moved, and the oracle's run counts were re-derived at the new +granularity (`action_merge_fork_branch_and_loop` now needs `explore:runs=10000` to complete). --- diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md index 23bd4bd13..49124f18a 100644 --- a/docs/project/spec-compliance.md +++ b/docs/project/spec-compliance.md @@ -535,7 +535,7 @@ by name is refused naming what is missing rather than approximated. | An action node reached over several successions is one performance that follows all of them: a step with no declared multiplicity holds one value (KerML 1.0 §7.4.5), and each succession into it is a `HappensBefore` link (Kernel Semantic Library `Occurrences.kerml`) whose later occurrence is that performance | `runtime/action_executor.go` `synchronize` — the join row's one gate, applied from `stepToken` to every node kind but a merge (`synchronizes`; `Actions::MergeAction` passes each arrival on) — with `awaitedSuccessions`, `reachableFrom` and `leaves` deciding which successions a plain node awaits; `runtime/action_subflow.go` `Token.positionIn` (a token in a nested flow stands at the node performing it) | `conformance/action_node_with_two_incoming_successions_runs_once.sysml` + trace golden, `action_nested_node_two_successions_per_performance.sysml` + trace golden (two performances of an action holding such a node each perform it once), `action_node_concurrent_performances` + trace golden and `action_node_concurrent_nested_bindings` + trace golden (a flow-owning node reached from two fork branches performs once, each flow at its own pin), all derived in [the semantic oracle](behavior-semantic-oracle.md); `action_node_converges_after_decision` + trace golden (a plain node behind a decision's two branches performs once for the branch taken, no deadlock) and `action_node_loop_back_reperforms` + trace golden (a plain node a loop re-enters performs once per pass), with `action_decision_else_done`, `action_guard_reads_calc_usage`, `action_succession_guard_fork_branch_pruned` and `f63_control_node_body` pinning the same at final nodes and under fork guards; `robustness_test.go:deadlock_join_starvation`, `:deadlock_join_same_succession_twice` pin that a join, unlike a plain node, awaits an unreachable source (`ErrActionDeadlock`) | ✅ Faithful (`hits = 1`: the tokens arriving over the node's successions collapse into one performance, per performance of the owning action. A join awaits every incoming succession, its sources being 1..1; a plain node awaits a succession only once it has delivered or while some token of the activation, other than one held at the node, can still reach its source without passing through the node or through a join that node must feed — a decision branch whose guard did not hold, or a succession back from a node downstream of this one, orders no performance before this one, so a loop through a plain node re-performs it once per iteration rather than deadlocking) | | Decision node (guarded branching): SysML v2 §7.17.3 rule 2 gives outgoing successions target multiplicity 0..1; `Actions::DecisionAction` selects exactly one outgoing `HappensBeforeLink` | `action_executor.go` `stepDecisionNode`, `probeGuard` (guards are evaluated in order until one holds, as `enabledSuccessions` evaluates them out of any other node; the ones after it are read in a `beginProbe` preview that restores the budget, the trace, every effect and the object identities the preview took; the first that holds is taken, an unguarded succession is the fallback when none holds; a previewed guard that fails to evaluate is no alternative and no error, recorded as a `guard-unevaluable` note by `noteUnevaluableGuard`), `action_choice.go` `noteDecisionBranches` (several holding guards are a choice point naming the branches by position and target) | `conformance/action_decision_merge_guarded_branch.sysml` + `.expected.json` + trace golden; `conformance/action_choice_decision_overlapping_guards.sysml` + `.expected.json` (both outcomes listed as admissible) + trace golden; `conformance/action_choice_unevaluable_guard.sysml` + `.expected.json` + trace golden; `choice_test.go:TestChoicesResetPerRun`, `:TestLaterGuardErrorIsNotAChoiceNorAFailure`, `:TestLaterGuardIsProbedWithoutCost`; `grpc/choice_test.go:TestExecuteAction_UnevaluableGuardDiagnostics`; `repl/choice_test.go:TestStepReportsUnevaluableGuards`; `robustness_test.go:decision_no_satisfied_guard`, `:decision_all_guards_false` (`ErrNoEnabledSuccession`) | ✅ Faithful (the library selects exactly one link but does not say which when several guards hold, so the pick is the executor's and is reported as one) | | Which linearization a run takes where the library orders nothing is tool-defined, so it is a named *scheduling policy* rather than one fixed rule: `reverse` (the default — reverse token-index order, first holding guard, first enabled transition — so every run recorded before policies were selectable replays unchanged), `declared` (tokens in spawn order, guards and transitions in declaration order) and `seed:` (every pick drawn from a PCG sequence the seed fixes, so one seed replays one run on every platform and two seeds may take two linearizations). The policy decides every choice point of the row above and the rows below — token order in a step, the holding guard a decision follows, the enabled transition that fires, the order the orthogonal regions one event enables react in, whose same-step write stands (it follows from the token order) — and nothing else: every choice point a run reaches is reported under every policy, and the `took …` of each is what the policy took (another linearization may reach other choice points, so their count is not fixed across policies). A spelling naming no policy (`seed`, `seed:`, `seed:-1`, `seed:abc`, an unknown name) is `ErrInvalidSchedulePolicy` before anything runs, on every surface: `sysml -schedule`, `%schedule`, and the `schedule` field of `ExecuteActionRequest`, `ExecuteStateRequest` and `RunAnalysisRequest` (`INVALID_ARGUMENT`; the `schedule` capability advertises the field). Guards read in a preview leave the seeded sequence where it was, so reporting a choice does not change which alternative the run takes; a decision branch picked past the first was only previewed, so the run reads its guard once more before taking it (what evaluating it materialized or derived is then the run's), as `fireTransition` reads a transition's guard again before it fires; an executor a debugger drives call by call keeps the scheduler its run started with when another run under another policy is driven to completion in between, and `Decide` previews the transition that run would fire from that same scheduler, putting its draw back; and a composite state every leaf of its orthogonal regions reaches is asked for its transition once per dispatch or change poll, so the choice among its enabled transitions draws once (one candidate, one `took …`), a composite state a nested state outranks draws nothing, the pick among a candidate's enabled transitions being made only once it survives conflict resolution, so the run's next reported choice takes the seed's next draw; and a token parked at a join its other branches have not reached or at an accept no message in flight answers keeps its place in the step's order, so a seed draws only among the tokens able to act and steps taken while every token is parked draw nothing | `runtime/scheduler.go` `SchedulePolicy`, `ParseSchedulePolicy`, `SchedulePolicyError`, `scheduler.orderTokens`, `scheduler.pick`, `scheduler.mark`; `runtime/context.go` `SetSchedule`, `scheduling`, `beginExecutorRun` (a run under way keeps the scheduler it started with, across the other runs driven while it is paused), `previewExecutorRun` (`Decide` previews under it); `action_executor.go` `scheduleTokens`, `parked` (the tokens `Step` and a nested flow in `action_subflow.go` move, in the policy's order, a seed ordering only those able to act), `stepDecisionNode`; `state_executor.go` `enabledTransitions`, `selectCandidates`, `chooseTransition`, `chooseRegion` (the next region to react, drawn from the same `scheduler.pick` and reported whenever two or more can); `state_change_trigger.go` `risenChangeTransitions`; `cmd/sysml/main.go` `schedulePolicy` flag; `repl/schedule.go` `doSchedule`; `grpc/service.go`, `grpc/analysis.go` (`CapabilitySchedule`); `client/opensysml/execute.go` `WithSchedule`, `analysis.go` `Schedule`; `clients/python/opensysml/connection.py` `schedule=` | `scheduler_test.go:TestParseSchedulePolicy`, `:TestParseSchedulePolicyRejectsUnknownSpellings`, `:TestReverseAndDeclaredOrders`, `:TestSeededSchedulingIsReproducible`, `:TestSeededTransitionChoiceMatchesTheRun`, `:TestProbeLeavesTheSeededSequenceInPlace`, `:TestPickedGuardIsReadByTheRun`, `:TestDrivenRunKeepsItsSchedulerAcrossOtherRuns`, `:TestDecidePredictsTheDrivenRunsTransition`, `:TestSharedAncestorChoiceDrawsOnce`, `:TestOutrankedChoiceDrawsNothing`, `:TestParkedTokensDrawNothing`, `explore_test.go:TestExploreSiblingRegionOrder` (`reverse` and `declared` take region declaration order and report the choice; `seed:1` and `seed:6` reach the two orders, each replaying), `choice_test.go:TestNotesOfATransitionBlockedBeforeFiringAreDropped`; `conformance_test.go:TestExecutionConformance` (the whole suite under the default, every `.expected.json` and `.trace.golden` unchanged), `:TestExecutionConformanceUnderPolicies` (the whole suite under `declared` and `seed:1`: no error, panic or hang, and every case pinning no policy and listing no `outcomes` produces its default outputs), `trace_test.go:TestExecutionTrace` (`.declared.trace.golden` and `.seed-1.trace.golden` for every `outcomes` case); `conformance/action_choice_shared_message_accept` lists `outcomes` (`a = 2, b = 1` and `a = 1, b = 2`, derived in `behavior-semantic-oracle.md` § Two accepts of one type racing for two sends) with a `.trace.order` and `declared`/`seed-1` trace goldens; `send_identity_same_named_ports` runs unpinned (it pinned `"schedule": "reverse"` while the via-less `accept Ping` over-matched a transfer addressed to `alpha.inPort`; with the accept held to the receiver the transfer reaches, `waiting` has one enabled transition under every policy); `cmd/sysml/run_test.go:TestRunActionUnderSchedule`; `repl/schedule_test.go`; `grpc/schedule_test.go`, `grpc/capability_test.go`; `client/opensysml/schedule_test.go`, `schedule_internal_test.go`; `clients/python/tests/test_schedule.py`; `conformance/scenarios/06-behavior.json` (`schedule` on the wire, in-process and over every transport) | ✅ Faithful (the three driven policies each take one linearization per run and say which at every choice point; `explore`, the bounded exhaustive replay of the row below, enumerates them all, and the harness checks every listed outcome is reachable and no unlisted one is, so a fixed order is never passed off as the only one. Same-step write order is not a pick of its own: it follows the token order, so under a policy that orders the writing tokens differently the other write stands, which is what the write-conflict goldens under `declared` and `seed:1` pin) | -| Every linearization the library admits is a valid run, so a model with choice points has a *set* of outcomes, not one: the `explore[:runs=N,depth=D]` policy enumerates it by replay — one run records the alternative each choice point took; each later run is a fresh context on the same lowered model (its own instances, message bus, clock, object behaviors, calc memo and notes — nothing of one run is seen by the next) that follows the recorded prefix and takes the next untried alternative at the frontier, depth-first, until no alternative is untried or a budget is hit. Runs agreeing on the observables the conformance harness compares — an action's outputs; a state machine's final state, states visited and values; an analysis case's outputs and verdicts — are one canonical outcome, counted by the linearizations reaching it and witnessed by one run's choice sequence (an object is compared by its type and feature values through the run's own context, never by the id that run gave it, so equal objects with different ids are one outcome and different objects under one id are two); a run that fails is an outcome of its own (`error: …`), not the end of the exploration; a behavior with no choice point explores in exactly one run; the same model explores to the same sorted table every time. The budget (1024 runs and 64 choice points per run by default) is never exceeded silently: `incomplete: budget hit after N runs` names each budget hit, `runs` before `depth`. `explore` is not a policy one context runs under (`ErrExploreUndriven` from `SetSchedule`), so a step-by-step debugger cannot explore: `%schedule explore` is a typed error at the prompt while `sysml -schedule explore` (`-action`, `-state`, `-analysis`, `-calc`) tables the outcomes, exit status `2` when incomplete, and the wire answers `outcomes` and `exploration` on `ExecuteActionResponse`, `ExecuteStateResponse` and `RunAnalysisResponse` under the `schedule_explore` capability. A malformed spelling (`explore:`, `explore:runs=0`, `explore:depth=-1`, `explore:bogus`, an option twice) is `ErrInvalidSchedulePolicy` on every surface. The harness explores every case listing `outcomes` and fails when a listed outcome is unreachable or an unlisted one is reached, naming the outcome and a witness, and when the budget is hit, telling the author to raise `exploreBudget`; cases without `outcomes` are not explored by default | `runtime/explore.go` `Explore`, `ExploreBudget`, `DefaultExploreBudget`, `ExploredOutcome`, `Exploration.Status`, `ChoiceTaken`, `FormatChoices`, `exploreRun.pick`/`beginStep`/`resolve`/`nextPrefix` (the replayed prefix and the frontier); `runtime/outcome.go` `Outcome.identity` (the canonical identity, every name quoted so no output name can spell another outcome), `Outcome.String` and `Outcome.RenderedOutputs` (the rendering), `objectSpeller` (objects by type and feature values), `Context.ActionOutcome`, `StateExecutor.Outcome`, `Context.VerifiedOutcome`; `runtime/scheduler.go` `parseExploreOptions`, `ExplorePolicy`, `SchedulePolicy.Exploration`; `runtime/context.go` `beginExploration` (the per-run scheduler of an exploring run), `SetSchedule` (`ErrExploreUndriven`); `action_choice.go` (token order and same-step writes through the exploring run); `cmd/sysml/main.go`, `report.go` (`outcomes`, `exploration` in `-json`); `repl/explore.go` `ExploreAtPromptError`, `exploreVerdict`; `repl/schedule.go` `doSchedule`; `grpc/explore.go` `Service.explore`, `grpc/service.go`, `grpc/analysis.go` (`CapabilityScheduleExplore`); `client/opensysml/explore.go` `ExploreAction`, `ExploreState`, `ExploreAnalysis`; `clients/python/opensysml/exploration.py`, `connection.py` `explore_action`, `explore_state`, `explore_analysis` | `explore_test.go:TestExploreThreeWritersReachEveryOutcomeOnce`, `:TestExploreIsDeterministic`, `:TestExploreNoChoicePointsIsOneRun`, `:TestExploreRunsBudgetIsIncomplete`, `:TestExploreDepthZeroIsIncomplete`, `:TestExploreErrorIsAnOutcome`, `:TestExploreDecisionInLoop`, `:TestExploreStateTransitionConflict`, `:TestExploreRejectsOtherPolicies`, `:TestParseExplorePolicy`, `:TestExploreRunsShareNoState`, `:TestExploreTellsObjectsApartByWhatTheyAre`, `:TestExploreEquatesObjectsByWhatTheyAre`, `:TestOutcomeIdentityQuotesNames`, `:TestOutcomeIdentityOpensEveryObject` (a ring of objects is spelled once around, and objects nested past the rendering's depth still tell outcomes apart), `:TestExploreSiblingRegionOrder`; `conformance_test.go:TestExecutionConformance` (`exploreConformanceCase` over every `outcomes` case); `conformance/action_explore_three_writers` (six linearizations, three outcomes, derived in `behavior-semantic-oracle.md` § Three concurrent writers of one feature: six orders, three values), `action_explore_decision_in_loop` (§ A decision inside a loop: every pass is its own open choice), `state_explore_transition_conflict` (§ Two transitions out of one state enabled by one event: exactly one fires, which one is open), `state_explore_region_order` (§ Transitions in sibling regions enabled by one event: each fires, in which order is open), each with a `.trace.golden` under the default and `declared`/`seed-1` goldens; `cmd/sysml/run_test.go:TestRunUnderExplore`, `:TestJSONReportsExploration`; `repl/explore_test.go`; `grpc/explore_test.go`; `client/opensysml/explore_test.go`; `clients/python/tests/test_explore.py`; `clients/rust/opensysml/tests/client.rs`, `clients/java/.../ApiIntegrationTest.java`, `clients/node/test/client.test.ts` (the `schedule_explore` capability) | ✅ Faithful (exploration is over the choice points the executors report, so a linearization two choice points do not distinguish is not run twice; a replay whose choice points differ from its recorded prefix is `ErrExplorationDiverged` rather than a table nobody can trust) | +| Every linearization the library admits is a valid run, so a model with choice points has a *set* of outcomes, not one: the `explore[:runs=N,depth=D]` policy enumerates it by replay — one run records the alternative each choice point took; each later run is a fresh context on the same lowered model (its own instances, message bus, clock, object behaviors, calc memo and notes — nothing of one run is seen by the next) that follows the recorded prefix and takes the next untried alternative at the frontier, depth-first, until no alternative is untried or a budget is hit. An action step under `explore` is one token advancing one node — the fixed policies move every steppable token once per step — so the tokens able to act are picked among afresh after each move, a branch of several nodes can be overtaken by a concurrent one between any two of them, and a `complete` exploration covers every interleaving of the nodes the library leaves unordered, at body granularity (a body's statements are not interleaved). Runs agreeing on the observables the conformance harness compares — an action's outputs; a state machine's final state, states visited and values; an analysis case's outputs and verdicts — are one canonical outcome, counted by the linearizations reaching it and witnessed by one run's choice sequence (an object is compared by its type and feature values through the run's own context, never by the id that run gave it, so equal objects with different ids are one outcome and different objects under one id are two); a run that fails is an outcome of its own (`error: …`), not the end of the exploration; a behavior with no choice point explores in exactly one run; the same model explores to the same sorted table every time. The budget (1024 runs and 64 choice points per run by default) is never exceeded silently: `incomplete: budget hit after N runs` names each budget hit, `runs` before `depth`. `explore` is not a policy one context runs under (`ErrExploreUndriven` from `SetSchedule`), so a step-by-step debugger cannot explore: `%schedule explore` is a typed error at the prompt while `sysml -schedule explore` (`-action`, `-state`, `-analysis`, `-calc`) tables the outcomes, exit status `2` when incomplete, and the wire answers `outcomes` and `exploration` on `ExecuteActionResponse`, `ExecuteStateResponse` and `RunAnalysisResponse` under the `schedule_explore` capability. A malformed spelling (`explore:`, `explore:runs=0`, `explore:depth=-1`, `explore:bogus`, an option twice) is `ErrInvalidSchedulePolicy` on every surface. The harness explores every case listing `outcomes` and fails when a listed outcome is unreachable or an unlisted one is reached, naming the outcome and a witness, and when the budget is hit, telling the author to raise `exploreBudget`; cases without `outcomes` are not explored by default | `runtime/explore.go` `Explore`, `ExploreBudget`, `DefaultExploreBudget`, `ExploredOutcome`, `Exploration.Status`, `ChoiceTaken`, `FormatChoices`, `exploreRun.pick`/`beginStep`/`resolve`/`nextPrefix` (the replayed prefix and the frontier), `exploreStep.next`/`acted` (one move ends the step); `runtime/scheduler.go` `tokenSchedule.Ended`, `Choice`; `runtime/action_executor.go` `stepTokens` (stops at an ended step); `runtime/outcome.go` `Outcome.identity` (the canonical identity, every name quoted so no output name can spell another outcome), `Outcome.String` and `Outcome.RenderedOutputs` (the rendering), `objectSpeller` (objects by type and feature values), `Context.ActionOutcome`, `StateExecutor.Outcome`, `Context.VerifiedOutcome`; `runtime/scheduler.go` `parseExploreOptions`, `ExplorePolicy`, `SchedulePolicy.Exploration`; `runtime/context.go` `beginExploration` (the per-run scheduler of an exploring run), `SetSchedule` (`ErrExploreUndriven`); `action_choice.go` (token order and same-step writes through the exploring run); `cmd/sysml/main.go`, `report.go` (`outcomes`, `exploration` in `-json`); `repl/explore.go` `ExploreAtPromptError`, `exploreVerdict`; `repl/schedule.go` `doSchedule`; `grpc/explore.go` `Service.explore`, `grpc/service.go`, `grpc/analysis.go` (`CapabilityScheduleExplore`); `client/opensysml/explore.go` `ExploreAction`, `ExploreState`, `ExploreAnalysis`; `clients/python/opensysml/exploration.py`, `connection.py` `explore_action`, `explore_state`, `explore_analysis` | `explore_test.go:TestExploreThreeWritersReachEveryOutcomeOnce`, `:TestExploreIsDeterministic`, `:TestExploreNoChoicePointsIsOneRun`, `:TestExploreRunsBudgetIsIncomplete`, `:TestExploreDepthZeroIsIncomplete`, `:TestExploreErrorIsAnOutcome`, `:TestExploreDecisionInLoop`, `:TestExploreStateTransitionConflict`, `:TestExploreRejectsOtherPolicies`, `:TestParseExplorePolicy`, `:TestExploreRunsShareNoState`, `:TestExploreTellsObjectsApartByWhatTheyAre`, `:TestExploreEquatesObjectsByWhatTheyAre`, `:TestOutcomeIdentityQuotesNames`, `:TestOutcomeIdentityOpensEveryObject` (a ring of objects is spelled once around, and objects nested past the rendering's depth still tell outcomes apart), `:TestExploreSiblingRegionOrder`; `conformance_test.go:TestExecutionConformance` (`exploreConformanceCase` over every `outcomes` case); `conformance/action_explore_three_writers` (six linearizations, three outcomes, derived in `behavior-semantic-oracle.md` § Three concurrent writers of one feature: six orders, three values), `action_explore_write_between_branch_nodes` (three linearizations, three outcomes, the third reached only when one branch's two nodes both run before the other branch's one; § A write between two nodes of a concurrent branch: three orders, three outcomes), `action_explore_decision_in_loop` (§ A decision inside a loop: every pass is its own open choice), `state_explore_transition_conflict` (§ Two transitions out of one state enabled by one event: exactly one fires, which one is open), `state_explore_region_order` (§ Transitions in sibling regions enabled by one event: each fires, in which order is open), each with a `.trace.golden` under the default and `declared`/`seed-1` goldens; `cmd/sysml/run_test.go:TestRunUnderExplore`, `:TestJSONReportsExploration`; `repl/explore_test.go`; `grpc/explore_test.go`; `client/opensysml/explore_test.go`; `clients/python/tests/test_explore.py`; `clients/rust/opensysml/tests/client.rs`, `clients/java/.../ApiIntegrationTest.java`, `clients/node/test/client.test.ts` (the `schedule_explore` capability) | ✅ Faithful (exploration is over the choice points the executors report, so a linearization two choice points do not distinguish is not run twice; a replay whose choice points differ from its recorded prefix is `ErrExplorationDiverged` rather than a table nobody can trust) | | A choice point is reported wherever the executor had several enabled alternatives the library does not order, and nowhere else: several steppable tokens in one step (`token order`), several holding guards of one decision (`decision branch`), several tokens writing one feature in one step (`write order`), several enabled transitions out of one state for one event (`transition`), and transitions in several regions selected for one event (`region order`). Each is one trace line `choice : (unordered; took )`, one informational diagnostic with code `choice-point` at the node, decision, feature or state that made it, and a count on the debugger's summary line; none is an error, and a run under a fixed policy reports the same set another fixed policy would have had to make on the linearization it took | `choice.go` `ChoiceKind` (`ChoiceTokenOrder`, `ChoiceDecisionBranch`, `ChoiceWriteOrder`, `ChoiceTransition`, `ChoiceRegionOrder`), `ChoicePoint.String` (the trace line), `ChoicePoint.Describe`, `ChoicePoint.Diagnostic` (`SeverityInfo`, code `ChoiceDiagnosticCode`), `Context.noteChoice`, `Context.Notes`, `Context.Choices`, `ActionExecutor.Notes`/`StateExecutor.Notes`; `action_choice.go` `noteTokenOrder`, `noteDecisionBranches`, `stepWriteLedger.noteChoices`; `state_executor.go` `transitionChoice`, `chooseRegion`; `repl/trace.go` `Session.noteSummary` (`N choice points; %trace on to see them`, or the lines themselves under `%trace on`); `grpc/convert.go` `RunNoteDiagnosticsToProto` (the `diagnostics` of `ExecuteActionResponse`, `ExecuteStateResponse` and `RunAnalysisResponse`) | `choice_test.go:TestChoicePointRendering`, `:TestChoicesResetPerRun`, `:TestTransitionChoiceNamesStateAndEvent`, `:TestWriteConflictChoice`, `:TestSharedMessageAcceptIsAChoice`, `:TestAncestorPriorityIsNotAChoice`; `explore_test.go:TestExploreSiblingRegionOrder` (the `region order` kind); `conformance/action_choice_fork_token_order`, `action_choice_decision_overlapping_guards`, `action_choice_same_step_write_conflict`, `state_choice_transition_conflict`, `state_explore_region_order`, each `+ .trace.golden` carrying its `choice` line; `repl/choice_test.go:TestStepReportsChoicePoints`, `:TestStepChoiceSummaryWithTraceOn`, `:TestContinueReportsChoicePoints`, `:TestAdvanceReportsChoicePoints`; `grpc/choice_test.go:TestExecuteAction_ChoicePointDiagnostics`, `:TestExecuteState_ChoicePointDiagnostics`, `:TestRunAnalysis_ChoicePointDiagnostics`; `conformance_test.go:TestConformanceDiagnosticsGate` (an informational note is no failure of a conformance case) | ✅ Faithful (the ancestor-priority case between a substate's transition and its enclosing state's is ordered by UML/SysML and is not reported — `state_choice_ancestor_priority_not_reported`, `state_choice_ancestor_outranked_not_reported`) | | A guard the executor reads only to report a choice — one after the branch or transition already taken — that fails to evaluate is no alternative and no error: a guard with no result is not true, so its succession is not selected, the run is unchanged, and the failure is an informational `guard-unevaluable` note, while the same failure at the guard the run does take still fails the run | `choice.go` `UnevaluableGuard`, `UnevaluableGuard.Diagnostic` (`SeverityInfo`, code `UnevaluableGuardCode`), `Context.noteUnevaluableGuard`, `Context.UnevaluableGuards`; `action_choice.go` `ActionExecutor.noteUnevaluableGuard`; `action_executor.go` `probeGuard` (a `beginProbe` preview that restores the budget, the trace, every effect and the object identities it took); `state_executor.go` `probeTransition`, `unevaluableTransition`; `state_change_trigger.go` `probeChangeGuard` | `conformance/action_choice_unevaluable_guard` + `.expected.json` + `.trace.golden`; `conformance/state_choice_unevaluable_transition` + `.expected.json` + `.trace.golden`; `choice_test.go:TestLaterGuardErrorIsNotAChoiceNorAFailure`, `:TestFirstTransitionFailureStillFailsTheRun`, `:TestLaterGuardIsProbedWithoutCost`, `:TestLaterChangeGuardErrorIsNotAChoiceNorAFailure`, `:TestProbedGuardLeavesObjectIdentitiesUntouched`; `grpc/choice_test.go:TestExecuteAction_UnevaluableGuardDiagnostics`; `repl/choice_test.go:TestStepReportsUnevaluableGuards`; `robustness_test.go:decision_no_satisfied_guard` (the taken path still fails) | ✅ Faithful (SysML v2 §7.17.3 selects a succession whose guard is true; a guard that cannot be evaluated is not true, and reading it changed nothing) | | A conformance case that admits several outcomes states the whole set: `outcomes` lists every admissible outcome in full — never "anything" — and `admissible` cites the section of `behavior-semantic-oracle.md` that derives the set; a `.trace.order` beside it states the partial order the library does fix as `earlier < later` over trace labels. The harness checks the run's outcome is exactly one listed member, checks the trace against every order constraint, then explores the case and fails on a listed outcome no linearization reached, a reached outcome the list omits, and a hit budget — each naming the outcome and a witness choice sequence | `conformance_test.go` `ExpectedOutcome.Outcomes`/`Admissible`/`ExploreBudget`, `admissibleSchemaProblems` (an `outcomes` list needs two or more full outcomes, an `admissible` title the oracle has, and no single-outcome fields beside it), `matchOutcome`, `runConformanceCase`, `exploreConformanceCase`; `trace_test.go` `checkTraceOrder`, `parseOrderConstraints`, `orderViolations`; `testdata/conformance/README.md` (the schema) | `conformance_test.go:TestAdmissibleOutcomesSchema`, `:TestMatchOutcomeRequiresExactlyOne`, `:TestExecutionConformance` (`exploreConformanceCase` over every `outcomes` case), `:TestExecutionConformanceUnderPolicies`; `trace_test.go:TestTraceOrderViolationFails`, `:TestExecutionTrace`; `conformance/action_explore_three_writers` (`outcomes` of three, `.trace.order` of six constraints; explored in six runs), `action_choice_shared_message_accept`, `action_choice_fork_token_order` (one outcome, a `.trace.order` admitting the tokens either way), `state_explore_region_order` | ✅ Faithful (a case without `outcomes` is not explored by the harness, so a fixture pinning one linearization of an unobservable openness stays a one-outcome case; the oracle names which fixtures those are) | diff --git a/docs/reference/cli.md b/docs/reference/cli.md index 00a9807a8..9429cfee3 100644 --- a/docs/reference/cli.md +++ b/docs/reference/cli.md @@ -608,8 +608,12 @@ event, two tokens writing one feature in one step — one run shows one lineariz point, and every later run replays the recorded prefix and takes the next untried alternative at the frontier, depth-first, until no alternative is left untried or a budget is hit. Every run starts from a fresh executor on the same loaded model: no object, message, clock, calc memo or -note of one run is seen by the next. The policy applies to `-action`, `-state`, `-analysis` and -`-calc` alike; a body with no choice point explores in exactly one run. With `-advance`, every +note of one run is seen by the next. Under `explore` an action step is one token advancing one +node, where the fixed policies move every steppable token once per step, so the tokens able to act +are picked among afresh after each move and every interleaving of the nodes the library leaves +unordered is a distinct linearization; a body's statements still run without interruption. The +policy applies to `-action`, `-state`, `-analysis` and `-calc` alike; a body with no choice point +explores in exactly one run. With `-advance`, every `-action` and `-state` behavior named is started on one clock in each run and the clock advanced once, as it is under any policy, so the order of executors due at one instant is explored like any other choice point: several behaviors come to one *joint* outcome, each behavior's observables under @@ -630,9 +634,9 @@ $ sysml -schedule explore -action test::race three-writers.sysml ✓ explored test::race: 3 outcomes outcome | linearizations | witness ---------------------------------------------+----------------+------------------------------------------------------------------ -aRan = true; bRan = true; cRan = true; x = 1 | 2 | step 3: 3@b first of 2@a, 3@b, 4@c; step 3: 4@c first of 2@a, 4@c -aRan = true; bRan = true; cRan = true; x = 2 | 2 | step 3: 2@a first of 2@a, 3@b, 4@c; step 3: 4@c first of 3@b, 4@c -aRan = true; bRan = true; cRan = true; x = 3 | 2 | step 3: 2@a first of 2@a, 3@b, 4@c; step 3: 3@b first of 3@b, 4@c +aRan = true; bRan = true; cRan = true; x = 1 | 2 | step 3: 3@b first of 2@a, 3@b, 4@c; step 4: 4@c first of 2@a, 4@c +aRan = true; bRan = true; cRan = true; x = 2 | 2 | step 3: 2@a first of 2@a, 3@b, 4@c; step 4: 4@c first of 3@b, 4@c +aRan = true; bRan = true; cRan = true; x = 3 | 2 | step 3: 2@a first of 2@a, 3@b, 4@c; step 4: 3@b first of 3@b, 4@c complete (6 runs) ``` diff --git a/docs/reference/wire-contract.md b/docs/reference/wire-contract.md index d2724bfd4..a3dc4a820 100644 --- a/docs/reference/wire-contract.md +++ b/docs/reference/wire-contract.md @@ -922,7 +922,7 @@ $ … /ExecuteAction -d '{"modelHash":"81b1…73fc","actionSymbolId":"Test::tall {"outcomes":[{"outputs":{"leftCount":{"intValue":"1"},"rightCount":{"intValue":"10"}},"linearizations":2,"witness":["step 3: 2@left first of 2@left, 3@right"],"diagnostics":[{"severity":"info","message":"choice point: step 3: tokens 2@left, 3@right (unordered; took 2@left first)","span":{"file":"tally.sysml",…},"code":"choice-point"}]}],"exploration":{"complete":true,"runs":2,"runsBudget":1024,"depthBudget":64}} $ … /ExecuteAction -d '{"modelHash":"81b1…73fc","actionSymbolId":"Test::race","schedule":"explore"}' -{"outcomes":[{"outputs":{"winner":{"intValue":"1"}},"linearizations":2,"witness":["step 3: 3@b first of 2@a, 3@b, 4@c","step 3: 4@c first of 2@a, 4@c"],"diagnostics":[…]},{"outputs":{"winner":{"intValue":"2"}},"linearizations":2,"witness":["step 3: 2@a first of 2@a, 3@b, 4@c","step 3: 4@c first of 3@b, 4@c"],"diagnostics":[…]},{"outputs":{"winner":{"intValue":"3"}},"linearizations":2,"witness":["step 3: 2@a first of 2@a, 3@b, 4@c","step 3: 3@b first of 3@b, 4@c"],"diagnostics":[…]}],"exploration":{"complete":true,"runs":6,"runsBudget":1024,"depthBudget":64}} +{"outcomes":[{"outputs":{"winner":{"intValue":"1"}},"linearizations":2,"witness":["step 3: 3@b first of 2@a, 3@b, 4@c","step 4: 4@c first of 2@a, 4@c"],"diagnostics":[…]},{"outputs":{"winner":{"intValue":"2"}},"linearizations":2,"witness":["step 3: 2@a first of 2@a, 3@b, 4@c","step 4: 4@c first of 3@b, 4@c"],"diagnostics":[…]},{"outputs":{"winner":{"intValue":"3"}},"linearizations":2,"witness":["step 3: 2@a first of 2@a, 3@b, 4@c","step 4: 3@b first of 3@b, 4@c"],"diagnostics":[…]}],"exploration":{"complete":true,"runs":6,"runsBudget":1024,"depthBudget":64}} ``` `tally`'s two orders write two different features, so its two linearizations are one outcome; diff --git a/internal/core/runtime/action_choice.go b/internal/core/runtime/action_choice.go index 4b09f97df..82abe4d95 100644 --- a/internal/core/runtime/action_choice.go +++ b/internal/core/runtime/action_choice.go @@ -252,22 +252,24 @@ func (e *ActionExecutor) tokenActed(before Token, count int) bool { return after.moved != before.moved || (before.Wait != nil && after.Wait == nil) } -// noteTokenOrder records the tokens a step advanced as a choice point when there -// are at least two; which went first is the executor's rule, not the library's. -func (e *ActionExecutor) noteTokenOrder(step int, order stepOrder) { - if len(order.acted) < 2 { - return - } - first := order.acted[0].ID - tokens := make([]Token, len(order.acted)) - copy(tokens, order.acted) - sort.Slice(tokens, func(i, j int) bool { return tokens[i].ID < tokens[j].ID }) - alts := make([]string, len(tokens)) - taken := 0 - for i, t := range tokens { - alts[i] = fmt.Sprintf("%d@%s", t.ID, nodeIdentifier(t.Location)) - if t.ID == first { - taken = i +// noteTokenOrder records the tokens a step advanced as a choice point when there are +// at least two, or the one an exploring step picked among those able to act. +func (e *ActionExecutor) noteTokenOrder(step int, order stepOrder, schedule *tokenSchedule) { + alts, taken, chosen := schedule.Choice() + if !chosen { + if len(order.acted) < 2 { + return + } + first := order.acted[0].ID + tokens := make([]Token, len(order.acted)) + copy(tokens, order.acted) + sort.Slice(tokens, func(i, j int) bool { return tokens[i].ID < tokens[j].ID }) + alts = make([]string, len(tokens)) + for i, t := range tokens { + alts[i] = fmt.Sprintf("%d@%s", t.ID, nodeIdentifier(t.Location)) + if t.ID == first { + taken = i + } } } e.ctx.noteChoice(ChoicePoint{ diff --git a/internal/core/runtime/action_executor.go b/internal/core/runtime/action_executor.go index c6c424c73..bde140a08 100644 --- a/internal/core/runtime/action_executor.go +++ b/internal/core/runtime/action_executor.go @@ -258,13 +258,14 @@ func (e *ActionExecutor) Step() error { order := e.beginStepOrder() endWrites := e.beginStepWrites(e.stepCount + 1) - err := e.stepTokens(e.scheduleTokens(&order, func(t Token) bool { + schedule := e.scheduleTokens(&order, func(t Token) bool { return !t.drivenByBody() && t.body == nil - }), paused, &order) + }) + err := e.stepTokens(schedule, paused, &order) // What the tokens wrote and the order they took are facts of the step whether // or not it failed. endWrites() - e.noteTokenOrder(e.stepCount+1, order) + e.noteTokenOrder(e.stepCount+1, order, schedule) if err != nil { e.endPausedBodies() return err @@ -1321,8 +1322,8 @@ func (e *ActionExecutor) parked(t Token, order *stepOrder) bool { return waitsForMessage && !order.offered[t.ID] } -// stepTokens gives each of the scheduled tokens its step, in the order given, then -// the tokens a breakpoint left paused; a breakpoint reached on the way ends the sweep. +// stepTokens gives each scheduled token its step, then the tokens a breakpoint +// left paused; a breakpoint on the way or an exploring step's one move ends the sweep. func (e *ActionExecutor) stepTokens(schedule *tokenSchedule, paused []int64, order *stepOrder) error { for id, ok := schedule.Next(); ok; id, ok = schedule.Next() { if e.state == StateSuspended { @@ -1342,7 +1343,7 @@ func (e *ActionExecutor) stepTokens(schedule *tokenSchedule, paused []int64, ord } } for _, id := range paused { - if e.state == StateSuspended { + if e.state == StateSuspended || schedule.Ended() { break } if i := e.tokenIndex(id); i >= 0 { diff --git a/internal/core/runtime/action_subflow.go b/internal/core/runtime/action_subflow.go index 02454ae11..fcfce3fd4 100644 --- a/internal/core/runtime/action_subflow.go +++ b/internal/core/runtime/action_subflow.go @@ -135,7 +135,7 @@ func (e *ActionExecutor) stepSubflow(perf *actionFrame) (bool, error) { } } endWrites() - e.noteTokenOrder(e.stepCount+1, order) + e.noteTokenOrder(e.stepCount+1, order, schedule) if err != nil { return false, err } diff --git a/internal/core/runtime/explore.go b/internal/core/runtime/explore.go index a02ad587c..a6592a1ec 100644 --- a/internal/core/runtime/explore.go +++ b/internal/core/runtime/explore.go @@ -235,14 +235,16 @@ func (r *exploreRun) describe(c ChoicePoint) { } } -// exploreStep tries a step's tokens one at a time, each a choice among the -// tokens able to act at that moment. +// exploreStep tries a step's tokens one at a time until one acts: that move is +// the step, a choice among the tokens able to act at that moment. type exploreStep struct { run *exploreRun tokens stepTokens - remaining []int64 // sorted by ID, not yet tried - held []int64 // tried last, as they never act on their own - slot int // index in run.record of the slot open, -1 between picks + remaining []int64 // sorted by ID, not yet tried + held []int64 // tried last, as they never act on their own + slot int // index in run.record of the slot open, -1 between picks + moved bool // a token acted, so the step is over + choice *exploreSlot // the pick the move resolved, nil when one token alone could act } // beginStep opens the step's picks. @@ -263,6 +265,9 @@ func (r *exploreRun) beginStep(tokens stepTokens) *exploreStep { // next picks the token to try: the planned or first of those able to act when at // least two are, the only one when one is, else the first left, which will not act. func (s *exploreStep) next() (int64, bool) { + if s.moved { + return 0, false + } if len(s.remaining) == 0 { if len(s.held) == 0 { return 0, false @@ -299,17 +304,22 @@ func (s *exploreStep) next() (int64, bool) { return slot.tokens[slot.taken], true } -// acted closes the pick when the token acted; one that did not was no -// alternative, so it leaves the slot and the pick is made again. +// acted ends the step when the token acted, closing the pick; one that did not +// was no alternative, so it leaves the slot and the pick is made again. func (s *exploreStep) acted(id int64, acted bool) { if i := slices.Index(s.remaining, id); i >= 0 { s.remaining = slices.Delete(s.remaining, i, i+1) } - if s.slot < 0 { + if acted { + s.moved = true + if s.slot >= 0 { + slot := s.run.record[s.slot] + s.choice = &slot + s.slot = -1 + } return } - if acted { - s.slot = -1 + if s.slot < 0 { return } slot := &s.run.record[s.slot] diff --git a/internal/core/runtime/scheduler.go b/internal/core/runtime/scheduler.go index be1476a84..fd6e8fc5f 100644 --- a/internal/core/runtime/scheduler.go +++ b/internal/core/runtime/scheduler.go @@ -237,6 +237,21 @@ func (ts *tokenSchedule) Acted(id int64, acted bool) { } } +// Ended reports whether the step is over before every token had its turn: an +// exploring step is one token's move. +func (ts *tokenSchedule) Ended() bool { + return ts.explore != nil && ts.explore.moved +} + +// Choice is the token-order pick an exploring step resolved, as the trace names +// the tokens able to act and the index of the one moved; false when it made none. +func (ts *tokenSchedule) Choice() (alternatives []string, taken int, ok bool) { + if ts.explore == nil || ts.explore.choice == nil { + return nil, 0, false + } + return ts.explore.choice.labels, ts.explore.choice.taken, true +} + // scheduleStep fixes how the step tries its tokens: reversed, declared, // seeded shuffle, or one at a time as the exploration picks them. func (s *scheduler) scheduleStep(tokens stepTokens) *tokenSchedule { diff --git a/internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.declared.trace.golden b/internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.declared.trace.golden new file mode 100644 index 000000000..1773202ac --- /dev/null +++ b/internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.declared.trace.golden @@ -0,0 +1,14 @@ +step 1: token 1@split +step 2: token 2@left1, token 3@right +stmt assign x + eval literal 1 -> 1 +stmt assign x + eval literal 2 -> 2 +choice step 3: writes x := 1 by token 2, x := 2 by token 3 (unordered; x := 2 by token 3 stood) +choice step 3: tokens 2@left1, 3@right (unordered; took 2@left1 first) +step 3: token 2@left2, token 3@sync +stmt assign y + eval feature x -> 2 +step 4: token 2@sync, token 3@sync +step 5: token 4@done +step 6: no active tokens diff --git a/internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.expected.json b/internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.expected.json new file mode 100644 index 000000000..e9bfc67ca --- /dev/null +++ b/internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.expected.json @@ -0,0 +1,25 @@ +{ + "type": "action", + "trace": true, + "outcomes": [ + { + "outputs": { + "x": {"type": "Integer", "value": 1}, + "y": {"type": "Integer", "value": 1} + } + }, + { + "outputs": { + "x": {"type": "Integer", "value": 2}, + "y": {"type": "Integer", "value": 1} + } + }, + { + "outputs": { + "x": {"type": "Integer", "value": 2}, + "y": {"type": "Integer", "value": 2} + } + } + ], + "admissible": "A write between two nodes of a concurrent branch: three orders, three outcomes" +} diff --git a/internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.seed-1.trace.golden b/internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.seed-1.trace.golden new file mode 100644 index 000000000..1773202ac --- /dev/null +++ b/internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.seed-1.trace.golden @@ -0,0 +1,14 @@ +step 1: token 1@split +step 2: token 2@left1, token 3@right +stmt assign x + eval literal 1 -> 1 +stmt assign x + eval literal 2 -> 2 +choice step 3: writes x := 1 by token 2, x := 2 by token 3 (unordered; x := 2 by token 3 stood) +choice step 3: tokens 2@left1, 3@right (unordered; took 2@left1 first) +step 3: token 2@left2, token 3@sync +stmt assign y + eval feature x -> 2 +step 4: token 2@sync, token 3@sync +step 5: token 4@done +step 6: no active tokens diff --git a/internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.sysml b/internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.sysml new file mode 100644 index 000000000..9f7d3b40d --- /dev/null +++ b/internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.sysml @@ -0,0 +1,29 @@ +package test { + private import ScalarValues::*; + + // Oracle (docs/project/behavior-semantic-oracle.md): one fork branch is two + // nodes, `left1` writing `x` and `left2` reading it into `y`; the other branch, + // `right`, writes `x` once. The library orders `left2` after `left1` and nothing + // against `right`, so `right` may run before both, between them, or after both: + // three linearizations, and each leaves a different pair of values. + action overtake { + attribute x : Integer = 0; + attribute y : Integer = 0; + + first start; + fork split; + action left1 { assign x := 1; } + action left2 { assign y := x; } + action right { assign x := 2; } + join sync; + done; + + succession first start then split; + succession first split then left1; + succession first left1 then left2; + succession first split then right; + succession first left2 then sync; + succession first right then sync; + succession first sync then done; + } +} diff --git a/internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.trace.golden b/internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.trace.golden new file mode 100644 index 000000000..6a279e036 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.trace.golden @@ -0,0 +1,14 @@ +step 1: token 1@split +step 2: token 2@left1, token 3@right +stmt assign x + eval literal 2 -> 2 +stmt assign x + eval literal 1 -> 1 +choice step 3: writes x := 1 by token 2, x := 2 by token 3 (unordered; x := 1 by token 2 stood) +choice step 3: tokens 2@left1, 3@right (unordered; took 3@right first) +step 3: token 2@left2, token 3@sync +stmt assign y + eval feature x -> 1 +step 4: token 2@sync, token 3@sync +step 5: token 4@done +step 6: no active tokens diff --git a/internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.trace.order b/internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.trace.order new file mode 100644 index 000000000..ccc2a3fee --- /dev/null +++ b/internal/core/runtime/testdata/conformance/action_explore_write_between_branch_nodes.trace.order @@ -0,0 +1,9 @@ +# The fork precedes both branches; left2 follows left1; the join waits for both. +# A token parked at the join is mentioned as soon as the first branch arrives, so +# the branch arriving second is ordered against the join's successor instead. +split < left1 +left1 < left2 +split < right +left2 < done +right < done +sync < done diff --git a/internal/repl/explore_test.go b/internal/repl/explore_test.go index 3ee2ec361..c8c2af794 100644 --- a/internal/repl/explore_test.go +++ b/internal/repl/explore_test.go @@ -60,9 +60,9 @@ func TestRunActionExploresEveryLinearization(t *testing.T) { wantsInOrder(t, strings.Join(v.Lines, "\n"), "✓ explored Race::race: 3 outcomes", "outcome | linearizations | witness", - "x = 1 | 2 | step 3: 3@b first of 2@a, 3@b, 4@c; step 3: 4@c first of 2@a, 4@c", - "x = 2 | 2 | step 3: 2@a first of 2@a, 3@b, 4@c; step 3: 4@c first of 3@b, 4@c", - "x = 3 | 2 | step 3: 2@a first of 2@a, 3@b, 4@c; step 3: 3@b first of 3@b, 4@c", + "x = 1 | 2 | step 3: 3@b first of 2@a, 3@b, 4@c; step 4: 4@c first of 2@a, 4@c", + "x = 2 | 2 | step 3: 2@a first of 2@a, 3@b, 4@c; step 4: 4@c first of 3@b, 4@c", + "x = 3 | 2 | step 3: 2@a first of 2@a, 3@b, 4@c; step 4: 3@b first of 3@b, 4@c", "complete (6 runs)") if len(v.Outcomes) != 3 || v.Exploration == nil || !v.Exploration.Complete || v.Exploration.Runs != 6 { t.Errorf("verdict outcomes = %+v, exploration = %+v", v.Outcomes, v.Exploration) @@ -110,7 +110,8 @@ func TestRunActionExploreReportsTheBudgetHit(t *testing.T) { wants(t, strings.Join(v.Lines, "\n"), "incomplete: depth budget 1 hit after 3 runs") } -// With tracing on, the trace shown per outcome is its witness run's. +// With tracing on, the trace shown per outcome is its witness run's: one token +// moves per explored step, so the last write to x is the witness's last move. func TestRunActionExploreTracesTheWitnessOfEachOutcome(t *testing.T) { s := loadSource(t, exploreRaceSource) run(t, s, "%trace on") @@ -121,12 +122,17 @@ func TestRunActionExploreTracesTheWitnessOfEachOutcome(t *testing.T) { wantsInOrder(t, out, "complete (6 runs)", "trace of outcome 1's witness (run 4):", - "x := 1 by token 2 stood", "took 3@b first", + "took 4@c first", + "eval literal 1 -> 1", "trace of outcome 2's witness (run 2):", - "x := 2 by token 3 stood", + "took 2@a first", + "took 4@c first", + "eval literal 2 -> 2", "trace of outcome 3's witness (run 1):", - "x := 3 by token 4 stood") + "took 2@a first", + "took 3@b first", + "eval literal 3 -> 3") if strings.Count(out, "trace of outcome") != 3 { t.Errorf("want one trace per outcome:\n%s", out) } From 07a9d8d80738aa3fc73d89edbd02372395b25f80 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Wed, 9 Sep 2026 21:31:02 +0000 Subject: [PATCH 07/33] fix(lower): source a sourceless transition from the state declared before it MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A transition written without a source part (`accept go then s;`, `if c then s;`, `then s;`) leaves the closest lexically previous state usage in the body that declares it (SysML v2 7.18.3, TargetTransitionUsage), not the state whose body contains it. Lowering took the containing state, so the shorthand failed at a machine's top level and, nested in a composite state, fired from every substate (timers re-armed, entry actions re-ran). Derive the source in the AST helper, report a missing or non-vertex preceding member at the constraint tier with a typed error, and keep the same errors as a lowering backstop. Migrate fixtures and docs from the `state s { accept … then t; }` placement the pilot rejects to the flat form it accepts. Co-Authored-By: jason.han --- .agents/skills/testing-sysml-repl/SKILL.md | 10 +- .../target-transition-source.fixed.md | 1 + cmd/sysml/run_test.go | 18 +- cmd/sysml/unset_feature_value_test.go | 3 +- docs/guide/03-command-line.md | 10 +- docs/guide/06-behavior.md | 26 +- docs/internals/architecture.md | 2 +- docs/internals/testing.md | 2 +- docs/project/demo.md | 9 +- docs/project/pilot-differential.md | 23 +- docs/project/spec-compliance.md | 6 +- docs/reference/grammar/README.md | 7 + internal/core/ast/transition_source.go | 31 +++ internal/core/lower/state_graph.go | 34 +-- internal/core/lower/state_inheritance.go | 25 +- internal/core/lower/transition_source.go | 67 +++++ internal/core/lower/transition_source_test.go | 251 ++++++++++++++++++ .../core/model/behavior_body_resolve_test.go | 3 +- internal/core/model/state_endpoint_test.go | 2 +- .../testdata/parse/state_call_trigger.golden | 7 +- .../testdata/parse/state_call_trigger.sysml | 5 +- .../state_target_transition_placements.golden | 96 +++++++ .../state_target_transition_placements.sysml | 53 ++++ .../parse/state_timed_triggers.golden | 24 +- .../testdata/parse/state_timed_triggers.sysml | 12 +- internal/core/passes/state_transition.go | 49 +++- internal/core/passes/state_transition_test.go | 138 +++++++++- internal/core/passes/typecheck_expr_test.go | 15 +- .../core/passes/typecheck_trigger_test.go | 15 +- internal/core/resolve/event_feature_test.go | 2 +- internal/core/resolve/state_type.go | 2 +- internal/core/resolve/transition.go | 12 +- internal/core/resolve/transition_test.go | 5 +- .../core/runtime/classifier_behavior_test.go | 15 +- internal/core/runtime/connector_test.go | 12 +- internal/core/runtime/debug_api_test.go | 12 +- internal/core/runtime/explore_test.go | 3 +- internal/core/runtime/robustness_test.go | 151 +++++++---- internal/core/runtime/scheduler_test.go | 6 +- .../core/runtime/signal_injection_test.go | 3 +- .../core/runtime/state_change_trigger_test.go | 50 ++-- .../state_composite_transition_test.go | 2 +- .../core/runtime/state_time_trigger_test.go | 30 +-- .../accept_then_transition.expected.json | 2 +- .../conformance/accept_then_transition.sysml | 11 +- .../clock_action_signal_delayed_state.sysml | 10 +- .../clock_action_state_due_together.sysml | 5 +- .../clock_do_action_while_token_waits.sysml | 5 +- .../clock_two_machines_share_clock.sysml | 17 +- .../exhibited_state_two_objects.sysml | 5 +- ...tance_nested_parts_run_to_quiescence.sysml | 3 +- .../object_addressed_send_one_sibling.sysml | 10 +- .../object_mutual_addressed_send.sysml | 7 +- .../send_bind_relay_aliased_ends.sysml | 7 +- .../send_bind_relay_connector_order.sysml | 5 +- .../conformance/send_bind_relay_inbound.sysml | 5 +- .../conformance/send_bind_relay_nested.sysml | 5 +- .../send_bind_relay_outbound.sysml | 5 +- .../state_call_trigger_nested.sysml | 5 +- .../state_change_trigger_autonomous.sysml | 2 +- .../state_change_trigger_event_order.sysml | 5 +- .../state_parallel_accept_after.sysml | 5 +- .../state_parallel_broadcast.sysml | 10 +- .../state_redefined_state_accept.sysml | 5 +- .../state_redefined_state_accept_symbol.sysml | 5 +- ...t_transition_after_do_action.expected.json | 5 + ...te_target_transition_after_do_action.sysml | 19 ++ ...tate_target_transition_guard.expected.json | 10 + .../state_target_transition_guard.sysml | 18 ++ ...rget_transition_nested_timed.expected.json | 15 ++ ...state_target_transition_nested_timed.sysml | 26 ++ ...arget_transition_nested_timed.trace.golden | 15 ++ ...t_transition_top_level_timed.expected.json | 15 ++ ...te_target_transition_top_level_timed.sysml | 22 ++ ...et_transition_top_level_timed.trace.golden | 12 + .../state_time_quantity_instant.sysml | 5 +- .../state_time_quantity_seconds.sysml | 5 +- .../state_time_quantity_unit_ordering.sysml | 10 +- ...te_time_trigger_restarts_on_re_entry.sysml | 15 +- .../conformance/state_timed_transitions.sysml | 17 +- .../two_objects_exhibit_independently.sysml | 5 +- internal/perfbench/perf_test.go | 9 +- internal/perfbench/workload_test.go | 9 +- internal/repl/explore_test.go | 3 +- internal/repl/features_command_test.go | 3 +- internal/repl/object_ref_test.go | 20 +- .../repl/testdata/collection_machine.sysml | 2 +- .../repl/testdata/exhibited_machine.sysml | 2 +- .../repl/testdata/named_usage_machine.sysml | 7 +- internal/repl/testdata/nested_machine.sysml | 2 +- .../repl/testdata/performed_machine.sysml | 5 +- internal/repl/testdata/ping_counter.sysml | 3 +- internal/repl/testdata/quoted_names.sysml | 5 +- internal/repl/testdata/shared_machine.sysml | 5 +- internal/repl/testdata/state_debug.sysml | 10 +- .../repl/testdata/state_do_far_event.sysml | 2 +- internal/repl/testdata/state_tick.sysml | 10 +- .../repl/testdata/state_typed_usage.sysml | 2 +- internal/repl/testdata/two_machines.sysml | 10 +- 99 files changed, 1292 insertions(+), 419 deletions(-) create mode 100644 changes/unreleased/target-transition-source.fixed.md create mode 100644 internal/core/ast/transition_source.go create mode 100644 internal/core/lower/transition_source.go create mode 100644 internal/core/lower/transition_source_test.go create mode 100644 internal/core/parser/testdata/parse/state_target_transition_placements.golden create mode 100644 internal/core/parser/testdata/parse/state_target_transition_placements.sysml create mode 100644 internal/core/runtime/testdata/conformance/state_target_transition_after_do_action.expected.json create mode 100644 internal/core/runtime/testdata/conformance/state_target_transition_after_do_action.sysml create mode 100644 internal/core/runtime/testdata/conformance/state_target_transition_guard.expected.json create mode 100644 internal/core/runtime/testdata/conformance/state_target_transition_guard.sysml create mode 100644 internal/core/runtime/testdata/conformance/state_target_transition_nested_timed.expected.json create mode 100644 internal/core/runtime/testdata/conformance/state_target_transition_nested_timed.sysml create mode 100644 internal/core/runtime/testdata/conformance/state_target_transition_nested_timed.trace.golden create mode 100644 internal/core/runtime/testdata/conformance/state_target_transition_top_level_timed.expected.json create mode 100644 internal/core/runtime/testdata/conformance/state_target_transition_top_level_timed.sysml create mode 100644 internal/core/runtime/testdata/conformance/state_target_transition_top_level_timed.trace.golden diff --git a/.agents/skills/testing-sysml-repl/SKILL.md b/.agents/skills/testing-sysml-repl/SKILL.md index 9ec04481a..7e8701d28 100644 --- a/.agents/skills/testing-sysml-repl/SKILL.md +++ b/.agents/skills/testing-sysml-repl/SKILL.md @@ -2233,7 +2233,7 @@ fixed from broken, each with a visible A/B against `main`: - **Calc parameter** — `in redefines factor = 3;` overriding an inherited `in factor = 2`. The giveaway is a *wrong number*, not an error: the invocation silently uses the inherited default (`Scaled(7)` → 14 instead of 21), so assert the value, never just "it evaluated". -- **State** — `state redefines waiting { accept go then active; }`. A lost name makes the sourceless +- **State** — `state redefines waiting; accept go then active;`. A lost name makes the sourceless accept vanish: `%state` shows `Events: 0` and `%advance 1` never leaves the initial state. Ready-made fixtures for all of these live in `internal/core/runtime/testdata/conformance/` @@ -3596,7 +3596,7 @@ False-positive traps to always include as *legal* rows, since each exercises a d one; run it with `%state TransitionSiblingRegion` + `%advance 1` → `Current state: lidle | rtarget` and `crossed = 1`. - `entry point into;` / `exit point outOf;` as endpoints (`state_entry_exit_points.sysml`). -- A sourceless `accept after 5 then ;` written *inside* a state (source is implicit). +- A sourceless `accept after 5 then ;` written after a state (the source is the state declared before it). - `first start then off;` with no `initial`. - A junction left by a **succession** (`route then finishedUp;`) rather than a `transition`, and a `fork`/`join` reached by one — the pass tracks succession sources *by name*, so a regression here @@ -5250,7 +5250,7 @@ to diff against a document's table verbatim. Use `%send [to ]` followed by `%step` to drive signal transitions. The signal lists in `internal/core/runtime/testdata/conformance/*.expected.json` belong to the conformance harness and are not automatically injected by the REPL. Alternatively, write -fixtures with **timed triggers** (`state a { accept after 5 then done; }`) +fixtures with **timed triggers** (`state a; accept after 5 then done;`) and step them with `%advance `; each region can be given a different delay so a partial configuration is observable. `sysml -state ` only *starts* the executor and prints the initial configuration — it does not run to completion, so use @@ -5280,8 +5280,8 @@ Completion (a transition whose endpoint is the unqualified `done`) shows up as, ```sysml state def M { entry; then outer; state outer parallel { - state r1 { entry; then x; state x { accept after 5 then done; } } - state r2 { entry; then y; state y { accept after 7 then done; } } } } + state r1 { entry; then x; state x; accept after 5 then done; } + state r2 { entry; then y; state y; accept after 7 then done; } } } ``` `%advance 5` → `done | y` + `Running`, no completion line; `%advance 2` → `done | done` + `Completed`. Add a *two-level* variant (a `parallel` state inside a region of another `parallel` state) whose inner diff --git a/changes/unreleased/target-transition-source.fixed.md b/changes/unreleased/target-transition-source.fixed.md new file mode 100644 index 000000000..c72e0513b --- /dev/null +++ b/changes/unreleased/target-transition-source.fixed.md @@ -0,0 +1 @@ +- **A transition written without a source (`accept … then`, `if … then`, `then`) now leaves the state declared before it in the same body, as SysML v2 §7.18.3 specifies and the OMG pilot implements.** It used to take the state whose body contained it as the source, and to refuse the form at a state machine's top level at instantiation, so a nested `accept after 5 [SI::s] then decelerating;` fired from every substate and re-armed its timer forever, and the top-level form failed with `sourceless transition at top level has no containing state`. The shorthand is now a member of the body that declares the state it leaves, written after that state (the pinned pilot rejects it inside the state's own body), several in a row all leave the same state, and one written first in its body or after a member that is not a state — an attribute, a `do` action, a succession, an entry action with a trigger, an orthogonal region — is reported by validation with the member named. The guarded entry transition (`entry; if c then off;`) is accepted by validation but not lowered yet; the executor reports it with the `entry; then s;` form to use. diff --git a/cmd/sysml/run_test.go b/cmd/sysml/run_test.go index 4626e0018..dfd931a7c 100644 --- a/cmd/sysml/run_test.go +++ b/cmd/sysml/run_test.go @@ -42,12 +42,10 @@ const behaviorModel = `package Mission { state Cycle { entry; then init; state init; - state waiting { - accept after 10 [SI::s] then working; - } - state working { - accept after 5 [SI::s] then done; - } + state waiting; + accept after 10 [SI::s] then working; + state working; + accept after 5 [SI::s] then done; succession first init then waiting; } } @@ -457,8 +455,8 @@ const fleetModel = `package Fleet { assign log := log + "W"; assign level := level + 10; } - accept after 5 [SI::s] then moving; } + accept after 5 [SI::s] then moving; state moving { entry action m { assign log := log + "M"; @@ -568,7 +566,8 @@ func TestStateNamesTheUsageToInstantiate(t *testing.T) { const sharedMachineModel = `package Shared { state def Blink { entry; then dark; - state dark { accept after 2 [SI::s] then lit; } + state dark; + accept after 2 [SI::s] then lit; state lit; } part def Lamp { @@ -903,7 +902,8 @@ const dueTogetherModel = `package Due { attribute lit : Boolean = false; exhibit state blinking { entry; then dark; - state dark { accept after 5 [s] then shining; } + state dark; + accept after 5 [s] then shining; state shining { entry assign lit := true; } } } diff --git a/cmd/sysml/unset_feature_value_test.go b/cmd/sysml/unset_feature_value_test.go index 8068fd8df..829e73693 100644 --- a/cmd/sysml/unset_feature_value_test.go +++ b/cmd/sysml/unset_feature_value_test.go @@ -75,7 +75,8 @@ const pingCounterModel = `package P { attribute got : Integer = 0; exhibit state sm { entry; then Idle; - state Idle { accept Ping via i then Got; } + state Idle; + accept Ping via i then Got; state Got { entry assign got := got + 1; } } } diff --git a/docs/guide/03-command-line.md b/docs/guide/03-command-line.md index 185bda6bd..369af3462 100644 --- a/docs/guide/03-command-line.md +++ b/docs/guide/03-command-line.md @@ -55,9 +55,8 @@ package MyModel { entry; then off; state off; - state warming { - accept after 10 [SI::s] then running; - } + state warming; + accept after 10 [SI::s] then running; state running; transition first off then warming; } @@ -189,9 +188,8 @@ package M { state off { defer Alarm; } - state warming { - accept after 10 [SI::s] then done; - } + state warming; + accept after 10 [SI::s] then done; succession first off then warming; } } diff --git a/docs/guide/06-behavior.md b/docs/guide/06-behavior.md index f4957cf44..fcd9103c1 100644 --- a/docs/guide/06-behavior.md +++ b/docs/guide/06-behavior.md @@ -51,13 +51,27 @@ and the machine completes only once every region has reached it. sysml> state TrafficLight { ...> entry; then start; ...> state start; - ...> state green { accept after 25 [SI::s] then yellow; } - ...> state yellow { accept after 5 [SI::s] then red; } - ...> state red { accept after 30 [SI::s] then done; } + ...> state green; + ...> accept after 25 [SI::s] then yellow; + ...> state yellow; + ...> accept after 5 [SI::s] then red; + ...> state red; + ...> accept after 30 [SI::s] then done; ...> succession first start then green; ...> } ✓ state TrafficLight +``` + +A transition written without `transition … first`, as the three `accept after … then …` +lines above are, leaves the state declared right before it in the same body (SysML v2 +§7.18.3): `accept after 25 [SI::s] then yellow;` leaves `green` because `state green;` +precedes it. Several such transitions in a row all leave the same state, and the shorthand +takes the same triggers (`accept Signal`, `accept after`, `accept at`, `accept when`), guards +(`if …`) and effects (`do …`) as the full form. It has to follow the state it leaves +directly, so write it in the body that declares that state, not inside the state's own body; +written first in a body, or after a member that is not a state, it is reported. +```sysml sysml> %state TrafficLight ✓ Started state machine executor for "TrafficLight" Current state: start @@ -621,10 +635,8 @@ sysml> part def Monitor { ...> attribute count = 0; ...> exhibit state modes { ...> entry; then idle; - ...> state idle { - ...> entry action bump { assign count := count + 1; } - ...> accept after 10 [SI::s] then awake; - ...> } + ...> state idle { entry action bump { assign count := count + 1; } } + ...> accept after 10 [SI::s] then awake; ...> state awake { entry action mark { assign count := count + 10; } } ...> } ...> action bumpBy { in n; action apply { assign count := count + n; } first apply; then done; } diff --git a/docs/internals/architecture.md b/docs/internals/architecture.md index 4c43fbb7c..4d2c6c27d 100644 --- a/docs/internals/architecture.md +++ b/docs/internals/architecture.md @@ -688,7 +688,7 @@ go test -v -run TestExecutionConformance ./internal/core/runtime - Deadlocked action (join starvation) - Decision with no satisfied guard - State machine with dangling transition -- Sourceless accept...then at top level +- Sourceless accept...then written first in its body or after a member that is not a state - Calc with unbound parameter, surplus or unknown-named arguments, no result, non-calc target, direct or mutual recursion - Constraint referencing missing feature - Step budget exceeded diff --git a/docs/internals/testing.md b/docs/internals/testing.md index a08a2108c..93363f2f5 100644 --- a/docs/internals/testing.md +++ b/docs/internals/testing.md @@ -153,7 +153,7 @@ go test -run TestExecutionTrace -update-traces ./internal/core/runtime - Deadlocked action (join starvation) - Decision with no satisfied guard - State machine with dangling transition -- Sourceless accept...then at top level +- Sourceless accept...then written first in its body or after a member that is not a state - Calc with unbound parameter, surplus or unknown-named arguments, no result, non-calc target, direct or mutual recursion - Constraint referencing missing feature - Step budget exceeded diff --git a/docs/project/demo.md b/docs/project/demo.md index caba0695d..6588af16a 100644 --- a/docs/project/demo.md +++ b/docs/project/demo.md @@ -342,9 +342,12 @@ package Mission { state rover { entry; then idle; - state idle { accept after 5 [SI::s] then driving; } - state driving { accept after 10 [SI::s] then charging; } - state charging { accept after 20 [SI::s] then idle; } + state idle; + accept after 5 [SI::s] then driving; + state driving; + accept after 10 [SI::s] then charging; + state charging; + accept after 20 [SI::s] then idle; } } EOF diff --git a/docs/project/pilot-differential.md b/docs/project/pilot-differential.md index 6a8547bc1..3ffeab991 100644 --- a/docs/project/pilot-differential.md +++ b/docs/project/pilot-differential.md @@ -692,8 +692,27 @@ retired rows were agreement. diagnostic from either side: files 33 → **34** and fully agreeing 25 → **26** on the root, 367 → **368** and 337 → **338** overall, with every diagnostic count unmoved. The model writes its timed transition in the full form (`transition first coasting accept after 5 [SI::s] then decelerating;`) -because the pinned reference does not parse a target transition inside the body of its source state, -and this implementation does not lower a sourceless target transition at the state machine's top level. +because the pinned reference does not parse a target transition inside the body of its source state; +the shorthand form (`state coasting; accept after 5 [SI::s] then decelerating;`) is equivalent, and both +sides accept it. + +### Target transition source round + +A transition written without a source now leaves the state declared before it in its body +(SysML v2 §7.18.3 `TargetTransitionUsage`), where it used to leave the state whose body contained +it. No corpus file moves: 368 files, 338 fully agreeing, 34 agreed, 21 only ours, 596 only the +pilot's, identical on the parent commit and on this branch. The corpora write the shorthand only +in the flat placement both sides accept (the training `25. Transitions` models leave `normal`, +`maintenance` and `degraded` by it), and no corpus file writes it inside the state it leaves, or +first in its body, or after a member that is not a state — the placements this implementation now +reports at the constraint tier and the reference rejects by its grammar (`no viable alternative +at input 'accept'`, `missing '}' at 'go'`) or by `A transition with an accepter must have a state +as its source`. Three placements were refereed by probe rather than by corpus, with the same +verdict on both sides: a `doc` between the state and the shorthand makes the documentation the +member before it (rejected), a guarded shorthand directly after `entry;` is the guarded entry +transition (accepted by both; this implementation does not lower it yet, see +`spec-compliance.md`), and a shorthand directly inside a `parallel` state is `A parallel state +cannot have successions or transitions` on both sides. ## Adjudications diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md index 23bd4bd13..994c1a3ec 100644 --- a/docs/project/spec-compliance.md +++ b/docs/project/spec-compliance.md @@ -84,7 +84,7 @@ what cannot be checked by anything is in - Transition guard evaluation - Transition effect actions - AcceptEvent triggers (when signal) -- Sourceless transitions (`accept...then`, nested form) +- Sourceless transitions (`accept … then`, `if … then`, `then`): the source is the state declared before them in the same body - ChangeEvent triggers (when expression) - TimeEvent triggers (`after` duration, `at` instant) - Signal discrimination (name matching) @@ -641,9 +641,9 @@ by name is refused naming what is missing rather than approximated. | A signal injected from outside the model (`%send` at the REPL) travels the same bus as `send Signal(args) to ` from a behavior, typed by the signal definition and addressed to the object, and an argument the signal has no feature for is refused | `runtime/signal.go` `Context.SignalMessage`, `NamedSignalMessage`; `state_executor.go` `Performer`; `classifier_behavior.go` `Context.ExhibitedMachineOf`; `repl/send.go` `%send`; `repl/meta.go` `%state ` attaches to the exhibited machine of that kind | `runtime/signal_injection_test.go:TestSignalMessageDrivesTheExhibitedMachine`, `:TestExhibitedMachineOf`; `repl/send_test.go` (`TestSendDrivesAnAcceptTransition` through `TestSendIsInHelpAndCompletion`, `TestStateOnAnObjectAttachesToItsRunningMachine`, `TestStateOnAnObjectStartsWhatItDoesNotRun`) | ✅ Faithful, **self-assessed** (the pinned reference has no prompt to inject a signal from, so nothing external adjudicates this) | | A message in flight is taken by one machine of the object it reaches: a machine whose guards would drop it leaves it for a sibling machine of the same object that would fire on or defer it, in attachment order, so a run and a single step route it alike; deciding a message beforehand is a probe that leaves nothing behind — no budget spent, no behavior started, no object, variant selection or feature value materialized by a guard kept | `state_executor.go` `takesMessage`, `yieldsTo`, `siblingsAccepting`, `Decide`; `classifier_behavior.go` `abandonInstancesSince`, `forgetVariantsNaming`, `forgetValuesNaming`; `signal.go` `TakeMessage` | `runtime/signal_injection_test.go:TestSignalGoesToTheSiblingMachineThatFiresOnIt`, `:TestDecideLeavesNoVariationSelectionAGuardMaterializes`; `repl/send_test.go:TestSendReachesTheMachineWhoseGuardLetsItThrough` | ✅ Faithful, **self-assessed** (the pinned reference runs one machine per test, so nothing external adjudicates the choice among siblings) | | CallEvent triggers (`accept op(param)` notation, operation and argument matching, arguments bound for guard/effect) | `parser/behavior.go` parseTriggerEvent/parseCallEvent; `symbols/bodyscopes.go` newTriggerScope (parameters visible to the transition's own guard/effect); `state_executor.go` matchesEvent EventCall case, bindTriggerArguments, InvokeOperation | `parser/testdata/parse/state_call_trigger.golden`, `lower/trigger_test.go:TestTriggerClassification_CallTrigger`, `model/behavior_body_resolve_test.go` call-trigger parameter cases, `state_call_trigger{,_guard,_nested,_regions}.sysml` conformance, `signal_test.go:TestCallEventMatchesOperationName`, `:TestRejectedCallLeavesNoArgumentsBehind`, `robustness_test.go:call_of_unhandled_operation`, `:call_argument_of_wrong_type` | ✅ Faithful (a call trigger on an enclosing composite state sees the invocation while a substate is active) | -| Sourceless transitions (`accept … then`, `if … then`, `transition if … then`, `transition then`) — SysML v2 7.17.3 `TargetTransitionUsage`, whose source is the state that owns it | `parser/behavior.go` `parseStateBody` dispatches `if` and a source-less `transition` clause to `parseAcceptTransition`; `lower/state_graph.go` `lowerTransitionMember` takes the containing state as the source | `parser/behavior_test.go` `TestParseStateBody_SourcelessTransitionForms`, golden `state_target_transition_guard.sysml` (accepted clean by the pinned pilot), `accept_then_transition.sysml` | ✅ Faithful (nested form only; flat form errors intentionally) | +| Sourceless transitions (`accept … then`, `if … then`, `then`, `transition if … then`, `transition then`) — SysML v2 §7.18.3 `TargetTransitionUsage`: a transition usage written without a source part, whose source "is taken to be the closest lexically previous state usage" in the body that declares it, so it is a member of the body that declares the state it leaves, written after that state, at any depth (a state def body, an exhibited or performed state usage body, a composite state's body, an orthogonal region's body); the pilot's `UsageUtil.getPreviousFeature` derives it the same way, looking back over the other transitions chained off that state | `ast/transition_source.go` `ImplicitTransitionSource` (the previous-member rule over the complete ordered body, looking past the sourceless transitions chained off the same state and the succession `then state s;` lists after `s`); `lower/transition_source.go` `ImplicitSource`, `IsEntryTransition`, the typed `ErrNoTransitionSource`, `TransitionSourceError` and `ErrEntryTransitionUnsupported`; `lower/state_graph.go` `lowerTransitionMember` lowers the shorthand from the vertex the rule names, over the inherited and own members `lower/state_inheritance.go` materialises with their owner and scope; `passes/state_transition.go` `(*transitionChecker).checkImplicitSource` reports the same rule at the constraint tier | `parser/behavior_test.go` `TestParseStateBody_SourcelessTransitionForms`, goldens `state_target_transition_guard.sysml` and `state_target_transition_placements.sysml` (top-level, composite, orthogonal-region placements with trigger, guard, effect and dotted targets, each `source=""`; both accepted clean by the pinned pilot), `lower/transition_source_test.go` (`TestToStateGraph_SourcelessTransitionLeavesThePrecedingState`, `:…InheritedSourcelessTransitionLeavesEachMaterialization`, `:…SourcelessTransitionWithNothingBefore`, `:…SourcelessTransitionAfterANonVertex`, `:…SourcelessTransitionAfterARegion`, `:…GuardedEntryTransitionIsUnsupported`), `passes/state_transition_test.go:TestSourcelessAcceptTransitionIsLegal`, `:TestSourcelessTransitionChainAndSuccessionAreLegal`, `:TestSourcelessTransitionWithNothingBeforeIsReported`, `:TestSourcelessTransitionAfterANonVertexIsReported`, `:TestSourcelessTransitionAfterARegionIsReported`, `:TestGuardedEntryTransitionIsLegal`, conformance `accept_then_transition.sysml`, `state_target_transition_top_level_timed.sysml` (+ trace golden), `state_target_transition_nested_timed.sysml` (+ trace golden: one firing, one entry action, no self-loop), `state_target_transition_guard.sysml`, `state_target_transition_after_do_action.sysml`, `robustness_test.go:sourceless_transition_with_nothing_before`, `:sourceless_transition_after_a_non_state`, `:guarded_entry_transition_is_not_lowered` | ✅ Faithful (the earlier reading — the shorthand written *inside* the state it leaves, with that containing state as its source, and refused at the machine's top level — was wrong: the pinned pilot rejects the nested placement with parse errors (`no viable alternative at input 'accept'`), and accepts the flat placement this implementation now lowers, so `accept_then_transition.sysml` was rewritten into the flat form. A shorthand written first in its body, or after a member that is not a state of this machine — an entry action with a trigger, a `do` action, an attribute, a succession, documentation, a region of a parallel state — is reported by the constraint tier with the member named, and the lowering keeps the same typed errors as a backstop; the pilot rejects each of those placements too, by its grammar or by `A transition with an accepter must have a state as its source`. **Known limitation:** the guarded entry transition of §7.18.3 (`entry; if c then off; if not c then on;`, `EntryTransitionMember`), which chooses the starting state by guard, is accepted by validation as the pilot accepts it but is not lowered yet: the state executor reports `ErrEntryTransitionUnsupported` naming the `entry; then s;` form to use) | | ChangeEvent triggers (when expr) | `state_executor.go` matchesEvent, RunToCompletion (polls after each micro-step and again at quiescence); `state_change_trigger.go` pollChangeEvents, SuspendReason | `state_executor_test.go:TestStateChangeEvent`, `state_change_trigger_test.go:TestChangeTriggerRunsWithoutAnExternalPoll`, `:TestChangeTriggerFiresOnRiseFromDoBehavior`, `:TestChangeTriggerDoesNotRefireUnchangedCondition`, `:TestChangeTriggerFalseConditionIsReported`, `conformance/state_change_trigger_autonomous.sysml`, `:state_change_trigger_rising_edge.sysml`, `:state_change_trigger_event_order.sysml` + trace golden | ⚠️ Approximate (driven by the run itself and fired on the condition rising; KerML has no clock, so re-testing once per micro-step is a tool-defined cadence — see the known limitation) | -| TimeEvent triggers (`accept after ` relative, `accept at