Repository navigation
chore(release): bring develop's execution, migration, extension-library and documentation changes into 0.10.0 - #1064
Merged
Merged
Conversation
Co-Authored-By: jason.han <[email protected]>
Co-Authored-By: jason.han <[email protected]>
…reads and bindings Co-Authored-By: jason.han <[email protected]>
… on parts Co-Authored-By: jason.han <[email protected]>
Co-Authored-By: jason.han <[email protected]>
…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 <[email protected]>
Co-Authored-By: jason.han <[email protected]>
…uarded successions Co-Authored-By: jason.han <[email protected]>
Co-Authored-By: jason.han <[email protected]>
…s out of the entry action Co-Authored-By: jason.han <[email protected]>
Co-Authored-By: jason.han <[email protected]>
Co-Authored-By: jason.han <[email protected]>
Co-Authored-By: jason.han <[email protected]>
…get end Co-Authored-By: jason.han <[email protected]>
Co-Authored-By: jason.han <[email protected]>
…nd compliance map Co-Authored-By: jason.han <[email protected]>
Co-Authored-By: jason.han <[email protected]>
…odec Co-Authored-By: jason.han <[email protected]>
…ge triggers, adjudicate PSSM movements Co-Authored-By: jason.han <[email protected]>
Co-Authored-By: jason.han <[email protected]>
Co-Authored-By: jason.han <[email protected]>
…ition out of an entry action Co-Authored-By: jason.han <[email protected]>
…f an entry action Co-Authored-By: jason.han <[email protected]>
…ed it A join reached per performance consumes the earliest sibling arrival and mints the token that performs it, so the tried token neither moves nor changes the token count and the step looked unacted. Compare the token-ID counter before and after the step too, so the explore slot and the check replay see the synchronization as that token's act. Pin every checkable repeated-step conformance case with a check expectation; a case with a check expectation may carry an explore budget without outcomes. Co-Authored-By: jason.han <[email protected]>
The runtime reaches a repeated step in one step, splits the token into its siblings in the next, then performs the step in a third. The encoding placed the siblings on the arriving move, compressing the split into the arrival, so every witness step and choice was off by one and witnesses would not replay. Arrivals into a repeated step now land the token pending and the next move mints its siblings, mirroring the runtime, and the SMT witness tests pin that violated properties over repeated steps replay. Co-Authored-By: jason.han <[email protected]>
…arget ends Co-Authored-By: jason.han <[email protected]>
…rdinary action node Co-Authored-By: jason.han <[email protected]>
Co-Authored-By: jason.han <[email protected]>
* feat(verify): bind the in parameters of a constraint or requirement at check time VerifyConstraint and VerifyRequirement take positional and named arguments, as RunAnalysis binds a case's inputs, under the verification_arguments capability. The runtime binds them in declaration order or by name and leaves the verdict undecided on an unknown name, an arity overrun, a parameter with neither an argument, a default nor a same-named value on the checked object, or a value of the wrong type; holds and satisfiable refuse arguments. The CLI and REPL accept the invocation grammar -analysis uses (-requirement 'P::R(limit = 5) P::t', %constraint C(3.0) t), and every client binds through the same option. Co-Authored-By: jason.han <[email protected]> * chore(client): order Rust capability imports for rustfmt; keep the Python stub at the pinned grpcio-tools version Co-Authored-By: jason.han <[email protected]> * fix(runtime): keep a renamed inherited input's slot and default when binding check arguments; never share verdicts of checks with arguments Co-Authored-By: jason.han <[email protected]> * fix(matlab): send verification namedArguments given as a containers.Map Co-Authored-By: jason.han <[email protected]> --------- Co-authored-by: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Co-authored-by: jason.han <[email protected]>
…ty-kind Co-Authored-By: jason.han <[email protected]> # Conflicts: # docs/project/sysml-v1-transformation-census-baseline.json # docs/project/sysml-v1-transformation-census.md
…ion index actionStepSymbol materialized and scanned every member of each enclosing scope on every step, so performing a chain of N steps cost O(N^2). Scope already indexes members by declaration; use it. Co-Authored-By: jason.han <[email protected]>
Co-Authored-By: jason.han <[email protected]>
Co-Authored-By: jason.han <[email protected]>
Co-Authored-By: jason.han <[email protected]>
… feat/repeated-step-coverage Co-Authored-By: jason.han <[email protected]> # Conflicts: # internal/ir/lower/action_graph.go
* fix(lower): perform inherited action steps and inherit step multiplicity Co-Authored-By: jason.han <[email protected]> * fix(lower): prefer owned action successions when merging inheritance Co-Authored-By: jason.han <[email protected]> * fix(runtime): merge typed action bodies without forwarding writes past 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 <[email protected]> * docs(changelog): describe inherited action steps from the user's side Co-Authored-By: jason.han <[email protected]> * docs(changelog): name inherited-step examples without probe labels Co-Authored-By: jason.han <[email protected]> * fix(lower): bound typed-body merging of actions nested in their own type Co-Authored-By: jason.han <[email protected]> * refactor(lower): remove dead code flagged by staticcheck Co-Authored-By: jason.han <[email protected]> * fix(lower): thread the resolver into block flows and refuse clock waits in stepped entry behaviors Co-Authored-By: jason.han <[email protected]> * refactor(lower): group succession edge lowering fields Co-Authored-By: jason.han <[email protected]> * fix(ir): preserve inherited assertions and pin bindings Co-Authored-By: jason.han <[email protected]> * fix(lower): preserve unchecked inherited assertions Co-Authored-By: jason.han <[email protected]> * fix(lower): carry ordered assertions through action inheritance Co-Authored-By: jason.han <[email protected]> * fix(runtime): sequence nested typed action output reads Co-Authored-By: jason.han <[email protected]> * fix(lower): preserve inherited succession flow gates Co-Authored-By: jason.han <[email protected]> * fix(lower): let a specialization's own flows connect inherited steps Co-Authored-By: jason.han <[email protected]> * fix(lower): resolve inherited gates in their declaring scope Co-Authored-By: jason.han <[email protected]> * test(lower): sequence inherited action fixture steps Co-Authored-By: jason.han <[email protected]> * fix(lower): retain inherited case-step lowering Co-Authored-By: jason.han <[email protected]> * fix(lower): let a specialization's pin binding replace the inherited one Co-Authored-By: jason.han <[email protected]> * test(runtime): order the typed-node output read with then in state_block_flow_typed_node Per #850's statement-order rule, direct statements without then are unordered; the fixture orders the output read after the typed node. Co-Authored-By: jason.han <[email protected]> * fix(client): restore generated Java protobuf sources byte-for-byte The develop merge stripped trailing whitespace protoc emits in ExecuteStateResponse and its OrBuilder, so the proto-buf drift check regenerated a diff. Restore the generated output. Co-Authored-By: jason.han <[email protected]> * fix(lower): keep a differently guarded inherited succession alongside an owned one Co-Authored-By: jason.han <[email protected]> * chore(changes): drop fragment for a fix that never shipped Co-Authored-By: jason.han <[email protected]> * fix(lower): keep the binding of inherited pins on bodied typed usages Co-Authored-By: jason.han <[email protected]> * fix(lower): keep inherited successions whose end multiplicities differ Co-Authored-By: jason.han <[email protected]> * test(runtime): cover inherited content in composite redefining steps Co-Authored-By: jason.han <[email protected]> --------- Co-authored-by: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Co-authored-by: jason.han <[email protected]>
* wip: untyped property kind Co-Authored-By: jason.han <[email protected]> * fix(migrate): an untyped property follows its tool's kind marker; unmarked, it is an attribute, or a part when composite Co-Authored-By: jason.han <[email protected]> * fix(migrate): a slot of an untyped part is typed by its individual instead of crashing Co-Authored-By: jason.han <[email protected]> * fix(migrate): a slot of an untyped part is checked against the type the part inherits by redefinition, subsetting or name Co-Authored-By: jason.han <[email protected]> * fix(migrate): a slot of an untyped part is checked against every type the part inherits by redefinition, subsetting or name Co-Authored-By: jason.han <[email protected]> --------- Co-authored-by: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Co-authored-by: jason.han <[email protected]>
actionStepSymbol materialized and scanned every member of each enclosing scope on every step, so performing a chain of N steps cost O(N^2). Scope already indexes members by declaration; use it. Co-authored-by: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Co-authored-by: jason.han <[email protected]>
…t Kit (MDK2) Co-Authored-By: jason.han <[email protected]>
…ary main Co-Authored-By: jason.han <[email protected]>
Co-authored-by: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Co-authored-by: jason.han <[email protected]>
* feat(runtime): execute repeated steps in block flows, part performs, reads and bindings Co-Authored-By: jason.han <[email protected]> * test(parser): add parse goldens for repeated steps in loop bodies and on parts Co-Authored-By: jason.han <[email protected]> * fix(runtime): give each repeated part performance its own occurrence Co-Authored-By: jason.han <[email protected]> * feat(runtime): execute repeated steps adjacent to control nodes and guarded successions Co-Authored-By: jason.han <[email protected]> * feat(smt): encode exact repeated action steps Co-Authored-By: jason.han <[email protected]> * test(parser): add parse golden for a guarded succession's written target end Co-Authored-By: jason.han <[email protected]> * fix(smt): refuse the repeated-step shapes CheckStep refuses Co-Authored-By: jason.han <[email protected]> * docs(project): record repeated-step coverage in the semantic oracle and compliance map Co-Authored-By: jason.han <[email protected]> * fix(ast): encode the written target end of a succession through the codec Co-Authored-By: jason.han <[email protected]> * fix(export): carry a guarded succession's written target end Co-Authored-By: jason.han <[email protected]> * fix(runtime): credit a synchronization to the token whose try performed it A join reached per performance consumes the earliest sibling arrival and mints the token that performs it, so the tried token neither moves nor changes the token count and the step looked unacted. Compare the token-ID counter before and after the step too, so the explore slot and the check replay see the synchronization as that token's act. Pin every checkable repeated-step conformance case with a check expectation; a case with a check expectation may carry an explore budget without outcomes. Co-Authored-By: jason.han <[email protected]> * fix(smt): spend a move on a repeated step's split The runtime reaches a repeated step in one step, splits the token into its siblings in the next, then performs the step in a third. The encoding placed the siblings on the arriving move, compressing the split into the arrival, so every witness step and choice was off by one and witnesses would not replay. Arrivals into a repeated step now land the token pending and the next move mints its siblings, mirroring the runtime, and the SMT witness tests pin that violated properties over repeated steps replay. Co-Authored-By: jason.han <[email protected]> * chore(workspace): regenerate the stdlib snapshot for the succession target ends Co-Authored-By: jason.han <[email protected]> * fix(lower): fix a control node's count to a repeated step's only where the successions derive it Co-Authored-By: jason.han <[email protected]> * fix(exec): report repeated steps in block bodies as observed rather than proved or bounded Co-Authored-By: jason.han <[email protected]> * docs(project): derive control-node and block-body repeated-step semantics from the spec Co-Authored-By: jason.han <[email protected]> * fix(lower): read an unwritten control node's count as one unless its ends force the repeated step's A control node that declares no multiplicity takes the executor's one-performance reading beside a repeated step, so a written [*] into a fork or decision is a barrier and a written [*] out of a join or merge fans out. The four derived crossings — a bijective crossing into a join or out of a fork, the lone incoming edge of a merge, the lone outgoing edge of a decision — still fix the node's count to the step's, and a merge or decision carrying another succession is unsatisfiable under count one through the mandated 0..1 ends. Restores the fork-barrier, decision-barrier and merge-fanout conformance fixtures to running, and the corresponding SMT witness and outcome cases. The conformance README notes that an exploration budget raise is pinned for completeness only and never changes a standing. Co-Authored-By: jason.han <[email protected]> * docs(project): describe the one-performance reading for unwritten nodes beside repeated steps Co-Authored-By: jason.han <[email protected]> * test(conformance): pin the merge per-performance exploration budget The default 1024-run budget leaves the check-agrees exploration of the merge per-performance fixture incomplete; raise it like the join per-performance fixture's. Co-Authored-By: jason.han <[email protected]> * fix(smt): land a fork's token pending at a repeated target so its split makes the siblings Co-Authored-By: jason.han <[email protected]> * fix(runtime): capture coverage notes in snapshots and fold them during the check search Co-Authored-By: jason.han <[email protected]> * fix(exec): prune a literal-false succession into a single performance instead of refusing it Co-Authored-By: jason.han <[email protected]> * fix(exec): return every direct behavior match so repeated performances stay ambiguous Co-Authored-By: jason.han <[email protected]> * docs(project): note the pending fork landing at a repeated target and the pruned single-performance guard Co-Authored-By: jason.han <[email protected]> * test(runtime): state every interleaving of a repeated step's unordered body statements Co-Authored-By: jason.han <[email protected]> * test(check): expect open order for a repeated step in an unordered inherited loop body The repeated-step coverage change lifts the block-body multiplicity refusal, so a repeated step in a loop body is refused only when its body states no succession: the inherited [2] case now expects the order-open finding, and an ordered inherited loop body is covered as supported at both the pass and the runtime (tick performs its inherited count per pass). Co-Authored-By: jason.han <[email protected]> * fix(parser): read a guarded succession's written target end through the transition member A keywordless first a if g then [m] b matches atMultiplicityFirstSuccession (the then-[ probe fires before the guard check), so it fell into the succession-usage parse and errored instead of reaching parseTransitionMember's then-[m] handling. An if at depth 0 before then means the member is a GuardedSuccession: bail so the guarded-succession dispatch reads it. Co-Authored-By: jason.han <[email protected]> * test(semantics): expect both guarded-succession spellings as transition members The keywordless first a if g then [m] b is a GuardedSuccession and parses as a TransitionMember like the succession-keyword spelling, so both edges are counted there instead of one under InitialNode. Co-Authored-By: jason.han <[email protected]> * test(smt): expect the inherited repeated-step count to encode A redefining step declaring no multiplicity takes the redefined step's [n], and the effective count is encoded like a declared one, so the inherited-step case is a count test rather than a refusal test. Co-Authored-By: jason.han <[email protected]> * fix(smt): let a fork honour a repeated step's pending gate On a pending split move the fork's actor landing, its none-retire, and its sibling placements applied unconditionally, contradicting the split's own constraints so a fan-out from a repeated step proved vacuously. Landings, the retire, placements, nextID, fails and full now apply under the same gate succeed uses, with the barrier retirement for a gate-false move; under pending only the split's constraints apply. Co-Authored-By: jason.han <[email protected]> * fix(runtime): report open order for a false guard into an inherited repeated step falseGuardLeavesRepeated skipped an inherited [n] because it read the declared-multiplicity table; it now gates on the effective HasStepMultiplicity, so a redefining step that takes the redefined step's count refuses the same way. Co-Authored-By: jason.han <[email protected]> * fix(runtime): bound a performed action's performance count classifierPerformanceCount answers the count both the deferred and the eager attachment loops then mint; it now applies the same step budget splitRepeatedStep enforces, so a huge declared count fails with ErrActionStepLimitExceeded before any behavior is allocated. Co-Authored-By: jason.han <[email protected]> * style: shorten new test comments to the house limit Trims the comments added with the inherited-step cases to at most two lines each. Co-Authored-By: jason.han <[email protected]> * fix(lower): keep an inherited succession whose ends carry multiplicities sameUnconditionalActionEdge compared ends, guard, name and carrier but not the written end multiplicities, so an owned plain succession restating the same ends swallowed the inherited edge and dropped its [*]..[1] crossing. An edge whose ends state multiplicities is now never the same unconditional edge as one without them or with different ones. Co-Authored-By: jason.han <[email protected]> * fix(lower): deduplicate a restated succession by its ends' ranges sameUnconditionalActionEdge compared written end multiplicities by node identity, so a derived action restating an inherited succession verbatim kept a second edge and the runtime had two orderings over the same ends. The comparison now evaluates each end's range in its own declaring scope and deduplicates only when both ends agree; an unevaluable bound still keeps both edges. Co-Authored-By: jason.han <[email protected]> --------- Co-authored-by: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Co-authored-by: jason.han <[email protected]>
…ension-libraries Co-Authored-By: jason.han <[email protected]> # Conflicts: # internal/workspace/libs/stdlib.snapshot
pymdown-extensions 12.2 changed the Highlight constructor, which mkdocstrings 1.0.6 calls without the new argument, so every documentation build failed with "Highlight.__init__() missing 1 required positional argument: 'md'" once the unpinned transitive dependency resolved to it. mkdocstrings 1.0.7 follows the new signature; pinning pymdown-extensions keeps the toolchain fully reproducible. Co-Authored-By: jason.han <[email protected]>
mkdocstrings 1.0.7 requires Python 3.11, while the project's Python floor is 3.10. Pinning pymdown-extensions to 12.1, the last release with the Highlight constructor that mkdocstrings 1.0.6 calls, restores the documentation build without raising that floor. Co-Authored-By: jason.han <[email protected]>
* ci(docs): pin pymdown-extensions and take mkdocstrings 1.0.7 pymdown-extensions 12.2 changed the Highlight constructor, which mkdocstrings 1.0.6 calls without the new argument, so every documentation build failed with "Highlight.__init__() missing 1 required positional argument: 'md'" once the unpinned transitive dependency resolved to it. mkdocstrings 1.0.7 follows the new signature; pinning pymdown-extensions keeps the toolchain fully reproducible. Co-Authored-By: jason.han <[email protected]> * ci(docs): keep mkdocstrings 1.0.6 and pin pymdown-extensions to 12.1 mkdocstrings 1.0.7 requires Python 3.11, while the project's Python floor is 3.10. Pinning pymdown-extensions to 12.1, the last release with the Highlight constructor that mkdocstrings 1.0.6 calls, restores the documentation build without raising that floor. Co-Authored-By: jason.han <[email protected]> --------- Co-authored-by: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Co-authored-by: jason.han <[email protected]>
…ries * feat(libs): pin and sync the vendored extension libraries from OpenSysML-Extensions-Library The extension libraries live upstream; scripts/sync-extension-libraries.sh vendors the pinned commit, --check fails CI on drift, and engine-contract.json records the qualified names the engine binds. Co-Authored-By: jason.han <[email protected]> * test(libs): hold the runtime registry and bound names to engine-contract.json Co-Authored-By: jason.han <[email protected]> * ci,docs: extension-libraries drift check, advisory upstream workflow, and the new library home Co-Authored-By: jason.han <[email protected]> * fix(contract): re-pick extensions pin; reject duplicate manifest entries; name all 14 libraries in README Co-Authored-By: jason.han <[email protected]> * docs: exclude the extension-libraries engineering record from the built site Co-Authored-By: jason.han <[email protected]> * fix(libs): refuse an upstream without engine-contract.json; test the tools module in the upstream job Co-Authored-By: jason.han <[email protected]> * chore: retrigger pull request checks Co-Authored-By: jason.han <[email protected]> * chore(libs): pin the extension libraries to the merged Extensions-Library main Co-Authored-By: jason.han <[email protected]> * chore: retrigger pull request checks Co-Authored-By: jason.han <[email protected]> * build(libs): pin the extension libraries to the develop sync branch Co-Authored-By: jason.han <[email protected]> * build(libs): pin the extension libraries to OpenSysML-Extensions-Library main Co-Authored-By: jason.han <[email protected]> * fix(stdlib): pin the extension libraries with library package declarations Co-Authored-By: jason.han <[email protected]> * chore(oracle): re-record the pilot differential baseline for the library package declarations Co-Authored-By: jason.han <[email protected]> * build(libs): pin the extension libraries to OpenSysML-Extensions-Library main Co-Authored-By: jason.han <[email protected]> --------- Co-authored-by: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Co-authored-by: jason.han <[email protected]>
… toolchain pin into 0.10.0 Co-Authored-By: jason.han <[email protected]>
Contributor
Author
|
I'll fix CI failures and address comments from users with write access. I'll skip comments containing "(aside)".
|
Merged
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
Hotfix from
mainfor the 0.10.0 release: merges currentdeveloponce and folds the changelog fragments into the existing## 0.10.0 — 2026-10-08section. No code is changed beyond whatdevelopcarries; the only hand edit isCHANGELOG.mdplus the removal of the folded fragments.Brought in from
develop(#830, #833, #834, #837, #881, #1020, #1032, #1033, #1035, #1036, #1038, #1040, #1055):actionStepSymbollookup.-strictoutput refers to no OpenSysML library, object flows, use case diagrams drawn as connections between usages, untyped properties following their tool's kind marker, individual-slot crash fix.OpenSysML Libraries/extensions are vendored from Open-MBEE/OpenSysML-Extensions-Library (pinned tomainat5a47e595), with the engine-contract manifest and drift check; the four extension libraries are declaredlibrary packagerather thanstandard library package; the SIMagneticDipoleMomentUniterrata fix.docs-requirements.txtpinspymdown-extensions==12.1so the documentation site builds again on Python 3.10.Three fragments already folded into 0.10.0 by earlier hotfixes (
case-step-order,migrate-object-flows,terminate-usage-body-flow) were amended ondevelop; their entries in the 0.10.0 section carry the amended wording and the fragments are removed.changes/unreleased/holds only its README afterwards.How it was verified
On the merged tree:
gofmt -l .empty,go build ./...,go vet ./...,make lint,make docs-check,scripts/check-doc-links.py,scripts/changelog.py check,scripts/check-doc-ids.py,make proto-breaking BUF_BREAKING_REF=origin/main,CIRCLE_TAG=v0.10.0 check_version.py --editors,make extension-libraries-check,make stdlib-snapshot-check, stdlib conformance,go test -race -count=1 ./...with the training, pilot-corpora, pilot-library-XMI and PSSM require flags set,make build-grpc, and the Python client suite (1459 passed).Checklist
make testandmake lintpass locallydocs/project/releasing.md)make docs-countsrun if a gate count moved (carried by the merged pull requests)F4,K5) in the body, docs, or changelogLink to Devin session: https://nasa-jpl-demo.devinenterprise.com/sessions/3db6a090aa214667b2a66d372c6e36b1
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/3db6a090aa214667b2a66d372c6e36b1?variant=devin
Requested by: @HuiJun