JPL-Devin · HuiJun · Aug 18, 2026 · Aug 18, 2026 · Aug 18, 2026
diff --git a/CHANGELOG.md b/CHANGELOG.md
diff --git a/README.md b/README.md
@@ -135,6 +135,7 @@ sysml> %advance 30
 
 - **Language Server** — A standard LSP server (`sysml-lsp`) with live diagnostics, semantic hover, go-to-definition, find references, completion, workspace-wide symbol search, formatting, rename, semantic tokens and quick fixes. A VS Code extension with TextMate grammars for `.sysml` and `.kerml` ships in [editors/vscode](editors/vscode), and any editor with a generic LSP client can drive the server directly — [guide chapter 8](docs/guide/08-editors.md) walks through both. *Not yet:* the extension is built from source rather than published to a marketplace, and the server answers no semantic token delta requests or signature help.
 - **Interactive REPL** — Exploratory modeling environment: define models incrementally, evaluate expressions on-the-fly, instantiate parts, run calculations, inspect runtime state—like IPython/Jupyter for systems engineering.
+- **Constraint Solving** *(experimental)* — Beyond evaluating what holds of an object: an external SMT solver answers whether a constraint, requirement or satisfaction assertion *can* hold, which conditions conflict when it cannot, what values would satisfy it, which variants a model permits, and what optimizes an `analysis def`'s objectives. The solver is optional and discovered at runtime — [the REPL command reference](docs/reference/repl-commands.md) documents each command and [installing a solver](docs/guide/01-install.md#installing-a-solver-optional) how to get one.
 - **Execution Runtime** — Not just a validator: instantiate parts, evaluate constraints against concrete values, execute calc/analysis cases. Action/state executor infrastructure complete (activity fork/join parallelism, decision guards, hierarchical/orthogonal states, choice/junction pseudostates, TimeEvent/ChangeEvent/AcceptEvent, sourceless transitions). See [spec compliance](docs/project/spec-compliance.md) for measured behavioral coverage.
 - **Python Client Library** — gRPC-based Python bindings for programmatic access: parse models, resolve symbols, evaluate expressions, instantiate parts, execute actions/state machines. Includes IPython display hooks for Jupyter notebooks and pandas DataFrame integration. Constraint, requirement, satisfaction and calc verdicts are available as RPCs (`verify_constraint`, `verify_requirement`, `verify_satisfaction`, `calc`).
 - **Modern Toolchain** — Incremental compilation, bundled standard library, persistent semantic caches. A model is a set of files, named on the command line or opened by the editor.
