Repository navigation
fix(lower): perform inherited action steps and inherit step multiplicity - #830
devin-ai-integration[bot] wants to merge 26 commits into
Conversation
Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
…t the performance Remove name-based write forwarding from invoked actions, observe state and classifier perform bodies through bound inout pins, run state entry flows stepped under one-move schedulers so check sees their token-order choices, and record the open outcomes of typed nodes whose own statements race the callee's steps. Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
|
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>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
|
Runtime-tested a fresh
Not exercised in this pass: the separate do/exit and part-perform variants, which the conformance fixtures cover. |
Co-Authored-By: jason.han <hanhuijun@gmail.com>
…ts in stepped entry behaviors Co-Authored-By: jason.han <hanhuijun@gmail.com>
…on-steps Co-Authored-By: jason.han <hanhuijun@gmail.com> # Conflicts: # internal/ir/lower/action_graph.go
Co-Authored-By: jason.han <hanhuijun@gmail.com>
…on-steps Co-Authored-By: jason.han <hanhuijun@gmail.com> # Conflicts: # internal/ir/lower/action_graph.go
Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
…on-steps Co-Authored-By: jason.han <hanhuijun@gmail.com> # Conflicts: # internal/ir/lower/action_graph.go # internal/ir/lower/action_nodes.go
Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
|
This branch now conflicts with
To resolve: merge current Planned merge order for the execution PRs: #844 → #850 → #838 → (#851 → #853 → #857) → #830 → #833 → #842 → #837 → #834 → #816. Re-run the full gate ( |
|
Hold on pushes: please don't push to this branch, including |
What and why
Two defects in action performance, both silent wrong answers:
action def Plain :> B1;completed with no results, andaction def Extra :> B1 { action b {…} }gavec = 100(only its ownb). Inherited steps, successions, starts, flows and direct statements are now lowered into the specialization'sActionGraph(lower/action_inherited.gomergeInheritedActionContent), each recorded with its declaring scope so names resolve where they were written; the runtime only consumes the lowered graph.resolve.ActionGeneralBodies).@Probabilityweights and the recursive-typing guard apply there too.assert constraintfollows develop's sequenced-assertion rule across the whole hierarchy. If any succession or flow in a merged body orders it (its own general, an intermediate general, or the specialization itself), it becomes a node, evaluated in its declaring scope, and a violation ends the run withViolationError(inherited_action_steps_sequenced_assertion_holds/_violated). An assertion that no succession names stays unchecked in the specialization, as it does in its general.action heat : Heat { in b = bread; }) bind to the specializing frame's inherited parameters, both at run time and in the action view. Pin-value bindings are lowered after the inherited content is merged. SoPins::SpecializedandPins::toasternow drawX.bread == heat.bbeside the inheritedpack.boxed == X.toastand the inherited flowheat.t => pack.t.first a if g then f;wherefis a succession flow, added on develop) is resolved in the specialization like its general: the flow's carrying succession takes the gate's guard, soS :> Gfollows the same guarded path asG. A gate resolves its flow in the scope it was written in, so a specialization's own same-named flow from the same source does not capture an inherited gate.action def S :> G { flow f2 from a.y to b.v; }), conformanceinherited_action_steps_own_flow_inherited_steps.lower.ErrCyclicSpecialization,ErrRedefinedStepMissing,ErrIncompatibleRedefinedStep,ErrAmbiguousInheritedStep;checkreports the same four on the same lowered graph.ActionGraph.StepCount/HasStepMultiplicitynow use the existing semantic derivation (semantics.Model.GoverningMultiplicityOf: own, else the redefined feature's, else1; subsetting alone carries nothing). Runtime,check(passes/behavior/action_step_multiplicity.go), explore and the SMT refusal (exec/smt/support.go) share it. All fix(exec): honor exact action-step multiplicities #784 behaviour is kept: exact counts,[0]no-op, non-fixed counts refused, plainthenaround repeated steps refused,ErrIntegerUnaddressablebeyond 64 bits.Scope addition, same lowering:
action u : B { … }) or a typed nested node with executable members of its own is lowered exactly asaction def P :> B; own redefinitions replace inherited steps, and the graph marks the merged subflow (ActionGraph.MergedTypedSubflows) so the type is not invoked a second time. A body that only binds features/pins keeps the existing invocation path.perform) behaviours that perform an action and state a body now run the performed action specialized by the body, as one started flow (lower/state_behavior.golowerMergedBehaviorBody). The former execution-time refusal (and its robustness subtest asserting the refusal) is removed; the known-limitations entry is deleted.What now executes (hand-derived, each a conformance fixture)
Plain :> B1,WithAttr :> B1 { attribute z … }c = 1Extra :> B1 { action b { c += 100 } }c = 101u1 : B1c = 1(unchanged)Narrow :> Base { action :>> a[2]; }atwice →c = 2Keep :> Base { action :>> a { c += 10 } }athree times (inherited[3]), each running the inheritedc += 1and ownc += 10→c = 33assign/send, inherited unordered startsperformof a specialized definition; entry/do/exit typed by a specialized definitionperformwith own bodyBehaviour changes to existing fixtures (consequence of item 3)
A typed node's own statements are now unordered with the callee's steps (KerML: owned features of a specialization carry no ordering against inherited ones unless a succession states one). Previously the own body ran after the callee.
action_invoked_node_body_writes_outputandstate_block_flow_typed_node_body_writes_output: the owny := y + 1may run before or after the callee'sscaling, so the admissible results are{30, 31}(outcome sets; check reports the state fixture as divergent ony/seen; the action fixture's pinned traces are replaced by a partial.trace.order).state_block_flow_typed_node: its owntotal += ywould readybeforescalingsets it in some orders, and ordering it with a succession from the inheritedscalingis refused by the existing multiple-successors policy, so the fixture now readsscaled.yafter the pin-only node; expected values (total = 120,runs = 3) are unchanged.action_accept_nested_call_chainandaction_accept_nested_chain_clock(added on develop while this PR was open): each read the callee's output inside the typed node's own body (action m : Mid2 { assign received := m.got; }), which under the merge is unordered with the callee and can readm.gotbefore it is set. Each fixture now uses a bodylessmfollowed by a sequencedtake { assign received := m.got; }; expected values (received = 7) are unchanged, and the trace goldens only gain thetakestep.runtime/state_statements.gorunBehavior). A clock wait inside such a stepped entry/exit still reportsErrStateBehaviorWaits, as under the fixed policy.Specification basis
Type::multiplicityderivation and the redefinition multiplicity constraints.FeatureTypingas specialization for usages; SysML v2 §7.17PerformActionUsage; Systems LibraryStates.sysmlStateActionfor entry/do/exit.Keep::a: the pilot implementation (TypeAdapter.getInheritedMemberships,FeatureAdapter.removeRedefinedFeatures/addRedefinitions,ActionUsageAdapter.getRelevantFeatures/getRedefinedFeature) removes only inherited members a subtype member (directly or indirectly) redefines.Base::a's unnamedassignis not redefined byKeep::a's own unnamedassign, so both are members ofKeep::a. Nothing was left undetermined, so nothing is refused for that case.docs/project/behavior-semantic-oracle.md;docs/project/spec-compliance.mdrows are updated (the former "own body wins, definition content not inherited" approximation, the mixed entry/do/exit approximation and its known limitation are replaced; new rows for inherited steps, effective step multiplicity, typed-usage merge and entry/do/exit merge).Known limitations
[1]stays refused, including inherited counts.action def A { action x : A { assign … } }, directly or through inheritance) is refused when executed withErrRecursiveActionTyping, because the merge would unfold without end. A self-typed body that binds only features, like the library'sAction::subactions, stays a lazy invocation. A finite typed usage of a general type (P :> Base { action x : Base { … } }) still merges.How it was verified
inherited_action_steps_*(+ trace goldens for the ordering-sensitive ones),TestRuntimeRobustnessInheritedActionSteps,TestInheritedActionStepFixturesAnalyseCleanly(every new fixture analyses with no errors), lowerer tests inlower/action_inherited_test.go, resolver/semantic multiplicity tests, checker tests for inherited fixed/non-fixed/loop/plain-then, SMT inherited-multiplicity refusal test.go build ./...,go vet ./...,gofmt -l .make lint(staticcheck root + tools, gosec)go test ./internal/ir/... ./internal/check/... ./internal/exec/... ./internal/frontend/... ./internal/translate/... ./tests/...go test ./... -count=1withOPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 OPENSYSML_REQUIRE_PILOT_LIBRARY_XMI=1 OPENSYSML_REQUIRE_PSSM_SUITE=1(all four corpora downloaded)make docs-check,scripts/changelog.py check,scripts/check-doc-ids.py-check-check-check-updateneededtests/corpus/testdata/training_examples_expected.txtAction::subactions(typed byAction, with a reference-only body). It is covered byTestExprTypeCheckNoStdlibFalsePositivesand by the lowerer tests for feature-only self-typing, direct and mutual recursion, and a finite typed usage of a general type.cmd/sysmlbuild was driven through the CLI and REPL. The results are in the PR comment.Checklist
make testandmake lintpass locallychanges/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)F4,K5) in the body, docs, or changelogLink to Devin session: https://nasa-jpl-demo.devinenterprise.com/sessions/b88f96ab8ab74044a8467c8e5060b190
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/b88f96ab8ab74044a8467c8e5060b190?variant=devin
Requested by: @HuiJun