chore(release): 0.7.0 — bring the analysis fixes on develop onto main by devin-ai-integration[bot] · Pull Request #159 · Open-MBEE/OpenSysML

devin-ai-integration · 2026-09-10T01:45:05Z

What and why

Brings develop onto main a second time before v0.7.0 is tagged. main already carries the folded ## 0.7.0 entry (#154) but not the fixes merged to develop since, three of which correct results the release would otherwise ship wrong:

fix(runtime): explore advances one token per step so complete covers every interleaving #153 — explore advances one token per step, so complete (N runs) now covers every interleaving. explore is new in 0.7.0; on main it permutes one lockstep step and can report complete while missing linearizations.
fix(lower): source a sourceless transition from the state declared before it #155 — a sourceless transition (accept … then s;, if c then s;, then s;) leaves the state declared before it; guarded entry transitions select the start state; a machine's own entry/do/exit run for every machine. Top-level sourceless transitions were refused at instantiation and nested ones fired from every substate. This refuses the nested state s { accept x then t; } form the docs used to teach, so it belongs in the minor release rather than after it.
fix(view): draw guarded entry transitions instead of marking every alternative initial #161 — the state rendering (view, Mermaid, LSP) draws a body's entry transitions as start edges in guard order ([*] --> heating : [cold]) and marks only an unconditional start initial; with fix(lower): source a sourceless transition from the state declared before it #155's guarded entry every alternative was labelled (initial) and given its own start arrow, with the guards shown nowhere. IsInitial keeps its "may be entered here" meaning for lowering and the runtime; the view uses the new UnconditionalStart. Existing state goldens only move each [*] line after the body's substates.
fix(runtime): bind a verification objective's subject to the case subject #156 — a verification case's objective checks the case's subject, not its verdict.
fix(runtime): type sweep and sample values by the parameter they bind #157 — sweep and sample values are typed by the parameter they bind (a Real swept over 1..4 binds 1.0…, an Integer over 1.0..3.0:1.0 binds Integers, ill-typed ranges are refused before any run). The only api/proto difference against main is this change's comment on the range fields; no message or field changed.
docs(examples): add expression feature walkthrough #147, docs(runtime): document scheduling, choice points and exploration #150, docs(design): propose SMT bounded model checking of behaviors #158 — expression-forms worked example, scheduling internals design note, SMT bounded-model-checking design note.

