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/.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/CHANGELOG.md b/CHANGELOG.md index 7febd89b1..be771a52d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,7 +7,7 @@ release is described in [docs/project/releasing.md](docs/project/releasing.md). ## Unreleased -## 0.7.0 — 2026-09-09 +## 0.7.0 — 2026-09-10 ### Added @@ -213,6 +213,18 @@ release is described in [docs/project/releasing.md](docs/project/releasing.md). - **A worked walkthrough of analysis cases, `examples/analysis-demo`.** One lander model asked every way the tool answers: an analysis whose action steps feed each other and whose objective is a requirement, run bound, with arguments and on an object; a verification case whose body verdict is reported beside its objective; a parameter sweep and a seeded sample; two trade studies choosing among three landers, one swept over its cost parameter; and an action and a state machine due at the same instant of the shared clock, run under the default and `declared` scheduling policies and under `explore`. Each command is shown with its output and what to read in it, with `-trace` and `-json`, the REPL forms and the same questions asked through the Python client in `lander_demo.py`. +- **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. + +- **A design note for SMT bounded model checking of behaviors** + (`docs/internals/design/smt-model-checking.md`). It proposes unrolling an action's token flow + to a bounded number of moves and asking the SMT solver whether any schedule, for any value of + the inputs the model leaves unbound, violates a requirement, deadlocks or leaves a feature's + final value depending on the order of two moves. It fixes what a verdict may claim — proved + within a stated bound, violated with a witness the interpreter replays, sensitive with the two + schedules, or not covered with the reason — a per-construct coverage table, the referee gate + against `-schedule explore`, and the stages. Nothing is implemented; the note exists to be + reviewed before code is written. + ### Changed - **What may differ from 0.6.0.** A model that mixes actions and state machines can take another @@ -251,6 +263,8 @@ release is described in [docs/project/releasing.md](docs/project/releasing.md). `release/x.y.z` pull requests and are tagged there, and CircleCI builds and tests both branches. `make proto-breaking` compares against `origin/develop` by default. +- **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`. + ### Fixed - **A transition's `accept` with no `via` no longer takes a transfer addressed to a port.** An accept naming no port receives as the performer of the machine (SysML v2 §7.16.7), and a port is a sub-occurrence of its part, not the part, so `send new Ping() to alpha.inPort` — or a send routed to `inPort` over a connector — is now taken only by `accept Ping via inPort`; a via-less `accept Ping` on the same state is not enabled by it and no choice point is reported between the two. A transfer addressed to the part itself, `send new Ping() to alpha`, is still taken by the via-less accept and not by the `via` one. The state executor now judges every message by the same rule its dispatch check and the action executor already applied, so the two agree on what a machine can react to; call and change triggers are unaffected. @@ -288,6 +302,29 @@ release is described in [docs/project/releasing.md](docs/project/releasing.md). - **Tests that could not fail now test what they name.** A Java test that compared a `SetValue` with a `Sequence` through `assertNotEquals`, which no two such values could ever satisfy, now asserts that the order of a sequence tells it apart from a set through `sameValue`; two Python assertions that compared an expression with itself now compare independently built measurement references. The Java exactness test also pins whole scales beyond a `long`. - **The SonarCloud findings outside cognitive complexity are cleared again.** Duplicated Go literals are named constants, intentional no-op closures state their contract, a negated comparison is written directly, an underscore-suffixed local is renamed, unnecessary locals are inlined, the Java transport tells a connect timeout from a read timeout in one catch block, `exactBaseMagnitude` returns an empty array instead of `null`, `valueHash` lives in `SetValue`, and the Java and Python tests hold one call per exception assertion, one property per assertion, fewer than 25 assertions per method and a single argument order. No behavior changes. +- **`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. + A performed action paused on the clock is among the tokens an exploring step picks from once + its wait has ended, so a sibling accept due at the same instant no longer always runs first: + `action_explore_performed_and_accept_due_together` reaches both writes, six linearizations. + +- **Sweep and sample values are typed by the parameter they bind, not by the literals of the range.** `-sweep`, `-samples`, `%sweep`, `%samples` and `RunSweep` resolve each range against the parameter's declaration: a `Real` or `Rational` parameter swept over `1..4:1` is bound to `1.0`, `2.0`, `3.0`, `4.0` and the table shows them so, and sampled over `1..4` draws reals in `[1, 4)` rather than the four Integers; an `Integer`, `Natural` or `Positive` parameter — or an `attribute def` specializing one — swept over `1.0..3.0:1.0` is bound to the Integers `1`, `2`, `3`, and sampled over `1.0..4.0` draws Integers inclusively. A fractional endpoint or step over an Integer parameter (`1.0..3.0:0.5`, `1.5..3`), a value below what a `Natural` or `Positive` holds, and a range over a `Boolean`, `String`, enumeration or non-scalar parameter are refused before any run, naming the parameter and its type, where before half the rows failed one by one. A quantity-typed parameter is typed through its `num` — refusing a magnitude a `num : Natural` or `num : Positive` cannot hold, and any range where the `num` holds no number — and keeps the first endpoint's unit; a `Number`-typed parameter and one declaring no type take the range as written, the untyped one noted under the table. A range between whole numbers needs no step whatever the parameter's type — `0.0..1.0` over a `Real` steps by one — while a range with a fractional endpoint still needs `:`. A range read as reals takes an Integer endpoint or step only where a Real holds it without rounding, and steps only where the reals tell its rows apart, so a `Real` parameter swept from 2⁶⁰ to 2⁶⁰+3 is refused rather than collapsed onto one row. + +- **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, a `choice` or `join` pseudostate, an orthogonal region — is reported by validation with the member named; a pseudostate is left by `transition first … then …;` only. +- **The guarded entry transition (`entry; if cold then heating; if not cold then idle;`, SysML v2 §7.18.3 `EntryTransitionMember`) now chooses the state a body starts in.** The transitions out of a body's entry action are lowered in declaration order and tried in that order each time the body is entered — when the machine starts and whenever a transition enters the composite state whose body it is — after the entry action itself has run; the first whose guard holds is entered, an unguarded `then s;` among them is taken when reached, and when none holds the machine reports `no entry transition holds` rather than starting somewhere. A body's entry transitions are tried inside a composite state, an orthogonal region and an exhibited state alike, and a transition into a composite state now starts that state's body by its entry transition rather than leaving it without an active substate. A state usage typed by a definition that writes entry transitions of its own starts by those alone, replacing the inherited ones as its own entry behavior does, instead of starting where the definition's came first. An entry transition written with a trigger or an effect, or reaching something other than a state, is reported by validation and by lowering, as the OMG pilot rejects those shapes. +- **The state rendering now draws a body's entry transitions and marks only an unconditional start as `initial`.** For `entry; if cold then heating; if not cold then idle;` the text, Mermaid and LSP renderings labelled both `heating` and `idle` `(initial)` and the diagram drew a start arrow into each, though the machine enters only the first alternative whose guard holds, and the guards appeared nowhere. Each body that says where it starts — the machine, a composite state, an orthogonal region — now has a `start` node whose edges are its entry transitions in the order the guards are tried in, carrying the guard as `[cold]` like any transition edge (`[*] --> heating : [cold]` in Mermaid); the `initial` detail is kept for the target of a body's first entry transition when that one is unguarded, so a state reached only through a guarded alternative is no longer `initial`. +- **A state machine's own `entry`, `do` and `exit` behaviors now run for every machine.** They were skipped unless the machine had orthogonal regions of its own, so `state def M { entry assign started := true; then idle; … }` never assigned; the entry behavior now runs before the start state is chosen, and the exit behavior once a transition to `done` has completed the machine. + +- **A verification case's objective checks the case's subject, not its verdict.** The library binds it so — `VerificationCases::VerificationCase::obj` redefines `Cases::Case::obj` with `subject subj = VerificationCase::subj` — but the runtime applied the redefined objective's `default Case::result` to every case kind, so an objective typed by a requirement with a typed subject (`subject lander : Lander`) was `undecided` with `type mismatch: VerdictKind::pass (enumeration literal) is not a Lander`, and a sweep over such a case printed `undecided` in every row. An unbound objective subject now holds the value the library states for it, read through the redefinition chain: an analysis case's objective still defaults to the result, a verification case's evaluates the requirement against the verification subject whatever the requirement names it, and the objective is decided on `-analysis`, `-requirement`, `-satisfy`, the REPL and gRPC alike. A requirement subject the verification subject cannot be is `undecided` naming both types, and a usage restating the library's `=` binding is still refused. + ### Performance - **Loading a model no longer merges the library's visible member set once per declaration.** The inherited-name conflict rule looks each name up in the memoized member maps of a declaration's library bases and passed-through types instead of copying them into a fresh map per part, attribute, action and state; its diagnostics are unchanged. The OOSEM method rule memoizes a type's classification, so an attribute type shared by many features is conformance-checked once. Loading and validating a 4 000-element model is 15% faster and allocates a third fewer bytes than before; `sysml -validate` on 3 000–12 000-element models is now at or ahead of release 0.4.2. `docs/project/performance-release-0.6-vs-0.4.2.md` records the comparison, the remaining costs of the validation rules added since 0.4.2, and how to repeat it. The Apollo 11 load figure on the landing page and in `docs/internals/performance.md` is re-measured at 0.43 s: the earlier 0.37 s was taken while the model's three calculation-arity findings were still errors, before the higher validation tiers ran. diff --git a/README.md b/README.md index d0c494481..04c102f94 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/api/proto/sysml.pb.go b/api/proto/sysml.pb.go index a1930d175..9e86a5a1f 100644 --- a/api/proto/sysml.pb.go +++ b/api/proto/sysml.pb.go @@ -6230,9 +6230,10 @@ func (x *QueryResultElement) GetProperties() map[string]string { } // SweepRange is one parameter's range: the endpoints a swept run advances -// between and the step it advances by. A sampled range states no step; a swept -// range between Integers steps by one where it states none, and one between -// reals must state one. +// between and the step it advances by, typed by the parameter it binds rather +// than by how they are written. A sampled range states no step; a swept range +// between whole numbers steps by one where it states none, and one with a +// fractional endpoint must state one. type SweepRange struct { state protoimpl.MessageState `protogen:"open.v1"` // Name of the input parameter the range binds, which the target must declare diff --git a/api/proto/sysml.proto b/api/proto/sysml.proto index 6b1d0ef60..8c3bf42be 100644 --- a/api/proto/sysml.proto +++ b/api/proto/sysml.proto @@ -1175,9 +1175,10 @@ message QueryResultElement { } // SweepRange is one parameter's range: the endpoints a swept run advances -// between and the step it advances by. A sampled range states no step; a swept -// range between Integers steps by one where it states none, and one between -// reals must state one. +// between and the step it advances by, typed by the parameter it binds rather +// than by how they are written. A sampled range states no step; a swept range +// between whole numbers steps by one where it states none, and one with a +// fractional endpoint must state one. message SweepRange { // Name of the input parameter the range binds, which the target must declare // and the request's own arguments must not bind. diff --git a/clients/java/opensysml-client/src/main/java/org/openmbee/opensysml/proto/SweepRange.java b/clients/java/opensysml-client/src/main/java/org/openmbee/opensysml/proto/SweepRange.java index 4f420968a..e01584f52 100644 --- a/clients/java/opensysml-client/src/main/java/org/openmbee/opensysml/proto/SweepRange.java +++ b/clients/java/opensysml-client/src/main/java/org/openmbee/opensysml/proto/SweepRange.java @@ -8,9 +8,10 @@ /** * 
  * SweepRange is one parameter's range: the endpoints a swept run advances
