Repository navigation
fix(runtime): identify a deferred signal's keeping accept by the DeferredKeeper annotation the migrator writes - #808
Merged
Conversation
Contributor
Author
|
I'll fix CI failures and address comments from users with write access. I'll skip comments containing "(aside)".
|
…rredKeeper annotation the migrator writes The runtime recognized the keeping accept of a deferring state's do action by its shape — a root-level accept of a signal the state defers — so an ordinary accept of the same signal written 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 standard encoding now declares its keeper: the shared deferred-signal writer, used by the SysML v1 migrator and the PSSM referee, marks each keeping loop's accept `#MigrationMetadata::DeferredKeeper`, a new definition of the bundled MigrationMetadata library. Lowering reads the annotation by resolved type into Accept.Keeper, and the runtime's keeps consults that alone; StateGraph.Deferred, which the shape inference read, is removed. The parser takes prefix metadata on an accept node, as PrefixMetadataMember allows, so the mark is ordinary notation. A conformance case exercises a direct accept beside the keeping loop under every scheduling policy; the lowering test covers resolution by type against a homonymous definition. Co-Authored-By: jason.han <hanhuijun@gmail.com>
… the DeferredKeeper marker The runtime knows the keeping accept of the standard deferred-signal encoding by its MigrationMetadata::DeferredKeeper annotation alone, so output migrated before the marker existed runs the loop as an ordinary accept that consumes each occurrence. The deferred-keeper-unmarked lint reports each accept of a deferred signal at the root of the do action of a state annotated MigrationMetadata::DeferredEvent when no accept of that signal there carries the marker, as a warning in every mode: the model still analyses and runs, and re-migrating it or writing the marker clears it. Both annotations are known by resolved type, not spelling; an accept nested below the root, one beside a marked keeper, or one under a state deferring nothing is the ordinary accept it is written as and is not reported. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…egistry Co-Authored-By: jason.han <hanhuijun@gmail.com>
devin-ai-integration
Bot
force-pushed
the
fix/deferred-keeper-marker
branch
from
October 2, 2026 05:37
7b6ab37 to
2facaf3
Compare
…red-keeper fixture The new passes/deferred_keeper.sysml fixture joins the testdata root: one only-ours row, the deferred-keeper-unmarked lint it exists to draw, and thirteen only-pilot rows that follow from the reference having no MigrationMetadata library; both are adjudicated in the differential record. The examples digest moves with the self-model's pass registry entry alone. Documentation counts regenerated with make docs-counts. Co-Authored-By: jason.han <hanhuijun@gmail.com>
Merged
6 tasks done
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What and why
Follow-up to #792's remaining review finding: the runtime identified the accept that keeps a deferred signal (the accept loop of the standard deferral encoding) by its shape — an accept at the root of a deferring state's do action, typed by a signal the state defers — so a hand-written ordinary accept of the same signal at that level was indistinguishable from the generated keeper, and an occurrence arriving while both were parked could be kept rather than taken, depending on the schedule. The migrator never writes that shape (a state's own do behavior becomes a nested action), but the runtime rule was still inference, not declaration.
The keeping accept is now declared, and the declaration flows through the layers losslessly:
MigrationMetadata.sysmlgainsmetadata def DeferredKeeperbesideDeferredEvent.internal/translate/deferred(shared by the v1 migrator and the PSSM emitter) takesEncoding.Keeperand writes the marker on every keeping accept; both producers configure it (the migrator$::-qualifies it when the package shadowsMigrationMetadata).#M action a accept e : E;/#M accept e : E;asPrefixMetadataMemberallows for any usage member; previously onlymetadata M about a;could annotate an accept.lower.Accept.Keeper. The oldStateGraph.Deferredside table (DeferredSignal,recordDeferred,ActionExecutor.deferred) existed only to feed the shape heuristic and is removed — nothing else read it.keepsconsultsAccept.Keeper; the keeper still yields to any other accept able to take the occurrence that step (not one held for an arrival it awaits), and every unmarked accept is an ordinary consumer wherever it stands.Pre-marker output: a diagnostic, not inference. Per the maintainer's decision on the review question, the runtime carries no compatibility path for migrated output written before the marker; instead the checker warns. The new lint
deferred-keeper-unmarked(internal/check/passes/lint_deferred_keeper.go, name-resolution level, non-blocking like the other lints, switchable with--disable-lint) fires for exactly the shape the old inference recognized: a state carrying a resolvedMigrationMetadata::DeferredEventannotation whose do action has, at its root, an accept typed by one of the deferred signals while no accept of that signal there carriesMigrationMetadata::DeferredKeeper:Both annotations are matched by resolved type (import, alias and
$::MigrationMetadata::…all count; a homonymousmetadata defof the model does not). It is silent on a marked loop, on an unmarked accept under a state withoutDeferredEvent, on an accept nested below the do action's root, and on a bare accept beside a marked keeper — the ordinary consumer the marker exists to tell apart. The model still analyses and runs with the warning present.Specification basis
UML 2.5.1 §14.2.3.9.3 (deferred events: an occurrence a state defers is retained until a state that does not defer it is active, while an enabled transition or the state's own behavior may consume it) — the migrated encoding is unchanged; what moves is how the runtime tells the keeping accept from the state's own accepts. SysML v2 textual notation
PrefixMetadataMemberfor the marker form. The deferred-signal row indocs/project/spec-compliance.mdis rewritten to describe the declared keeper (status unchanged, ✅);docs/reference/sysml-v1-migration.mdand the migration guide document the marker.How it was verified
New/updated tests
tests/parser/testdata/parse/accept_action_prefix_metadata.sysml; negativesprefixed_accept_no_payload,prefixed_accept_no_terminator;TestStdlibConformanceclean.TestAccept_KeeperIsReadByResolvedAnnotation(qualified, imported and locally-spelled annotation → keeper; unmarked accept → not),TestAccept_KeeperIgnoresAHomonymousDefinition(a model's ownDeferredKeeperdef does not mark).state_deferred_do_direct_accept_takes— a deferring state whose do action has the marked keeping loop and an ordinary accept of the same signal beside it; the ordinary accept takes the occurrence (heard == 1). With the marker removed from the fixture the old inference is gone and the case fails (heard: value = 0, want 1), so the marker is load-bearing. Existingstate_deferred_do_accept_takes_before_keeping/…_held_keepsfixtures carry the marker.internal/translate/deferredtests andtests/migrate/behavior_more_test.goassert the marker on every generated keeping accept (plain, named,viaport) and its absence on ordinary accepts; goldenaccept_via_context_portregenerated.TestDeferredKeeperUnmarkedLint(positive on an unmarked loop; silent on a marked loop, on a state withoutDeferredEvent, on a nested accept, on a bare accept beside a marked keeper, on an unrelated signal and on a homonymous model-defined annotation; resolution through import and alias; two unmarked accepts both warned) and the oracle fixturetests/testdata/passes/deferred_keeper.sysml+.golden(TestPassesGoldenDeferredKeeper);TestSelfModelPassRegistryMatchesImplementationmodels the new pass.Gates (all from the branch rebased on
develop@ 80ce1c2)Pilot differential (
docs/project/pilot-differential-baseline.json, re-recorded against the provisioned2026-08validators): the newtests/testdata/passes/deferred_keeper.sysmlfixture adds one file to thetestdataroot — 1 only-ours row (thedeferred-keeper-unmarkedwarning it exists to draw) and 13 only-pilot rows, all from the reference having noMigrationMetadatalibrary (the same cause as theDocumentQueriesrows ofself-model/document.sysml). Headline380 → 381files,345fully agreeing unchanged, only-ours40 → 41, only-pilot1616 → 1629; no pre-existing row moved. Theexamplesdigest moves with the self-model's pass-registry entry alone (noexamplesrow changed). Both rows are adjudicated indocs/project/pilot-differential.md; the generated README/architecture figures and the skill headlines were refreshed bymake docs-counts/ the baseline tests.TMT (
TMT-2024x.mdzip+TMT_mtip.xml,develop@ 80ce1c2 vs this branch, same binary flags,-seed 1)-validate: 0 errors before and after (3823 warnings both).deferred-keeper-unmarked: 0 on this branch's migratedTMT.sysml(the migrator marks every keeper it writes); run againstdevelop's pre-markerTMT.sysml, this branch's checker reports exactly 1593 — one per keeping accept, the same count as the marker lines below.TMT.sysmldiffers from develop's only by the 1593#MigrationMetadata::DeferredKeeperlines; migration report byte-identical.-compare-results -seed 1:completed 31 / stopped 10 / compared 25 / comparable 169 / exact 142 / differ 14before and after; the compare output is byte-identical (no observable or stop changed), as expected — the heuristic and the marker agree on every keeper the migrator writes.-strict(migrate, validate and compare all with-strict):-validate0 errors before and after;completed 31 / stopped 10 / compared 25 / comparable 169 / exact 142 / differ 14before and after, compare output and migration report byte-identical;TMT.sysmlagain differs only by the 1593 marker lines.Checklist
make testandmake lintpass locally (fullgo test ./...andmake lintgreen; race run scoped to the touched packages, CI runs the full race suite)docs/reference/diagnostics.md,cli.md,sysml-v1-migration.md, guide, spec-compliance row, adjudications,sysml(1)regeneratedchanges/unreleased/<slug>.<section>.md, not as an edit toCHANGELOG.mdmake docs-countsrun if a gate count moved (compliance rows need nothing: the census is counted at docs build) — pilot-differential baseline re-recorded for the new fixture,make docs-countsrunF4,K5) in the body, docs, or changelogLink to Devin session: https://nasa-jpl-demo.devinenterprise.com/sessions/d4b4403c1dd54e0390049c64e3535b0f
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/d4b4403c1dd54e0390049c64e3535b0f?variant=devin
Requested by: @HuiJun