The release branch is cut from develop, merges origin/main (the earlier fold, so develop's copies of the three fragments folded by #154 are dropped without conflict), and adds one commit per round folding the eight fragments merged since into the existing ## 0.7.0 sections rather than opening a new version, since 0.7.0 is not yet tagged. The entry's date moves to 2026-09-10. changes/unreleased/ is back to its README only.

How it was verified

python3 scripts/changelog.py check and make docs-check pass on the fold.
gofmt -l . prints nothing; go build ./... and go vet ./... are clean.
api/proto differs from origin/main only in a field comment, so the wire-compatibility check against the released schema has nothing to flag.
Every change here was merged to develop through a green pull-request workflow; CircleCI on develop is green through the fix(runtime): type sweep and sample values by the parameter they bind #157 merge (5f5187298, including Go race tests and the SonarCloud gate); the fix(view): draw guarded entry transitions instead of marking every alternative initial #161 merge (7baacce13) is the latest commit brought over.

After merging: tag v0.7.0 on main, then merge main back into develop (plain merge) as docs/project/releasing.md describes.

Checklist

make test and make lint pass locally (the branch is develop plus a changelog fold; gofmt, go build, go vet and make docs-check re-run here)
Tests added or updated for the change — release fold only
Documentation extended where it already covers the surface — none needed
Changelog: fragments folded into the ## 0.7.0 entry, which is what a release branch does per docs/project/releasing.md
baselines regenerated and make docs-counts run if a gate count moved — no gate count moved
No internal work-item labels in the body, docs, or changelog

Add examples/expressions-demo.sysml and its walkthrough EXPRESSIONS-DEMO.md, taking casts, the unbounded value, .metadata, function values, sets, rank-three tensors and typed collection bodies through one payload model, and give each a section with REPL transcripts in the guide's expressions chapter. Pin the new example as stable in the RDF round-trip ratchet and re-record the examples count and digest in the differential baseline. Co-Authored-By: jason.han <[email protected]>

Instance ids in the walkthrough follow a session that also runs the intervening %calc commands, and the guide's redeclaration transcript shows the note the REPL prints after the error. Co-Authored-By: jason.han <[email protected]>

Add a design note on how a run resolves what the library leaves unordered: the six choice kinds and how each is recorded without altering the run, the reverse, declared, seed and explore policies, replay-based exploration from a fresh context per run, and the conformance contract of plural outcomes, .trace.order constraints, per-policy trace goldens and the declared/seed:1 sweep. Point the architecture, testing and orthogonal-regions notes at it, the last now describing scheduler-drawn region order for events and change triggers. List region order among the choice kinds the --trace, %trace and SchedulePolicy descriptions name, and add %schedule to the REPL guide's command table. Co-Authored-By: jason.han <[email protected]>

Re-record the pilot differential baseline over the 34-file examples root so the new example is in the measured census, not only in its provenance: 368 files, 600 pilot-only, 636 pilot diagnostics, with the generated counts in README, architecture, the differential record and the testing skills regenerated together. Write the example to what both implementations accept where the notation allows it: metadata reads cast the Metaobject to its metadata def, metadata sequences and the held function are ref features, and the Heritage default uses the default keyword. The four remaining pilot-only rows are a calc def passed as an argument, adjudicated as a deliberate extension. Co-Authored-By: jason.han <[email protected]>

Co-Authored-By: jason.han <[email protected]>

…rough beside the expressions demo Both walkthroughs now sit in the examples root, so the differential baseline and the RDF round-trip ratchet are re-recorded over the 35-file root: 369 files, 338 fully agreeing, 600 pilot-only, 636 pilot diagnostics; 348 stable round trips. The generated counts and the testing skills' figures follow. Co-Authored-By: jason.han <[email protected]>

Exploration permuted the tokens of one lockstep step, in which every steppable token moved once, so a branch of two nodes could never both run before a concurrent branch's one node and `complete` under-reported the admissible outcomes. Under `explore` a step is now one token advancing one node; the tokens able to act are picked among afresh after each move and each pick is its own choice point. Fixed policies keep their sweep. Adds `action_explore_write_between_branch_nodes`, re-derives the oracle's run counts at the new granularity, and updates the guide, CLI, wire and compliance prose. Co-Authored-By: jason.han <[email protected]>

…fore it A transition written without a source part (`accept go then s;`, `if c then s;`, `then s;`) leaves the closest lexically previous state usage in the body that declares it (SysML v2 7.18.3, TargetTransitionUsage), not the state whose body contains it. Lowering took the containing state, so the shorthand failed at a machine's top level and, nested in a composite state, fired from every substate (timers re-armed, entry actions re-ran). Derive the source in the AST helper, report a missing or non-vertex preceding member at the constraint tier with a typed error, and keep the same errors as a lowering backstop. Migrate fixtures and docs from the `state s { accept … then t; }` placement the pilot rejects to the flat form it accepts. Co-Authored-By: jason.han <[email protected]>

…and as its source The pilot's grammar rejects `accept … then` after an `in` parameter or a `succession first a then b;` just as after an attribute, so the constraint tier keeps naming that member as the source it cannot leave; a parameter is now named as such rather than as an attribute usage. Co-Authored-By: jason.han <[email protected]>

…o act A body paused on the clock whose wait has ended is an enabled move of an exploring step, an alternative to a sibling accept due at the same instant, rather than work swept up only after every ordinary token has acted. The fixed policies keep resuming paused bodies last. A dropped token pick restores the run's duplicate flag. Co-Authored-By: jason.han <[email protected]>

Co-Authored-By: jason.han <[email protected]>

* docs(examples): add expression feature walkthrough Add examples/expressions-demo.sysml and its walkthrough EXPRESSIONS-DEMO.md, taking casts, the unbounded value, .metadata, function values, sets, rank-three tensors and typed collection bodies through one payload model, and give each a section with REPL transcripts in the guide's expressions chapter. Pin the new example as stable in the RDF round-trip ratchet and re-record the examples count and digest in the differential baseline. Co-Authored-By: jason.han <[email protected]> * docs(examples): match walkthrough transcripts to a full session Instance ids in the walkthrough follow a session that also runs the intervening %calc commands, and the guide's redeclaration transcript shows the note the REPL prints after the error. Co-Authored-By: jason.han <[email protected]> * docs(examples): measure the expressions demo in the pilot differential Re-record the pilot differential baseline over the 34-file examples root so the new example is in the measured census, not only in its provenance: 368 files, 600 pilot-only, 636 pilot diagnostics, with the generated counts in README, architecture, the differential record and the testing skills regenerated together. Write the example to what both implementations accept where the notation allows it: metadata reads cast the Metaobject to its metadata def, metadata sequences and the held function are ref features, and the Heritage default uses the default keyword. The four remaining pilot-only rows are a calc def passed as an argument, adjudicated as a deliberate extension. Co-Authored-By: jason.han <[email protected]> * docs(examples): re-measure the examples root with the analysis walkthrough beside the expressions demo Both walkthroughs now sit in the examples root, so the differential baseline and the RDF round-trip ratchet are re-recorded over the 35-file root: 369 files, 338 fully agreeing, 600 pilot-only, 636 pilot diagnostics; 348 stable round trips. The generated counts and the testing skills' figures follow. 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]>

…ject An objective subject nothing binds now holds the case feature the library's objective states for it, read through the redefinition chain, instead of the case result for every case kind. Cases::Case::obj declares `subject subj default Case::result`; VerificationCases::VerificationCase::obj redefines it with `subject subj = VerificationCase::subj`, so a verification case's objective evaluates its requirement against the verification subject while an analysis case's still defaults to the result. The run's member index maps the features a declared member redefines to the name the run binds it under, so `VerificationCase::subj` resolves to the usage's own subject whatever the requirement names it. Co-Authored-By: jason.han <[email protected]>

Cover -analysis, -requirement, -satisfy and a -sweep over the case parameter, the REPL %analysis/%requirement/%satisfy commands, and gRPC RunAnalysis and VerifyRequirement, each reporting the objective decided beside the body verdict. Co-Authored-By: jason.han <[email protected]>

The compliance rows distinguish the analysis default (the case result) from the verification binding (the case subject); the behavior guide shows a requirement-typed objective decided against the verification subject. Co-Authored-By: jason.han <[email protected]>

…bjective-subject

A range's values were produced in the type its literals spelled: `1..4` over a Real parameter swept and sampled Integers, `1.0..3.0:1.0` over an Integer parameter wrote Reals through it, and `1.0..3.0:0.5` failed row by row instead of being refused. `ResolveSweepPlan` replaces `CheckSweepParameters`: it resolves each range against the target's effective parameter declaration and carries the parameter's type on the range. Integer, Natural and Positive parameters (and attribute defs specializing them) take Integers however the endpoints are written and refuse a fractional endpoint or step before any run; Real and Rational parameters take reals, so `1..4:1` binds and prints `1.0`..`4.0`; quantity parameters are typed through their `num` and keep the first endpoint's unit; Number-typed and untyped parameters read the range as written, the untyped one noted under the table; Boolean, String, enumeration and non-scalar parameters refuse a numeric range naming their type. Sampling follows the parameter's type: Integers inclusively, reals over `[from, to)`. A range between whole numbers needs no step whatever the parameter's type. Co-Authored-By: jason.han <[email protected]>

Lower a body's entry transitions (`entry; if c then s;`, `entry; then s;`, `entry action boot { … } if c then s;`) into StateGraph.EntryTransitions in declaration order and evaluate them each time the body is entered — at machine start and on every transition into the composite state, region or exhibited state whose body they belong to — after the body's entry behavior has run. The first alternative whose guard holds is entered; when none holds the executor returns ErrNoEntryTransitionHolds. An entry transition with a trigger or an effect, or whose target is not a state, is rejected by validation and lowering as the pinned pilot rejects those shapes. A state machine's own entry, do and exit behaviors now run for every machine, not only for one with orthogonal regions; the machine root is always built. A pseudostate, initial or final marker before a sourceless transition is reported rather than taken as its source. Co-Authored-By: jason.han <[email protected]>

…fixtures The pilot validator rejects an objective body whose only owned parameter is `in limit = limit;`: a usage's owned parameters redefine its definition's by position, so that input lands on the subject, which the verification library binds with `=`. Declaring `subject :>> subj;` ahead of the input is the shape the pilot accepts; the runtime decides both shapes identically, and the surface tests keep the bare-input shape. Co-Authored-By: jason.han <[email protected]>

A quantity parameter's dimension check admitted any magnitude, so a quantity redefining num as Natural or Positive took values below what that type holds and one whose num holds no number was swept as written. Each endpoint's magnitude is now admitted against the num's type before any row runs, naming the parameter and its type. Co-Authored-By: jason.han <[email protected]>

The wire contract, the proto comment, the Python client docstring and its integration test still stated that a range between reals must state a step; a range between whole numbers now steps by one whatever the parameter's type, and one with a fractional endpoint needs a step. Co-Authored-By: jason.han <[email protected]>

The state enterStartOf descends to is now the one a region records as active, the one events are scheduled from and the one checked for completion, on every path that enters a body: initialize, enterRegionsInto, moveBetweenRegions and enterOutside. An entry transition into done completes the machine as it starts, running its exit behavior, and a region's transition into a composite state whose alternative chooses a nested state leaves that state answering signals and arming its timer. Co-Authored-By: jason.han <[email protected]>

…t hold apart A range read as reals took an Integer endpoint or step through float64 before enumerating, so a Real parameter swept over 2^60..2^60+3 ran one row for four requested. An Integer endpoint or step no Real holds without rounding is now refused before any run, naming it and the parameter, and a stepped range whose consecutive rows would bind one value is refused rather than run. Co-Authored-By: jason.han <[email protected]>

…teps * fix(runtime): explore advances one token per step Exploration permuted the tokens of one lockstep step, in which every steppable token moved once, so a branch of two nodes could never both run before a concurrent branch's one node and `complete` under-reported the admissible outcomes. Under `explore` a step is now one token advancing one node; the tokens able to act are picked among afresh after each move and each pick is its own choice point. Fixed policies keep their sweep. Adds `action_explore_write_between_branch_nodes`, re-derives the oracle's run counts at the new granularity, and updates the guide, CLI, wire and compliance prose. Co-Authored-By: jason.han <[email protected]> * fix(runtime): explore picks a due paused body among the tokens able to act A body paused on the clock whose wait has ended is an enabled move of an exploring step, an alternative to a sibling accept due at the same instant, rather than work swept up only after every ordinary token has acted. The fixed policies keep resuming paused bodies last. A dropped token pick restores the run's duplicate flag. 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]>

Over a narrow real range lo + u*width can round to the end the range excludes. The step back to the real below the end, already applied where the width overflows, now applies to every real draw. Co-Authored-By: jason.han <[email protected]>

…ons all start in done Co-Authored-By: jason.han <[email protected]>

…negative step Co-Authored-By: jason.han <[email protected]>

Co-Authored-By: jason.han <[email protected]>

…nsitions say A region synthesized for a direct substate of a parallel state is now entered through the graph-only state standing for that substate: its entry behavior runs first, and its entry-transition guards then read the attributes that substate declares rather than the enclosing composite's frame, where they fell back to the declared defaults. Co-Authored-By: jason.han <[email protected]>

…tion needs an uncut relation Co-Authored-By: jason.han <[email protected]>

… needs bounded tokens and bus Co-Authored-By: jason.han <[email protected]>

…p carries a structural invariant Co-Authored-By: jason.han <[email protected]>

…the machine startsAt resolved its target with endpointVertex, which knows only declared vertices, so `transition begin then done;` and `succession first begin then done;` out of a named entry action found no vertex and fell through to the ordinary transition path, which rejects the entry action as a source. The target is now resolved with targetVertex, which synthesizes the body's completion state for an undeclared `done` exactly as `entry; then done;` does, so the named form starts complete too. Co-Authored-By: jason.han <[email protected]>

* docs(design): propose SMT bounded model checking of behaviors Co-Authored-By: jason.han <[email protected]> * docs(design): merge is stateless, sensitivity needs completion, induction needs an uncut relation Co-Authored-By: jason.han <[email protected]> * docs(design): sensitivity needs every schedule to complete; induction needs bounded tokens and bus Co-Authored-By: jason.han <[email protected]> * docs(design): order the sensitivity completion queries; induction step carries a structural invariant 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]>