- * between and the step it advances by. A sampled range states no step; a swept
- * range between Integers steps by one where it states none, and one between
- * reals must state one.
+ * between and the step it advances by, typed by the parameter it binds rather
+ * than by how they are written. A sampled range states no step; a swept range
+ * between whole numbers steps by one where it states none, and one with a
+ * fractional endpoint must state one.
  *
* * Protobuf type {@code sysml.SweepRange} @@ -401,9 +402,10 @@ protected Builder newBuilderForType( /** * 
    * SweepRange is one parameter's range: the endpoints a swept run advances
-   * between and the step it advances by. A sampled range states no step; a swept
-   * range between Integers steps by one where it states none, and one between
-   * reals must state one.
+   * between and the step it advances by, typed by the parameter it binds rather
+   * than by how they are written. A sampled range states no step; a swept range
+   * between whole numbers steps by one where it states none, and one with a
+   * fractional endpoint must state one.
    *
* * Protobuf type {@code sysml.SweepRange} diff --git a/clients/node/src/generated/sysml_pb.ts b/clients/node/src/generated/sysml_pb.ts index 49a6367ef..c3f0ccdaf 100644 --- a/clients/node/src/generated/sysml_pb.ts +++ b/clients/node/src/generated/sysml_pb.ts @@ -3301,9 +3301,10 @@ export const QueryResultElementSchema: GenMessage = /*@__PUR /** * SweepRange is one parameter's range: the endpoints a swept run advances - * between and the step it advances by. A sampled range states no step; a swept - * range between Integers steps by one where it states none, and one between - * reals must state one. + * between and the step it advances by, typed by the parameter it binds rather + * than by how they are written. A sampled range states no step; a swept range + * between whole numbers steps by one where it states none, and one with a + * fractional endpoint must state one. * * @generated from message sysml.SweepRange */ diff --git a/clients/python/opensysml/connection.py b/clients/python/opensysml/connection.py index 85c398ac8..9a87fef1d 100644 --- a/clients/python/opensysml/connection.py +++ b/clients/python/opensysml/connection.py @@ -1785,8 +1785,9 @@ def run_sweep(self, symbol_id, model_hash, ranges, subject=None, model_hash (str): Hash from ParseFile response ranges (dict): Range per swept parameter, as ``{"speed": (0, 10, 2)}`` or ``{"speed": (0.0, 10.0)}`` where - the rows are drawn; a range between Integers steps by one where - it states no step, one between reals must state one + the rows are drawn; a range between whole numbers steps by one + where it states no step, one with a fractional endpoint must + state one; the values are typed by the parameter they bind subject (str, optional): FQN of a part/usage to instantiate and run an analysis case on arguments (list, optional): Positional arguments every row binds diff --git a/clients/python/tests/test_sweep_integration.py b/clients/python/tests/test_sweep_integration.py index 4ee49284a..236291eff 100644 --- a/clients/python/tests/test_sweep_integration.py +++ b/clients/python/tests/test_sweep_integration.py @@ -145,10 +145,18 @@ def test_a_parameter_both_bound_and_swept_raises(self): "Sw::Twice", {"n": (1, 2)}, named_arguments={"n": 3} ) - def test_a_real_range_without_a_step_raises(self): + def test_a_real_range_between_whole_numbers_steps_by_one(self): + table = self.model.run_sweep( + "Sw::Ratio", {"b": (1.0, 2.0)}, named_arguments={"a": 1.0} + ) + assert [row.inputs["b"] for row in table] == [1.0, 2.0] + assert all(isinstance(row.inputs["b"], float) for row in table) + assert [row.outputs["result"] for row in table] == [1.0, 0.5] + + def test_a_range_with_a_fractional_endpoint_and_no_step_raises(self): with pytest.raises(ExecutionError) as exc_info: self.model.run_sweep( - "Sw::Ratio", {"b": (1.0, 2.0)}, named_arguments={"a": 1.0} + "Sw::Ratio", {"b": (1.0, 2.5)}, named_arguments={"a": 1.0} ) assert "step" in str(exc_info.value) diff --git a/clients/rust/conformance/sysml.descriptor.binpb b/clients/rust/conformance/sysml.descriptor.binpb index 230345690..301958b6d 100644 Binary files a/clients/rust/conformance/sysml.descriptor.binpb and b/clients/rust/conformance/sysml.descriptor.binpb differ diff --git a/clients/rust/opensysml/src/proto/sysml/sysml.rs b/clients/rust/opensysml/src/proto/sysml/sysml.rs index 62e25fae4..737480e9d 100644 --- a/clients/rust/opensysml/src/proto/sysml/sysml.rs +++ b/clients/rust/opensysml/src/proto/sysml/sysml.rs @@ -1442,9 +1442,10 @@ pub struct QueryResultElement { pub properties: ::std::collections::HashMap<::prost::alloc::string::String, ::prost::alloc::string::String>, } /// SweepRange is one parameter's range: the endpoints a swept run advances -/// between and the step it advances by. A sampled range states no step; a swept -/// range between Integers steps by one where it states none, and one between -/// reals must state one. +/// between and the step it advances by, typed by the parameter it binds rather +/// than by how they are written. A sampled range states no step; a swept range +/// between whole numbers steps by one where it states none, and one with a +/// fractional endpoint must state one. #[derive(Clone, PartialEq, ::prost::Message)] pub struct SweepRange { /// Name of the input parameter the range binds, which the target must declare 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/sweep_test.go b/cmd/sysml/sweep_test.go index 0065b14b5..3f649ba9c 100644 --- a/cmd/sysml/sweep_test.go +++ b/cmd/sysml/sweep_test.go @@ -15,6 +15,7 @@ const sweepCLIModel = `package Sw { calc def Twice { in n : Integer; return : Integer = n * 2; } calc def Ratio { in a : Real; in b : Real; return : Real = a / b; } calc def Lift { in 'launch mass' : Integer; return : Integer = 'launch mass' * 2; } + calc def Toggle { in on : Boolean; return : Boolean = not on; } part def Ship { attribute cost : Real = 5.0; } analysis def Priced { subject s : Ship; @@ -62,6 +63,72 @@ func TestSweepThroughCLI(t *testing.T) { } } +// TestSweepBindsInTheParameterTypeThroughCLI checks a range is typed by the +// parameter it sweeps, not by its literals: Integer literals over a Real +// parameter bind and print as Reals, real literals over an Integer parameter +// bind and print as Integers, and a Real parameter samples reals. +func TestSweepBindsInTheParameterTypeThroughCLI(t *testing.T) { + binary := buildCLI(t) + + got := check(t, binary, sweepCLIModel, "-calc", "Sw::Ratio(b = 2.0)", "-sweep", "a=1..4:1") + if got.status != 0 { + t.Fatalf("exit status = %d, want 0\n%s", got.status, got.output()) + } + want := strings.Join([]string{ + "a | result | time", + "-+-+-", + "1.0 | 0.5 |