@@ -167,10 +168,13 @@ sysml> %advance 30
 | REPL debugging commands | ✅ Complete — `%constraint`, `%requirement`, `%satisfy` and `%calc` also answer from the command line (`-constraint`, `-requirement`, `-satisfy`, `-calc`) and over gRPC, on one evaluation |
 | Model save to notation (`%save model.sysml`, `sysml -convert sysml`) | ✅ Complete — writes the source through the formatter, so comments and spacing survive |
 | SysML ↔ RDF Turtle conversion (`%save model.ttl`, `sysml -convert ttl`) | 🧪 **Experimental** — packages, definitions, usages, ports, connections, values, documentation, and the nodes an action or state body states (102 of 120 `examples/` models convert; what is not mapped is refused with the construct named), but the vocabulary may change without a compatibility path. Every run says so; see [the RDF mapping's status](docs/reference/rdf-mapping.md#status-experimental) and [worked example](examples/rdf-interop-demo.sysml) |
+| View rendering (`%render <view>`, `sysml -render`) | ✅ Complete for the kinds produced — containment tree, interconnection diagram, state machine, action flow and table, as indented text or in the kind's machine-readable form (Mermaid, Markdown). State and action renderings read the graph the runtime executes; the notation itself is tool-defined ([SysML v2 §10.2](docs/project/spec-compliance.md)) |
+| Constraint solving (`%check`, `%explain`, `%solve`, `%configure`, `%optimize`) | 🧪 **Experimental** — an external SMT-LIB 2 solver decides whether conditions *can* be satisfied, explains an `unsat` with a minimal unsat core, synthesises satisfying values, enumerates the variant selections a model permits and optimizes an `analysis def`'s objectives (optimization needs z3, which implements it). The solver is optional and discovered on `PATH` or through `OPENSYSML_SMT`; a build with none reports that rather than a verdict — see [installing a solver](docs/guide/01-install.md#installing-a-solver-optional) |
+| Source-preserving model edits (`ApplyEdits`, `model.edit()`) | ✅ Complete for the two operations offered — set a feature's value, rename a declaration — rewriting the bytes of the model's own source so every untouched byte is identical. A rename of a referenced element, and element creation or deletion, are refused rather than approximated |
 | Standard library bundling | ✅ Complete |
 | LSP server implementation | ✅ Diagnostics, hover, go-to-definition, references, symbols, completion, formatting, rename, semantic tokens (full + range), code actions (quick fixes) — semantic token deltas and signature help not implemented |
-| gRPC service layer | ✅ Complete (parse, symbols, diagnostics, runtime, verification, conversion and Query RPCs) |
-| Python client library | ✅ Complete for the RPCs that exist (connection lifecycle, parse/symbols/eval/instantiate/execute, constraint/requirement/satisfaction/calc verification, conversion, Query, IPython hooks, DataFrame) |
+| gRPC service layer | ✅ Complete (parse, symbols, diagnostics, runtime, verification, conversion, edit and Query RPCs) |
+| Python client library | ✅ Complete for the RPCs that exist (connection lifecycle, parse/symbols/eval/instantiate/execute, constraint/requirement/satisfaction/calc verification, conversion, edits, Query, IPython hooks, DataFrame) |
 
 **Current commit:** All tests pass (`go test -race ./...`), builds clean (`go build ./...`).
 **Test coverage:** 4,447 tests and subtests (4,440 pass, 7 skip themselves; 2,351 top-level `Test` functions) covering parsers, semantics, runtime (actions, states, instances, operators, validation). Behavioral robustness: 86 golden ASTs, 129 negatives, 297 conformance cases, 98 golden traces, 165 runtime robustness cases and 8 gRPC ones.

diff --git a/docs/project/releasing.md b/docs/project/releasing.md
@@ -325,7 +325,7 @@ whole rule, so the happy path has no extra switch to forget. To rehearse a
 release:
 
 ```bash
-# 1. Declare a pre-release version, e.g. VERSION = "0.1.0rc1"
+# 1. Declare a pre-release version, e.g. VERSION = "0.3.0rc1"
 $EDITOR python/opensysml/_version.py
 # 2. Land it, then tag it
 git tag -a opensysml-v0.3.0rc1 -m "opensysml 0.3.0rc1" && git push origin opensysml-v0.3.0rc1
@@ -339,7 +339,7 @@ dependencies from PyPI:
 ```bash
 python -m venv /tmp/opensysml-rc && . /tmp/opensysml-rc/bin/activate
 pip install --index-url https://test.pypi.org/simple/ \
-            --extra-index-url https://pypi.org/simple/ opensysml==0.1.0rc1
+            --extra-index-url https://pypi.org/simple/ opensysml==0.3.0rc1
 python -c "import opensysml; print(opensysml.__version__)"
 ```
 
@@ -354,8 +354,8 @@ In a clean virtualenv, from the index — not from the source tree:
 
 ```bash
 python -m venv /tmp/opensysml-verify && . /tmp/opensysml-verify/bin/activate
-pip install opensysml==0.1.0
-python -c "import opensysml; print(opensysml.__version__)"    # must print 0.1.0
+pip install opensysml==0.3.0
+python -c "import opensysml; print(opensysml.__version__)"    # must print 0.3.0
 ```
 
 Then check the client end to end against a published core release, since that

diff --git a/examples/README.md b/examples/README.md
@@ -20,6 +20,17 @@ That fetches `sysml/src/training` from the pinned pilot release
 [docs/project/training-examples.md](../docs/project/training-examples.md), with the files that
 still report errors and why.
 
+## Walkthroughs
+
+Each of these is a model and a walkthrough of the commands that exercise it.
+
+| Model | Walkthrough | What it demonstrates |
+| --- | --- | --- |
+| [solver-demo.sysml](solver-demo.sysml) | [SOLVER-DEMO.md](SOLVER-DEMO.md) | `%check`, `%explain`, `%solve`, `%configure` and `%optimize` — what conditions *can* hold, which conflict, what satisfies them, which variants are permitted, what is best (needs z3 or cvc5) |
+| [views-demo.sysml](views-demo.sysml) | [VIEWS-DEMO.md](VIEWS-DEMO.md) | `%view` and `%render` — the five rendering kinds, the text/Mermaid/Markdown forms, viewpoint conformance and filtered exposure |
+| [action-executor-demo.sysml](action-executor-demo.sysml) | [ACTION-EXECUTOR-DEMO.md](ACTION-EXECUTOR-DEMO.md) | executing actions, and stepping one in the REPL |
+| `parser_features_demo_*.sysml`/`.kerml` | [PARSER_FEATURES_DEMOS.md](PARSER_FEATURES_DEMOS.md) | the notation the parser accepts, feature by feature |
+
 ## Other Examples
 
 Add your own example models here! SysML v2 files use `.sysml` extension, KerML files use `.kerml`.
diff --git a/examples/SOLVER-DEMO.md b/examples/SOLVER-DEMO.md
@@ -0,0 +1,170 @@
+# Solver demo
+
+[`solver-demo.sysml`](solver-demo.sysml) is a rover's power, mass and configuration
+budget, written so that each of the experimental solver commands has something to
+answer. Constraint solving asks whether conditions *can* hold, which is not what
+`%constraint`/`%satisfy` answer — those evaluate what does hold of an object.
+
+Every command below needs an external solver: `z3` or `cvc5` on `PATH`, or
+`OPENSYSML_SMT` pointing at one — see
+[installing a solver](../docs/guide/01-install.md#installing-a-solver-optional).
+`%optimize` needs z3 specifically, since optimization is a z3 extension cvc5 does
+not implement.
+
+Load the model and run the commands at the prompt:
+
+```bash
+./bin/sysml examples/solver-demo.sysml
+```
+
+## `%check` — can it hold?
+
+```
+%check SolverDemo::Rover::powerFitsBudget
+```
+
+```
+✓ Constraint powerFitsBudget is satisfiable (z3, 7ms)
+  SolverDemo::Rover::drivePower = 220
+  SolverDemo::Rover::sciencePower = 0
+```
+
+A requirement states several conditions at once, so one query is about all of
+them, and a satisfaction assertion asks the same of the requirement asserted of
+an object:
+
+```
+%check SolverDemo::PowerBudgetRequirement
+%check SolverDemo::rover1::powerIsBudgeted
+```
+
+`sat`, `unsat` and `unknown` are kept distinct: an `unknown` is reported as
+undecided, never as either verdict.
+
+## `%explain` — which conditions conflict?
+
+`OverbookedBudget` requires a drive power and a science power that together
+exceed its own budget, so it cannot hold:
+
+```
+%check SolverDemo::OverbookedBudget
+%explain SolverDemo::OverbookedBudget
+```
+
+```
+✗ Requirement OverbookedBudget is unsatisfiable: 3 conditions conflict (z3, 26ms)
+  Every condition below is needed: dropping any one leaves the rest satisfiable.
+  1. required condition: `rover.drivePower + rover.sciencePower <= 200` — requirement OverbookedBudget, at …:65:13
+  2. required condition: `rover.drivePower >= 150` — requirement OverbookedBudget, at …:69:13
+  3. required condition: `rover.sciencePower >= 90` — requirement OverbookedBudget, at …:73:13
+```
+
+The core is minimal: every condition listed is needed for the conflict.
+
+## `%solve` — what values would satisfy it?
+
+```
+%solve SolverDemo::PowerBudgetRequirement
+```
+
+```
+✓ Requirement PowerBudgetRequirement has values satisfying it (z3, 7ms)
+  Synthesised:
+    SolverDemo::PowerBudgetRequirement::'rover.drivePower' = 60
+    SolverDemo::PowerBudgetRequirement::'rover.sciencePower' = 40
+  One witness: a solver may answer with any of the assignments that satisfy it.
+```
+
+The assignment is one witness of possibly many; another solver, or another
+version of the same one, may answer with different values.
+
+## `%configure` — which variants are permitted?
+
+`roverFamily` has two variation points whose choices interact: a steerable
+antenna requires the rugged chassis, which rules out one of the four
+combinations.
+
+```
+%configure SolverDemo::roverFamily::steerableNeedsRugged all
+```
+
+```
+✓ Constraint steerableNeedsRugged permits 3 selections of variants, which are all of them (z3, 11ms)
+  1.
+    SolverDemo::roverFamily::antenna = SolverDemo::roverFamily::antenna::fixed
+    SolverDemo::roverFamily::chassis = SolverDemo::roverFamily::chassis::light
+  2.
+    …
+```
+
+A selection can be chosen instead of synthesised, and the rest is filled in
+around it:
+
+```
+%configure SolverDemo::roverFamily::steerableNeedsRugged antenna=steerable
+```
+
+```
+✓ the chosen variants are consistent with Constraint steerableNeedsRugged (z3, 9ms)
+  Already fixed:
+    SolverDemo::roverFamily::antenna = SolverDemo::roverFamily::antenna::steerable  (chosen)
+  Synthesised:
+    SolverDemo::roverFamily::chassis = SolverDemo::roverFamily::chassis::rugged
+```
+
+Enumeration is bounded by `OPENSYSML_SMT_MAX_CONFIGURATIONS` (`all <count>` for a
+smaller bound), and the report says whether the selections are all of them or
+were cut short.
+
+## `%optimize` — what is best? (z3 only)
+
+Each `objective` of an `analysis def` is improved the way the trade-study
+definition typing it says, within the conditions the case requires:
+
+```
+%optimize SolverDemo::PowerBudget
+```
+
+```
+✓ Analysis PowerBudget is optimized (z3, 8ms)
+  maximize mostScience = `sciencePower`: 160
+  SolverDemo::PowerBudget::drivePower = 60
+  SolverDemo::PowerBudget::sciencePower = 160
+```
+
+`MassBudget` has a quantity-valued objective, reported with its unit, and
+`MassThenScience` has two objectives, improved lexicographically in declaration
+order — the least mass first, and among the platforms achieving it the most
+science power:
+
+```
+%optimize SolverDemo::MassBudget
+%optimize SolverDemo::MassThenScience
+```
+
+Under cvc5 the same `%optimize` is an error rather than a plain satisfiability
+check presented as an optimum:
+
+```
+OPENSYSML_SMT=$(command -v cvc5) ./bin/sysml examples/solver-demo.sysml
+```
+
+```
+error: the SMT solver does not implement optimization: cvc5 lacks `(maximize …)`/`(minimize …)`
+with `(get-objectives)`, a solver extension: … install z3 or set OPENSYSML_SMT to it
+```
+
+## What the model states, and why
+
+| Element | The query it answers |
+| --- | --- |
+| `Rover` | asserted constraints, each a `%check`/`%solve` target of its own |
+| `PowerBudgetRequirement` | several conditions in one query |
+| `OverbookedBudget` | conditions that conflict, for `%explain` |
+| `rover1` | a satisfaction assertion, asserted of an object |
+| `roverFamily` | interacting variation points, for `%configure` |
+| `PowerBudget`, `MassBudget`, `MassThenScience` | one objective, a quantity-valued one, and two improved in order |
+
+Every command is documented in
+[the REPL command reference](../docs/reference/repl-commands.md), which is
+normative where this walkthrough and it differ.