…ject * fix(runtime): bind a verification objective's subject to the case subject An objective subject nothing binds now holds the case feature the library's objective states for it, read through the redefinition chain, instead of the case result for every case kind. Cases::Case::obj declares `subject subj default Case::result`; VerificationCases::VerificationCase::obj redefines it with `subject subj = VerificationCase::subj`, so a verification case's objective evaluates its requirement against the verification subject while an analysis case's still defaults to the result. The run's member index maps the features a declared member redefines to the name the run binds it under, so `VerificationCase::subj` resolves to the usage's own subject whatever the requirement names it. Co-Authored-By: jason.han <[email protected]> * test(cli,repl,grpc): decide a verification objective on every surface Cover -analysis, -requirement, -satisfy and a -sweep over the case parameter, the REPL %analysis/%requirement/%satisfy commands, and gRPC RunAnalysis and VerifyRequirement, each reporting the objective decided beside the body verdict. Co-Authored-By: jason.han <[email protected]> * docs(project): record verification objective subject binding The compliance rows distinguish the analysis default (the case result) from the verification binding (the case subject); the behavior guide shows a requirement-typed objective decided against the verification subject. Co-Authored-By: jason.han <[email protected]> * test(runtime): state the objective subject first in the verification fixtures The pilot validator rejects an objective body whose only owned parameter is `in limit = limit;`: a usage's owned parameters redefine its definition's by position, so that input lands on the subject, which the verification library binds with `=`. Declaring `subject :>> subj;` ahead of the input is the shape the pilot accepts; the runtime decides both shapes identically, and the surface tests keep the bare-input shape. 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]>

