Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
46 commits
Select commit Hold shift + click to select a range
2f8e723
docs(examples): add expression feature walkthrough
devin-ai-integration[bot] Sep 9, 2026
b858410
docs(examples): match walkthrough transcripts to a full session
devin-ai-integration[bot] Sep 9, 2026
27ec257
docs(runtime): document scheduling, choice points and exploration
devin-ai-integration[bot] Sep 9, 2026
b506467
docs(examples): measure the expressions demo in the pilot differential
devin-ai-integration[bot] Sep 9, 2026
1a4c6f0
Merge branch 'main' into docs/expression-features-guide
devin-ai-integration[bot] Sep 9, 2026
a52275f
docs(examples): re-measure the examples root with the analysis walkth…
devin-ai-integration[bot] Sep 9, 2026
a8c12b7
fix(runtime): explore advances one token per step
devin-ai-integration[bot] Sep 9, 2026
07a9d8d
fix(lower): source a sourceless transition from the state declared be…
devin-ai-integration[bot] Sep 9, 2026
872ccd7
test(passes): pin a parameter or written succession before the shorth…
devin-ai-integration[bot] Sep 9, 2026
ea5266d
fix(runtime): explore picks a due paused body among the tokens able t…
devin-ai-integration[bot] Sep 9, 2026
b107fdd
chore: merge develop into feature/explore-single-token-steps
devin-ai-integration[bot] Sep 9, 2026
be8991d
Merge pull request #147 from Open-MBEE/docs/expression-features-guide
HuiJun Sep 9, 2026
5594c3d
fix(runtime): bind a verification objective's subject to the case sub…
devin-ai-integration[bot] Sep 9, 2026
b829fec
test(cli,repl,grpc): decide a verification objective on every surface
devin-ai-integration[bot] Sep 9, 2026
68ad9ca
docs(project): record verification objective subject binding
devin-ai-integration[bot] Sep 9, 2026
26ff886
Merge remote-tracking branch 'origin/develop' into fix/verification-o…
devin-ai-integration[bot] Sep 9, 2026
b13337e
fix(runtime): type sweep and sample values by the parameter they bind
devin-ai-integration[bot] Sep 9, 2026
6194d6b
feat(runtime): select the start state with guarded entry transitions
devin-ai-integration[bot] Sep 9, 2026
e77c191
test(runtime): state the objective subject first in the verification …
devin-ai-integration[bot] Sep 9, 2026
4bf120d
fix(runtime): bound a swept quantity's magnitude by its num type
devin-ai-integration[bot] Sep 9, 2026
bcca4ee
test(python): a Real range between whole numbers steps by one
devin-ai-integration[bot] Sep 9, 2026
bdb21ea
fix(runtime): keep the state an entry transition descends to active
devin-ai-integration[bot] Sep 10, 2026
2c85a5b
fix(runtime): refuse a real range whose Integers or step a Real canno…
devin-ai-integration[bot] Sep 10, 2026
8706d0b
Merge pull request #153 from Open-MBEE/feature/explore-single-token-s…
HuiJun Sep 10, 2026
4150314
fix(runtime): keep a real sample below the range's end when it rounds up
devin-ai-integration[bot] Sep 10, 2026
ed58cb3
fix(runtime): complete a machine entering a parallel state whose regi…
devin-ai-integration[bot] Sep 10, 2026
9cb8edc
test(runtime): a Natural or Positive parameter sweeps downwards by a …
devin-ai-integration[bot] Sep 10, 2026
749aa88
docs(design): propose SMT bounded model checking of behaviors
devin-ai-integration[bot] Sep 10, 2026
791b357
fix(runtime): start a parallel region where its own state's entry tra…
devin-ai-integration[bot] Sep 10, 2026
e744fcc
docs(design): merge is stateless, sensitivity needs completion, induc…
devin-ai-integration[bot] Sep 10, 2026
d4d6dbf
docs(design): sensitivity needs every schedule to complete; induction…
devin-ai-integration[bot] Sep 10, 2026
c52031e
docs(design): order the sensitivity completion queries; induction ste…
devin-ai-integration[bot] Sep 10, 2026
302ccc8
fix(lower): let a named entry action's transition into done complete …
devin-ai-integration[bot] Sep 10, 2026
9e12dfa
Merge pull request #158 from Open-MBEE/docs/smt-model-checking
HuiJun Sep 10, 2026
4be399d
Merge pull request #156 from Open-MBEE/fix/verification-objective-sub…
HuiJun Sep 10, 2026
5f51872
Merge pull request #157 from Open-MBEE/fix/sweep-parameter-typing
HuiJun Sep 10, 2026
a115d69
fix(lower): let a state's own entry transitions replace the ones it i…
devin-ai-integration[bot] Sep 10, 2026
92d616c
docs(runtime): drop deterministic-schedule wording from design notes
devin-ai-integration[bot] Sep 10, 2026
c27e84f
Merge pull request #155 from Open-MBEE/fix/target-transition-source
HuiJun Sep 10, 2026
2ca20b8
Merge pull request #150 from Open-MBEE/docs/execution-choice-internals
HuiJun Sep 10, 2026
dd395a8
Merge remote-tracking branch 'origin/main' into release/0.7.0
devin-ai-integration[bot] Sep 10, 2026
5f45ccf
chore(release): fold the 0.7.0 changelog fragments added since the re…
devin-ai-integration[bot] Sep 10, 2026
618423a
fix(view): draw guarded entry transitions instead of marking every al…
devin-ai-integration[bot] Sep 10, 2026
7baacce
Merge pull request #161 from Open-MBEE/fix/view-guarded-entry-initials
HuiJun Sep 10, 2026
4d9fa8b
Merge remote-tracking branch 'origin/develop' into release/0.7.0
devin-ai-integration[bot] Sep 10, 2026
92d476b
chore(release): fold the state-rendering fix into the 0.7.0 changelog…
devin-ai-integration[bot] Sep 10, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions .agents/skills/testing-pilot-corpora-gate/SKILL.md
Original file line number Diff line number Diff line change
Expand Up @@ -183,8 +183,8 @@ gate's own helpers are package-private but reusable (`pilotCorporaGate.files(t)`

