refactor(lang): remove the defer state-body extension - #694
Merged
Merged
Conversation
`defer <event> [, <event>]*;` in a state body was an OpenSysML extension SysML v2 has no counterpart for. `defer` is now an ordinary identifier; a legacy defer member is one `defer-notation-removed` parse error with an ErrorNode. The lexer, parser, AST, codec, resolver, checker, IR lowering, views, runtime deferral queue and priority rule, REPL/gRPC/client surfaces, RDF terms, grammars and docs lose the extension; a deferred signal is modelled with the standard ordered buffer, do-action accept loop and exit-action flush, which the SysML v1 migrator and the PSSM referee now write through one shared package (internal/translate/deferred). Extension-only conformance fixtures are replaced with standard-notation ones; the outranking scenarios pin the standard behaviour (a transition that is enabled fires). PSSM buckets move 60/12/30/1 -> 52/12/34/5, the rejection oracle's x05 case rejects in both modes, and a legacy Turtle graph carrying sysx:DeferMember/sysx:deferredEvent is refused with a diagnostic. Co-Authored-By: jason.han <hanhuijun@gmail.com>
Contributor
Author
|
I'll fix CI failures and address comments from users with write access. I'll skip comments containing "(aside)".
|
Co-Authored-By: jason.han <hanhuijun@gmail.com>
…nd guard drop by its own payload Co-Authored-By: jason.han <hanhuijun@gmail.com>
…fer-extension Co-Authored-By: jason.han <hanhuijun@gmail.com> # Conflicts: # docs/project/pilot-differential-baseline.json
…onal when classifying a deferral The emitter spells a literal true and an else guard as no if clause, so a completion transition under either leaves a deferring state exactly as an unguarded one does: never, once the accept loop is the state's do action. Classify and refuse such a deferral the same way, through one predicate the guard translator shares. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…fer-extension Co-Authored-By: jason.han <hanhuijun@gmail.com> # Conflicts: # README.md # docs/internals/architecture.md # docs/project/pilot-differential-baseline.json # docs/project/pilot-rejection-baseline.json # docs/project/spec-compliance.md # docs/reference/repl-commands.md # internal/semantic/resolve/document.go # internal/syntax/ast/astcodec/nodes.go # internal/syntax/parser/behavior.go # internal/workspace/libs/stdlib.snapshot # tests/export/behavior_test.go
Two deferrableTrigger elements of a state naming the same signal produced two buffers with identically named receive/keep actions in one do action, which the emitted model could not declare. The emitter now coalesces the state's deferred triggers by signal before writing the encoding. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…fer-extension Co-Authored-By: jason.han <hanhuijun@gmail.com> # Conflicts: # internal/workspace/libs/stdlib.snapshot
…d-notation recovery A specialization keyword after the word (`defer references setting;`) names a feature, so the removed `defer <event>;` detector no longer claims it; parser tests and the ordinary-name golden cover the shape. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…lop merge The three end-multiplicity movements (Behaviors.kerml:14 and delta-v-budget.sysml:93 no longer warn, parser_features_demo_connectors.sysml:108 now does) come from develop (#711, hydrating recorded scopes) and reproduce on develop alone; the totals move 83 -> 82 / 42 -> 41 identically. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…the develop merge" This reverts commit 4605202.
…e-multiplicity movement The committed differential baseline no longer reproduced on develop: a parameter that writes no multiplicity takes its effective multiplicity (145a146), which silences the unbound-parameter advisory on Behaviors.kerml:14 and delta-v-budget.sysml:93, and the end-feature multiplicity warning on parser_features_demo_connectors.sysml:108 surfaces with the syntax-backed scopes of recorded files (#711). Re-record the baseline (only ours 42 -> 41, our diagnostics 83 -> 82), add the round to pilot-differential.md, and bring the README, architecture and skill headline figures along. Co-Authored-By: jason.han <hanhuijun@gmail.com>
Resolves the pilot-differential baseline and its generated figures on develop's re-record (345 / 40 / 81, which reproduces on the merged tree once the nested action-body source-multiplicity fix silences the succession-end warning), keeps the spec-compliance behavioral-nodes row without the removed defer notation, and re-records the examples digest for the corpus without the extension. Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
The undeclared-signal lint merged from develop covered the removed defer state member; it now covers when triggers only, and the pilot rejection and differential baselines are re-recorded on the merged tree. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…fer-extension Co-Authored-By: jason.han <hanhuijun@gmail.com> # Conflicts: # tests/export/testdata/convert/state_machine.golden.ttl # tests/export/testdata/convert/then_after_members.golden.ttl
…m; keep encoding names off kept signals A signal queued from outside the model (QueuedEvent.Signal) was resolved in the scope of the part exhibiting the machine only, so a signal the machine alone imports — a state def's private import — reached a typed accept as a name-only message whose payload could not bind. The queued name now resolves where the machine's accepts are written: its own body, the bodies of the definitions it inherits from, then its owner's scope, falling back to the name alone as before. The PSSM referee's standard deferred-signal encoding named its payload `kept` and its do action `buffer` regardless of the kept signal's name, so a signal named `kept` was hidden by its own accept (`accept kept : kept`) and the model failed validation. The names the encoding makes up now step aside from the kept signals' (`accept kept_2 : kept`). Co-Authored-By: jason.han <hanhuijun@gmail.com>
…fer-extension Co-Authored-By: jason.han <hanhuijun@gmail.com> # Conflicts: # docs/project/pilot-differential-baseline.json
…ing part, else at the accept A signal queued from outside the model by name (QueuedEvent.Signal) is what that name denotes to the part exhibiting the machine, as a `send` written there is: an occurrence of that definition, taken by conformance, so a transition the machine inherits, written against the same definition, takes it even where the machine's own body imports another signal under the same name. A name the part sees no signal definition by is matched by name alone and typed by the accept that takes it (Message.TypedByAccept), in that accept's own scope, so a machine's private import types the payload it binds without the injection choosing between scopes. Replaces the machine-scope-first search, which typed the queued name by the machine's own import and so kept an inherited transition written against the part's definition from firing. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…nformance in the accept's scope A queued signal the exhibiting part sees no definition of is resolved in the scope of each accept it is compared against (messageSignal), so a subtype only the machine's private import declares satisfies an accept of its supertype by conformance and binds as that subtype; a name no scope resolves is still compared by name. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…fer-extension Co-Authored-By: jason.han <hanhuijun@gmail.com> # Conflicts: # docs/project/pilot-differential-baseline.json # internal/ir/view/behavior.go # internal/translate/migrate/states.go
…fer-extension Co-Authored-By: jason.han <hanhuijun@gmail.com> # Conflicts: # docs/project/spec-compliance.md # internal/workspace/libs/stdlib.snapshot
…fer-extension Co-Authored-By: jason.han <hanhuijun@gmail.com> # Conflicts: # docs/project/spec-compliance.md
…fer-extension Co-Authored-By: jason.han <hanhuijun@gmail.com> # Conflicts: # internal/check/passes/lint_undeclared_signal.go
Merged
3 of 6 tasks
Merge origin/develop into refactor/remove-defer-extension. develop's StateMachines metadata library keeps its pseudostate annotations (#choice, #junction, #shallowHistory, #deepHistory); its DeferredMetadata / #deferred ref spelling of a deferred event is removed along with the lowering, notation quick-fix, metadata conformance fixtures and docs that carried it, so the standard buffer / accept-loop / exit-flush encoding is the only way to model a deferred signal. Stdlib snapshot, pilot differential and rejection baselines and the documentation figures are re-recorded on the merged tree. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…e metadata deferral removal Co-Authored-By: jason.han <hanhuijun@gmail.com>
…fer-extension Co-Authored-By: jason.han <hanhuijun@gmail.com>
4 of 6 tasks
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
defer <event> [, <event>]*;inside a state body was an OpenSysML-only extension — SysML v2 has no deferral notation — and PR #669 already made the SysML v1 migrator write every deferred signal in standard notation (ordered bufferitem, do-action accept loop, exit-action flush,@MigrationMetadata::DeferredEventprovenance). This PR removes the extension itself from the language, the runtime and every surface:deferis no longer a contextual keyword;ast.DeferMember,StateNode.Defer, the codec/dump/succession handling andparseDeferMemberare gone.deferis an ordinary name (attribute defer : Real;,action defer,state defer,defer.x— goldentests/parser/testdata/parse/defer_ordinary_name). A legacydefer <event>;member is one parser diagnostic, codedefer-notation-removed, spanned on the word, with anErrorNodein the tree; recovery consumes to the semicolon or the next member start, sodefer Ping state b;still yields substateb.nonstandard_notation.gono longer knows the word (it is a parse error in both modes, not a warning escalated under-strict);StateGraph.Deferred, the inheritance merge and theSig / deferview labels are removed.deferred,defersEvent,deferringStates,deferralOutranks,recallDeferredEvents,DeferredEvents(),Decision.Deferred,Dispatch.Deferred, the deferral branches of dispatch, the state-deferral footprint incheck_reduce.goand the snapshot/debug serialization of held events are gone. A standard-encoded deferral runs on the ordinary do-behavior andsendmachinery, unchanged. A signal queued from outside the model by name (QueuedEvent.Signal) is what that name denotes to the exhibiting part, as asendwritten there is, and is taken by conformance; a name the part sees no signal definition by is resolved in the scope of each accept it is compared against (Message.TypedByAccept,messageSignal) — matched by conformance where that scope declares it, by name where none does — and typed by the accept that takes it, so a machine-localprivate importmatches supertype accepts and binds its payload without the injection choosing between scopes.Acceptance.Deferredis removed from the Go client and gRPC conversion (Acceptance.Resumesstays); the REPL's%current"Deferred by the active state" report, the%sendwording and thedefercompletion entry are gone; LSP publishes the removed-notation diagnostic in both modes.sysx:DeferMember/sysx:deferredEventare removed from the ontology, the writer and the reader; a legacy Turtle graph carrying them is refused with a diagnostic naming the standard encoding rather than read with the member dropped (tests/export/behavior_test.go).internal/translate/deferredis the one writer of the buffer / accept-loop / exit-flush encoding;internal/translate/migrate/states.goand the PSSM referee (tools/referee/pssm/emit.go) both render through it (unit-tested indeferred_test.go; the migrator'sTestStrictDeferredSignals*/TestDeferral*and the PSSM suite test exercise it end to end). The migrator's output is byte-identical todevelop.state_deferred_event,state_deferral_outranks_*,state_deferral_nested_override) are retired and each scenario the standard notation can express is re-pinned in standard notation:state_deferred_signal_kept_and_replayed,state_guard_reads_deferred_payload,state_nested_parallel_region_owner_behavior,state_then_skips_non_feature_members, plus fourstate_deferred_buffer_yields_to_*cases that pin the standard behaviour where the extension's priority rule used to hold the signal back (a transition that is enabled fires).state_deferred_test.gois removed; its two tests that did not depend on the extension (TestUndeferredEventIsDroppedWhereNoTransitionHandlesIt,TestExitedNestedRegionDoesNotReactToTheSameEvent) live on instate_composite_transition_test.go.not-expressible; the Deferred 006 rows (a deferral in a state an unguarded completion transition leaves) arenot-expressible; see the bucket table below.develop, PR fix(grpc): report the parser's warnings as the workspace does #751).parser.AsDiagnosticsis the one mapping every frontend uses; its errors are coded byDiagnostic.ErrorCode()— the diagnostic's own code when the parser gave it one (defer-notation-removed), elsesyntax— so the removed-notation code survives the refactor on the LSP, gRPC, REPL and edit surfaces.develop, PR feat(state-machines): express pseudostates and deferred events as standard metadata #639). The pseudostate annotations stay —#choice state,#junction state,#shallowHistory state,#deepHistory state, theirnonstandard-notationquick-fixes and the migrator's use of them. Its second half, event deferral as metadata (deferredEvents,metadata def <deferred> DeferredMetadata,#deferred ref : Ping;, lowering intoStateGraph.Deferred, thedefer e;→#deferred ref : e;quick-fix, eight*_metadataconformance fixtures, the%currentand gRPC reporting of held events), is removed here rather than kept beside the standard encoding:StateMachines.sysmland the stdlib snapshot,internal/ir/lower/state_metadata.go,nonstandard_notation.go, the LSP code-action test, the workspace and PSSM validation tests,docs/project/statemachines-library.md, the guide/reference pages and thestate-machine-metadata.*changelog fragments now describe pseudostates only, and a legacydefermember is a parse error in both modes, not a deprecation warning.x05-defer-member.sysmlis now rejected by OpenSysML in both default and strict modes (verdicts.go+docs/project/pilot-rejection.md): 311 cases, 302 both reject, 0 only the pilot, 9 only we, 0 both accept (2 of them agreeing only under-strict;-conformance defaultgives 300 both reject, 2 only the pilot). The baseline is re-recorded on the merged tree for one movement that isdevelop's own: PR feat(state-machines): express pseudostates and deferred events as standard metadata #639 maderequireoutside a requirement body (x08) a parse error, so it moved from strict-only to both-reject by default — a build oforigin/developrejects it the same way — anddevelop's baseline had not been re-recorded;pilot-rejection.mdadjudicates it. Theundeclared-signallint merged fromdevelopcovered adefer <name>member as well as awhen <name>trigger; with the member gone it coverswhenonly (passes/lint_undeclared_signal.go, its tests and the lint's documentation).spec-compliance.md,pssm-migration.md,pssm-referee.md,pilot-rejection.md, the design notes (pseudostates.md,precise-semantics-alignment.md,orthogonal-regions.md,scheduling.md, …), the VS Code grammars (regenerated) and snippets,examples/self-modeland theREADMElose the extension. One "removed" note stays indocs/reference/grammar/README.mdand points at the standard encoding (docs/reference/sysml-v1-migration.md, Deferred signals).Semantics that are no longer expressible (accepted losses, documented rather than recreated)
acceptin a do behavior; an enabled transition anywhere in the configuration fires firstdocs/project/spec-compliance.md(deferred-signal rows),docs/reference/grammar/README.md,docs/internals/design/precise-semantics-alignment.md§ deferred events, the fourstate_deferred_buffer_yields_to_*conformance casesforloop; UML leaves event-pool order opendocs/reference/sysml-v1-migration.md§ Deferred signals,docs/project/pssm-referee.md(Deferred 001 / 005)docs/project/pssm-referee.md(Deferred 007),docs/project/pssm-migration.md,docs/reference/grammar/README.mdSpecification basis
The SysML v2 textual notation has no deferral production in a state body; event deferral is a UML state-machine / PSSM notion, which SysML v2 models with an ordinary buffer, accept loop and flush. The compliance rows for deferred events in
docs/project/spec-compliance.mdmove from the extension to the standard encoding (✅ for the kept-and-replayed signal and the guard reading its payload; the priority rule and the pooled replay order are recorded as known losses).How it was verified
Gates (all on the branch head;
gofmt -l .prints nothing):internal/frontend/lsp: theTestWire*/TestRunServes*stream tests time out (30 s waiting forpublishDiagnostics) on this machine onorigin/develop(074aceb) as well as on this branch, identically; every other LSP test in the package passes, including the newTestPublishDiagnosticsReportsRemovedDeferNotation. Treating it as an environment issue here — CI will tell.Pilot differential baseline (
docs/project/pilot-differential-baseline.json):developre-recorded it (345 fully agreeing / 40 only ours / 1616 only the pilot's) with its own adjudication indocs/project/pilot-differential.md, and every diagnostic figure reproduces on this merged tree withpilot-diff -check, so this PR carriesdevelop's figures and prose unchanged. The one thing re-recorded here is theexamplesroot digest, because the corpus underexamples/loses the extension. The branch's earlier Parameter effective-multiplicity round section is withdrawn: the end-feature multiplicity warning it recorded onexamples/parser_features_demo_connectors.sysml:108no longer fires oncedevelop's nested action-body source-multiplicity fix is merged in, and the advisory movement isdevelop's own.make docs-countspasses.PSSM referee bucket movements (
docs/project/pssm-referee-baseline.json,pass60 → 52,not-expressible30 → 34,differs-by-design1 → 5,fail12 unchanged):TMT end-to-end (
TMT-2024x.mdzip+TMT_mtip.xml, this branch vs a build oforigin/developat 074aceb, default and-strict):rg -c '^\s*defer ' out-*/TMT.sysml→ 0 in both modes, both builds.DeferredEventoccurrences → 823 in both modes, both builds.TMT.sysml,TMT.migration-report.txtandTMT.migration-results.jsonare byte-identical between this branch anddevelopin both modes — the PR changes no migration output.-validatediagnostics are identical between the two builds apart from the temporary output-directory prefix (both exit 2 on the same pre-existing diagnostics of the migrated model).Checklist
make testandmake lintpass locally (make lint: staticcheck on both module roots + gosec,✓ Lint passed;go testas above)changes/unreleased/remove-defer-extension.removed.md/.changed.md, not as an edit toCHANGELOG.mdmake docs-countsrun if a gate count moved (PSSM referee, pilot rejection, pilot differential provenance)Link to Devin session: https://nasa-jpl-demo.devinenterprise.com/sessions/5a86143306ca4cde86c4dad4e9f9b48a
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/5a86143306ca4cde86c4dad4e9f9b48a?variant=devin
Requested by: @HuiJun