* fix(runtime): type sweep and sample values by the parameter they bind A range's values were produced in the type its literals spelled: `1..4` over a Real parameter swept and sampled Integers, `1.0..3.0:1.0` over an Integer parameter wrote Reals through it, and `1.0..3.0:0.5` failed row by row instead of being refused. `ResolveSweepPlan` replaces `CheckSweepParameters`: it resolves each range against the target's effective parameter declaration and carries the parameter's type on the range. Integer, Natural and Positive parameters (and attribute defs specializing them) take Integers however the endpoints are written and refuse a fractional endpoint or step before any run; Real and Rational parameters take reals, so `1..4:1` binds and prints `1.0`..`4.0`; quantity parameters are typed through their `num` and keep the first endpoint's unit; Number-typed and untyped parameters read the range as written, the untyped one noted under the table; Boolean, String, enumeration and non-scalar parameters refuse a numeric range naming their type. Sampling follows the parameter's type: Integers inclusively, reals over `[from, to)`. A range between whole numbers needs no step whatever the parameter's type. Co-Authored-By: jason.han <[email protected]> * fix(runtime): bound a swept quantity's magnitude by its num type A quantity parameter's dimension check admitted any magnitude, so a quantity redefining num as Natural or Positive took values below what that type holds and one whose num holds no number was swept as written. Each endpoint's magnitude is now admitted against the num's type before any row runs, naming the parameter and its type. Co-Authored-By: jason.han <[email protected]> * test(python): a Real range between whole numbers steps by one The wire contract, the proto comment, the Python client docstring and its integration test still stated that a range between reals must state a step; a range between whole numbers now steps by one whatever the parameter's type, and one with a fractional endpoint needs a step. Co-Authored-By: jason.han <[email protected]> * fix(runtime): refuse a real range whose Integers or step a Real cannot hold apart A range read as reals took an Integer endpoint or step through float64 before enumerating, so a Real parameter swept over 2^60..2^60+3 ran one row for four requested. An Integer endpoint or step no Real holds without rounding is now refused before any run, naming it and the parameter, and a stepped range whose consecutive rows would bind one value is refused rather than run. Co-Authored-By: jason.han <[email protected]> * fix(runtime): keep a real sample below the range's end when it rounds up Over a narrow real range lo + u*width can round to the end the range excludes. The step back to the real below the end, already applied where the width overflows, now applies to every real draw. Co-Authored-By: jason.han <[email protected]> * test(runtime): a Natural or Positive parameter sweeps downwards by a negative step 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]>