`actionlint`, `shellcheck`, `python3 scripts/check-doc-links.py`, `gofmt`, `go vet`,
`go run ./cmd/pilot-diff` (validators pre-downloaded; ~4min, prints e.g.
the headline the committed baseline holds — `368 file(s), 338 fully agreeing; 34 agreed
diagnostic(s), 21 only ours, 596 only the pilot's` after the unbound-parameter round, so read it from
the headline the committed baseline holds — `369 file(s), 338 fully agreeing; 34 agreed
diagnostic(s), 21 only ours, 600 only the pilot's` after the expressions example joined `examples/`, so read it from
`docs/project/pilot-differential-baseline.json` rather than from this line)
and `make lint` (staticcheck+gosec, ~2min) all work. There is **no** `yamllint` and **no**
`circleci` CLI, so `.circleci/config.yml` can only be parsed as YAML, not schema-validated — say so
Expand Down
10 changes: 5 additions & 5 deletions .agents/skills/testing-pilot-differential/SKILL.md
Original file line number Diff line number Diff line change
Expand Up @@ -21,9 +21,9 @@ GNU-format diagnostics **relative to `--root`**. Consequences for testing:
- The pin `cmd/pilot-diff` reports comes from `build/pilot-sysml-validator/pilot-pin.txt`
(written by the new script), not from the DeciSym `pom.xml`.
- `-validator /nonexistent` now says `run ./scripts/download-pilot-sysml-validator.sh`.
- Measured after the unbound-parameter round, with a fresh library cache: `368 file(s), 338 fully agreeing; 34 agreed,
21 only ours, 596 only the pilot's`, JSON totals `openSysMLDiagnostics 57 / pilotDiagnostics
632 / severityMismatch 2`; ~2 min wall, byte-identical across runs *and* after a from-scratch
- Measured after the expressions example joined `examples/`, with a fresh library cache: `369 file(s), 338 fully agreeing; 34 agreed,
21 only ours, 600 only the pilot's`, JSON totals `openSysMLDiagnostics 57 / pilotDiagnostics
636 / severityMismatch 2`; ~2 min wall, byte-identical across runs *and* after a from-scratch
rebuild of `build/pilot-validator`. `kerml-examples` carries no `syntax` diagnostic on either
side. Refresh this paragraph with every rebaseline, and treat a stale one as a finding.
- **`cmd/pilot-diff` has no `-jobs` flag.** Its full flag set is
Expand Down Expand Up @@ -134,8 +134,8 @@ The harness compares OpenSysML diagnostics against the OMG SysML v2 Pilot Implem
(via two pinned plain-Java bridges over the pilot's own validators) over four corpus roots and writes
`build/pilot-diff/pilot-diff.{txt,json}`. `docs/project/pilot-differential-baseline.json` is the
committed result of the *last refreshed* run, so **the harness is testable by reproduction** —
but only while the baseline is current. Check that first. As of the rebaseline that came with the unbound-parameter round it **is**
current: a live run gives `368 file(s), 338 fully agreeing; 34 agreed, 21 only ours, 596 only the
but only while the baseline is current. Check that first. As of the rebaseline that came with the expressions walkthrough round it **is**
current: a live run gives `369 file(s), 338 fully agreeing; 34 agreed, 21 only ours, 600 only the
pilot's`, byte-identical to the committed baseline, and `docs/project/pilot-differential.md`'s
"Results" table matches. The rebaseline before it, at the architecture self-model's landing, covered two rounds, because the succession-shorthand
removal before it landed without refreshing the baseline; a control run of its merge commit gives
Expand Down
4 changes: 2 additions & 2 deletions .agents/skills/testing-pilot-execution-referee/SKILL.md
Original file line number Diff line number Diff line change
Expand Up @@ -108,8 +108,8 @@ subset it or none does (and folds a `default null` one to `0`). See
`pilot-exec-diff: <file>:<line>: model no/such/model.sysml: stat <abs>: no
such file or directory`.
- **Additivity.** `go run ./cmd/pilot-diff` must still print the headline the
committed baseline holds (`368 file(s), 338 fully agreeing; 34 agreed
diagnostic(s), 21 only ours, 596 only the pilot's` after the unbound-parameter round — read it from the baseline JSON, not from this line, since each
committed baseline holds (`369 file(s), 338 fully agreeing; 34 agreed
diagnostic(s), 21 only ours, 600 only the pilot's` after the expressions example joined `examples/` — read it from the baseline JSON, not from this line, since each
fix round moves it) and `jq -S` diff clean against
`docs/project/pilot-differential-baseline.json`; `git status --porcelain`
empty at the end.
Expand Down
4 changes: 2 additions & 2 deletions .agents/skills/testing-pilot-xpect/SKILL.md
Original file line number Diff line number Diff line change
Expand Up @@ -416,8 +416,8 @@ census in `w5c_census_test.go` is live two ways: perturb one pinned triple (e.g.
## Regression neighbour

`go run ./cmd/pilot-diff` (~1m12s) must still print the headline the *committed* baseline holds —
after the unbound-parameter round that is `368 file(s), 338 fully agreeing; 34 agreed diagnostic(s), 21
only ours, 596 only the pilot's`. Read the number out of
after the expressions walkthrough round that is `369 file(s), 338 fully agreeing; 34 agreed diagnostic(s), 21
only ours, 600 only the pilot's`. Read the number out of
`docs/project/pilot-differential-baseline.json` rather than trusting this line, since a landing fix
round moves it. When the baseline is itself stale (it was at `19a3ce03`, holding 273 / 281 / 317), a
failing `cmp` against it is *not* evidence of an Xpect regression — compare the summary line, and see
Expand Down
10 changes: 5 additions & 5 deletions .agents/skills/testing-sysml-repl/SKILL.md
Original file line number Diff line number Diff line change
Expand Up @@ -2233,7 +2233,7 @@ fixed from broken, each with a visible A/B against `main`:
- **Calc parameter** — `in redefines factor = 3;` overriding an inherited `in factor = 2`. The
giveaway is a *wrong number*, not an error: the invocation silently uses the inherited default
(`Scaled(7)` → 14 instead of 21), so assert the value, never just "it evaluated".
- **State** — `state redefines waiting { accept go then active; }`. A lost name makes the sourceless
- **State** — `state redefines waiting; accept go then active;`. A lost name makes the sourceless
accept vanish: `%state` shows `Events: 0` and `%advance 1` never leaves the initial state.

Ready-made fixtures for all of these live in `internal/core/runtime/testdata/conformance/`
Expand Down Expand Up @@ -3596,7 +3596,7 @@ False-positive traps to always include as *legal* rows, since each exercises a d
one; run it with `%state TransitionSiblingRegion` + `%advance 1` → `Current state: lidle | rtarget`
and `crossed = 1`.
- `entry point into;` / `exit point outOf;` as endpoints (`state_entry_exit_points.sysml`).
- A sourceless `accept after 5 then <s>;` written *inside* a state (source is implicit).
- A sourceless `accept after 5 then <s>;` written after a state (the source is the state declared before it).
- `first start then off;` with no `initial`.
- A junction left by a **succession** (`route then finishedUp;`) rather than a `transition`, and a
`fork`/`join` reached by one — the pass tracks succession sources *by name*, so a regression here
Expand Down Expand Up @@ -5250,7 +5250,7 @@ to diff against a document's table verbatim.
Use `%send <SignalName> [to <object>]` followed by `%step` to drive signal transitions.
The signal lists in `internal/core/runtime/testdata/conformance/*.expected.json` belong to the
conformance harness and are not automatically injected by the REPL. Alternatively, write
fixtures with **timed triggers** (`state a { accept after 5 then done; }`)
fixtures with **timed triggers** (`state a; accept after 5 then done;`)
and step them with `%advance <t>`; each region can be given
a different delay so a partial configuration is observable. `sysml <model> -state <name>` only
*starts* the executor and prints the initial configuration — it does not run to completion, so use
Expand Down Expand Up @@ -5280,8 +5280,8 @@ Completion (a transition whose endpoint is the unqualified `done`) shows up as,
```sysml
state def M { entry; then outer;
state outer parallel {
state r1 { entry; then x; state x { accept after 5 then done; } }
state r2 { entry; then y; state y { accept after 7 then done; } } } }
state r1 { entry; then x; state x; accept after 5 then done; }
state r2 { entry; then y; state y; accept after 7 then done; } } }
```
`%advance 5` → `done | y` + `Running`, no completion line; `%advance 2` → `done | done` + `Completed`.
Add a *two-level* variant (a `parallel` state inside a region of another `parallel` state) whose inner
Expand Down
Loading
Loading