diff --git a/.agents/skills/testing-pilot-corpora-gate/SKILL.md b/.agents/skills/testing-pilot-corpora-gate/SKILL.md index 55b36e21a7..1bbe6831e3 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 -C tools ./cmd/pilot-diff` (validators pre-downloaded; ~4min, prints e.g. -the headline the committed baseline holds — `380 file(s), 345 fully agreeing; 38 agreed -diagnostic(s), 40 only ours, 1616 only the pilot's` at the `2026-08` pin, so read it from +the headline the committed baseline holds — `381 file(s), 345 fully agreeing; 38 agreed +diagnostic(s), 41 only ours, 1629 only the pilot's` at the `2026-08` pin, 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 e870ccd909..d9894c2719 100644 --- a/.agents/skills/testing-pilot-differential/SKILL.md +++ b/.agents/skills/testing-pilot-differential/SKILL.md @@ -23,8 +23,8 @@ GNU-format diagnostics **relative to `--root`**. Consequences for testing: - `-validator /nonexistent` now says `run ./scripts/download-pilot-sysml-validator.sh`. - Measured at the `2026-08` pin after bare parameters took their effective range `[0..*]`, removing the adjudicated `Behaviors.kerml:14` multiplicity warning (the `[1]` `RocketEquation` inputs keep - its warning at `delta-v-budget.sysml:93`): `380 file(s), 345 fully agreeing; 38 agreed, 40 only - ours, 1616 only the pilot's`, JSON totals `openSysMLDiagnostics 80 / pilotDiagnostics 1656 / + its warning at `delta-v-budget.sysml:93`): `381 file(s), 345 fully agreeing; 38 agreed, 41 only + ours, 1629 only the pilot's`, JSON totals `openSysMLDiagnostics 81 / pilotDiagnostics 1669 / severityMismatch 2`; ~2 min wall, byte-identical across runs *and* after a from-scratch rebuild of `build/pilot-validator`. The six `kerml-examples` pilot-only rows the `2026-07` run carried (`The opposite features 'owningType' … do not refer to each other`) are gone: the pilot fixed its @@ -142,8 +142,8 @@ committed result of the *last refreshed* run, so **the harness is testable by re but only while the baseline is current. Check that first. The latest rebaseline, after bare parameters took their effective range `[0..*]` and removed the adjudicated `Behaviors.kerml:14` warning (the `[1]` `RocketEquation` inputs still produce the warning at -`delta-v-budget.sysml:93`), is current: a live run gives `380 file(s), 345 fully agreeing; 38 -agreed, 40 only ours, 1616 only the pilot's`, byte-identical to the committed baseline, and +`delta-v-budget.sysml:93`), is current: a live run gives `381 file(s), 345 fully agreeing; 38 +agreed, 41 only ours, 1629 only the pilot's`, byte-identical to the committed baseline, and `docs/project/pilot-differential.md`'s "Results" table matches. The prior rebaseline, when the Legend of the Red Dragon example left for its own repository, gave `380 file(s), 344 fully agreeing; 38 agreed, 42 only ours, 1614 only the pilot's`. diff --git a/.agents/skills/testing-pilot-execution-referee/SKILL.md b/.agents/skills/testing-pilot-execution-referee/SKILL.md index 359678f6fd..c9ed4fa961 100644 --- a/.agents/skills/testing-pilot-execution-referee/SKILL.md +++ b/.agents/skills/testing-pilot-execution-referee/SKILL.md @@ -148,8 +148,8 @@ pilot answers the representation's own. See `pilot-exec-diff: :: model no/such/model.sysml: stat : no such file or directory`. - **Additivity.** `go run -C tools ./cmd/pilot-diff` must still print the headline the - committed baseline holds (`380 file(s), 345 fully agreeing; 38 agreed - diagnostic(s), 40 only ours, 1616 only the pilot's` at the `2026-08` pin — read it from the baseline JSON, not from this line, since each + committed baseline holds (`381 file(s), 345 fully agreeing; 38 agreed + diagnostic(s), 41 only ours, 1629 only the pilot's` at the `2026-08` pin — 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 2f701e6320..76e414ba43 100644 --- a/.agents/skills/testing-pilot-xpect/SKILL.md +++ b/.agents/skills/testing-pilot-xpect/SKILL.md @@ -423,8 +423,8 @@ census in `w5c_census_test.go` is live two ways: perturb one pinned triple (e.g. ## Regression neighbour `go run -C tools ./cmd/pilot-diff` (~1m12s) must still print the headline the *committed* baseline holds — -at the `2026-08` pin that is `380 file(s), 345 fully agreeing; 38 agreed diagnostic(s), 40 -only ours, 1616 only the pilot's`. Read the number out of +at the `2026-08` pin that is `381 file(s), 345 fully agreeing; 38 agreed diagnostic(s), 41 +only ours, 1629 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 1fdb4509ae..3266471e1f 100644 --- a/README.md +++ b/README.md @@ -312,11 +312,11 @@ The project is under active development, with the core infrastructure operationa **Measured against the pinned reference** (`PILOT_TAG=2026-08`, artifact `0.62.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:** 345 of 380 files agree diagnostic-by-diagnostic; 40 diagnostics are ours alone and 1616 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 -C tools ./cmd/pilot-diff`). +- **Corpus agreement:** 345 of 381 files agree diagnostic-by-diagnostic; 41 diagnostics are ours alone and 1629 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 -C tools ./cmd/pilot-diff`). - **Declared-diagnostic silence:** of the 512 declared `errors` rows in the reference's own Xpect suites, we report nothing for 0. 245 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 -C tools ./cmd/pilot-xpect`). - **Scope agreement:** 230 of 230 declared scope assertions match exactly (same source). - **Permissiveness gaps:** of 311 invalid models we wrote ourselves, the reference rejects 2 that we accept by default, and 300 both reject; 2 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 -C tools ./cmd/pilot-reject`). -- **Declared errata:** the registry declares 12 defect(s) in the published reference material — 4 with a specification-derived correction, 8 documented without one, since no intended reading can be inferred ([OMG issues](docs/project/omg-issues.md), `tools/oracle/errata`). Every figure above is as published and stays the conformance statement; running the same oracles over the corrected text instead reports 346 of 380 files agreeing, 39 diagnostics ours alone and 1616 the reference's alone, 0 declared rows we are silent on, and 0 of 311 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 12 defect(s) in the published reference material — 4 with a specification-derived correction, 8 documented without one, since no intended reading can be inferred ([OMG issues](docs/project/omg-issues.md), `tools/oracle/errata`). Every figure above is as published and stays the conformance statement; running the same oracles over the corrected text instead reports 346 of 381 files agreeing, 40 diagnostics ours alone and 1629 the reference's alone, 0 declared rows we are silent on, and 0 of 311 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. @@ -328,7 +328,7 @@ What these numbers cannot show: the OMG corpora are demonstrations rather than a **Test coverage:** top-level `Test` functions (counted from the `_test.go` files, as `go test ./...` runs them) covering parsers, semantics, runtime (actions, states, instances, operators, validation), behind golden ASTs, negatives, execution conformance cases, golden traces, runtime robustness cases and gRPC conformance and robustness cases. The figures are counted from the tree when the documentation site is built into the test inventory of [spec compliance](docs/project/spec-compliance.md), never committed, so a branch adding a test does not rewrite this page. A test skips only for want of something the run did not provide, and says what: the held-image round trip declines a conformance case that creates no instance, a few gate on a PDF or Mermaid toolchain, a pinned pilot artifact, the PSSM suite, a locale, a case-insensitive filesystem or a live Flexo stack, and the OMG corpus gates skip until the corpora are downloaded unless asked to fail. **Parser coverage:** 105/105 bundled library files parse cleanly — the 94 official SysML v2 standard library files and the non-normative `OpenSysML Libraries/OpenSysMLMathFunctions.kerml`, `OpenSysML Libraries/DocumentQueries.sysml`, `OpenSysML Libraries/IdentityMetadata.sysml`, `OpenSysML Libraries/DiagramLayout.sysml`, `OpenSysML Libraries/OOSEM.sysml`, `OpenSysML Libraries/MOSA.sysml`, `OpenSysML Libraries/StateSpaceIntegration.sysml`, `OpenSysML Libraries/Stochastic.sysml`, `OpenSysML Libraries/RandomFunctions.kerml`, `OpenSysML Libraries/Simulation.sysml` and `OpenSysML Libraries/MigrationMetadata.sysml` extensions. Conformance verified by [stdlib_conformance_test.go](internal/workspace/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 (every conformance case 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:** 380 files compared diagnostic-by-diagnostic against the pinned OMG pilot implementation (`2026-08`), 345 in full agreement; every divergence is enumerated and adjudicated in [the differential](docs/project/pilot-differential.md), reproducible with `go run -C tools ./cmd/pilot-diff`. +**Reference differential:** 381 files compared diagnostic-by-diagnostic against the pinned OMG pilot implementation (`2026-08`), 345 in full agreement; every divergence is enumerated and adjudicated in [the differential](docs/project/pilot-differential.md), reproducible with `go run -C tools ./cmd/pilot-diff`. **Rejection oracle:** the reverse direction — do we reject what the reference rejects? 311 hand-written invalid models validated by both implementations, 302 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 -C tools ./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 `tests/corpus/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/changes/unreleased/deferred-keeper-marker.added.md b/changes/unreleased/deferred-keeper-marker.added.md new file mode 100644 index 0000000000..39413f00d3 --- /dev/null +++ b/changes/unreleased/deferred-keeper-marker.added.md @@ -0,0 +1,2 @@ +- **`MigrationMetadata::DeferredKeeper` marks the keeping accept of a deferred signal.** The SysML v1 migrator and the PSSM referee write the accept of each keeping loop of the standard deferred-signal encoding as `#MigrationMetadata::DeferredKeeper action receive accept kept : Sig;`, so the accept that keeps the signal for the state is declared rather than recognized by its shape. An accept node takes prefix metadata like any other usage (`#M action a accept e : E;`), as the grammar's `PrefixMetadataMember` allows. +- **The `deferred-keeper-unmarked` lint reports a keeping loop written without the marker.** An accept of a deferred signal at the root of the do action of a state annotated `MigrationMetadata::DeferredEvent` where no accept of that signal carries `MigrationMetadata::DeferredKeeper` — the shape the migrator wrote before the marker existed, not an ordinary consumer written beside a marked keeper — is reported as a warning in every mode, since the runtime now runs it as an ordinary accept that consumes the occurrence rather than keeping it; the model still analyses and runs, and re-migrating it or writing the marker on the accept clears the warning. The annotations are known by their resolved type, however the model spells them. The lint is switched off like the others, by its code. diff --git a/changes/unreleased/deferred-keeper-marker.fixed.md b/changes/unreleased/deferred-keeper-marker.fixed.md new file mode 100644 index 0000000000..7ea185a74c --- /dev/null +++ b/changes/unreleased/deferred-keeper-marker.fixed.md @@ -0,0 +1 @@ +- **An accept of a deferred signal written beside the keeping loop takes the occurrence first.** The runtime identified the keeping accept of a deferring state's do action by its position and signal, so an ordinary accept of the same signal declared at the do action's own level counted as a second keeper, and an occurrence arriving while both were parked could be kept instead of taken, depending on the schedule. The keeping accept is now the one the `MigrationMetadata::DeferredKeeper` annotation marks, lowered by resolved type into the action graph; every other accept is an ordinary consumer the keeper yields to whenever it can take the occurrence that step. diff --git a/cmd/sysml/usage.go b/cmd/sysml/usage.go index 0cd8d1fbca..7e046da5c3 100644 --- a/cmd/sysml/usage.go +++ b/cmd/sysml/usage.go @@ -596,7 +596,7 @@ func registerFlags(fs *flag.FlagSet) { fs.StringVar(&queryText, "query", "", "Evaluate this OSLC Query text against the model and exit") fs.Var(&modelChecks.validate, "validate", "Report the model's diagnostics and exit, nonzero on an error; -validate= checks instead every assertion about that object (repeatable)") - fs.Var(&disabledLints, "disable-lint", "Leave this lint out of the model's diagnostics: undeclared-signal or port-type-mismatch, comma-separated or repeated") + fs.Var(&disabledLints, "disable-lint", "Leave this lint out of the model's diagnostics: undeclared-signal, port-type-mismatch or deferred-keeper-unmarked, comma-separated or repeated") fs.BoolVar(&noRecordCache, "no-record-cache", false, "Parse every file loaded and hold it loaded, reading no interface record from the record cache and writing none; default off, or OPENSYSML_RECORD_CACHE=0") fs.BoolVar(&strictMode, "strict", false, "Judge the model as conforming SysML v2: notation no pinned production admits is an error, not a warning; a SysML v1 migration writes none of it") fs.Var(&modelChecks.constraints, "constraint", "Evaluate this constraint and exit (repeatable)") diff --git a/docs/guide/03-command-line.md b/docs/guide/03-command-line.md index 11091dd2a4..b1c481ed7d 100644 --- a/docs/guide/03-command-line.md +++ b/docs/guide/03-command-line.md @@ -261,10 +261,11 @@ each extension is measured against. The same setting is available as `%strict` a ## Lints -Two further warnings, `undeclared-signal` and `port-type-mismatch`, are *lints*: the model -is valid SysML v2, but a `when ` that no declaration or `send` -accounts for, or a connection between ports whose definitions are unrelated, is almost -always a slip. `-strict` leaves them warnings, since they are not about notation. +Three further warnings, `undeclared-signal`, `port-type-mismatch` and +`deferred-keeper-unmarked`, are *lints*: the model is valid SysML v2, but a `when ` that +no declaration or `send` accounts for, a connection between ports whose definitions are +unrelated, or a deferred signal's accept loop written without the `DeferredKeeper` marker that +names it as the keeper, is almost always a slip. `-strict` leaves them warnings, since they are not about notation. `-disable-lint ` switches one off (`%lint off` at the prompt, `disabledLints` in an editor); [the diagnostics reference](../reference/diagnostics.md) states exactly what each reports. diff --git a/docs/guide/11-migrating-from-sysml-v1.md b/docs/guide/11-migrating-from-sysml-v1.md index 603c20b49f..822b681d46 100644 --- a/docs/guide/11-migrating-from-sysml-v1.md +++ b/docs/guide/11-migrating-from-sysml-v1.md @@ -339,7 +339,9 @@ action fills from an accept loop while the state is active, substates included, action sends the kept occurrences back to the object once the state is left, so the state entered next takes them as if they had just arrived. The state is annotated `@MigrationMetadata::DeferredEvent { ref :>> signal : Sig; }` as well, so a reader sees what -was deferred without reading the encoding; the encoding and its rules are described under +was deferred without reading the encoding, and the loop's accept is marked +`#MigrationMetadata::DeferredKeeper`, which names it as the one keeping the signal rather than +consuming it; the encoding and its rules are described under [Deferred signals](../reference/sysml-v1-migration.md#deferred-signals). A transition out of the deferring state into a `choice` accepts the signal in both modes, since the pseudostate metadata spelling is written either way. diff --git a/docs/internals/architecture.md b/docs/internals/architecture.md index 7baf28783d..813dc68923 100644 --- a/docs/internals/architecture.md +++ b/docs/internals/architecture.md @@ -841,11 +841,11 @@ Every behavioral feature must have: **Measured against the pinned reference** (`PILOT_TAG=2026-08`, artifact `0.62.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:** 345 of 380 files agree diagnostic-by-diagnostic; 40 diagnostics are ours alone and 1616 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 -C tools ./cmd/pilot-diff`). +- **Corpus agreement:** 345 of 381 files agree diagnostic-by-diagnostic; 41 diagnostics are ours alone and 1629 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 -C tools ./cmd/pilot-diff`). - **Declared-diagnostic silence:** of the 512 declared `errors` rows in the reference's own Xpect suites, we report nothing for 0. 245 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 -C tools ./cmd/pilot-xpect`). - **Scope agreement:** 230 of 230 declared scope assertions match exactly (same source). - **Permissiveness gaps:** of 311 invalid models we wrote ourselves, the reference rejects 2 that we accept by default, and 300 both reject; 2 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 -C tools ./cmd/pilot-reject`). -- **Declared errata:** the registry declares 12 defect(s) in the published reference material — 4 with a specification-derived correction, 8 documented without one, since no intended reading can be inferred ([OMG issues](../project/omg-issues.md), `tools/oracle/errata`). Every figure above is as published and stays the conformance statement; running the same oracles over the corrected text instead reports 346 of 380 files agreeing, 39 diagnostics ours alone and 1616 the reference's alone, 0 declared rows we are silent on, and 0 of 311 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 12 defect(s) in the published reference material — 4 with a specification-derived correction, 8 documented without one, since no intended reading can be inferred ([OMG issues](../project/omg-issues.md), `tools/oracle/errata`). Every figure above is as published and stays the conformance statement; running the same oracles over the corrected text instead reports 346 of 381 files agreeing, 40 diagnostics ours alone and 1629 the reference's alone, 0 declared rows we are silent on, and 0 of 311 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/internals/design/precise-semantics-alignment.md b/docs/internals/design/precise-semantics-alignment.md index b94673b77d..925f9f3794 100644 --- a/docs/internals/design/precise-semantics-alignment.md +++ b/docs/internals/design/precise-semantics-alignment.md @@ -2048,7 +2048,7 @@ package Deferred001 { attribute deferred : Continue[*] ordered; do action buffer { first start then receive; - action receive accept kept : Continue; + #MigrationMetadata::DeferredKeeper action receive accept kept : Continue; then action keep { assign deferred := SequenceFunctions::including(deferred, receive.kept); } then receive; } diff --git a/docs/project/adjudications.md b/docs/project/adjudications.md index 39a0d1e6d7..a96474ed01 100644 --- a/docs/project/adjudications.md +++ b/docs/project/adjudications.md @@ -235,15 +235,18 @@ it, three ends typed by `BinaryInterface` do. **Pilot limitation** for the fixture that declares the rule universally. -### Two lints report models the specification accepts +### Three lints report models the specification accepts `undeclared-signal` reports a `when ` — an OpenSysML spelling — whose -name no visible declaration and no `send` in the workspace accounts for, and `port-type-mismatch` +name no visible declaration and no `send` in the workspace accounts for, `port-type-mismatch` reports a `connect`, interface usage or `flow` joining ports whose definitions are unrelated and -whose directed features are not conjugate (SysML v2 §7.12.2). Neither is a rule of the -specification, and the pilot reports neither, so both are **warnings in every mode**: `-strict` -promotes notation, and neither lint is about notation. Each has a code a surface can switch off -([diagnostics reference](../reference/diagnostics.md)), and neither fires on a model of the four OMG +whose directed features are not conjugate (SysML v2 §7.12.2), and `deferred-keeper-unmarked` +reports an accept of a deferred signal at the root of a `MigrationMetadata::DeferredEvent` +state's do action that the `MigrationMetadata::DeferredKeeper` marker does not name as the +keeping loop. None is a rule of the +specification, and the pilot reports none, so all are **warnings in every mode**: `-strict` +promotes notation, and no lint is about notation. Each has a code a surface can switch off +([diagnostics reference](../reference/diagnostics.md)), and none fires on a model of the four OMG corpora, the gate every new warning passes. --- diff --git a/docs/project/pilot-differential-baseline.json b/docs/project/pilot-differential-baseline.json index 2655ef78c7..81f0954ca4 100644 --- a/docs/project/pilot-differential-baseline.json +++ b/docs/project/pilot-differential-baseline.json @@ -53,15 +53,15 @@ "name": "testdata", "dir": "tests/testdata", "origin": "ours", - "files": 18, - "digest": "sha256:0bf9cc92df5634289ecb4d8a49016aeac48d637a69f4452ba27fb36ac2fb3152" + "files": 19, + "digest": "sha256:b77b1163db27281d114c44e6c28b23552681140ec1ac752e28cbbe64a3077fc4" }, { "name": "examples", "dir": "examples", "origin": "ours", "files": 45, - "digest": "sha256:3129c7cfdbf7b68313c1be401bc36bafd0db4f75bb1e9c5dcc55805f79063656" + "digest": "sha256:c5b573db17c7c8f47b9f0c9fd7574b1118b501141cc10832ee4cc55e2926e0d3" }, { "name": "probes", @@ -71,17 +71,17 @@ "digest": "sha256:b0153c55bbfcdacabab911725dc44e0e7f4d3a501a281b1f3f2a13cda19737c6" } ], - "recorded": "2026-10-01" + "recorded": "2026-10-02" }, "totals": { - "files": 380, + "files": 381, "filesFullyAgreeing": 345, "agreement": 38, "severityMismatch": 2, - "openSysMLOnly": 40, - "pilotOnly": 1616, - "openSysMLDiagnostics": 80, - "pilotDiagnostics": 1656 + "openSysMLOnly": 41, + "pilotOnly": 1629, + "openSysMLDiagnostics": 81, + "pilotDiagnostics": 1669 }, "roots": [ { @@ -352,14 +352,14 @@ "name": "testdata", "dir": "tests/testdata", "totals": { - "files": 18, + "files": 19, "filesFullyAgreeing": 10, "agreement": 34, "severityMismatch": 1, - "openSysMLOnly": 8, - "pilotOnly": 20, - "openSysMLDiagnostics": 43, - "pilotDiagnostics": 55 + "openSysMLOnly": 9, + "pilotOnly": 33, + "openSysMLDiagnostics": 44, + "pilotDiagnostics": 68 }, "files": [ { @@ -575,6 +575,57 @@ "openSysMLOnly": [], "pilotOnly": [] }, + { + "path": "passes/deferred_keeper.sysml", + "agreement": [], + "severityMismatch": [], + "openSysMLOnly": [ + { + "line": 12, + "severity": "warning", + "category": "unmapped", + "count": 1 + } + ], + "pilotOnly": [ + { + "line": 8, + "severity": "error", + "category": "kind-mismatch", + "count": 3 + }, + { + "line": 8, + "severity": "error", + "category": "unresolved-reference", + "count": 2 + }, + { + "line": 28, + "severity": "error", + "category": "kind-mismatch", + "count": 3 + }, + { + "line": 28, + "severity": "error", + "category": "unresolved-reference", + "count": 2 + }, + { + "line": 32, + "severity": "error", + "category": "kind-mismatch", + "count": 2 + }, + { + "line": 32, + "severity": "error", + "category": "unresolved-reference", + "count": 1 + } + ] + }, { "path": "passes/errors.sysml", "agreement": [ @@ -8120,6 +8171,11 @@ "message": "This modular system interface satisfies no requirement: the model declares interface requirements, so MOSA expects a `satisfy` naming it (or its definition) after `by`.", "count": 1 }, + { + "side": "opensysml", + "message": "accept of deferred signal Ping is not marked #MigrationMetadata::DeferredKeeper, so it is an ordinary accept, not the keeping loop; re-migrate the model or mark it", + "count": 1 + }, { "side": "opensysml", "message": "operator '-' requires a numeric operand, found String", @@ -8360,14 +8416,14 @@ } ], "totals": { - "files": 380, + "files": 381, "filesFullyAgreeing": 346, "agreement": 38, "severityMismatch": 2, - "openSysMLOnly": 39, - "pilotOnly": 1616, - "openSysMLDiagnostics": 79, - "pilotDiagnostics": 1656 + "openSysMLOnly": 40, + "pilotOnly": 1629, + "openSysMLDiagnostics": 80, + "pilotDiagnostics": 1669 }, "findings": [ { diff --git a/docs/project/pilot-differential.md b/docs/project/pilot-differential.md index 01b9cf66b8..50ebf0d0b3 100644 --- a/docs/project/pilot-differential.md +++ b/docs/project/pilot-differential.md @@ -228,7 +228,7 @@ nor double-counted as two independent disagreements. --- -## Results (pilot `2026-08`, 380 files) +## Results (pilot `2026-08`, 381 files) | Root | Files | Fully agreeing | Ours | Pilot | Agreed | Severity-only | Only ours | Only pilot | |---|---:|---:|---:|---:|---:|---:|---:|---:| @@ -236,10 +236,10 @@ nor double-counted as two independent disagreements. | `examples/pilot-corpora/sysml-examples` | 99 | 92 | 11 | 0 | 0 | 0 | 11 | 0 | | `examples/pilot-corpora/sysml-validation` | 56 | 56 | 0 | 0 | 0 | 0 | 0 | 0 | | `examples/pilot-corpora/kerml-examples` | 58 | 56 | 9 | 0 | 0 | 0 | 9 | 0 | -| `tests/testdata` | 18 | 10 | 43 | 55 | 34 | 1 | 8 | 20 | +| `tests/testdata` | 19 | 10 | 44 | 68 | 34 | 1 | 9 | 33 | | `examples` | 45 | 30 | 11 | 1601 | 4 | 1 | 6 | 1596 | | `tools/referee/diff/testdata` (probes) | 4 | 1 | 6 | 0 | 0 | 0 | 6 | 0 | -| **Total** | **380** | **345** | **80** | **1656** | **38** | **2** | **40** | **1616** | +| **Total** | **381** | **345** | **81** | **1669** | **38** | **2** | **41** | **1629** | **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 @@ -258,8 +258,8 @@ the [runtime showcase round](#runtime-showcase-round)): the non-standard-notatio `junction` of `pseudostates-demo.sysml`, the one demo that keeps the pseudostate notation because no SysML v2 spelling of it exists. It carried 64 before the demos were rewritten to standard notation: the succession shorthands retired 30, removing `initial ;` and `transition to ;` -retired 27 more, and the standard-notation round below retired the last 7. `testdata` carries 8: -the 3 adjudicated below and the 5 value-uniqueness diagnostics of `passes/unique_values.sysml`, a +retired 27 more, and the standard-notation round below retired the last 7. `testdata` carries 9: +the 4 adjudicated below and the 5 value-uniqueness diagnostics of `passes/unique_values.sysml`, a fixture that exists to draw them (see [Value uniqueness](#value-uniqueness--only-ours-5)) — the pilot has no value-level uniqueness constraint, so all 5 are one-sided by construction. **Those that remain are true positives about our own examples, not candidate false positives about our implementation** — the @@ -812,8 +812,8 @@ cascades through the rest of the file. The movement is entirely one file, | Count | Before the initializer rewrite | Now | |---|---:|---:| -| only pilot | 82 | **1616** | -| pilot diagnostics | 123 | **1656** | +| only pilot | 82 | **1629** | +| pilot diagnostics | 123 | **1669** | | severity-only | 9 | **2** | The rewrite itself took only-pilot to 61 and pilot diagnostics to 101; the `Now` column states @@ -942,9 +942,9 @@ Xpect assertions not present in these seven differential roots. Per category, the only-ours totals are: `pilot-examples` 4 `unmapped`, 2 `units`, 5 `kind-mismatch`; `kerml-examples` 9 `unmapped`; `examples` 4 `unmapped`, 2 `multiplicity` (the five warnings the MOSA demo draws on purpose, below, and the unbound-parameter -advisory of the [runtime showcase round](#runtime-showcase-round)); `testdata` 7 +advisory of the [runtime showcase round](#runtime-showcase-round)); `testdata` 8 `unmapped`, 1 `multiplicity`; `probes` 6 `unmapped`. -Only-pilot: `testdata` 12 `kind-mismatch`, 3 `unmapped`, 3 syntax, 2 `unresolved-reference`; +Only-pilot: `testdata` 20 `kind-mismatch`, 3 `unmapped`, 3 syntax, 7 `unresolved-reference`; `examples` 6 syntax, 29 `unmapped`, 673 `kind-mismatch`, 888 `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 @@ -1036,11 +1036,11 @@ page's history. | Count | Now | |---|---:| -| overall: fully agreeing / only ours / our diagnostics | **345 / 40 / 80** | -| only pilot | **1616** | -| pilot diagnostics | **1656** | +| overall: fully agreeing / only ours / our diagnostics | **345 / 41 / 81** | +| only pilot | **1629** | +| pilot diagnostics | **1669** | | severity-only | **2** | -| unmapped, our side | **34** | +| unmapped, our side | **35** | | kerml-examples: only ours | **9** | | pilot-examples: only ours | **11** | | examples: only pilot | **1596** | @@ -1226,6 +1226,7 @@ are gone from the three files listed in the movement table above. | ~~`passes/errors.sysml:4`, `resolve/errors.sysml:4`~~ | ~~`unresolved reference: Nowhere`~~ | **No longer a disagreement.** These were negative fixtures where the pilot was silent only because a bare `import` earlier in the same file broke its parse before it got there (see P1). Since F2 gave our fixtures an explicit visibility, the pilot parses them and reports `Nowhere` too: both rows are now agreement. | | `passes/constraints.sysml:2,3` | `A`/`B` `participates in a specialization cycle` (`unmapped`) | **Ours is right, and the pilot has no such check** — settled by F4, both by reading its validators and by probing it on clean files (see [Specialization cycles](#specialization-cycles-f4)). The silence is not a parse cascade of the kind P1 describes: the same three cycle shapes in files with nothing else in them are accepted by the pilot with zero diagnostics. A one-sided finding, so it is our extension of the reference rather than a disagreement — kept `unmapped` because no coarse category honestly covers it. | | `passes/constraints.sysml:9` | `multiplicity lower bound exceeds upper bound on lo` | **Ours is right**: `part lo [5..2];`. No pilot counterpart. | +| `passes/deferred_keeper.sysml:12` | `accept of deferred signal Ping is not marked #MigrationMetadata::DeferredKeeper, so it is an ordinary accept, not the keeping loop; re-migrate the model or mark it` (`unmapped`) | **Ours is right, and one-sided by construction.** The fixture exists to draw the `deferred-keeper-unmarked` lint on a deferral loop written without the marker the SysML v1 migrator emits; the two states beside it, one marked and one without `DeferredEvent`, draw nothing. The lint reads this repository's `MigrationMetadata` library, which the reference does not have, so no pilot counterpart can exist. | ### Value uniqueness — only ours (5) @@ -3078,10 +3079,10 @@ own `Must have a Boolean result` can agree with the pilot's identical string ins ## The remaining only-ours rows -The only-ours column is **27** as published and **26** with the declared errata applied, and every +The only-ours column is **28** as published and **27** with the declared errata applied, and every row in it is adjudicated. Three quarters of them are not candidate false positives at all: 7 are our own non-standard-notation warnings on our own demo models (`solver-demo.sysml`, 6 `require` outside a -requirement body, and `pseudostates-demo.sysml`, 1 `junction`), 3 are our own fixtures under +requirement body, and `pseudostates-demo.sysml`, 1 `junction`), 4 are our own fixtures under `testdata/passes/`, and 6+4+3 are the one-sided specialization-cycle family — the committed probes, `Simple Tests/PartTest.sysml:51,52,53,55` and `Simple Tests/Circular.kerml:9,10,11` — whose adjudication is [above](#specialization-cycles-f4). That leaves the reference's own corpora carrying @@ -3244,6 +3245,7 @@ true positive: the identical construct at line 10 is now an agreement. | 7 `Couldn't resolve reference to …` (`b`, `c`, `sciencePower`, `drivePower`, `ignite`, `start`, `touchdown`) | `parse/expressions.sysml`:3, `solver-demo.sysml`:120,124, `views-demo.sysml`:88,90,108, `pseudostates-demo.sysml`:17 | **Split, both defensible, no code change.** Three are later segments of a chain whose head we already reported unresolved (`a.b.c`), where repeating the failure per segment adds nothing; four name action or state vertices in files the reference cannot parse past, so the names are missing from *its* model rather than invented by ours. Left. | | 11 syntax errors (`no viable alternative at input 'entry'` / `'evaluate'` / `'if'` / `'then'`, `missing '}' at 'action'`, `mismatched input 'transition'`, `missing EOF`) | `phase-c-behavioral-bodies.sysml`:175,176, `pseudostates-demo.sysml`:12,18,19, `views-demo.sysml`:106,107,109 | **The reference failing to parse notation of ours.** These trace to retained extensions — `choice`/`junction` pseudostates, `entry;` as a bare entry marker, the inline `if`/`else` action form — for which the pinned grammar has no production. Not gaps of ours; we already warn on the non-standard ones under the conformance modes. Left. | | 5 `Must be an accessible feature (use dot notation for nesting)` | `semantic-layer/demo.sysml`:44,45,46,50,51 | **Recovery collateral, not a gap** — the reduced model the previous round asked for now exists. All five references (`MathConstants::pi`, `::e`, `::Derived::twoPi`, and the two expression forms) transcribed into a file that declares `MathConstants` as a `package` are silent in both implementations; changing that one keyword to `namespace`, which the SysML grammar has no production for, makes the reference report `no viable alternative at input` on each namespace **and** exactly these five accessibility errors, at the same relative positions and in the same order as the file. Its recovery turns the unparsed namespace into a feature, so each qualified reference becomes a subsetting whose subsetted feature is featured within another feature and fails `canAccess`. The construct it claims to see is not the construct in the file. Left; no rule to add. The five rows carried the same categorizer asymmetry as the row above — we word this message exactly as the reference does — and are now categorized alike on both sides, which does not pair them, since we report nothing on those lines. | +| 13 on this repository's `MigrationMetadata` annotations (8 `A metadata usage must be typed by one metadata definition.` / `Must have a concrete type` / `Must redefine an owning-type feature`, 5 `Couldn't resolve reference to Type 'MigrationMetadata::DeferredEvent'` / `'MigrationMetadata::DeferredKeeper'` / `Feature 'signal'`) | `passes/deferred_keeper.sysml`:8,28,32 | **Not a gap: the reference has no `MigrationMetadata` library.** The fixture annotates two states with `@MigrationMetadata::DeferredEvent` and one accept with `#MigrationMetadata::DeferredKeeper`, the markers the SysML v1 migrator writes, and the reference is run over the corpus without this repository's libraries, so every reference to them is unresolved there and the metadata usages typed by them draw the kind rows that follow from an unresolved type. Same cause as the `DocumentQueries` rows of `self-model/document.sysml` above. | ### The census the verdicts above account for diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md index 56e3ef2cbe..5dd4f365cf 100644 --- a/docs/project/spec-compliance.md +++ b/docs/project/spec-compliance.md @@ -802,7 +802,7 @@ checked after the result is bound is not a form the runtime offers, and none is | A state completes only once its do behavior has finished | `state_executor.go` scheduleCompletionTransitions | `state_do_activity_test.go:TestCompletionWaitsForTheDoBehavior` | ✅ Faithful | | A machine completes when a transition reaches `done`, the end shot `StateAction::done` the standard library gives every state (`stdlib/Systems Library/Actions.sysml`, written in a state body by the OMG pilot corpus `StateTest.sysml`): the states it leaves run their exit actions, the executor reports `StateCompleted`, an orthogonal machine completes only once every concurrent region has reached it, so a region completing leaves its siblings running. `done` written in a composite state's body is that composite's own `endShot` (`States.sysml`: `ref state done: StateAction :>> Action::done, StatePerformance::endShot;`), so the composite *completes* when its do behavior has ended and every one of its regions is at `done`: its nil-trigger transitions are scheduled as a leaf's are — guards read then, one event per enabled transition at the current instant, ordered as any completion event — and the machine ends only when its own top-level regions are all at `done`; a completed composite with no enabled completion transition stays completed and active, its triggered transitions still firing, and the machine runs on. Completion is stated, not inferred — a state with no outgoing transition does not complete, because an ancestor or cross-region transition may still leave it — and a machine declaring a state of its own named `done` reaches that state instead | `lower/state_graph.go` `targetVertex`, `completion` (a completion vertex per machine and per region, recorded in the graph's completion set), `StateGraph.Completes`; `lower/state_graph.go` `completionOwner` (a `done` among a declared state's members is that state's completion); `runtime/state_executor.go` completeIfDone → scheduleCompletedComposites, completedComposite, stateComplete, machineComplete (over `TopRegions`), regionComplete, settleDoActions and `runtime/state_region_transition.go` consume `Completes`, not syntax | `lower/state_completion_test.go`, `runtime/state_completion_test.go`, `runtime/testdata/conformance/state_completion_done`, `state_completion_absent`, `state_completion_all_regions`, `state_completion_nested_regions`, `state_completion_through_pseudostate`, `state_outer_completion_to_next`, `state_composite_completion_then_machine_done`, `state_composite_completion_nested`, `state_composite_completion_inside_region`, `state_entry_transition_nested_done`, `state_completion_nested_regions_stay_active`, `state_entry_transition_nested_done_stay_active` (+ their trace goldens), `state_completion_test.go:TestCompositeCompletionQueuesItsTransitionsLikeALeaf`, `:TestCompositeCompletesOnceItsDoBehaviorAndItsBodyHaveBothEnded`, `:TestCompletedCompositeWithoutCompletionTransitionStaysActive`, `snapshot_test.go:TestSnapshotStepsReachAPendingCompositeCompletionAndAHeldDeferral`, `robustness_test.go:state_event_after_completion`, `state_completion_rests_in_done`, `state_nested_region_completion_keeps_siblings_running`, `parser/removed_state_final_marker_test.go` | ✅ Faithful | | A signal trigger written `when ` (an OpenSysML spelling) names an event, not a model element, and is left unresolved; one whose name no declaration visible in scope and no `send` payload type or feature in the workspace accounts for is reported as the lint `undeclared-signal`, with the resolver's nearest names as suggestions. Its resolution and run-time matching by name are unchanged | `passes/lint_undeclared_signal.go` `UndeclaredSignalPass`; `passes/lint_signal_gather.go` | `passes/lints_test.go` `TestUndeclaredSignal*`; `workspace/model/lints_test.go`; `state_signal_discriminate.sysml` | ⚠️ Approximate (a lint over extension notation: a warning in every mode, switched off by its code) | -| A deferred signal is modelled in standard notation — an ordered buffer (`item deferred : Sig[*] ordered;`), a do action whose accept loop keeps each occurrence while the state (substates included) is active, an exit action that sends each kept occurrence to `self` — and runs on the ordinary do-behavior and `send` machinery: the accept loop is a parked `accept` that takes an occurrence no enabled transition consumes and no other accept of the state's own do behavior takes — the keeping accept yields to a sibling branch parked for the same occurrence and able to take it that step (not one held for an arrival it still awaits), so a state that defers `Sig` and whose own do behavior accepts `Sig` consumes the occurrence rather than keeping it (`action_choice.go` `stepOrder.yielding`, `ActionExecutor.keeps`/`yieldsKeeping`; the deferred signal types are lowered from the `MigrationMetadata::DeferredEvent` annotation into `StateGraph.Deferred` by `lower/state_metadata.go` `recordDeferred`), the flush re-sends each kept occurrence as the state is left, and the replay is dispatched, behind whatever is already queued, to the configuration that exit leaves; a guard of the receiving transition reads the replayed payload. The `defer ;` extension that once spelled this, with the runtime's deferral queue and priority rule, is removed: `defer` is an ordinary name and the legacy member is one `defer-notation-removed` parse error (`docs/reference/grammar/README.md`) | `parser/notation.go` (the removed-notation diagnostic), `lexer/contextual.go` (`defer` no longer contextual); `state_executor.go` `doBehaviorsTaking`, `bindAcceptPayload`; `perform.go` (a queued named signal materializes its typed occurrence) | `tests/parser/testdata/parse/defer_ordinary_name.golden`, `parser/state_notation_test.go`, `parser/negative_test.go`, `lower/state_notation_test.go:TestToStateGraph_DeferIsAnOrdinaryName`, `lsp/diagnostics_test.go`, conformance `state_deferred_signal_kept_and_replayed`, `state_deferred_do_accept_takes_before_keeping` + trace golden, `state_guard_reads_deferred_payload`, `state_nested_parallel_region_owner_behavior`, `state_then_skips_non_feature_members`; `state_terminate_test.go`, `snapshot_test.go` | ✅ Faithful (standard notation; the extension's priority and pooled replay order are the known losses recorded in the next rows) | +| A deferred signal is modelled in standard notation — an ordered buffer (`item deferred : Sig[*] ordered;`), a do action whose accept loop keeps each occurrence while the state (substates included) is active, an exit action that sends each kept occurrence to `self` — and runs on the ordinary do-behavior and `send` machinery: the accept loop is a parked `accept` that takes an occurrence no enabled transition consumes and no other accept of the state's own do behavior takes — the keeping accept yields to a sibling branch parked for the same occurrence and able to take it that step (not one held for an arrival it still awaits), so a state that defers `Sig` and whose own do behavior accepts `Sig` consumes the occurrence rather than keeping it (`action_choice.go` `stepOrder.yielding`, `ActionExecutor.keeps`/`yieldsKeeping`; the keeping accept is the one the `#MigrationMetadata::DeferredKeeper` annotation marks, lowered by resolved annotation type into `Accept.Keeper` by `lower/state_metadata.go` `isDeferredKeeper` and never inferred from the accept's position or signal, so an accept of the deferred signal written beside the loop at the do action's own level is an ordinary consumer and takes first; the `deferred-keeper-unmarked` lint of `passes/lint_deferred_keeper.go` warns, in every mode and without blocking analysis or a run, of an unmarked accept of the deferred signal at the root of a `DeferredEvent` state's do action where no accept of that signal is marked — the pre-marker shape of the loop, not an ordinary consumer beside a marked keeper — so a model migrated before the marker is re-migrated or marked rather than silently consuming what it kept), the flush re-sends each kept occurrence as the state is left, and the replay is dispatched, behind whatever is already queued, to the configuration that exit leaves; a guard of the receiving transition reads the replayed payload. The `defer ;` extension that once spelled this, with the runtime's deferral queue and priority rule, is removed: `defer` is an ordinary name and the legacy member is one `defer-notation-removed` parse error (`docs/reference/grammar/README.md`) | `parser/notation.go` (the removed-notation diagnostic), `lexer/contextual.go` (`defer` no longer contextual); `state_executor.go` `doBehaviorsTaking`, `bindAcceptPayload`; `perform.go` (a queued named signal materializes its typed occurrence) | `tests/parser/testdata/parse/defer_ordinary_name.golden`, `parser/state_notation_test.go`, `parser/negative_test.go`, `lower/state_notation_test.go:TestToStateGraph_DeferIsAnOrdinaryName`, `lsp/diagnostics_test.go`, conformance `state_deferred_signal_kept_and_replayed`, `state_deferred_do_accept_takes_before_keeping` + trace golden, `state_deferred_do_direct_accept_takes` + trace golden (under every scheduling policy), `state_deferred_do_accept_held_keeps` + trace golden, `lower/deferred_keeper_test.go`, `tests/parser/testdata/parse/accept_action_prefix_metadata.golden`, `state_guard_reads_deferred_payload`, `state_nested_parallel_region_owner_behavior`, `state_then_skips_non_feature_members`; `state_terminate_test.go`, `snapshot_test.go` | ✅ Faithful (standard notation; the extension's priority and pooled replay order are the known losses recorded in the next rows) | | Earliest transfer first (`Occurrence::incomingTransferSort` defaults to `earlierFirstIncomingTransferSort`): a completion event is dispatched before a signal due at the same instant. A replayed deferred signal is a new send and is dispatched behind the occurrences already queued — the standard encoding has no way to place it ahead of the pool, where PSSM §8.4 releases a deferred occurrence ahead of every non-completion occurrence | `executor_common.go` eventHeap.Less, isCompletionEvent | `choice_test.go:TestCompletionTransitionChoiceRereadsGuards`, `signal_injection_test.go:TestRunToCompletionTakesAPendingSignalBeforeALaterTimer`; PSSM referee rows *Deferred 001*, *Deferred 005* (`docs/project/pssm-referee.md`) | ⚠️ Approximate — the replay order of different deferred signals against one another and against the pool is not expressible in standard notation | | A transition out of a composite state is enabled while any of its substates is active: matching walks outward from every active leaf through the lowered containment (`StateGraph.ParentState`), the innermost enabled transition wins for the same event (KerML `StatePerformances::StatePerformance::acceptable`, whose `isDispatch` invariant lets an enclosing state performance accept a transfer only when no substate performance in the dispatch scope accepted it), and a false guard does not consume it | `state_executor.go` broadcastEvent, selectTransitions, losesToNestedTransition, nestedIn, activeLeaves, fireFrom, enabledTransitions, acceptsSignal/acceptsSignalFrom (an enclosing state's `accept` takes a signal off the bus) | `conformance/state_composite_outer_transition.sysml`, `:state_composite_inner_priority.sysml`, `state_composite_transition_test.go:TestCompositeStateHandlesEventItsSubstateDoesNot`, `:TestFalseGuardInsideACompositeStateFallsOutward`, `:TestTransitionOutOfAnIntermediateCompositeStateKeepsItsOwnerActive`, `:TestOuterCompositeStateStillHandlesItsEventAfterASubstateMoved`, `robustness_test.go:signal_no_level_of_a_composite_state_accepts` | ✅ Faithful | | Two transitions out of one state enabled by one event: each is a `StateTransitionPerformance` (Kernel Semantic Library `StatePerformances.kerml`) whose `transitionLink` is `HappensBefore[0..1]`, and nothing in the library orders one against another, so which fires is the executor's pick; the innermost-wins rule between a substate's transition and its enclosing state's is SysML v2/KerML order, not a pick | `state_executor.go` `enabledTransitions`, `transitionEnabled`, `probeTransition` (every transition out of the state is matched against the event and its guard and join evaluated — a call trigger's arguments bound for the guard and unbound after — the first enabled fires under the default policy; 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, and one that fails to evaluate is no alternative and no error, recorded as a `guard-unevaluable` note by `unevaluableTransition`), `chooseTransition`, `transitionChoice` (several enabled are a choice point naming the state, the trigger and the transitions by position and target; the pick among them is made only for a candidate that survived conflict resolution); the notes ride on the `dispatchCandidate` into `fireFrom`, and `transitionDecided` records them once the firing transition's guard has been read for the last time — a candidate another region's firing disabled meanwhile reports nothing — after `selectCandidates` has kept one candidate per transition and `losesToNestedTransition` has dropped a composite state's candidate to a nested one (a transition several regions select through their enclosing state is one choice, and ancestor priority is never among the alternatives); `state_change_trigger.go` `observeChangeConditions`, `probeChangeGuard`, `risenChangeTransitions` (every change transition risen by one poll is collected the same way: a state's guards are read live until the first enabled, the ones after it in a `beginProbe` preview, and one that fails to evaluate is no alternative and no error, noted as `guard-unevaluable` and left armed; the first declared fires) | `conformance/state_choice_transition_conflict.sysml` + `.expected.json` (both outcomes listed as admissible) + trace golden; `conformance/state_choice_ancestor_priority_not_reported.sysml` + `.expected.json` + trace golden (no `choice` line); `conformance/state_choice_shared_ancestor_regions.sysml` + `.expected.json` + trace golden (one `choice` line for two regions); `conformance/state_choice_ancestor_outranked_not_reported.sysml` + `.expected.json` + trace golden (no `choice` line); `conformance/state_choice_unevaluable_transition.sysml` + `.expected.json` + trace golden; `conformance/state_choice_change_transition_conflict.sysml` + `.expected.json` (both outcomes) + trace golden; `choice_test.go:TestTransitionChoiceNamesStateAndEvent`, `:TestAncestorPriorityIsNotAChoice`, `:TestSharedAncestorChoiceIsReportedOnce`, `:TestAncestorChoiceSuppressedByNestedTransitionIsNotReported`, `:TestLaterGuardErrorIsNotAChoiceNorAFailure`, `:TestFirstTransitionFailureStillFailsTheRun`, `:TestNotesOfATransitionBlockedBeforeFiringAreDropped`, `:TestNotesOfATransitionFailingInItsEffectAreKept`, `:TestChangeTransitionChoice`, `:TestLaterChangeGuardErrorIsNotAChoiceNorAFailure`, `:TestChangeTransitionChoiceUnderHierarchyAndRegions`, `:TestProbedGuardLeavesObjectIdentitiesUntouched`; `grpc/choice_test.go:TestExecuteState_ChoicePointDiagnostics`; `repl/choice_test.go:TestAdvanceReportsChoicePoints` | ✅ Faithful (declaration order is tool-defined and kept; the pick is reported, and the ordered case is not) | diff --git a/docs/reference/cli.md b/docs/reference/cli.md index 4837720a18..ead42bdc29 100644 --- a/docs/reference/cli.md +++ b/docs/reference/cli.md @@ -232,7 +232,7 @@ the same member-path parser as `Project` and `OrderBy`. | `--debug` | | Report every diagnostic over the whole session buffer, with the pass that produced it | | `--quiet` | | Report errors only, suppressing warnings | | `--strict` | | Judge the model as conforming SysML v2: notation no pinned production admits is an error, not a warning (see [Strict conformance](../guide/03-command-line.md#strict-conformance)) | -| `--disable-lint ` | | Leave the named [lint](diagnostics.md) out of the diagnostics: `undeclared-signal` or `port-type-mismatch`; comma-separated or repeated. An unknown code is a usage error | +| `--disable-lint ` | | Leave the named [lint](diagnostics.md) out of the diagnostics: `undeclared-signal`, `port-type-mismatch` or `deferred-keeper-unmarked`; comma-separated or repeated. An unknown code is a usage error | | `--no-record-cache` | | Parse every file loaded and hold it loaded, reading no interface record from the record cache and writing none: what a run does where `OPENSYSML_RECORD_CACHE=0`. By default a file whose bytes, library, conformance mode and record format match a record in the cache is held as that record — its scopes and symbols without its tree, and the diagnostics its analysis found — and a file analyzed by `-validate`, `-satisfy` or another load writes its record for the next run; see [Interface records](../internals/interface-records.md) | | `--trace` | | Report each execution step: expression evaluation, calc invocation, action tokens, state transitions, each `choice` the executor made among alternatives the library leaves unordered, 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)). Under `-schedule explore` the table is printed first, then the trace of one witness run per distinct outcome, each under a `trace of outcome 's witness (run ):` heading ([Exploring every linearization](#exploring-every-linearization)) | | `--convert ` | | Convert the model instead of running it: `sysml`, `kerml`, `ttl`, `turtle`, `rdf`, `api-json` or `json`. `ttl` writes the RDF graph in Turtle, `api-json` the same graph as the API's JSON element objects; both are [experimental](rdf-mapping.md#status-experimental) and every run that converts either says so on stderr (see [the RDF mapping](rdf-mapping.md)). The model argument may be a Flexo MMS project branch URL — `http(s)://host[:port][/base]/projects/{project}/branches/{branch}` or `flexo://{project}/{branch}` — both naming the endpoint `FLEXO_SYSMLV2_URL` configures — which is read as its head commit's RDF graph; see [Reading and pushing a repository branch](#reading-and-pushing-a-repository-branch) | diff --git a/docs/reference/diagnostics.md b/docs/reference/diagnostics.md index 01fdd5ce28..e12b247491 100644 --- a/docs/reference/diagnostics.md +++ b/docs/reference/diagnostics.md @@ -12,6 +12,7 @@ the exit status or blocks a check. |------|-------------|------| | `undeclared-signal` | a transition's `when ` whose name matches no declaration visible where it is written and no signal the model sends | name resolution | | `port-type-mismatch` | a `connect`, an interface usage or a `flow` joining two ports whose definitions are unrelated | constraint | +| `deferred-keeper-unmarked` | an accept of a deferred signal at the root of the do action of a state annotated `MigrationMetadata::DeferredEvent` that is not marked `MigrationMetadata::DeferredKeeper` | name resolution | ## Switching a lint off @@ -100,3 +101,36 @@ It covers `connect a.p to b.q;` (and `connection … connect`), interface usages `ConnectionUsage`, `InterfaceUsage` and `FlowUsage` (`SysML.xtext:1062`, `:1153`, `:1269`). An end that is not a port, or whose port type does not resolve, is not judged. The specification states no constraint of this kind, so it is a lint rather than an error. + +## `deferred-keeper-unmarked` + +A SysML v1 state's deferred signal is migrated to the standard encoding described under +[Deferred signals](sysml-v1-migration.md#deferred-signals): the state is annotated +`@MigrationMetadata::DeferredEvent { ref :>> signal : Sig; }`, and its do action keeps each +occurrence of `Sig` through an accept loop whose accept is written +`#MigrationMetadata::DeferredKeeper action receive accept kept : Sig;`. The runtime knows the +keeping accept by that annotation alone — it is the accept that yields an occurrence to any +other accept of the state able to take it, and keeps what nothing else takes — so an accept of +the deferred signal written without it is an ordinary accept, which consumes the occurrence. +Output migrated before the marker existed wrote the loop's accept bare, and so does a model +written by hand after the pattern. + +The lint reports each accept node at the root of the do action of a state annotated +`MigrationMetadata::DeferredEvent` whose payload is typed by the signal the annotation names, +when no accept of that signal there carries `MigrationMetadata::DeferredKeeper`: once one does, +the state has its keeping loop, and a bare accept of the signal beside it is the ordinary +consumer the marker exists to tell apart, which takes an occurrence first. Both annotations +are known by their resolved type, however the model spells them (through an import, an alias +or `$::MigrationMetadata`), and a metadata definition of the model that merely shares the +library name is not one of them. + +```text +m.sysml:12:5: warning: accept of deferred signal Ping is not marked #MigrationMetadata::DeferredKeeper, so it is an ordinary accept, not the keeping loop; re-migrate the model or mark it +``` + +The model still analyses and runs; the accept simply takes each occurrence rather than keeping +it. Re-migrate the model, which writes the marker on every keeping accept, or write +`#MigrationMetadata::DeferredKeeper` on the accept yourself. An accept of the signal nested +below the do action's root, one beside a marked keeper of the signal, or one under a state the +annotation does not name, is an ordinary accept by design and is not reported, nor is an +accept whose signal does not resolve, which name resolution reports. diff --git a/docs/reference/sysml-v1-migration.md b/docs/reference/sysml-v1-migration.md index 8e0fbf782c..86d4564dfd 100644 --- a/docs/reference/sysml-v1-migration.md +++ b/docs/reference/sysml-v1-migration.md @@ -274,7 +274,7 @@ model with the same help. See [wire-contract.md](wire-contract.md#migration-migr | Transition `effect` referring to a behavior owned elsewhere | `do action : Def` on the transition, the target following on the next line; the behavior's own `action def` is written once where it is owned | mapped | | `entry`, `doActivity`, `exit` behavior or transition `effect` referring to a behavior that is not written, or is written as something no state runs (a StateMachine, for one) | comment in the state's body or before the transition (a `/* */` comment is admitted only where a member may appear, not between the transition's clauses); the state or transition is written without it | approximated (the state or transition: "its … is not run"; a behavior not written: **unmapped**) | | Transition `effect` with `in` parameters | the accepted signal is named, `accept sig : Sig`, and each parameter typed by the signal (or a general of it), or the sole untyped one, is bound to it: `in p : Sig = sig;`; a parameter of another type takes no value | mapped (an unbound parameter: approximated) | -| State `deferrableTrigger` on a SignalEvent | the annotation `@MigrationMetadata::DeferredEvent { ref :>> signal : Sig; }` naming the deferred signal, and the standard encoding described under [Deferred signals](#deferred-signals): an `item` buffer the state's do action fills from an accept loop while the state is active, substates included, which its exit action sends back to the object once the state is left; the same in both modes | approximated | +| State `deferrableTrigger` on a SignalEvent | the annotation `@MigrationMetadata::DeferredEvent { ref :>> signal : Sig; }` naming the deferred signal, and the standard encoding described under [Deferred signals](#deferred-signals): an `item` buffer the state's do action fills from an accept loop, its accept marked `#MigrationMetadata::DeferredKeeper`, while the state is active, substates included, which its exit action sends back to the object once the state is left; the same in both modes | approximated | | State `deferrableTrigger` on a SignalEvent a transition out of the state itself accepts without a guard | the annotation alone by the routes the transition accepts by (all of them when its trigger names no port): in v1 the transition takes precedence over the deferral, so the signal is never kept there; a route the transition does not accept by, such as the object itself when the trigger names one port, keeps its accept loop. A transition on a general of the deferred signal accepts it too, as a v2 `accept` typed by the general does | approximated (the note names the transition) | | State `deferrableTrigger` on a SignalEvent a transition out of the state accepts under a guard, or a transition out of a substate accepts, or a transition accepts a specialization of | the standard encoding: the signal is kept while the guard is false or the substate inactive, or when the occurrence is not of the specialization, the transition taking it otherwise | approximated (the note names the transition) | | State `deferrableTrigger` on a SignalEvent the same state also defers a general of, or defers again by another trigger | the annotation alone by the routes the other deferral's accept loop accepts by: that loop keeps every occurrence of the signal already, and a loop of its own would keep each occurrence twice, the exit action then sending it twice | approximated (the note names the deferral that keeps it) | @@ -1946,7 +1946,7 @@ state Off { item deferred : Door[*] ordered; do action buffer { first start then receive; - action receive accept kept : Door; + #MigrationMetadata::DeferredKeeper action receive accept kept : Door; then action keep { assign deferred := SequenceFunctions::including(deferred, receive.kept); } then receive; } @@ -2013,3 +2013,18 @@ so). The `@MigrationMetadata::DeferredEvent` annotation is written for every signal the state declares deferrable, kept or not, so a consumer sees what the state deferred without reading the encoding; `MigrationMetadata` is a bundled OpenSysML library the migrated document imports. + +The accept of each keeping loop is written +`#MigrationMetadata::DeferredKeeper action receive accept kept : Sig;`. The annotation marks +it as the accept that keeps the signal for the state rather than consuming it: the runtime +lets any other accept of the signal the state's own do behavior is parked at take an +occurrence first, and the loop keeps only what nothing else of the state takes. The keeper is +known by the annotation's resolved type alone, never by where the accept stands, so an accept +of the deferred signal written without it — at any level of the do action — is an ordinary +accept. Output migrated before the marker existed wrote the loop's accept bare, so the checker +reports an unmarked accept of a deferred signal at the root of a `DeferredEvent` state's do +action, where no accept of that signal is marked, with the `deferred-keeper-unmarked` warning ([diagnostics](diagnostics.md#deferred-keeper-unmarked)): +the model still analyses and runs, the accept consuming each occurrence rather than keeping it; +re-migrate it, or write the marker on the accept. Both annotations are written through +`$::MigrationMetadata` where a package of the +model shadows the library's name. diff --git a/examples/self-model/pipeline.sysml b/examples/self-model/pipeline.sysml index f4d4d03a33..0f2d8e8be7 100644 --- a/examples/self-model/pipeline.sysml +++ b/examples/self-model/pipeline.sysml @@ -182,7 +182,7 @@ package OpenSysMLPipeline { #SemanticEngine part def PassRegistry :> Stage { attribute :>> goPackage = "internal/check/passes"; attribute tierCount : Integer = 4; - attribute passCount : Integer = 63; + attribute passCount : Integer = 64; attribute sortsByLevel : Boolean = true; attribute skipsDocumentScopedAboveFailure : Boolean = true; @@ -202,6 +202,8 @@ package OpenSysMLPipeline { } // A lint: a signal trigger's name no declaration and no send accounts for. part undeclaredSignals : NameResolutionCheck { attribute :>> goType = "UndeclaredSignalPass"; } + // A lint: a deferred signal's keeping loop written without its marker. + part deferredKeepers : NameResolutionCheck { attribute :>> goType = "DeferredKeeperPass"; } part typeCheck : TypeCheck { attribute :>> goType = "TypeCheckPass"; } part transitionGuards : TypeCheck { attribute :>> goType = "TransitionGuardPass"; diff --git a/internal/check/passes/analyze.go b/internal/check/passes/analyze.go index 625be9e5bc..00f2f1bac8 100644 --- a/internal/check/passes/analyze.go +++ b/internal/check/passes/analyze.go @@ -26,6 +26,7 @@ func DefaultRegistry() *Registry { reg.Register(behavior.StateTransitionPass{}) reg.Register(behavior.ActionEndpointPass{}) reg.Register(UndeclaredSignalPass{}) + reg.Register(DeferredKeeperPass{}) reg.Register(TypeCheckPass{}) reg.Register(TransitionGuardPass{}) reg.Register(TriggerArgumentPass{}) diff --git a/internal/check/passes/integration_test.go b/internal/check/passes/integration_test.go index 92038b5d0b..aa3825ec36 100644 --- a/internal/check/passes/integration_test.go +++ b/internal/check/passes/integration_test.go @@ -70,3 +70,9 @@ func TestPassesGoldenCorpusNotation(t *testing.T) { runPassesGolden(t, "corpus_n // A multi-valued feature is unique unless declared nonunique: a const-decidable // repeat is a diagnostic, one only a run decides is left to the runtime. func TestPassesGoldenUniqueValues(t *testing.T) { runPassesGolden(t, "unique_values") } + +// An accept of a deferred signal at the root of a deferring state's do action +// is the keeping loop only when marked DeferredKeeper: the unmarked one is +// warned about, the marked one and an accept under a state deferring nothing +// are not. +func TestPassesGoldenDeferredKeeper(t *testing.T) { runPassesGolden(t, "deferred_keeper") } diff --git a/internal/check/passes/lint_deferred_keeper.go b/internal/check/passes/lint_deferred_keeper.go new file mode 100644 index 0000000000..e499b628e9 --- /dev/null +++ b/internal/check/passes/lint_deferred_keeper.go @@ -0,0 +1,205 @@ +package passes + +import ( + "fmt" + + "github.com/Open-MBEE/OpenSysML/internal/check/passes/kit" + "github.com/Open-MBEE/OpenSysML/internal/ir/lower" + "github.com/Open-MBEE/OpenSysML/internal/semantic/resolve" + "github.com/Open-MBEE/OpenSysML/internal/semantic/symbols" + "github.com/Open-MBEE/OpenSysML/internal/syntax/ast" + "github.com/Open-MBEE/OpenSysML/internal/syntax/diag" +) + +// DeferredKeeperPass warns when a state annotated `MigrationMetadata::DeferredEvent` +// has, at the root of its do action, an accept typed by a signal the annotation +// defers that does not carry `MigrationMetadata::DeferredKeeper`. That is the +// keeping loop of the standard deferred-signal encoding as it was written before +// the marker existed: the runtime knows the keeping accept by the marker alone, +// so without it the loop is an ordinary accept of the signal, which consumes an +// occurrence instead of keeping it. +type DeferredKeeperPass struct{} + +// Level reports the name-resolution level: the annotations' types and the +// signals' names are all it reads. +func (DeferredKeeperPass) Level() PassLevel { return LevelNameResolution } + +// Run checks the deferring states of one workspace document. +func (DeferredKeeperPass) Run(ctx *Context, name string, root *ast.RootNamespace) []diag.Diagnostic { + if ctx == nil || ctx.Index == nil || root == nil || ctx.Index.IsLibraryDocument(name) { + return nil + } + rootScope := ctx.Index.DocumentRoot(name) + if rootScope == nil { + return nil + } + c := &deferredKeeperLint{ctx: ctx, resolver: ctx.Resolver()} + for _, at := range kit.ScopedNodes(ctx, rootScope) { + if u, ok := at.Node.(*ast.Usage); ok && u.Kind == ast.UsageState { + c.checkState(at.Scope, u) + } + } + return c.diags +} + +type deferredKeeperLint struct { + ctx *Context + resolver *resolve.Resolver + diags []diag.Diagnostic +} + +// checkState reports the unmarked accepts of each deferred signal at the root +// of the do action of the state usage u, written in scope, when no accept of +// that signal there is marked as its keeper. +func (c *deferredKeeperLint) checkState(scope *symbols.Scope, u *ast.Usage) { + deferred := lower.DeferredSignals(c.resolver, scope, u) + if len(deferred) == 0 { + return + } + body := scopeOwned(scope, u) + for _, member := range u.Members { + do, ok := memberNode(member).(*ast.DoMember) + if !ok { + continue + } + for _, action := range do.Actions { + if performed, ok := memberNode(action).(*ast.Usage); ok { + c.checkDoAction(scopeOwned(body, performed), performed, deferred) + } + } + } +} + +// rootAccept is an accept node at the root of a do action with the signal its +// payload is typed by. +type rootAccept struct { + node *ast.Usage + signal *symbols.Symbol +} + +// checkDoAction reports, for each of deferred, the accepts of the signal among +// the root nodes of the performed do action when none of them is marked. +func (c *deferredKeeperLint) checkDoAction(scope *symbols.Scope, performed *ast.Usage, deferred []lower.DeferredSignal) { + var accepts []rootAccept + for _, m := range performed.Members { + node, ok := memberNode(m).(*ast.Usage) + if !ok || node.Kind != ast.UsageAction { + continue + } + if signal := c.acceptedSignal(scope, node); signal != nil { + accepts = append(accepts, rootAccept{node: node, signal: signal}) + } + } + if len(accepts) == 0 { + return + } + seen := map[*symbols.Symbol]bool{} + for _, d := range deferred { + if c.ctx.DownstreamOfFailure(d.Type) { + continue + } + signal := c.symbolOf(d.Scope, d.Type) + if signal == nil || seen[signal] { + continue + } + seen[signal] = true + var unmarked []*ast.Usage + kept := false + for _, a := range accepts { + if a.signal != signal { + continue + } + if lower.IsDeferredKeeper(c.resolver, scope, a.node) { + kept = true + break + } + unmarked = append(unmarked, a.node) + } + if kept { + continue + } + for _, node := range unmarked { + c.diags = append(c.diags, diag.Diagnostic{ + Severity: diag.SeverityWarning, + Span: node.Span(), + Message: fmt.Sprintf( + "accept of deferred signal %s is not marked #MigrationMetadata::DeferredKeeper, so it is an ordinary accept, not the keeping loop; re-migrate the model or mark it", + qnText(d.Type)), + Code: CodeDeferredKeeperUnmarked, + Source: lintSource, + }) + } + } +} + +// acceptedSignal is the signal the payload of the accept node, written in +// scope, is typed by; nil for any other action usage or an unresolved type. +func (c *deferredKeeperLint) acceptedSignal(scope *symbols.Scope, node *ast.Usage) *symbols.Symbol { + payload := acceptPayload(node) + if payload == nil { + return nil + } + typeRef := typingTargetOf(payload) + if typeRef == nil || c.ctx.DownstreamOfFailure(typeRef) { + return nil + } + return c.symbolOf(scopeOwned(scope, node), typeRef) +} + +// symbolOf resolves qn in scope, through any alias; nil without a resolution. +func (c *deferredKeeperLint) symbolOf(scope *symbols.Scope, qn *ast.QualifiedName) *symbols.Symbol { + if scope == nil || qn == nil { + return nil + } + sym, ok := c.resolver.ReadQualified(scope, qn).Symbol() + if !ok || sym == nil { + return nil + } + if target, ok := c.resolver.ResolveAliasTarget(sym); ok && target != nil { + return target + } + return sym +} + +// acceptPayload is the payload parameter of an accept node, nil for any other +// action usage. +func acceptPayload(node *ast.Usage) *ast.Usage { + for _, member := range node.Members { + if m, ok := memberNode(member).(*ast.Usage); ok && m.IsAccept { + return m + } + } + return nil +} + +// typingTargetOf is the name the usage's first typing relationship states. +func typingTargetOf(usage *ast.Usage) *ast.QualifiedName { + for _, rel := range usage.Relationships { + if rel == nil || rel.Kind != ast.RelTyping { + continue + } + if qn := ast.AsQualifiedName(rel.Target); qn != nil && len(qn.Parts) > 0 { + return qn + } + } + return nil +} + +// memberNode is the declaration a membership wraps, or the node itself. +func memberNode(node ast.Node) ast.Node { + if m, ok := node.(*ast.Membership); ok { + return m.Member + } + return node +} + +// scopeOwned is the scope decl owns under parent, or parent when it owns none. +func scopeOwned(parent *symbols.Scope, decl ast.Node) *symbols.Scope { + if parent == nil { + return nil + } + if child := parent.ChildFor(decl); child != nil { + return child + } + return parent +} diff --git a/internal/check/passes/lint_deferred_keeper_test.go b/internal/check/passes/lint_deferred_keeper_test.go new file mode 100644 index 0000000000..7af1569a32 --- /dev/null +++ b/internal/check/passes/lint_deferred_keeper_test.go @@ -0,0 +1,80 @@ +package passes + +import "testing" + +// deferringMachine is a state machine whose state busy defers Ping and keeps it +// by the standard encoding, the keeping accept written as accept; other adds to +// the do action's root and annotation to the state's body. +func deferringMachine(annotation, accept, other string) string { + return `package P { + item def Ping; item def Go; + state def Machine { + entry; then busy; + state busy { + ` + annotation + ` + item deferred : Ping[*] ordered; + do action buffer { + first start then receive; + ` + accept + ` + then action keep { assign deferred := SequenceFunctions::including(deferred, receive.kept); } + then receive; + ` + other + ` + } + exit action flush { + for kept in deferred { send kept to self; } + then action clear { assign deferred := (); } + } + } + state ready; + transition first busy accept Go then ready; + } +}` +} + +const ( + deferredEventPing = `@MigrationMetadata::DeferredEvent { ref :>> signal : Ping; }` + unmarkedKeeper = `action receive accept kept : Ping;` + markedKeeper = `#MigrationMetadata::DeferredKeeper action receive accept kept : Ping;` +) + +func TestDeferredKeeperUnmarkedLint(t *testing.T) { + want := []string{ + "accept of deferred signal Ping is not marked #MigrationMetadata::DeferredKeeper", + "ordinary accept, not the keeping loop; re-migrate the model or mark it", + } + cases := []struct { + name string + src string + wants [][]string + }{ + {"unmarked loop under a deferring state", deferringMachine(deferredEventPing, unmarkedKeeper, ""), [][]string{want}}, + {"annotation imported by name", `package P { + private import MigrationMetadata::DeferredEvent; + ` + deferringMachine(`@DeferredEvent { ref :>> signal : Ping; }`, unmarkedKeeper, "")[len("package P {"):], [][]string{want}}, + {"annotation through an alias", `package P { + alias Kept for MigrationMetadata::DeferredEvent; + ` + deferringMachine(`@Kept { ref :>> signal : Ping; }`, unmarkedKeeper, "")[len("package P {"):], [][]string{want}}, + {"marked loop", deferringMachine(deferredEventPing, markedKeeper, ""), nil}, + {"unmarked accept under a state deferring nothing", deferringMachine("", unmarkedKeeper, ""), nil}, + {"homonymous annotation of the model", `package P { + metadata def DeferredEvent { ref signal : Base::Anything; } + ` + deferringMachine(`@DeferredEvent { ref :>> signal : Ping; }`, unmarkedKeeper, "")[len("package P {"):], nil}, + {"unmarked accept of another signal", deferringMachine(deferredEventPing, markedKeeper, `action other accept go : Go;`), nil}, + {"unmarked accept nested beside the marked loop", deferringMachine(deferredEventPing, markedKeeper, + `action work { action take accept p : Ping; }`), nil}, + {"ordinary accept beside the marked loop", deferringMachine(deferredEventPing, markedKeeper, + `action take accept p : Ping;`), nil}, + {"two unmarked accepts, neither the keeper", deferringMachine(deferredEventPing, unmarkedKeeper, + `action take accept p : Ping;`), [][]string{want, want}}, + {"signal deferred twice, reported once", deferringMachine( + deferredEventPing+"\n\t\t\t"+deferredEventPing, unmarkedKeeper, ""), [][]string{want}}, + {"second deferred signal kept by an unmarked loop", deferringMachine( + deferredEventPing+"\n\t\t\t@MigrationMetadata::DeferredEvent { ref :>> signal : Go; }", + markedKeeper, `action keepGo accept go : Go;`), [][]string{{"deferred signal Go is not marked"}}}, + } + for _, tc := range cases { + t.Run(tc.name, func(t *testing.T) { + wantLints(t, tc.src, CodeDeferredKeeperUnmarked, tc.wants...) + }) + } +} diff --git a/internal/check/passes/lints.go b/internal/check/passes/lints.go index 5a62bfeb16..8333bb7496 100644 --- a/internal/check/passes/lints.go +++ b/internal/check/passes/lints.go @@ -20,8 +20,12 @@ const CodeUndeclaredSignal = "undeclared-signal" // whose definitions are unrelated and whose directed features are not conjugate. const CodePortTypeMismatch = "port-type-mismatch" +// CodeDeferredKeeperUnmarked marks an accept of a deferred signal at the root +// of a deferring state's do action that is not marked as the keeping accept. +const CodeDeferredKeeperUnmarked = "deferred-keeper-unmarked" + // lintCodes are the codes of the lints, in the order surfaces list them. -var lintCodes = []string{CodeUndeclaredSignal, CodePortTypeMismatch} +var lintCodes = []string{CodeUndeclaredSignal, CodePortTypeMismatch, CodeDeferredKeeperUnmarked} // LintCodes returns the codes of the diagnostics a surface may disable. func LintCodes() []string { return slices.Clone(lintCodes) } diff --git a/internal/exec/runtime/action_choice.go b/internal/exec/runtime/action_choice.go index e013343f77..7bea578179 100644 --- a/internal/exec/runtime/action_choice.go +++ b/internal/exec/runtime/action_choice.go @@ -211,28 +211,15 @@ func (e *ActionExecutor) beginStepOrder() stepOrder { return order } -// keeps reports whether the token sits at an accept keeping a deferred signal -// of the state whose do behavior this flow runs: an accept of the flow's own -// typed by a signal the state defers, the accept loop of the standard deferral -// encoding (`item deferred : Sig[*] ordered; do action buffer { … accept kept : Sig; … }`). +// keeps reports whether the token sits at the accept keeping a deferred signal +// for the state whose do behavior this flow runs: the accept loop of the +// standard deferral encoding, which its DeferredKeeper annotation names +// (`#MigrationMetadata::DeferredKeeper action receive accept kept : Sig;`) and +// lowering records as Accept.Keeper; an accept of the same signal without the +// annotation is an ordinary consumer, wherever it stands. func (e *ActionExecutor) keeps(t Token) bool { - if len(e.deferred) == 0 || t.frame != e.root { - return false - } accept, ok := e.messageAccept(t) - if !ok || accept.SignalType == nil { - return false - } - kept := e.ctx.triggerType(accept.Scope, accept.SignalType) - if kept == nil { - return false - } - for _, d := range e.deferred { - if e.ctx.triggerType(d.Scope, d.Type) == kept { - return true - } - } - return false + return ok && accept.Keeper } // yieldsKeeping reports whether a message the keeping accept at k would take is diff --git a/internal/exec/runtime/action_executor.go b/internal/exec/runtime/action_executor.go index 68e0c91e93..b43f7c5cb0 100644 --- a/internal/exec/runtime/action_executor.go +++ b/internal/exec/runtime/action_executor.go @@ -46,10 +46,6 @@ type ActionExecutor struct { // holds what the action's own features hold, and data mirrors it. occurrence *Instance graph *lower.ActionGraph // Execution IR - // deferred are the signals the state whose do behavior this flow runs defers: - // an accept of the flow's own keeping one yields the message to another - // accept of the run (keeps, yieldsKeeping). Empty for every other flow. - deferred []lower.DeferredSignal // features are the attributes and parameters the performance holds: those the // graph declares, then the inherited ones none of them redefines. features []lower.Attribute diff --git a/internal/exec/runtime/state_statements.go b/internal/exec/runtime/state_statements.go index 5f37af5d66..bd0b57db4f 100644 --- a/internal/exec/runtime/state_statements.go +++ b/internal/exec/runtime/state_statements.go @@ -189,7 +189,6 @@ func (e *StateExecutor) newDoRun(behavior lower.StateBehavior, firing *firing) * return nil } host := e.behaviorHost(behavior, firing) - host.flow.deferred = e.graph.Deferred[behavior.Owner] body := &bodyRun{work: host, awaitsMessages: true, yields: true, steps: e.ctx.scheduling().oneMove()} return &doRun{host: host, body: body} } diff --git a/internal/exec/runtime/testdata/conformance/state_deferred_do_accept_held_keeps.sysml b/internal/exec/runtime/testdata/conformance/state_deferred_do_accept_held_keeps.sysml index 9db8011202..d8411c9562 100644 --- a/internal/exec/runtime/testdata/conformance/state_deferred_do_accept_held_keeps.sysml +++ b/internal/exec/runtime/testdata/conformance/state_deferred_do_accept_held_keeps.sysml @@ -22,7 +22,7 @@ package Test { fork split; then receive; then work; - action receive accept kept : Ping; + #MigrationMetadata::DeferredKeeper action receive accept kept : Ping; then action keep { assign deferred := SequenceFunctions::including(deferred, receive.kept); } then receive; action work { diff --git a/internal/exec/runtime/testdata/conformance/state_deferred_do_accept_takes_before_keeping.sysml b/internal/exec/runtime/testdata/conformance/state_deferred_do_accept_takes_before_keeping.sysml index 9b2248bed4..16bb08bdeb 100644 --- a/internal/exec/runtime/testdata/conformance/state_deferred_do_accept_takes_before_keeping.sysml +++ b/internal/exec/runtime/testdata/conformance/state_deferred_do_accept_takes_before_keeping.sysml @@ -21,7 +21,7 @@ package Test { fork split; then receive; then work; - action receive accept kept : Ping; + #MigrationMetadata::DeferredKeeper action receive accept kept : Ping; then action keep { assign deferred := SequenceFunctions::including(deferred, receive.kept); } then receive; action work { diff --git a/internal/exec/runtime/testdata/conformance/state_deferred_do_direct_accept_takes.expected.json b/internal/exec/runtime/testdata/conformance/state_deferred_do_direct_accept_takes.expected.json new file mode 100644 index 0000000000..bb572a6224 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_deferred_do_direct_accept_takes.expected.json @@ -0,0 +1,13 @@ +{ + "type": "state", + "libraries": true, + "events": [ + {"signal": "Ping", "args": null}, + {"signal": "Ping", "args": null}, + {"signal": "Go", "args": null} + ], + "finalState": "done", + "stateVisits": ["start", "busy", "ready", "done"], + "outputs": {"heard": {"type": "Integer", "value": 1}}, + "trace": true +} diff --git a/internal/exec/runtime/testdata/conformance/state_deferred_do_direct_accept_takes.sysml b/internal/exec/runtime/testdata/conformance/state_deferred_do_direct_accept_takes.sysml new file mode 100644 index 0000000000..ee26d7635d --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_deferred_do_direct_accept_takes.sysml @@ -0,0 +1,41 @@ +// A state deferring Ping whose do behavior accepts Ping at its own level, as a +// branch beside the keeping loop of the standard deferred-signal encoding: the +// DeferredKeeper annotation names the keeping accept, so the state's other +// accept of Ping — written at the same level, with no nested action around it — +// takes a Ping arriving while both are parked, whichever the schedule would +// run first. A Ping arriving once `take` has passed is kept, and replayed when +// `busy` exits. +package Test { + private import ScalarValues::Integer; + item def Ping; + item def Go; + + state DoDirectAcceptTakes { + attribute heard : Integer = 0; + entry; then start; + state start; + state busy { + @MigrationMetadata::DeferredEvent { ref :>> signal : Ping; } + item deferred : Ping[*] ordered; + do action buffer { + first start then split; + fork split; + then take; + then receive; + #MigrationMetadata::DeferredKeeper action receive accept kept : Ping; + then action keep { assign deferred := SequenceFunctions::including(deferred, receive.kept); } + then receive; + action take accept p : Ping; + then action count { assign heard := heard + 1; } + } + exit action flush { + for kept in deferred { send kept to self; } + then action clear { assign deferred := (); } + } + } + state ready; + succession first start then busy; + transition first busy accept Go then ready; + transition first ready accept Ping then done; + } +} diff --git a/internal/exec/runtime/testdata/conformance/state_deferred_do_direct_accept_takes.trace.golden b/internal/exec/runtime/testdata/conformance/state_deferred_do_direct_accept_takes.trace.golden new file mode 100644 index 0000000000..58775a5cf2 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_deferred_do_direct_accept_takes.trace.golden @@ -0,0 +1,38 @@ +exit: start +enter: busy +transition: start -> busy +do: busy +stmt action body +enter action node: state behavior buffer +do: busy +materialize: Ping #1 + stmt assign heard + eval feature heard -> 0 + eval literal 1 -> 1 + eval operator + -> 1 +do: busy +materialize: Ping #2 + stmt assign deferred + enter calc SequenceFunctions::including + eval feature deferred -> () + eval chain kept -> instance#2 + bind seq = () [argument] + bind values = instance#2 [argument] + exit calc SequenceFunctions::including -> (instance#2) + eval invoke SequenceFunctions::including -> (instance#2) +exit: busy (exit action) +stmt action body +enter action node: state behavior flush + stmt for kept + eval feature deferred -> (instance#2) + iteration 1 + stmt send + eval feature kept -> instance#2 + stmt assign deferred + eval null -> null +leave action node: state behavior flush +enter: ready +transition: busy -> ready (event: accept Go) +exit: ready +enter: done +transition: ready -> done (event: accept Ping) diff --git a/internal/ir/lower/action_graph.go b/internal/ir/lower/action_graph.go index 3190421fe3..b27dcd8d74 100644 --- a/internal/ir/lower/action_graph.go +++ b/internal/ir/lower/action_graph.go @@ -586,6 +586,11 @@ type Accept struct { Trigger ast.Node // Scope is the scope the accept was declared in, in which SignalType resolves. Scope *symbols.Scope + // Keeper reports the accept keeps the signal for a state deferring it, as a + // DeferredKeeper annotation on the node declares (`#MigrationMetadata::DeferredKeeper + // action receive accept kept : Sig;`): it takes an occurrence no other accept + // of the state's behavior is ready for. + Keeper bool } // Attribute is a lowered attribute default written among a behavior's members diff --git a/internal/ir/lower/action_subflow.go b/internal/ir/lower/action_subflow.go index e09ebf71b1..7ee799182a 100644 --- a/internal/ir/lower/action_subflow.go +++ b/internal/ir/lower/action_subflow.go @@ -155,6 +155,7 @@ func lowerAccept(graph *ActionGraph, node *ast.Usage, scope *symbols.Scope) { SubsetsEvent: subsettingTarget(m), Trigger: m.Value, Scope: scope, + Keeper: IsDeferredKeeper(graph.resolver, scope, node), } } } diff --git a/internal/ir/lower/deferred_keeper_test.go b/internal/ir/lower/deferred_keeper_test.go new file mode 100644 index 0000000000..e8413078c6 --- /dev/null +++ b/internal/ir/lower/deferred_keeper_test.go @@ -0,0 +1,47 @@ +package lower + +import "testing" + +// The accept a DeferredKeeper annotation marks lowers as the keeper of the +// signal it accepts, however the annotation is spelled; one without the +// annotation, or with one of a definition that merely shares its name, does not. +func TestAccept_KeeperIsReadByResolvedAnnotation(t *testing.T) { + graph, err := weightedActionGraph(t, ` + import MigrationMetadata::DeferredKeeper; + metadata def Keeper :> DeferredKeeper; + item def Ping; + #MigrationMetadata::DeferredKeeper action receive accept kept : Ping; + #DeferredKeeper action imported accept kept : Ping; + action spelled accept kept : Ping { @DeferredKeeper; } + action plain accept kept : Ping; + #Keeper action narrowed accept kept : Ping; + `) + if err != nil { + t.Fatalf("ToActionGraphWith: %v", err) + } + for name, want := range map[string]bool{"receive": true, "imported": true, "spelled": true, "plain": false, "narrowed": false} { + accept, ok := graph.Accepts[nodeNamed(t, graph, name)] + if !ok { + t.Fatalf("%s lowered no accept", name) + } + if accept.Keeper != want { + t.Errorf("%s: Keeper = %v, want %v", name, accept.Keeper, want) + } + } +} + +// A definition spelled like the library's, declared by the model itself, marks +// no keeper: detection is by the resolved definition, not the written name. +func TestAccept_KeeperIgnoresAHomonymousDefinition(t *testing.T) { + graph, err := weightedActionGraph(t, ` + metadata def DeferredKeeper; + item def Ping; + #DeferredKeeper action receive accept kept : Ping; + `) + if err != nil { + t.Fatalf("ToActionGraphWith: %v", err) + } + if accept := graph.Accepts[nodeNamed(t, graph, "receive")]; accept.Keeper { + t.Errorf("an accept marked by the model's own DeferredKeeper lowered as a keeper") + } +} diff --git a/internal/ir/lower/state_graph.go b/internal/ir/lower/state_graph.go index 913ec59ec0..843dd5a7f1 100644 --- a/internal/ir/lower/state_graph.go +++ b/internal/ir/lower/state_graph.go @@ -34,10 +34,6 @@ type StateGraph struct { // executable statements by the time it is reached. Behaviors map[*ast.StateNode]*StateBehaviors - // Deferred: state → the signals it defers, as the DeferredEvent annotations - // its declaration carries name them; absent for a state deferring none. - Deferred map[*ast.StateNode][]DeferredSignal - // HiddenStates are graph-only composite owners synthesized for parallel // regions. They execute behaviors but are not user-visible state visits. HiddenStates map[*ast.StateNode]bool @@ -640,7 +636,6 @@ func newStateGraph(scope *symbols.Scope, endpoints EndpointResolver) *StateGraph endpoints: endpoints, StateScopes: make(map[*ast.StateNode]*symbols.Scope), Behaviors: make(map[*ast.StateNode]*StateBehaviors), - Deferred: make(map[*ast.StateNode][]DeferredSignal), HiddenStates: make(map[*ast.StateNode]bool), HiddenRegionOf: make(map[*ast.StateNode]*ast.StateRegion), RegionState: make(map[*ast.StateRegion]*ast.StateNode), @@ -894,7 +889,6 @@ func collectStates(graph *StateGraph, state *ast.StateNode, parent *ast.StateNod graph.recordDecl(state) graph.StateScopes[state] = scope graph.Behaviors[state] = graph.lowerStateBehaviors(state, scope) - graph.recordDeferred(state, scope) if parent != nil { graph.ParentState[state] = parent } diff --git a/internal/ir/lower/state_metadata.go b/internal/ir/lower/state_metadata.go index 599625d78f..6e65eb1949 100644 --- a/internal/ir/lower/state_metadata.go +++ b/internal/ir/lower/state_metadata.go @@ -17,8 +17,13 @@ var pseudostateMetadataFQN = map[string]ast.PseudostateKind{ } // deferredEventMetadataFQN is the metadata definition a migration annotates a -// state with for each signal the source state deferred. -const deferredEventMetadataFQN = "MigrationMetadata::DeferredEvent" +// state with for each signal the source state deferred; deferredKeeperMetadataFQN +// the one marking the accept of the standard deferred-signal encoding that keeps +// the signal for the state. +const ( + deferredEventMetadataFQN = "MigrationMetadata::DeferredEvent" + deferredKeeperMetadataFQN = "MigrationMetadata::DeferredKeeper" +) // DeferredSignal is one signal a state defers, as a DeferredEvent annotation on // the state names it: `@MigrationMetadata::DeferredEvent { ref :>> signal : Sig; }`. @@ -121,30 +126,30 @@ func pseudostateAnnotationKeyword(kind ast.PseudostateKind) string { } } -// recordDeferred records the signals a state's declaration defers through its -// DeferredEvent annotations, read in the state's body scope, where they were written. -func (g *StateGraph) recordDeferred(state *ast.StateNode, scope *symbols.Scope) { - usage, ok := g.declOf[state].(*ast.Usage) - if !ok { - return - } - if deferred := deferredSignalsOf(g.resolver, scope, usage); len(deferred) > 0 { - g.Deferred[state] = deferred +// IsDeferredKeeper reports whether an accept node carries a DeferredKeeper +// annotation, read in the scope the node was written in. Detection is by +// resolved annotation type, never by the annotation's spelling. +func IsDeferredKeeper(resolver *resolve.Resolver, scope *symbols.Scope, node *ast.Usage) bool { + for _, a := range semantics.MetadataAnnotationsOf(node) { + if symbols.FQNOf(annotationSymbol(resolver, scope, node, a)) == deferredKeeperMetadataFQN { + return true + } } + return false } -// deferredSignalsOf reads the signals a state usage defers: one per DeferredEvent -// annotation whose body types its `signal`, in declaration order. Detection is -// by resolved annotation type, never by the annotation's spelling. -func deferredSignalsOf(resolver *resolve.Resolver, scope *symbols.Scope, usage *ast.Usage) []DeferredSignal { +// DeferredSignals reads the signals a state usage defers, for the scope it was +// written in: one per DeferredEvent annotation whose body types its `signal`, +// in declaration order, each with the state's body scope, where the body reads. +// Detection is by resolved annotation type, never by the annotation's spelling. +func DeferredSignals(resolver *resolve.Resolver, scope *symbols.Scope, usage *ast.Usage) []DeferredSignal { var deferred []DeferredSignal for _, a := range semantics.MetadataAnnotationsOf(usage) { - sym := annotationSymbolIn(resolver, []*symbols.Scope{scope}, a) - if symbols.FQNOf(sym) != deferredEventMetadataFQN { + if symbols.FQNOf(annotationSymbol(resolver, scope, usage, a)) != deferredEventMetadataFQN { continue } if signal := deferredSignalType(a.Node); signal != nil { - deferred = append(deferred, DeferredSignal{Type: signal, Scope: scope}) + deferred = append(deferred, DeferredSignal{Type: signal, Scope: childScope(scope, usage)}) } } return deferred @@ -161,14 +166,7 @@ func deferredSignalType(node *ast.PrefixMetadata) *ast.QualifiedName { if name, _ := ast.EffectiveName(u); name != "signal" { continue } - for _, rel := range u.Relationships { - if rel == nil || rel.Kind != ast.RelTyping { - continue - } - if qn, ok := rel.Target.(*ast.QualifiedName); ok { - return qn - } - } + return typingTarget(u) } return nil } diff --git a/internal/syntax/parser/behavior.go b/internal/syntax/parser/behavior.go index 19de83f97f..e7951e9d0f 100644 --- a/internal/syntax/parser/behavior.go +++ b/internal/syntax/parser/behavior.go @@ -545,7 +545,10 @@ func (p *Parser) parseActionMember() ast.Node { // An accept node is an action node (SysML.xtext ActionNode), so it stands // wherever a statement does: `accept e : E;`, `then action a accept e : E { … }`. if p.atAcceptNode() { - return p.parseBodyMember() + if len(prefixes) == 0 { + return p.parseBodyMember() + } + return p.parseAcceptNode(start, ast.VisibilityDefault, nil, prefixes) } // The words of our own node notation are names the lexer does not reserve, @@ -2709,24 +2712,30 @@ func (p *Parser) parseMemberLeadingSuccession(start int) ast.Node { // (SysML.xtext `AcceptNode`): the `accept` keyword, optionally preceded by the // `action` keyword and the node's own name. func (p *Parser) atAcceptNode() bool { - if p.atKeyword("accept") { + return p.atAcceptNodeAt(0) +} + +// atAcceptNodeAt is atAcceptNode for the member beginning i tokens ahead, past +// the prefix metadata a member may open with (`#M action a accept e : E;`). +func (p *Parser) atAcceptNodeAt(i int) bool { + if tok := p.peekN(i); tok.Kind == lexer.Keyword && tok.KeywordID == "accept" { return true } - if !p.atKeyword("action") { + if tok := p.peekN(i); tok.Kind != lexer.Keyword || tok.KeywordID != "action" { return false } - if p.peekN(1).Kind == lexer.Keyword && p.peekN(1).KeywordID == "accept" { + if p.peekN(i+1).Kind == lexer.Keyword && p.peekN(i+1).KeywordID == "accept" { return true } - switch p.peekN(1).Kind { + switch p.peekN(i + 1).Kind { case lexer.Identifier, lexer.UnrestrictedName, lexer.Lt: default: return false } // `action accept …`, and `action name accept …`, whose // identification spends four tokens before the keyword. - for i := 1; i <= 5; i++ { - tok := p.peekN(i) + for j := i + 1; j <= i+5; j++ { + tok := p.peekN(j) if tok.Kind == lexer.Keyword { return tok.KeywordID == "accept" } @@ -2745,7 +2754,7 @@ func (p *Parser) atAcceptNode() bool { // body like any other action node. // // ('action' ?)? accept ('via' )? (';' | '{' … '}') -func (p *Parser) parseAcceptNode(start int, vis ast.Visibility, trivia []ast.Trivia) ast.Node { +func (p *Parser) parseAcceptNode(start int, vis ast.Visibility, trivia []ast.Trivia, prefixes []*ast.PrefixMetadata) ast.Node { var ident ast.Identification // `action accept …` names no node of its own, so the keyword must not be read // as the declaration's name. @@ -2755,9 +2764,10 @@ func (p *Parser) parseAcceptNode(start int, vis ast.Visibility, trivia []ast.Tri p.advance() // consume 'accept' action := &ast.Usage{ - Kind: ast.UsageAction, - Keyword: "action", - Ident: ident, + Prefixes: prefixes, + Kind: ast.UsageAction, + Keyword: "action", + Ident: ident, } param := p.parsePayloadParameter() diff --git a/internal/syntax/parser/defusage.go b/internal/syntax/parser/defusage.go index 3e1da38107..d8291d39b0 100644 --- a/internal/syntax/parser/defusage.go +++ b/internal/syntax/parser/defusage.go @@ -2867,6 +2867,9 @@ func (p *Parser) parseBodyMember() ast.Node { if p.leadingPrefixIsActionNode() { return p.parseActionMember() } + if p.atAcceptNodeAt(p.prefixLookahead()) { + return p.parseAcceptNode(start, vis, trivia, p.parsePrefixMetadata()) + } // Delegate to parseDefUsage which handles prefixes; a prefixed // dependency keeps its prefixes the way a namespace member does. var inner ast.Node @@ -3040,7 +3043,7 @@ func (p *Parser) parseBodyMember() ast.Node { // (`accept when x > 1`) — and is parsed by the one payload parser triggers // also use, so every spelling reaches lowering the same way. if p.atAcceptNode() { - return p.parseAcceptNode(start, vis, trivia) + return p.parseAcceptNode(start, vis, trivia, nil) } // A transition usage stating its ends (SysML.xtext `TransitionUsage`): diff --git a/internal/translate/deferred/deferred.go b/internal/translate/deferred/deferred.go index a022fac3ff..c7c3a15983 100644 --- a/internal/translate/deferred/deferred.go +++ b/internal/translate/deferred/deferred.go @@ -43,9 +43,11 @@ type Encoding struct { // Buffer and Flush name the do and exit actions; Split names the fork that // runs the accept loops beside each other and the state's own do behavior. Buffer, Split, Flush string - // Including refers to SequenceFunctions::including from the state's scope. - Including string - Signals []Signal + // Including refers to SequenceFunctions::including from the state's scope; + // Keeper to MigrationMetadata::DeferredKeeper, the annotation marking each + // accept loop's accept as the one keeping the signal for the state. + Including, Keeper string + Signals []Signal } // Own is a state's own do or exit behavior rendered as the nested action the @@ -117,7 +119,7 @@ func (e *Encoding) Do(w Writer, own func() Own) { if l.Via != "" { via = " via " + l.Via } - w.Line("action " + l.Receive + " accept " + l.Payload + " : " + l.Accept + via + ";") + w.Line("#" + e.Keeper + " action " + l.Receive + " accept " + l.Payload + " : " + l.Accept + via + ";") w.Line("then action " + l.Keep + " { assign " + k.Buffer + " := " + e.Including + "(" + k.Buffer + ", " + l.Receive + "." + l.Payload + "); }") w.Line("then " + l.Receive + ";") w.MadeUp(l.Receive) diff --git a/internal/translate/deferred/deferred_test.go b/internal/translate/deferred/deferred_test.go index 14a61f1a7c..922ee4ed46 100644 --- a/internal/translate/deferred/deferred_test.go +++ b/internal/translate/deferred/deferred_test.go @@ -33,6 +33,7 @@ func oneSignal() *Encoding { return &Encoding{ Buffer: "keepDoor", Split: "keepDoorSplit", Flush: "flushDoor", Including: "SequenceFunctions::including", + Keeper: "MigrationMetadata::DeferredKeeper", Signals: []Signal{{ Ref: "Door", Buffer: "deferredDoor", Item: "kept", Clear: "clearDoor", Loops: []Loop{{Receive: "receiveDoor", Keep: "keepDoorOnce", Payload: "door", Accept: "Door"}}, @@ -49,7 +50,7 @@ func TestOneSignalOneRouteIsALoopWithNoFork(t *testing.T) { want := `item deferredDoor : Door[*] ordered; do action keepDoor { first start then receiveDoor; - action receiveDoor accept door : Door; + #MigrationMetadata::DeferredKeeper action receiveDoor accept door : Door; then action keepDoorOnce { assign deferredDoor := SequenceFunctions::including(deferredDoor, receiveDoor.door); } then receiveDoor; } @@ -92,10 +93,10 @@ do action keepDoor { then receiveDoor; then receiveDoorViaP; action work { } - action receiveDoor accept door : Door; + #MigrationMetadata::DeferredKeeper action receiveDoor accept door : Door; then action keepDoorOnce { assign deferredDoor := SequenceFunctions::including(deferredDoor, receiveDoor.door); } then receiveDoor; - action receiveDoorViaP accept door : Door via p; + #MigrationMetadata::DeferredKeeper action receiveDoorViaP accept door : Door via p; then action keepDoorViaP { assign deferredDoor := SequenceFunctions::including(deferredDoor, receiveDoorViaP.door); } then receiveDoorViaP; } diff --git a/internal/translate/migrate/states.go b/internal/translate/migrate/states.go index e037f5e279..4c1839e982 100644 --- a/internal/translate/migrate/states.go +++ b/internal/translate/migrate/states.go @@ -1363,8 +1363,12 @@ func (d *deferrals) encoded() bool { return len(d.kept) > 0 } -// deferredEventFQN names the library metadata marking a deferred signal. -const deferredEventFQN = "MigrationMetadata::DeferredEvent" +// deferredEventFQN names the library metadata marking a deferred signal; +// deferredKeeperFQN the one marking the accept that keeps it for the state. +const ( + deferredEventFQN = "MigrationMetadata::DeferredEvent" + deferredKeeperFQN = "MigrationMetadata::DeferredKeeper" +) // deferrals reads a state's deferrable triggers: v2 defers the signal a // transition would accept, so no other event kind can be, and a signal a @@ -1988,10 +1992,14 @@ func (s *stateRegion) encoding(v *sysmlv1.Element, d *deferrals) *deferred.Encod Split: d.split, Flush: writeName(d.flush), Including: "SequenceFunctions::including", + Keeper: deferredKeeperFQN, } if s.m.shadowsLibrary("SequenceFunctions", v) { e.Including = "$::" + e.Including } + if s.m.shadowsLibrary("MigrationMetadata", v) { + e.Keeper = "$::" + e.Keeper + } for _, k := range d.kept { sig := deferred.Signal{ Ref: s.m.ref(k.sig, v), diff --git a/internal/workspace/libs/stdlib.snapshot b/internal/workspace/libs/stdlib.snapshot index 98e64cb4d3..845d74b9ff 100644 Binary files a/internal/workspace/libs/stdlib.snapshot and b/internal/workspace/libs/stdlib.snapshot differ diff --git a/internal/workspace/libs/stdlib/OpenSysML Libraries/MigrationMetadata.sysml b/internal/workspace/libs/stdlib/OpenSysML Libraries/MigrationMetadata.sysml index fcaa0b31b2..1537f13755 100644 --- a/internal/workspace/libs/stdlib/OpenSysML Libraries/MigrationMetadata.sysml +++ b/internal/workspace/libs/stdlib/OpenSysML Libraries/MigrationMetadata.sysml @@ -17,6 +17,15 @@ standard library package MigrationMetadata { ref signal : Base::Anything[1]; } + metadata def DeferredKeeper { + doc /* The annotated accept keeps the deferred signal it accepts for + * the state that defers it: the accept loop of the standard + * encoding stores each occurrence in the state's buffer rather than + * consuming it as the state's own behavior would, so the state's + * other accepts of the signal take an occurrence first. Written as + * `#DeferredKeeper action receive accept kept : Sig;`. */ + } + metadata def LibraryNameAvoided { doc /* The annotated top-level package was named, in the source model, * like a standard library package, which a qualified name starting diff --git a/packaging/man/man1/sysml.1 b/packaging/man/man1/sysml.1 index ebf9212dee..37c37ce13f 100644 --- a/packaging/man/man1/sysml.1 +++ b/packaging/man/man1/sysml.1 @@ -42,8 +42,9 @@ Judge the model as conforming SysML v2: notation no pinned production admits is an error, not a warning; a SysML v1 migration writes none of it .TP .BR \-disable\-lint " \fIcode\fP" -Leave this lint out of the model's diagnostics: undeclared\-signal or -port\-type\-mismatch, comma\-separated or repeated +Leave this lint out of the model's diagnostics: undeclared\-signal, +port\-type\-mismatch or deferred\-keeper\-unmarked, comma\-separated or +repeated .TP .B \-no\-record\-cache Parse every file loaded and hold it loaded, reading no interface record from diff --git a/tests/migrate/behavior_more_test.go b/tests/migrate/behavior_more_test.go index 0cba4407fb..8d7f7f2960 100644 --- a/tests/migrate/behavior_more_test.go +++ b/tests/migrate/behavior_more_test.go @@ -256,7 +256,7 @@ func wantDeferredDoorEncoding(t *testing.T, r *migrate.Result) { "item deferred : Door[*] ordered;", "do action buffer {", "first start then receive;", - "action receive accept kept : Door;", + "#MigrationMetadata::DeferredKeeper action receive accept kept : Door;", "then action keep { assign deferred := SequenceFunctions::including(deferred, receive.kept); }", "then receive;", "metadata MigrationMetadata::SynthesizedName about receive, keep;", @@ -391,10 +391,10 @@ func checkDeferredSignalsAreKeptAndReplayed(t *testing.T, r *migrate.Result) { "then receiveBeep;", "action run {", "assign context.ticks := context.ticks + 1;", - "action receiveAlarm accept keptAlarm : Alarm;", + "#MigrationMetadata::DeferredKeeper action receiveAlarm accept keptAlarm : Alarm;", "then action keepAlarm { assign deferredAlarm := SequenceFunctions::including(deferredAlarm, receiveAlarm.keptAlarm); }", "then receiveAlarm;", - "action receiveBeep accept keptBeep : Beep;", + "#MigrationMetadata::DeferredKeeper action receiveBeep accept keptBeep : Beep;", "then action keepBeep { assign deferredBeep := SequenceFunctions::including(deferredBeep, receiveBeep.keptBeep); }", "then receiveBeep;", "metadata MigrationMetadata::SynthesizedName about split, run, receiveAlarm, keepAlarm, receiveBeep, keepBeep;", @@ -670,7 +670,7 @@ func TestStrictAcceptViaContextPortFixture(t *testing.T) { "in ref context : ActivityReceiver[1];", "action receive accept Ping via context.p;", "transition first Waiting accept Go via context.p then Done;", - "action 'receive via p' accept 'kept via p' : Ping via context.p;", + "#MigrationMetadata::DeferredKeeper action 'receive via p' accept 'kept via p' : Ping via context.p;", "action 'receive via p' accept 'ping via p' : Ping via p;", "exhibit state life : Life { in ref :>> context = this; }", "perform action await : Await { in ref :>> context = this; }", @@ -702,13 +702,13 @@ func TestStrictDeferredSignalsAreKeptByEveryRoute(t *testing.T) { "then receiveCmd;", "then 'receiveCmd via inbox';", "then 'receivePing via side';", - "action receiveCmd accept keptCmd : Cmd;", + "#MigrationMetadata::DeferredKeeper action receiveCmd accept keptCmd : Cmd;", "then action keepCmd { assign deferredCmd := SequenceFunctions::including(deferredCmd, receiveCmd.keptCmd); }", "then receiveCmd;", - "action 'receiveCmd via inbox' accept 'keptCmd via inbox' : Cmd via context.inbox;", + "#MigrationMetadata::DeferredKeeper action 'receiveCmd via inbox' accept 'keptCmd via inbox' : Cmd via context.inbox;", "then action 'keepCmd via inbox' { assign deferredCmd := SequenceFunctions::including(deferredCmd, 'receiveCmd via inbox'.'keptCmd via inbox'); }", "then 'receiveCmd via inbox';", - "action 'receivePing via side' accept 'keptPing via side' : Ping via context.side;", + "#MigrationMetadata::DeferredKeeper action 'receivePing via side' accept 'keptPing via side' : Ping via context.side;", "then action 'keepPing via side' { assign deferredPing := SequenceFunctions::including(deferredPing, 'receivePing via side'.'keptPing via side'); }", "then 'receivePing via side';", "exit action flush {", @@ -769,7 +769,7 @@ func TestStrictDeferralKeepsRoutesAPortTransitionSkips(t *testing.T) { wantNoLine(t, r.Notation, "defer Cmd;") for _, line := range []string{ "item deferredCmd : Cmd[*] ordered;", - "action receiveCmd accept keptCmd : Cmd;", + "#MigrationMetadata::DeferredKeeper action receiveCmd accept keptCmd : Cmd;", "then action keepCmd { assign deferredCmd := SequenceFunctions::including(deferredCmd, receiveCmd.keptCmd); }", "for keptCmd in deferredCmd { send keptCmd to self; }", "transition first Waiting accept Cmd via context.inbox then Working;", @@ -853,7 +853,7 @@ func TestStrictDeferralSurvivesInactiveSubstateTransition(t *testing.T) { for _, line := range []string{ "state Busy {", "item deferred : Door[*] ordered;", - "action receive accept kept : Door;", + "#MigrationMetadata::DeferredKeeper action receive accept kept : Door;", "transition first Heating accept Door then Opened;", } { wantLine(t, r.Notation, line) @@ -947,7 +947,7 @@ func TestStrictDeferralOutlivesTransitionWithNoForm(t *testing.T) { for _, line := range []string{ "state Off {", "item deferred : Door[*] ordered;", - "action receive accept kept : Door;", + "#MigrationMetadata::DeferredKeeper action receive accept kept : Door;", } { wantLine(t, r.Notation, line) } @@ -1117,7 +1117,7 @@ func TestStrictDeferralOutlivesGuardedCompletionTransition(t *testing.T) { for _, line := range []string{ "state Off {", "item deferred : Door[*] ordered;", - "action receive accept kept : Door;", + "#MigrationMetadata::DeferredKeeper action receive accept kept : Door;", "transition first Off if context.ready then Done;", } { wantLine(t, r.Notation, line) @@ -1195,7 +1195,7 @@ func TestStrictDeferralSurvivesInternalTransition(t *testing.T) { wantNoLine(t, r.Notation, "defer Door;") for _, line := range []string{ "item deferred : Door[*] ordered;", - "action receive accept kept : Door;", + "#MigrationMetadata::DeferredKeeper action receive accept kept : Door;", "transition first Off accept Tick", } { wantLine(t, r.Notation, line) @@ -1275,7 +1275,7 @@ func TestStrictDeferralYieldsToTransitionOnGeneralSignal(t *testing.T) { for _, line := range []string{ "@MigrationMetadata::DeferredEvent { ref :>> signal : Alarm; }", "item deferred : Stop[*] ordered;", - "action receive accept kept : Stop;", + "#MigrationMetadata::DeferredKeeper action receive accept kept : Stop;", "transition first Busy accept Notification then Idle;", } { wantLine(t, r.Notation, line) @@ -1299,7 +1299,7 @@ func TestStrictDeferralYieldsToTransitionOnGeneralSignal(t *testing.T) { r = migrateDocumentOptions(t, signals+special, block, migrate.Options{Strict: true}) for _, line := range []string{ "item deferredNotification : Notification[*] ordered;", - "action receiveNotification accept keptNotification : Notification;", + "#MigrationMetadata::DeferredKeeper action receiveNotification accept keptNotification : Notification;", "transition first Busy accept Alarm then Idle;", } { wantLine(t, r.Notation, line) @@ -1359,7 +1359,7 @@ func TestStrictOverlappingDeferralsKeepEachOccurrenceOnce(t *testing.T) { "@MigrationMetadata::DeferredEvent { ref :>> signal : Alarm; }", "@MigrationMetadata::DeferredEvent { ref :>> signal : Notification; }", "item deferred : Event[*] ordered;", - "action receive accept kept : Event;", + "#MigrationMetadata::DeferredKeeper action receive accept kept : Event;", } { wantLine(t, r.Notation, line) } @@ -1422,7 +1422,7 @@ func TestStrictDeferralNamesShadowNothingItRefersTo(t *testing.T) { for _, line := range []string{ "ref item SequenceFunctions : Stop;", "item deferred : receive[*] ordered;", - "action receive2 accept kept : receive;", + "#MigrationMetadata::DeferredKeeper action receive2 accept kept : receive;", "then action keep { assign deferred := $::SequenceFunctions::including(deferred, receive2.kept); }", "then receive2;", } { @@ -1478,7 +1478,7 @@ func TestStrictDeferralWithoutRunnableDoBehavior(t *testing.T) { "do action buffer {", "first start then receive;", "/* do action Aux is written as a state def, which no state runs */", - "action receive accept kept : Door;", + "#MigrationMetadata::DeferredKeeper action receive accept kept : Door;", } { wantLine(t, r.Notation, line) } diff --git a/tests/migrate/testdata/xmi/accept_via_context_port.golden.sysml b/tests/migrate/testdata/xmi/accept_via_context_port.golden.sysml index d2d9e3f71c..93c99ebf17 100644 --- a/tests/migrate/testdata/xmi/accept_via_context_port.golden.sysml +++ b/tests/migrate/testdata/xmi/accept_via_context_port.golden.sysml @@ -20,7 +20,7 @@ part def Receiver { item deferred : Ping[*] ordered; do action buffer { first start then 'receive via p'; - action 'receive via p' accept 'kept via p' : Ping via context.p; + #MigrationMetadata::DeferredKeeper action 'receive via p' accept 'kept via p' : Ping via context.p; then action 'keep via p' { assign deferred := SequenceFunctions::including(deferred, 'receive via p'.'kept via p'); } then 'receive via p'; metadata MigrationMetadata::SynthesizedName about 'receive via p', 'keep via p'; diff --git a/tests/parser/negative_test.go b/tests/parser/negative_test.go index 3060f85363..e37403a16d 100644 --- a/tests/parser/negative_test.go +++ b/tests/parser/negative_test.go @@ -317,6 +317,8 @@ func TestNegative(t *testing.T) { {"flow_from_without_to", "action def A { action a; flow x from a; }"}, {"flow_named_from_no_source", "action def A { flow x from to b; }"}, {"accept_when_no_condition", "action def A { accept when; }"}, + {"prefixed_accept_no_payload", "action def A { metadata def M; #M action a accept ; }"}, + {"prefixed_accept_no_terminator", "action def A { metadata def M; #M action a accept e : E }"}, {"accept_at_no_instant", "action def A { accept at; }"}, {"accept_no_payload", "action def A { accept; }"}, {"accept_subsets_no_event", "action def A { action i accept :>; }"}, diff --git a/tests/parser/testdata/parse/accept_action_prefix_metadata.golden b/tests/parser/testdata/parse/accept_action_prefix_metadata.golden new file mode 100644 index 0000000000..ae8ed1c4b3 --- /dev/null +++ b/tests/parser/testdata/parse/accept_action_prefix_metadata.golden @@ -0,0 +1,52 @@ +(RootNamespace + (Membership visibility="default" + (Package name="AcceptPrefixMetadata" library=false standard=false + (Membership visibility="default" + (Definition kind="metadata" abstract=false variation=false name="M")) + (Membership visibility="default" + (Definition kind="item" abstract=false variation=false name="Scene")) + (Membership visibility="default" + (Definition kind="port" abstract=false variation=false name="Camera")) + (Membership visibility="default" + (Definition kind="action" abstract=false variation=false name="Watch" + (Membership visibility="default" + (Usage kind="port" name="lens" ref=false direction="none" composite=false derived=false ordered=false nonunique=false + (Relationship kind="typing" target=Camera + (*ast.QualifiedName)))) + (Membership visibility="default" + (Usage kind="action" name="framed" ref=false direction="none" composite=false derived=false ordered=false nonunique=false + (PrefixMetadata type="M") + (Relationship kind="via" target=lens + (*ast.QualifiedName)) + (Membership visibility="default" + (Usage kind="attribute" name="scene" ref=true direction="out" composite=false derived=false ordered=false nonunique=false + (Relationship kind="typing" target=Scene + (*ast.QualifiedName)))))) + (Membership visibility="default" + (Usage kind="action" name=" framed2" ref=false direction="none" composite=false derived=false ordered=false nonunique=false + (PrefixMetadata type="M") + (Membership visibility="default" + (Usage kind="attribute" name="scene" ref=true direction="out" composite=false derived=false ordered=false nonunique=false + (Relationship kind="typing" target=Scene + (*ast.QualifiedName)))))) + (Membership visibility="default" + (Usage kind="action" name="" ref=false direction="none" composite=false derived=false ordered=false nonunique=false + (PrefixMetadata type="M") + (Membership visibility="default" + (Usage kind="attribute" name="scene" ref=true direction="out" composite=false derived=false ordered=false nonunique=false + (Relationship kind="typing" target=Scene + (*ast.QualifiedName)))))) + (Membership visibility="default" + (Usage kind="action" name="marked" ref=false direction="none" composite=false derived=false ordered=false nonunique=false + (PrefixMetadata type="$::AcceptPrefixMetadata::M") + (Membership visibility="default" + (Usage kind="attribute" name="scene" ref=true direction="out" composite=false derived=false ordered=false nonunique=false + (Relationship kind="typing" target=Scene + (*ast.QualifiedName)))))) + (Membership visibility="default" + (Usage kind="action" name="done" ref=false direction="none" composite=false derived=false ordered=false nonunique=false + (Membership visibility="default" + (Usage kind="attribute" name="scene" ref=true direction="out" composite=false derived=false ordered=false nonunique=false + (Relationship kind="typing" target=Scene + (*ast.QualifiedName)))))) + (SuccessionEdge source="marked" target="done")))))) \ No newline at end of file diff --git a/tests/parser/testdata/parse/accept_action_prefix_metadata.sysml b/tests/parser/testdata/parse/accept_action_prefix_metadata.sysml new file mode 100644 index 0000000000..84f7a87175 --- /dev/null +++ b/tests/parser/testdata/parse/accept_action_prefix_metadata.sysml @@ -0,0 +1,16 @@ +// An accept node takes prefix metadata like any usage (SysML.xtext +// PrefixMetadataMember): named or anonymous, with a body or without, and +// through `$::` where a package shadows the metadata's library. +package AcceptPrefixMetadata { + metadata def M; + item def Scene; + port def Camera; + action def Watch { + port lens : Camera; + #M action framed accept scene : Scene via lens; + #M action framed2 accept scene : Scene; + #M accept scene : Scene; + #$::AcceptPrefixMetadata::M action marked accept scene : Scene { } + then action done accept scene : Scene; + } +} diff --git a/tests/testdata/passes/deferred_keeper.golden b/tests/testdata/passes/deferred_keeper.golden new file mode 100644 index 0000000000..bf33f55727 --- /dev/null +++ b/tests/testdata/passes/deferred_keeper.golden @@ -0,0 +1 @@ +12:5 warning [lint/deferred-keeper-unmarked] accept of deferred signal Ping is not marked #MigrationMetadata::DeferredKeeper, so it is an ordinary accept, not the keeping loop; re-migrate the model or mark it diff --git a/tests/testdata/passes/deferred_keeper.sysml b/tests/testdata/passes/deferred_keeper.sysml new file mode 100644 index 0000000000..5069e869ca --- /dev/null +++ b/tests/testdata/passes/deferred_keeper.sysml @@ -0,0 +1,55 @@ +package DeferredKeeper { + item def Ping; + item def Go; + + state def Legacy { + entry; then busy; + state busy { + @MigrationMetadata::DeferredEvent { ref :>> signal : Ping; } + item deferred : Ping[*] ordered; + do action buffer { + first start then receive; + action receive accept kept : Ping; + then action keep { assign deferred := SequenceFunctions::including(deferred, receive.kept); } + then receive; + } + exit action flush { + for kept in deferred { send kept to self; } + then action clear { assign deferred := (); } + } + } + state ready; + transition first busy accept Go then ready; + } + + state def Marked { + entry; then busy; + state busy { + @MigrationMetadata::DeferredEvent { ref :>> signal : Ping; } + item deferred : Ping[*] ordered; + do action buffer { + first start then receive; + #MigrationMetadata::DeferredKeeper action receive accept kept : Ping; + then action keep { assign deferred := SequenceFunctions::including(deferred, receive.kept); } + then receive; + } + exit action flush { + for kept in deferred { send kept to self; } + then action clear { assign deferred := (); } + } + } + state ready; + transition first busy accept Go then ready; + } + + state def Undeferring { + entry; then busy; + state busy { + do action work { + action receive accept kept : Ping; + } + } + state ready; + transition first busy accept Go then ready; + } +} diff --git a/tools/referee/pssm/emit.go b/tools/referee/pssm/emit.go index ef8cc56ed7..20d15b47de 100644 --- a/tools/referee/pssm/emit.go +++ b/tools/referee/pssm/emit.go @@ -572,7 +572,7 @@ func (e *emitter) kept(state *Vertex, where string) (*keeping, error) { names = append(names, name) } } - enc := &deferred.Encoding{Including: "SequenceFunctions::including"} + enc := &deferred.Encoding{Including: "SequenceFunctions::including", Keeper: "MigrationMetadata::DeferredKeeper"} for _, name := range names { e.signals[name] = true base := "deferred"