…nherits A typed or specializing state that writes entry transitions of its own now starts by them alone, as its own entry behavior replaces the inherited one; a state writing none keeps the inherited start. Co-Authored-By: jason.han <[email protected]>

The bounded-model-checking and pseudostate notes described the executor's schedule as deterministic and fixed region firing to declaration order. Transition, guard and region-order choices are drawn by the run's policy; only region entry and exit order stays declaration order. Co-Authored-By: jason.han <[email protected]>

* fix(lower): source a sourceless transition from the state declared before it A transition written without a source part (`accept go then s;`, `if c then s;`, `then s;`) leaves the closest lexically previous state usage in the body that declares it (SysML v2 7.18.3, TargetTransitionUsage), not the state whose body contains it. Lowering took the containing state, so the shorthand failed at a machine's top level and, nested in a composite state, fired from every substate (timers re-armed, entry actions re-ran). Derive the source in the AST helper, report a missing or non-vertex preceding member at the constraint tier with a typed error, and keep the same errors as a lowering backstop. Migrate fixtures and docs from the `state s { accept … then t; }` placement the pilot rejects to the flat form it accepts. Co-Authored-By: jason.han <[email protected]> * test(passes): pin a parameter or written succession before the shorthand as its source The pilot's grammar rejects `accept … then` after an `in` parameter or a `succession first a then b;` just as after an attribute, so the constraint tier keeps naming that member as the source it cannot leave; a parameter is now named as such rather than as an attribute usage. Co-Authored-By: jason.han <[email protected]> * feat(runtime): select the start state with guarded entry transitions Lower a body's entry transitions (`entry; if c then s;`, `entry; then s;`, `entry action boot { … } if c then s;`) into StateGraph.EntryTransitions in declaration order and evaluate them each time the body is entered — at machine start and on every transition into the composite state, region or exhibited state whose body they belong to — after the body's entry behavior has run. The first alternative whose guard holds is entered; when none holds the executor returns ErrNoEntryTransitionHolds. An entry transition with a trigger or an effect, or whose target is not a state, is rejected by validation and lowering as the pinned pilot rejects those shapes. A state machine's own entry, do and exit behaviors now run for every machine, not only for one with orthogonal regions; the machine root is always built. A pseudostate, initial or final marker before a sourceless transition is reported rather than taken as its source. Co-Authored-By: jason.han <[email protected]> * fix(runtime): keep the state an entry transition descends to active The state enterStartOf descends to is now the one a region records as active, the one events are scheduled from and the one checked for completion, on every path that enters a body: initialize, enterRegionsInto, moveBetweenRegions and enterOutside. An entry transition into done completes the machine as it starts, running its exit behavior, and a region's transition into a composite state whose alternative chooses a nested state leaves that state answering signals and arming its timer. Co-Authored-By: jason.han <[email protected]> * fix(runtime): complete a machine entering a parallel state whose regions all start in done Co-Authored-By: jason.han <[email protected]> * fix(runtime): start a parallel region where its own state's entry transitions say A region synthesized for a direct substate of a parallel state is now entered through the graph-only state standing for that substate: its entry behavior runs first, and its entry-transition guards then read the attributes that substate declares rather than the enclosing composite's frame, where they fell back to the declared defaults. Co-Authored-By: jason.han <[email protected]> * fix(lower): let a named entry action's transition into done complete the machine startsAt resolved its target with endpointVertex, which knows only declared vertices, so `transition begin then done;` and `succession first begin then done;` out of a named entry action found no vertex and fell through to the ordinary transition path, which rejects the entry action as a source. The target is now resolved with targetVertex, which synthesizes the body's completion state for an undeclared `done` exactly as `entry; then done;` does, so the named form starts complete too. Co-Authored-By: jason.han <[email protected]> * fix(lower): let a state's own entry transitions replace the ones it inherits A typed or specializing state that writes entry transitions of its own now starts by them alone, as its own entry behavior replaces the inherited one; a state writing none keeps the inherited start. 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]>

* docs(runtime): document scheduling, choice points and exploration Add a design note on how a run resolves what the library leaves unordered: the six choice kinds and how each is recorded without altering the run, the reverse, declared, seed and explore policies, replay-based exploration from a fresh context per run, and the conformance contract of plural outcomes, .trace.order constraints, per-policy trace goldens and the declared/seed:1 sweep. Point the architecture, testing and orthogonal-regions notes at it, the last now describing scheduler-drawn region order for events and change triggers. List region order among the choice kinds the --trace, %trace and SchedulePolicy descriptions name, and add %schedule to the REPL guide's command table. Co-Authored-By: jason.han <[email protected]> * docs(runtime): drop deterministic-schedule wording from design notes The bounded-model-checking and pseudostate notes described the executor's schedule as deterministic and fixed region firing to declaration order. Transition, guard and region-order choices are drawn by the run's policy; only region entry and exit order stays declaration order. 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]>

…lease branch was cut Co-Authored-By: jason.han <[email protected]>

devin-ai-integration · 2026-09-10T01:45:09Z

🤖 Devin AI Engineer

I'll be helping with this pull request! Here's what you should know:

✅ I will automatically:

Address comments on this PR. Add '(aside)' to your comment to have me ignore it.
Look at CI failures and help fix them

Note: I can only respond to comments from users who have write access to this repository.

⚙️ Control Options:

Disable automatic comment, CI, and merge conflict monitoring

…ternative initial A body's entry transitions are now edges from a start node of that body into their targets, in declaration order, carrying the guard as ordinary transition edges do; Mermaid draws them as `[*] --> target : [guard]` inside the body. The `initial` detail is reserved for the target of a body's first entry transition when that one is unguarded, via the exported StateGraph.UnconditionalStart; StateGraph.IsInitial keeps meaning "may start here" for lowering and the runtime. Co-Authored-By: jason.han <[email protected]>

A body's entry transitions are now edges from a start node of that body into their targets, in declaration order, carrying the guard as ordinary transition edges do; Mermaid draws them as `[*] --> target : [guard]` inside the body. The `initial` detail is reserved for the target of a body's first entry transition when that one is unguarded, via the exported StateGraph.UnconditionalStart; StateGraph.IsInitial keeps meaning "may start here" for lowering and the runtime. Co-authored-by: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Co-authored-by: jason.han <[email protected]>

… entry Co-Authored-By: jason.han <[email protected]>

devin-ai-integration Bot and others added 30 commits September 9, 2026 17:33

Merge branch 'main' into docs/expression-features-guide

1a4c6f0

Co-Authored-By: jason.han <[email protected]>

chore: merge develop into feature/explore-single-token-steps

b107fdd

Co-Authored-By: jason.han <[email protected]>

Merge remote-tracking branch 'origin/develop' into fix/verification-o…

26ff886

…bjective-subject

fix(runtime): complete a machine entering a parallel state whose regi…

ed58cb3

…ons all start in done Co-Authored-By: jason.han <[email protected]>

test(runtime): a Natural or Positive parameter sweeps downwards by a …

9cb8edc

…negative step Co-Authored-By: jason.han <[email protected]>

docs(design): propose SMT bounded model checking of behaviors

749aa88

Co-Authored-By: jason.han <[email protected]>

docs(design): merge is stateless, sensitivity needs completion, induc…

e744fcc

…tion needs an uncut relation Co-Authored-By: jason.han <[email protected]>

devin-ai-integration Bot and others added 12 commits September 10, 2026 00:47

docs(design): sensitivity needs every schedule to complete; induction…

d4d6dbf

… needs bounded tokens and bus Co-Authored-By: jason.han <[email protected]>

docs(design): order the sensitivity completion queries; induction ste…

c52031e

…p carries a structural invariant Co-Authored-By: jason.han <[email protected]>

Merge remote-tracking branch 'origin/main' into release/0.7.0

dd395a8

chore(release): fold the 0.7.0 changelog fragments added since the re…

5f45ccf

…lease branch was cut Co-Authored-By: jason.han <[email protected]>

devin-ai-integration Bot assigned HuiJun Sep 10, 2026

devin-ai-integration Bot requested a review from HuiJun September 10, 2026 01:45

devin-ai-integration Bot changed the base branch from develop to main September 10, 2026 01:45

devin-ai-integration Bot closed this Sep 10, 2026

devin-ai-integration Bot reopened this Sep 10, 2026

devin-ai-integration Bot marked this pull request as ready for review September 10, 2026 02:04

This comment was marked as resolved.

Sign in to view

devin-ai-integration Bot and others added 4 commits September 10, 2026 02:42

Merge remote-tracking branch 'origin/develop' into release/0.7.0

4d9fa8b

chore(release): fold the state-rendering fix into the 0.7.0 changelog…

92d476b

… entry Co-Authored-By: jason.han <[email protected]>

HuiJun merged commit e0fbfea into main Sep 10, 2026
12 checks passed

HuiJun deleted the release/0.7.0 branch September 10, 2026 03:49

Navigation Menu

Uh oh!

chore(release): 0.7.0 — bring the analysis fixes on develop onto main - #159

chore(release): 0.7.0 — bring the analysis fixes on develop onto main#159
HuiJun merged 46 commits into
mainfrom
release/0.7.0

devin-ai-integration Bot commented Sep 10, 2026 •

edited

Loading

Uh oh!

devin-ai-integration Bot commented Sep 10, 2026

Uh oh!

This comment was marked as resolved.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

devin-ai-integration Bot commented Sep 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What and why

How it was verified

Checklist

Uh oh!

devin-ai-integration Bot commented Sep 10, 2026

🤖 Devin AI Engineer

Uh oh!

This comment was marked as resolved.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

devin-ai-integration Bot commented Sep 10, 2026 •

edited

Loading