Sysprose user guide

For an engineer who has been handed the tool and has an afternoon.

It assumes you know systems engineering — blocks, interfaces, requirements, states — and it does not assume you know SysML v2. Everything you have to type is introduced here, in the order you need it.

Sysprose runs entirely in a browser tab. There is no server and no project on anyone's disk but yours — and no login, unless you choose to keep your model in your own Google Drive on a site that offers it (§8.1). That shapes everything below, especially what is kept and what is not.

Contents

1. What this is, and what it is not
2. The first ten minutes
3. The notation you actually type
4. The views, and what each one answers
5. Authoring, and the one dangerous button
6. Checking and analysing
7. Three kinds of statement
8. What is kept, and what is not
   • 8.1 Google Drive (optional)
9. Limits
10. Where to go next

• Appendix A — every control, and the id a test can find it by
• Appendix B — keyboard shortcuts

1. What this is, and what it is not

Sysprose is a modeling tool for one model at a time, held in your browser. You author a system as text or by drawing, and it gives you back 17 views of the same model — block diagrams, an interconnection diagram, action and state diagrams, requirement tables, a contract inventory, a traceability matrix, a dependency-structure matrix, a 3D massing view — plus a rule-based check, a numeric solver, an execution engine, a verification lane you drive from a terminal and a scriptable API.

What it is not:

• Not a repository. There is no shared server, no check-in/check-out, no branching that survives closing the tab. The Versions tab is real version control over your working model, and it lives in memory only.
• Not a CAD or a physics tool. The geometry view draws boxes, spheres and cylinders from attributes you wrote. The solver solves the algebra you wrote.
• Not certified. Sysprose implements a SysML v2–style textual notation and an OMG-API-shaped element graph; it is a candidate implementation and nothing here is a claim about conformance to a standard.
• Not multi-file. One model, one text buffer. import resolves against the bundled standard library and within the file, not across files on disk.

What it is unusually good at, and why you might keep it: the model is text, so it diffs and reviews like code; everything is a pure function, so the same answer comes out of the browser, the terminal and a script; and the feedback is machine-readable, so an agent can write a model, read the findings and repair them.

Source of truth: src/diagram/types.ts:17-34 (the view list), README.md ("Name and standards status"), src/api/versioning.ts:172-187 (the Versions tab's repository, an in-memory one).

2. The first ten minutes

Open the app. The first thing you see is a "Loading standard library…" screen. That is the standard library — an 8.2 MB download of 38761 elements in 98 packages — being merged into the model before anything is interactive. It is once per page load; see Limits.

When it clears you get a small VehicleModel sample and a three-zone shell:

┌───────────────────────── Toolbar (row 1 commands · row 2 views) ─────────────────────────┐
├──────────────┬──────────────────────────────────────────────────────┬────────────────────┤
│  Explorer    │  Palette │ Breadcrumb + canvas / table / graph        │  Properties        │
│  (the tree)  │          │ (the active view)                          │  (the selection)   │
├──────────────┴──────────────────────────────────────────────────────┴────────────────────┤
│  Problems · Text · API Console · Simulation · Versions                                   │
└──────────────────────────────────────────────────────────────────────────────────────────┘

Load the example. Toolbar → Import, and pick examples/uav-isr.sysml. Import replaces the whole model (one undo restores what was there). You now have a small ISR unmanned air system: an air vehicle whose subsystems are wired through power, data and RF ports, plus a mission action flow, a flight-mode state machine and the requirements they have to meet.

On a site that offers Google Drive, a Drive ▾ button sits beside Collaborate: Drive ▾ → Sign in to Google…, then Save to Drive as…, keeps this model as a .sysml file in your own Drive, where any device you sign in on can open it again. How that works, and what it does and does not send, is §8.1.

Six things to do with it, in order.

1. Find the air vehicle. In the Explorer, expand UAVSurveillanceSystem and click AirVehicle. Properties (right) fills in: metaclass, documentation, its attributes, and a Used by list of everything that references it.
2. See it wired. Switch to the Interconnection view (view bar, or press 2). Right-click the AirVehicle box → Scope diagram to this. The diagram now shows that assembly's parts and the connections between their ports instead of the whole model. Scope follows containment, so scope to the definition that owns the parts: the uav box beside it is a usage typed by AirVehicle (part uav : AirVehicle;) and owns nothing, so scoping to it draws one box and no edges. While a scope is set, the chip Diagrams: AirVehicle at the start of the breadcrumb says so; its × (or right-click any node → Show whole model) shows the whole model again.
3. Read the requirements. Switch to the Requirements view. One row per requirement: an outline number, its text, and a Satisfied By chip pointing at uav. The ID column reads (id) on both rows, and that is correct — an id comes from a declared short name (requirement def <R-UAV-001> EnduranceRequirement), and this example writes attribute id = "R-UAV-001"; instead, which is an ordinary attribute and does not fill the column. This table is editable: click a cell and type.
4. Check it. Toolbar → Validate. The Problems tab fills with the validation findings — for this file, none. Then → Check, which adds a row per constraint saying whether it holds. Both requirements are satisfied: the derived endurance beats 45 min and the mass is under 25 kg.
5. Solve it. Toolbar → Solve. The Problems tab is replaced by solved values and a feasibility verdict. Note replaced — see the Problems panel below.
6. Break something on purpose. Open the Text tab, change 45.0 [min] to 100.0 [min], and press Apply text → model. Check again: the endurance constraint now reads violated. Check says which constraints hold, never by how much; press Solve for that, and Problems gains a violated inequality: uav.endurance >= 100.0 [min] (by … [s]) row with the shortfall in seconds. Undo (Ctrl+Z) puts the model back.

The same file, from a terminal, without opening a browser at all:

$ npm run sysprose -- stats examples/uav-isr.sysml
examples/uav-isr.sysml: 113 element(s) — 82 node(s), 31 relationship(s), 1 root(s), max depth 4
  library elements   38761
  (the library is bound alongside the model and left out of every figure above)
  by metaclass
    FeatureTyping           25
    AttributeUsage          16
    PortUsage               15
    ...

Source of truth: src/ui/App.tsx:163-286, src/ui/panels/Toolbar.tsx:524-660, src/core/factory.ts:194 (the boot sample), scripts/sysprose.ts.

3. The notation you actually type

The Text tab is the whole model as text, and it is the fastest way in. A short list of constructs covers almost everything.

A container. Everything lives in a package.

package UAVSurveillanceSystem {
    // ...
}

A block, and a use of one. part def declares a kind of thing; part declares one, typed by a definition. Definitions are the reusable half; usages are the ones that end up in your architecture.

part def BatteryPack {
    attribute capacity : ISQ::EnergyValue = 640.0 [Wh];
}

part uav : AirVehicle;          // a usage, typed by the definition

Attributes, with units. A value can carry a unit in brackets. Units are converted, not compared: 45.0 [min] and a value in seconds are the same dimension and the comparison is done properly. A plain Real is fine when the quantity is a ratio.

attribute mass : ISQ::MassValue = 3.4 [kg];
attribute usableEnergyFraction : Real = 0.8;
attribute endurance : ISQ::DurationValue = battery.capacity * usableEnergyFraction / cruisePower;

That last line is a derived attribute: an expression over other attributes, recomputed by the solver rather than stored.

Ports and connections. A port is a typed interaction point with a direction; a connection wires two of them.

port def PowerPort { attribute voltage : ISQ::ElectricPotentialValue; }

part def BatteryPack { out port powerOut : PowerPort; }
part def FlightController { in port powerIn : PowerPort; }

connection powerToComputer connect battery.powerOut to flightComputer.powerIn;

Behaviour: actions. first … then … chains successions; a bare then X; continues the chain from the previous step. then X; references a step, it does not declare one — every name in the chain needs its own action X; line.

action def FlyMission {
    action takeoff;
    action transitToArea;
    action surveilTarget;
    first takeoff then transitToArea;
    then surveilTarget;
}

Behaviour: states.

state def FlightModes {
    state standby;
    state manual;
    transition standby -> manual;
}

Requirements. A requirement names its subject and, optionally, a constraint that decides it. satisfy … by … is the trace link from the requirement to the thing that meets it.

requirement def EnduranceRequirement {
    attribute id = "R-UAV-001";
    doc /* The air vehicle shall sustain at least 45 minutes of flight. */
    subject uav : AirVehicle;
    require constraint { uav.endurance >= 45.0 [min] }
}

satisfy EnduranceRequirement by uav;

Documentation. doc /* … */ is part of the model and survives a round-trip. // line notes do not — they are stripped, like whitespace. A statement can also say what it is for — a rule, an explanation, or guidance for an agent — with one keyword in front of its declaration: §7.

Everything else you will meet: import, alias … for …, dependency A to B, allocate, verify, refine, trace, derive, @Metadata, and constraint/calc bodies. If you write something the parser does not accept, you get an exact line, column and hint — that is what the checker is for.

Source of truth: src/text/langium/sysml.langium, examples/uav-isr.sysml, examples/vehicle.sysml.

4. The views, and what each one answers

Row 2 of the toolbar groups the views the way this section does. All of them show the same model; none of them is a separate document you have to keep in sync. Switching views never changes the model.

examples/views-tour.sysml populates every view in this section, one labelled block per view, so you can open it and switch through the toolbar to see what each one draws and what text produced it. Measured on that file: general 30 nodes / 26 edges, tree 47, interconnection 8, requirement 8 / 3, case 5 / 3, parametric 5, action 2 / 1, state 2 / 2, sequence 2 lifelines and 1 message, grid 47 rows, requirements 2 rows.

The two questions that file answers which nothing else here does: a sequence view is derived from flow from a to b (falling back to succession control edges), and an allocation view needs allocate x to y — a satisfy will not populate it.

A graph view can be narrowed to one subtree — right-click a node → Scope diagram to this, or ⊞ on its row in the Explorer (the way to scope to a package, which most views draw no box for). That is what makes an interconnection diagram of one assembly readable, and a layered model readable one layer at a time. While a scope is set, a chip at the start of the breadcrumb says so — Diagrams: SA — and its × shows the whole model again. A different view or scope opens fitted to the canvas.

The bottom panel (Problems, Checks, Text, …) folds down to its tabs with the ▾ at the end of its tab strip, giving the diagram the room; clicking any tab opens it again.

Diagrams

The drawn views. Auto-layout and Export → Diagram SVG / PNG work on the graph views — General, Interconnection, Action, State, Requirement, Tree, Parametric and Case — and are greyed out everywhere else, with the reason in the tooltip. Sequence and Geometry are drawn by their own renderers and lay themselves out: Sequence has no drawing palette, Geometry does.

Every view has a palette, though: the views that draw nothing still carry the Edit and Checks sections, which is where the allocation matrix gets trace, the contracts table gets refine and fault-tree, and the analysis views get stats and where-used. A check marked not here is one this page cannot run — z3 needs a cross-origin-isolated page — and its row carries the command that runs it in a terminal instead of a verdict nobody measured.

How the diagrams are laid out

Every graph view reads left to right: owner before part, first step before last, the initial state before the ones it leads to, the root of a tree before its leaves (a box that many dependency lines end on may lead its piece instead, below). The layout keeps to the readability criteria of the UML-layout literature (Sun & Wong, IWPC 2005, after Purchase): no box overlaps another, no connector runs through a box it does not connect, connectors run horizontally and vertically and cross as little as the graph allows, and labels sit where the layout made room for them — never on a box, a line or another label.

• Many pieces become rows, not a strip. A view's disconnected pieces are laid out one by one and packed row by row to about the screen's proportions: the largest piece top-left, then single boxes grouped by kind.
• A layered model reads layer by layer. When the boxes of a General view all lie in two or more packages that sit directly in one package — the model's single top-level package, or the package the view is scoped to (Kinds, Common, OA, SA, LA, PA, EPBS, say) — those packages become columns in that order, and the boxes of each connected piece that reaches across them get a header over each column naming its package. The header is a band the layout keeps above the boxes, so as laid out it lies over none (a box moved by hand can cover it). Its label is sized for the zoom, so it still reads when the whole model is fitted — and Fit frames the headers with the boxes, below the canvas's toolbar — and a package name wider than its column is shrunk to fit, then ends in an ellipsis. The headers are drawn into the SVG and PNG exports. A piece inside one package has no header, and neither does a view of a single layer package. A file with several top-level packages, or one wrapper package around the layers, has no columns in its whole-model view: scope the view to the package that holds the layers.
• A box that many dependency lines end on leads its piece. In a General view with no layer columns (a view scoped to one package, or the whole model of a file with several top-level packages), a box that three or more «allocate», «satisfy», «trace» or other dependency lines end on — a part that a dozen activities are allocated to, a requirement many things satisfy — is drawn at the left, and those lines fan out of it to the boxes they come from, their arrowheads pointing back at it, instead of each running the width of the diagram to a box at the far right. The layout draws the piece both ways and keeps this one only if it has at least three crossings fewer and reads better overall, so a view that already reads well keeps every line running left to right, as does a whole-model view with its layer columns. Adding or removing a few lines can tip a piece from one drawing to the other, and its hub then moves from one side to the other. Pieces of more than 200 boxes are not tried both ways.
• A label that would say the same thing on every line is left off. When every dependency in a view is of one kind — the Requirement view's «satisfy», for instance — the keyword is dropped and lines that leave one box share a trunk; a view that mixes kinds keeps its keywords.
• Large models: scope the view to a package (the diagram shows one layer at a time) — a whole model's General view is an overview, not a page. Layout runs in a background worker, so a large diagram never freezes the page.

Arranging by hand. Drag a box and it stays where you drop it, through model edits and view switches; its connectors step around to meet it. Text edits keep it too. An apply of text (Apply text → model, or the apply that Save, Ctrl/⌘ + S and Export ▾ → SysML make of typed text) builds every element anew from the text, and each moved box goes to the element with the same qualified name (Package::Part). A box lays out afresh when you renamed its element, moved it to another owner, or gave another element the same name. Auto-layout (toolbar, or the canvas mini-toolbar) forgets the boxes you moved in the current diagram and lays it out afresh. Moves are kept per view and scope. Save keeps them with the project in this browser, beside the model, and Open ▾ puts each box back where you left it. New, Import and Reload from Drive start from a fresh layout, and their Undo brings the boxes back with the model. A file opened from Google Drive (Browse Drive…, Recent, a ?drive= link) or from a ?model= link starts from a fresh layout too, but Undo starts over there (§8.1): an arrangement never saved with Save is gone for good, so press Save first. The boxes are not part of the model's text: the Text view, the SysML and JSON exports and a Google Drive file never hold them. Moving a box is not an edit: it spends no Undo step, and the model does not read unsaved for it, so the question that guards a command which replaces the model (§8) is not asked for boxes. Press Save to keep an arrangement.

Tables

Read-only, except the Requirements table, which is the one editable grid in the app.

The Contracts view is read-only and reaches no verdict: it shows what a requirement states, never whether it holds. There is no solver in the browser (SharedArrayBuffer needs COOP/COEP headers GitHub Pages cannot set), so under the table it prints the exact command that does decide. A clause a unit or typing gate refused is shown with its reason rather than dropped, because a view that showed the clauses and hid the refusals would let you believe a requirement was fully encoded when half its body had been turned away.

The Requirements view edits the model directly: adding a chip creates the backing relationship, and ✕ deletes it. + on a chip cell opens a search box: typing narrows the list of candidates and links nothing; a click (or Enter on the highlighted one) makes the link, and Escape closes it. A cell with a closed list of values is a drop-down offering exactly what a write will accept; the rest are click-to-edit text. Kind says what a row is for — a prose or prompt row stays in the grid, labelled, and is left out of the coverage figure rather than counted as a gap nothing can close.

Analyze

Workbenches for models too big to read. They are the least self-explanatory views in the app, so each gets a sentence of theory.

• A cluster / community is a set of elements more connected to each other than to the rest. PageRank sizes a node by how much of the graph flows through it. Both are heuristics for where to look, not verdicts.
• A DSM (dependency-structure matrix) is the model's adjacency matrix with rows and columns in the same order: a block on the diagonal is a subsystem, a mark far above it is a long-range dependency.
• A delegation port is the port Regroup synthesizes on a new composite when a connection you kept crosses the boundary you just drew.

Regroup's preview never touches the model. Apply does, in one undoable step.

Source of truth: src/diagram/build.ts:9-22, src/diagram/matrix.ts, grid.ts, sequence.ts, geometry3d.ts, graph-analysis.ts, planning.ts, regroup.ts, requirements-table.ts, contracts-table.ts; src/ui/panels/Toolbar.tsx:54-80 (the grouping); src/ui/store.ts:320-333 (diagramRootId, the diagram scope), 1512-1620 (carryPins, pinsOf: boxes moved by hand, and how a saved project keeps them), 2340-2357 (pinNodePositions: the move itself), 3393-3445 (applyText: an apply of text carries them over by qualified name), 4074-4115 (openText: a file opened as text starts afresh).

5. Authoring, and the one dangerous button

The loop

There is one loop, and everything else is a detail of it:

Edit anywhere → the model changes → the derived surfaces catch up → the Text tab can push a change back the other way.

You can edit in four places, and they are equal: the Explorer tree (add child, rename, drag to reparent, delete), the canvas (draw with the palette, drag, right-click), the Properties panel (every field of the selection), and the Requirements table.

Drawing on the canvas. Pick a tool in the palette and a strip at the top of the canvas says what the next click does: for a box, click empty canvas to place it under the selection, or a box to place it inside; for a line, click the source box, then the target — once the source is picked it is outlined and the strip asks for the target. Esc puts the tool down at any point. The General view's palette draws every dependency the views show — Specialize, Typed by, Satisfy, Allocate, Trace — so a line whose other end has left a view (a satisfier whose requirement was deleted, say) can still be drawn where both ends are. A typing, specialization or subsetting line belongs to the box it starts from; any other line to the source's owner.

Typing a part in Properties. The Type field shows what the selection is typed by. Type the name of a definition and press Enter (or leave the field): the name is looked up the way the text would look it up, and the typing is bound, replacing the old one — the diagram draws the new : Type and any typing line at once. A name that resolves to nothing is kept as text, as the notation would keep it, and an empty field removes the typing. One undo takes it back.

Wiring ports. In the Interconnection view a part shows its ports on its edges — the ones it declares, and the ones it has through its type (part memberA : SwarmMember shows SwarmMember's ports). Pick Connection or Interface in the palette and click a port handle on one part, then one on the other: the line ends on the PORTS, written as feature chains — interface connect memberA.meshOut to memberB.meshIn; — exactly what the text form parses to. Name it and give it its interface definition in Properties (Name, Type). Clicking two boxes instead of two ports still connects the parts.

Tags and a requirement's subject. Tags in Properties holds the #Tag keywords written on the element (#Hazard #Accepted); Enter writes them, and the Keywords list under it says what each one resolves to. A statement kind (#prose, #prompt) stays with the Kind control. On a requirement, Subject takes name : Type (holder : SwarmMember) and writes subject holder : SwarmMember;; an empty field removes it, and a type that names nothing is not written.

The standard library in the Explorer. With the Explorer's library toggle on, the library's packages are rows like any other, but the text never holds them — not the Text view, not Export ▾ → SysML, not a Google Drive file. So an element added under a library element (its +, or a palette tool with one selected), dragged onto one, or pasted onto one (Ctrl/⌘ + V), goes to the top level of your model instead, and the strip under the toolbar says so. One Undo takes it back, as any edit, and the note with it. Replacing the model — New, Open, Import, a file opened from Drive — takes the note down too: it names an element of the model that is gone. For the same reason the Documentation box in Properties is read-only on a library element: it shows the library's own documentation, and a doc typed there would be in no file.

The tree and Properties update instantly. The diagram, the Problems list and the Text tab are derived, and they lag a burst of edits by up to 250 ms. That is deliberate: it keeps typing responsive. On a large model, where working them out takes a while itself, the lag grows with it — up to four times the last recompute — so the keyboard is never kept waiting.

The Text tab, in both directions

• Model → text happens by itself. The buffer is re-serialised after every edit, and the indicator under the editor reads in sync with model. An edit made through the SDK on window.sysml (§6) is re-serialised too — except over text typed here and not yet applied: an SDK edit, like a collaborator's, never replaces that. The text stays, reading modified — not yet applied; applying it — or saving it, or exporting it with Export ▾ → SysML, outside a collaboration room — puts it over the SDK's edit, which one Undo brings back.
• Text → model happens when you press Apply text → model — or Save / Ctrl/⌘ + S or Export ▾ → SysML, which apply it first unless it has a syntax error or a collaboration room is connected (§8). Until then the indicator reads modified — not yet applied — unless you type the text back as it was (delete what you typed) before the model changes: nothing typed stands then, and it reads in sync with model again.
• Parse findings sit in a strip under the editor. Errors are shown in full; warnings alone fold to one line — ▸ 12 parse warnings — also listed under Problems — which a click opens, so a model with a few warnings still leaves the text most of the panel.

⚠ Apply text → model replaces the entire model

It parses the whole buffer and resets the model to the result. Three consequences you have to know before you press it:

1. A syntax error does not cancel the apply. Error recovery produces a partial reading, and that partial reading becomes your model. The parse errors appear in Problems and in the strip under the editor.
2. One undo restores exactly what you had — one snapshot is pushed first, and that is the whole safety net. A second edit and it is gone.
3. Editing the model discards unapplied text edits. A local model edit force-overwrites the buffer. If you typed into the Text tab and then clicked something in the tree, your typing is gone. (An edit made through window.sysml does not overwrite it; see above.)

After an apply, the standard library is re-merged asynchronously, which is why Problems and the text buffer visibly refresh a second time a few hundred milliseconds later. When a parse error is standing, that refresh deliberately leaves your text alone rather than serialising the partial model over it — as it leaves alone text you typed after the apply, while the library merged.

Undo

Undo is 50 snapshots deep, it covers model changes (not view changes, not the theme), and any new edit clears the redo stack. One view change rides along: undoing New, Open, Import or an apply of text also puts back the boxes moved by hand on the model it restores (Arranging by hand, §4). Copy is not undoable; paste is.

Source of truth: src/ui/store.ts:1682-1777 (RECOMPUTE_DEBOUNCE_MS, flushRecompute: the recompute cycle), 1900-1983 (recomputeNow), 1985-2065 (afterSdkEdit: an SDK edit), 868-915 (inLibrary, userOwner, sdkIntoLibrary: nothing added to the standard library), 2656-2676 (createElement: a new element), 2934-3001 (reparent, reparentMany: a move), 4724-4769 (libraryNote: the note that says so), 3393-3445 (applyText), 3877-3923 (undo, redo), 4811-4869 (refreshAfterLibraryLoad: the post-apply refresh); src/ui/panels/TextEditor.tsx, src/ui/panels/Properties.tsx (the Documentation box); test/e2e/text-apply-contract.spec.ts:30 (the one-undo guarantee, as a test).

6. Checking and analysing

Four buttons that answer four different questions

Two names worth separating:

• The Simulate button and the Simulation tab are different things. The button is a one-shot batch run that dumps a trace into Problems. The tab is an interactive stepper: pick a machine, Start, then Play / Step / Inject an event / scrub the trace, with the active states glowing on the state diagram.
• feasible means "no known violation." A relation neither engine could judge is reported under unknowns and leaves the flag true. Read the two together; an unjudged constraint is not a satisfied one.
• A design freedom is reported as one, never as a value. When the equations leave a feature free — mass == dry + fuel and fuel == mass * 0.2 with no value for dry — Solve lists it as a free: row instead of a value: row, and every relation over it is unjudged: the point the solver happened to stop at is one choice among many, so mass >= 130.0 is neither met nor missed there. A feature that reads a free one is free with it, however slight the dependence (a range in kilometres moved by an offset in millimetres). An equation the solve itself imposed holds along the freedom and stays satisfied; a plain (not assert) constraint the solve took as a design equation to fix such a value is marked imposed by the solve, because it holds by construction, not as a check the design passes. A value the model's own facts fix — a bind to a determined value, an assert over an instance (assert constraint { p.x == 3.0 }) — is no freedom, and a plain constraint over it is judged, never imposed — and so is a feature whose stated value expression those facts determine (y = x * 2.0 over an asserted x): y == 7.0 beside it is violated, never the value y is solved to. The test is local: of two separate roots (x * x == 4.0) the one the solver found is still the one judged. A constraint of a definition read in a usage is judged at the values the model states; with any of them fixed by an API caller, solveFeasible leaves it unjudged (decided: false), and so does the numeric check (unknown). Every other relation is read at the fixed point, every feature the point moves at the value it has there — y != 18.0 over y = x * 2.0 holds with x fixed to 1. A value the caller fixes is the decimal it is, read exactly as a value the model states, and so are the literals the point keeps: x <= 0.99999999999 is violated with x fixed to 1, never held within the solve's tolerance, which reads only the values the solve produced (y, there). A name the point gives no value — a Boolean ok = x > 5.0 over the fixed x — would read the model's own, so a relation over it is unjudged at that point, and solveFeasible leaves it unjudged too.
• A point the solver stopped at without converging is no solution. When the solve ends off one of the equations it solved — a Newton step that diverged, an instance's value it could not read — the values it produced there are neither listed as values nor as freedoms, and every relation over them is unjudged with the reason the solve did not converge: never violated at a point the model does not sit at. solveFeasible does not hold them there either: it searches them as freedoms, and a violation over them is unresolved, never decided. A model with a binding past a cap (below) reads so too: the values that binding holds are not read, the solve counts them undetermined and reports did not converge, and the rows over them name the cap.

A target on a measure with no value of its own is read where the values are. A brief often states its targets once, on abstract measures that carry no value (package Common { attribute m : Real; require constraint t { m >= 0.9 } }), and each layer gives its own estimate as a feature that subsets or redefines the measure (LA::m :> Common::m = 0.78, PA::m :> Common::m fixed by an asserted equation). t itself stays could not be evaluated, because the layers may disagree and no one value belongs to Common — but its message now says why (m has no value here; evaluated per specialisation: LA::m, PA::m, or … nothing specialises it), and the target is judged once per layer through that layer's estimate, by the same unit rules as any other check. Check lists each reading as its own row under the target, and Validate and npm run check report it as validation/target-by-specialisation at the estimate: a warning when it misses (LA::m = 0.78 misses Common::t (m >= 0.9)), info when it meets the target or cannot be read — two estimates of one measure in the same layer, or a layer that specialises only some of the measures a target names, are named rather than guessed between. A miss is its own code, not a constraint-violation, because an estimate that misses is a result to record, not a contradiction in the model.

The Problems panel is one list

Validate, Check, Simulate, Solve, parse diagnostics and the FMI-import error all write into the same list, and each one replaces the last. They do not accumulate. Click Solve after Validate and the validation findings are gone until you click Validate again. Every row with an element selects it when clicked.

The same answers from a terminal

Every question you can put to the app you can also put to a terminal. On the unmarked rows below the subcommand runs the same function the control runs, so those two figures cannot disagree. A † marks a row where the app answers the same question by drawing its own projection instead — there the two figures may legitimately differ, and the difference is spelled out under the table.

† Validate re-runs the rule engine over the model already in the editor; check parses the file first and then applies those same rules. The Allocation view tabulates only the elements that take part in a link, where trace tabulates every element of the row and column kinds and so also shows what links to nothing. The Interconnection view draws the ports and connections; it computes no connectivity report — connectivity exists only in the terminal and the SDK, as do orphans, prompts, obligations, property-draft, property-check, evidence-attach, evidence-detach and the depth walk behind where-used. The Contracts view projects the rows and the census contractReport returns, where contracts also prints the keyword inventory, the exclusion counts and every refusal reason, and can be scoped to one element with --element. The Requirements view's Evidence column reads what a run left in the file — current, stale or unrecorded, with the record's claim word beside it — where evidence-status prints every row with its digest, its slice and its verification/* code; nothing in the app writes a verdict. Properties → Used by lists everything referencing the selection, library and re-derived copies included, where where-used drops the library, walks to the --depth you ask for and tells you what it left out.

Three real answers on the shipped example:

$ npm run sysprose -- requirements examples/uav-isr.sysml
examples/uav-isr.sysml: 2 of 2 requirement(s) satisfied (100%)
  [x] 1  EnduranceRequirement — satisfied by uav
  [x] 2  MassRequirement — satisfied by uav
  24 bundled library requirement(s) and 0 re-derived copy/copies are not counted

$ npm run sysprose -- connectivity examples/uav-isr.sysml
examples/uav-isr.sysml: 15 port(s), 9 connection(s), 14 connected, 1 unconnected
  ...
  unconnected ports
    UAVSurveillanceSystem::DataLink::antenna
  ...

$ npm run sysprose -- orphans examples/uav-isr.sysml
examples/uav-isr.sysml: 2 of 14 definition(s) unused
  UAVSurveillanceSystem::FlyMission [ActionDefinition]
  UAVSurveillanceSystem::FlightModes [StateDefinition]
  1 package(s) skipped as namespaces; 1434 library and 0 re-derived definition(s) excluded
  an unused definition is valid — this is an inventory, not a diagnostic

Two things those transcripts are telling you, and both are on purpose. Every report excludes the bundled library and the tool's own re-derived elements, so the numbers are about your file, and says how many it left out — stats counts the library, elements the re-derived copies, the rest both. And orphans is an inventory, not a verdict: the two "unused" definitions are the mission behaviour and the flight modes, which nothing in the model references yet — that is a fact about the model, not a defect in it.

Two of the subcommands are about what a statement is for rather than what it constrains. requirements --kind prose (or prompt, or requirement) narrows the listing to statements of one kind without moving the coverage ratio, which counts requirements alone; by default every statement is listed and the ones the ratio leaves out say so on their own line. prompts --element X answers the question an agent has instead: what guidance applies here — the prompts written on that element, on what it is, on where it sits, and on where what it is sits, nearest first, each with the words it carries. Both are worth a section of their own: §7.

Add --json to any sysprose subcommand for {ok, file, <report>} on stdout. npm run check -- model.sysml --json is the other shape — {ok, files: [...]}, plural, because check takes several files at once — and it is the other exit-code contract too. For a subcommand, 0 means clean, 1 the model did not load cleanly (you still get a report, of what parsed, with a degraded banner on stderr) and 2 you asked for something impossible; check judges, so its 1 means the file has findings — a file that parsed perfectly and broke one validation rule exits 1. Full flag list: CLI-REFERENCE.md.

What a requirement promises, and what would have to be shown

Two subcommands read a requirement the way a proof engineer does, and both of them ship before any solver exists. They report structure. Neither of them ever says a requirement holds.

contracts is the inventory. For each requirement it prints the subject it is about, what it assumes, what it guarantees, which satisfy, verify, derive and refine statements name it, the variables the clauses it wrote read with their units, and the arithmetic fragment each clause lands in — linear (QF_LRA), nonlinear (QF_NRA) or not encodable at all. A case with an objective { assume … require … } is a contract too: that is the standard's own home for a behaviour's precondition and postcondition, and it is why Sysprose ships no #precondition keyword for something the notation already expresses.

$ npm run sysprose -- contracts examples/uav-isr.sysml
examples/uav-isr.sysml: 2 contract(s) on 1 subject(s); 2 guarantee(s) in QF_LRA, 0 in QF_NRA, 0 unsupported
  an inventory of what is written — this command says nothing about whether any of it holds
  UAVSurveillanceSystem::EnduranceRequirement  [RequirementDefinition]
    subject uav : AirVehicle (declared)
    require uav.endurance >= 45.0 [min]  [QF_LRA — linear real arithmetic]
    satisfy uav
    variables uav.endurance (derived)
  ...

obligations is the worklist: what would have to be shown, what may be assumed while showing it, and which facts the model simply states. The three buckets are fixed, and the one worth knowing is the last:

That last row is deliberate. A plain constraint is what the Analyze button judges, so it has to be what a solver judges as well; filing it as an axiom would let one false constraint make the whole axiom set unsatisfiable and turn every real violation in the run into "cannot tell".

A redefinition is the feature in its context, and = binds. In part p : P { attribute :>> m = 20.0 [kg]; } every surface reads p.m as p's own feature — named or not, renamed (heavy redefines m), however deep the chain that reaches it. Whether it may have a value of its own depends on how P wrote m:

• attribute m default = 18.5 [kg]; — overridable: p.m is 20 kg.
• attribute m = 18.5 [kg]; — a binding every P holds, so p states two values for one feature. That is a contradiction: the check reports it as a violation at the redefinition (validation/constraint-violation), no surface reads either value for p.m, and the solver lane finds the axioms inconsistent. Write default where a usage is meant to override.

The two values are compared as values, not as spelled: 1000.0 [g] restates 1.0 [kg], 10.0-k restates 10.0 - k, and 2.0 * 0.5 restates 1.0 — none of them contradicts anything. A pair only an evaluation could compare (:>> m = 50.0 over m = 2.0 * k, where p may change k) is reported unknown at the redefinition, p.m is read by no surface, and the solver lane, which carries both values in SI, decides whether they meet. A feature that hides P's m by its name alone (attribute m = 20.0 [kg]; with no :>>) overrides it all the same, and so does the same check. Two values a context inherits under one name from two general types (part def C :> A, B over A's and B's :>> m) are read by no surface there, nor through a binding one of them is joined to (a part :>> p : P2 whose P2 writes :>> extra = 9.5, under Q's bind p.extra = X, reads neither 9.5 nor X's default); two literal bindings that differ are a contradiction reported at C.

A binding overrides a default as a redefinition does. bind p.m = M in part def Q, over P's attribute m default = 18.5 [kg], makes p's m Q's M in every Q — wherever M has a value of its own: written with =, set in a context (part q : Q { attribute :>> M = 20.0 [kg]; }), or fixed by an asserted equation. Every surface reads q.p.m as 20 kg, and no surface reads the 18.5 kg: the numeric surface and the solver lane at the path q.p.m, the check and the literal engine in q's p, the instance the binding carries q's M into, in a sentence that names the binding the value came through (q.p.m = 20 in …::q::p, its M …::q::M through …::q's bind). The same holds for a default on a feature the binding names directly (bind m = M), for one a context writes on the bound end (part q : Q { part :>> p { attribute :>> m default = 30.0 [kg]; } } against Q's M = 20.0 [kg]), and along a chain of bindings: bind B = A; bind C = B; reads C as A, and R's bind q.M = N over Q's bind p.m = M reads r.q.p.m as r's N. A redefinition that renames the bound usage (part q : Q { part pp :>> p; }) is the slot the binding fills: q's pp's m is q's M. A package's binding on a definition's feature (bind P::m = M beside part def P) holds in every instance of P — part p2 : P, Q's part p : P and each q's — and over a redefinition's own default there (part p3 : P { attribute :>> m default = 30.0 [kg]; } reads M too). Where one instance's m gets a value outside that binding — its own :>> m = 25.0 [kg], another binding (Q's bind p.m = N), or an asserted equation (p2.m == 25.0 [kg]) — that value is M's and every instance's, which the check and the literal engine do not read: no default the binding joins stands, and they name what fixes it (could not be evaluated). One that joins two features of a definition (bind P::m = P::cap) joins them in each instance at that instance's values: the check and the literal engine do not read it, the numeric surface solves it, and the solver lane proves what holds there but abstains on a refutation the check cannot confirm. An instance of P written in another package is not read through the binding by the check and the literal engine (could not be evaluated). Bindings are read in every context they hold in, each end the feature at its path there, and a default gives way where the bindings joined to it reach a value of its own — in that context. Whether it gives way is decided for each instance: a LITERAL default still stands in an instance whose own component states no value and whose every default is a literal agreeing exactly (where q1 : Q sets an M that Q leaves valueless, a q2 : Q that leaves it unset reads P's 18.5 kg; a default that reads a name, or two defaults that differ, stand nowhere). A binding to a feature nothing gives a value (attribute w; bind w = p.m;) carries the default into it instead: w is 18.5 kg. Two defaults bound to each other with no value beside them stand where they state one constant value — numbers, booleans or expressions that read no name, compared exactly (1000.0 [g] and 1.0 [kg] are one) — and give way otherwise, where they differ and where one reads a name, however alike the text (bind a1.v = a2.v over A's v default = 2.0 * K joins two values where a2 sets K). The model states neither, and no surface calls it a contradiction. A definition's constraint over a value read through a binding is read anew in every usage a binding above joins to another value, once per instance, as a constraint over a redefined value is. One read in a usage (P's load <= 10.0 in Q::p) whose value a binding of Q joins to another in a context of Q (q's L) is read for Q's own p — the usage's own instance, named P::c in Q::p (Q's own) on the verify lane — and again for each other instance, q's p included, whose load the binding carries q's L into. So is one where a binding written in or around one instance reaches into it and no binding of Q tells the instances apart (part q2 : Q { attribute E = 20.0; bind p.extra = E; }, or the package's bind q2.p.extra = E: q2's p is read in its own element, at q2's extra of 20). The rows are read apart, each at the value of the instance it names, so an instance that breaks the relation is reported against that instance — at the line that makes it differ: the member of its own stating the value the binding carries in (q's attribute :>> L = 50.0), else the element the instance is read in, else its innermost own usage (part q : Q) or definition (part def Q2 :> Q), never the usage the instances share — and the check rolls two or more of them up into one finding for each usage (past twenty usages of one relation, into one finding for the relation, counting every instance and naming its first five usages, with at most five violated instances after it; and past twenty contexts a binding carries a value into, one finding per verdict and cause). The roll-up counts the instances that hold, those it is violated in (the first five named, then an ellipsis), those it could not be read in — with the cause of each kind, up to three, and the first instance of each (defaults differ: R::q1::p) — and those it did not read, with the cap (not read in 2,001 (more than 16,384 instance readings in this model), counts printed with thousands separators); a group of more instances than the tool reads is one info finding that counts them all unread (where a binding holds in more than 4,096 contexts, not read in at least the instances found, and the instances payload then carries atLeast: true). A violated instance names the value it reads, the value the binding carries in and the binding (load = 50 — q1.L = 50 through R17::Q's `bind p.load = L` ), and a path with a segment holding in or @ is quoted (R::'q in 1'::p; the instance and instances.listed fields keep the names as written). A relation written in the usage itself and read for one instance besides the usage's own (part q1 : Q and no other) has no roll-up, and a violation there is that instance's finding alone — one the check could not read there, an info finding of its own. Solve lists an instance as a row of its own (violated inequality: load <= 10.0 in R::q1::p); past five rows of one relation, the violated ones fold into one row, and so do the unjudged ones that give one reason or abstain for one cause (defaults that differ, no value, a cap) — the first five instances, the count, and the first one's sentence, which names that instance. In a terminal, verify text folds the same way: past five rows of one relation and one claim it prints five and one line counting the rest (… and 3 more rows of R::c: refuted in 8; the rows of one relation and one claim print together), and the footer's findings fold by relation and code, counted against the relation (… and 3 more verification/refuted on R::c), not against the instance of its first row; --json keeps every row. An instance whose own element — the most specific one that denotes it — reads a name of the relation, or a name that name's value reads, through another feature is read in that element, at the instance's own values: a redefinition with a value of its own on its path (part q2 : Q { part :>> p { attribute :>> extra = 20.0; } } reads q2's extra of 20), a specialised type (part :>> p : P2, for Q2's p and for every Q2 that redefines nothing of it), a binding written there, a reference to another part (ref part :>> r = ra). That row is the element's own reading too: q2's part :>> p has no row of its own beside it, and each instance is one row under its name. One that redefines the relation itself is could not be evaluated in that row on every surface, and counted not read in the roll-up (in a group of one, an info finding of its own); so is one where a reference the relation is read through stands for another feature than where its value is written (ref part :>> r = s written in Q's p is Q's s, and q2's p reads q2's own s), or for one a binding reaches into; one whose path inherits a name twice, neither feature redefining the other (part def Q3 :> Q2, Q4 over Q2's part :>> p : P2 and Q4's part :>> p : P4, or part q3 : Q2, Q4: q3's p is P2's and P4's at once, and no one element stands for it); and one whose own element states a default that an asserted equation of its own constrains (part :>> p { assert constraint { extra == 20.0 } } over P's extra default = 0.0). An instance row that reads a value an assert of an instance around it constrains, the package's included, is could not be evaluated too, read in its own element (`part q2 : Q { part :>> p { … } assert constraint { p.load

= 0.5 } }) or through the usage (part q1 : Q { assert constraint { p.x >= 5.0 } }, or the package's assert constraint { q1.p.x >= 5.0 }, for q1's p's x) — unless the assert is an equation that gives a defaultthere a value of its own, which is read as that value (below). So is one that reads such a value through a value derived from it (P'ss = load + xins <= 10.0), in units or not, and so is a check or literal row of a relation outside the instance's rows that reads it there (a package constraint over q1.p.xorq1.p.s); the numeric surface reads x's default past an inequality, which leaves it standing. A relation read through a part a binding joins to another (bind p.r = s, the relation reading r.x) is read per instance nowhere, the usage's own row included: that row is *could not be evaluated*, as it was before any instance was read. A relation written in such a usage (part p : P { constraint c2 { load <= 10.0 } }in Q) is read the same way; anassert there stays an axiom, read for the usage's own instance. A part, port or item a binding equates with another (bind pp = top.a) is read as that other where it says nothing of its own — no feature, value or binding below it, one such binding, no type the other lacks, no reference, subject or satisfythat names it, and a feature of the element the binding is written in or of a package:pp.loadis top's a's load on every surface, and in each instance of that element the instance's own (W'sbind pp = top.aread ass.w.pp, for part s : Sys whose w is a W, is s's w's top's a). Where neither is so plain (part pp : T0 { attribute :>> load default = 3.0; }, a port bound to two inner ports), a row that may read a value the binding carries is *could not be evaluated*, in a sentence that names the binding: one that reads through either end or a usage above one, or through a feature a binding, a value or an assert ties to one, and one read for an instance at or below one. Every other row of the model reads as before. A part, port or item valued with another (part pp : T0 = top.a, part :>> p = other) equates the two the same way, and is never read through: such rows are *could not be evaluated*, in a sentence that names the value. A reference valued so is read as what it names (ref part pp : T0 = top.a: top's a's load), but one written in a definition reads the definition's own top, not each instance's (W's, read in w whose top differs), and an attribute a binding equates with another attribute (bind q = top.pos) reads its own default: known gaps. A value the partner of a binding derives (Q's L = 2.0 * K) is read for the bound feature only where every instance it stands for reads the partner alike — not for q's p, whose K q sets. A relation of Q read in a usage or a specialisation that redefines such an input (Q's c { load <= 5.0 }overbind load = L, read in q2 : Q { attribute :>> K = 25.0; }) is read at that context's own instance, on every surface: q2's load is 50. Where another member the binding joins states a value of its own there (load = 1.0 beside it), q2's load would be 1 and 50, and that reading is *could not be evaluated*. A context that sets the input by an asserted equation instead (q2 : Q { assert constraint { K == 25.0 } }, or a package's assert constraint { q2.K == 25.0 }), or that also redefines the bound feature under a name of its own (attribute ld :>> load), lists no such reading on any surface: known gaps. A binding written in a usage's body to a feature of the definition around it (part q : Q { bind p.load = L; }in R, over R's L) is read in the instance of that definition around each reading, on every surface: r's q reads r's L (50 wherer : Rsets K), and r0's q r0's. No value is read through a binding for any one instance where it holds in more than 4,096 contexts or more than 32 usages deep, nor through a binding joined to such a one, end to end or through a feature an end redefines (a package'sbind Y = top.a.….a.loadbeside thebind a.load = L33 usages down that gives that load its value: Y'sdefaultgives way, and the check reads no value for Y), nor through one whose end has no instance in a context it holds in (R's nested Q used outside any R). A binding joins such a one through a feature an end redefines only where that feature is itself another binding's end: U'sbind a.load = Mon its ownpart a : T0is not joined to T1's capped binding by the T0load both redefine. A value held so, which no binding carries from a stated value, is no design freedom to the numeric surface either: a relation reading it is *could not be evaluated* there too, never solved as a design equation (s.a.load == 9.0for a shallowpart s : T1 beside the capped chain), and the feasibility search does not move it. A model with such a capped binding reports *did not converge* in the Solve header — the check keeps its fail-closed reading, and the rows over a value the binding holds name the cap (*a binding of this model is read deeper than 32 usages*). A context that reads a definition's relation otherwise only because a value the binding carries is its own there (q2 : Q { attribute :>> K = 25.0; }) is listed and read at its own instance, as above. Such a context, and one whose own value a binding of the definition carries into what the relation reads (q : Q { attribute :>> L = 50.0; }over Q'sbind p.load = L, for Q's constraint c { p.m2 >= 0.0 }), is that instance's reading: a validation/constraint-by-instancefinding at the member of the context stating the carried value (q's:>> L), else at the context itself, never a target's validation/target-by-specialisation verdict. A per-instance reading that fails inside the tool makes the row it was read for *could not be evaluated*, in a sentence naming the failure (… the per-instance reading failed (RangeError); reported, not dropped; a group's roll-up counts it *not read*), and every other row and finding stands. A value a binding carries is read in the unit the feature it fills declares — the copy bind p.load = Lmakes of P'sloadincluded — and compared as the quantity it is: q1'sL = 20.0 [kg]is 20 kg against P'scap = 10000.0 [g](violated, on every surface), q2'sL = 5000.0 [g] is 5 kg (load = 5in the row's sentence), and a bare literal beside it is read inload's unit (load <= 10.0holds for q2). A value of another dimension carried into it (a length into a mass) is compared by no surface. Against a value written with=, a binding is a **contradiction**, as a redefinition is: bind p.m = Mwhere P writesm = 18.5 [kg]and q's M is 20 kg is reported violated at the binding (in a context that specialises the binding's owner, at that context) by the check and the numeric surface,solveFeasibledecides the model infeasible, and the solver lane finds the axioms inconsistent. Neither value is read where the binding joins them: a relation readingq.p.morq.M is *could not be evaluated* on the check, the literal engine and the numeric surface; the check and the literal engine say why in a sentence that names the binding and the two features it joins, and the numeric surface reports that the feature has no value in scope. A relation written in P itself is still judged on P's own row at 18.5 kg by the check and the literal engine, even where q's p is the only P. The two are compared as written, as a redefinition's value is against the one it redefines: a pair written the same (1000.0 [g]and1.0 [kg]) is one value, and is read. A pair only an evaluation could compare (a value expression that reads a name) is still read, each value where it is stated, where neither should be: a known gap. The binding is reported violated where the check finds the two differ, and a pair it cannot compare is left to the solver lane. A binding to a feature of the instance around the usage it is written in (R's Linpart q : Q { bind p.load = L; }, against r2's own :>> load = 3.0 in its q's p) files no such row, and the solver lane, which has no axiom of it where that usage is redefined, decides the relation at the value written there: a known gap. Only a binding whose own two ends state the differing values is reported: a binding beside it in the same chain (bind K = Lwith both 30, next tobind L = M with M 50) is not. An instance the binding does not join (part p0 : Poutside any Q) still reads P's 18.5 kg on the check and the literal engine; the numeric surface, which reads P'sm once for every instance, reads it nowhere. For a package's binding on a definition's feature (bind P::m = M, M written with =) against an instance's own :>> m = 25.0 [kg], only that instance's own value goes unread: M, a package's feature and so one instance, and another instance's m, which the binding makes M, are still read on the check and the literal engine, though not on the numeric surface, which reads P's m` once for every instance; and no binding finding reports the pair. Where the two values carry units, as here, the solver lane encodes no binding for that instance, and decides its rows at the instance's own 25 kg: a known gap.

An asserted equation overrides a default too. attribute L default = 2.0; beside assert constraint qa { L == 5.0 } is L = 5 on every surface: the assert's row reads defines L = 5, L <= 3.0 is violated, and no surface reads the 2. The same holds where the equation is written in a type the feature's owner specialises, over a redefinition's own default (Q's assert constraint { L == 5.0 } makes part q : Q { attribute :>> L default = 9.0; } read 5). The equation defines the side whose other side has a value of its own: L == M, M declared without one, still makes M the 2 L's default gives; two defaults set equal (L == K) are both read as no value. An inequality defines nothing (assert constraint { L >= 5.0 }): the default stands and the assert is reported violated against it; a plain = value never gives way, and an equation that contradicts it is reported violated. An equation that names a feature by its path, assert constraint { p.x == 3.0 } over part p : P whose P declares x with no value, gives p's x that value, and P's y = x * 2.0 is 6 in p; not where a binding gives p's x a value (the assert is checked against it) or two such asserts give it two (it is read as no value). Where that binding's value is a default (bind p.x = L with L default = 4.0), the assert should stand over it. This is a known gap: the check, the literal engine and the numeric surface read the 4 and report the assert violated, and the solver lane finds the axioms inconsistent. An assert written in an instance around the feature, over a default (part q1 : Q { assert constraint { p.x == 50.0 } }), defines it in that instance alone: q1's p's x is 50 on every surface, while P's own x, Q's p's and every other instance's keep the default 2. P's relations are then read per instance — c in q1::p is a row of its own, read at 50, whether or not the model writes a binding — as is Q's c { p.x <= 10.0 } in q1 (Q::c in q1), a package constraint over q1.p.x, and the assert's own row, which holds. The same goes for the package's assert constraint { q1.p.x == 50.0 }, for an assert of q1's type (part def Q2 :> Q { assert constraint { p.x == 50.0 } }, with part q1 : Q2), in every instance of that type, and for a bare L == 5.0 in a definition that specialises L's owner; q1's own part :>> p { attribute :>> x default = 9.0; } under such an assert reads 50 too, its 9 read nowhere. So does a redefinition that renames p (part pp :>> p), at pp.x, on every surface but the SMT engine, which cannot read the assert's p.x in that instance and leaves its rows undecided. A path through a reference or a subject, or through a part some usage redefines as one or with a value (ref part :>> r = p1, part :>> p = other), is not read so: the instance there may be another one, so the default stands, the assert is reported violated against it, and the solver lane finds the axioms inconsistent. A binding into the instance whose value is written with = is read over the assert (bind p.x = K in q1, K = 7.0, under Q's p.x == 50.0): q1's p reads K, and the assert is reported violated against it. One whose value is a default is read the same way, the known gap above. An equation over names, p.x == M, is read over q1's own M — it is could not be evaluated where it is written in an element that is not the instance's own (an assert in a usage nested in a definition) or beside a [unit] literal. Two such equations that give the value two values, or two over names written in two places, are read as no value; so is one that sets the default equal to another default (p.x == L with q1's L default = 9.0, or an M whose = reads one): both defaults give way in q1, and every constraint over q1's p's x or L is could not be evaluated, on the solver lane too — but in an instance that states that name with = (part q : Q { attribute :>> L = 50.0; } under Q's p.load == L), the equation reads it, and q's p's load is 50. An inequality (p.x >= 5.0) defines nothing: the default stands, the assert is reported violated against it, and the solver lane finds the axioms inconsistent.

A value P derives from what p changes (attribute e = m * 2.0;, e = 10.0 - part1.m, a calculation's body, an asserted equation, a value read through another part's redefinition) is p's own value: P's expression evaluated over p's names, on every surface — p.e is 40 kg where P's own e is 37 kg. A redefinition that states nothing (attribute :>> e;, or the copy a bind w = p.e makes) reads it the same way, in p. P's constraints and asserts hold in p too: each is read again in every context that changes what it reads, as rows named P::c in R::p, beside P's own verdict, on every surface — the numeric surface and solveFeasible included.

Every instance has its own values. Two parts of one type, g1 : G and g2 : G, are two values of G's g: the verification lane reads them by symbols of their own (R::g1::g, R::g2::g — and R::q1::p::x for an instance reached through two usages), the solver solves each by itself, and nothing one of them states fixes the other — g1.g == g2.g is not proved of two values nothing relates. What G states holds of each instance: its value expressions, its asserts and its bindings are filed again for every instance a relation reads, as rows named G::c in R::g1 — and so is what the types of every instance ENCLOSING it state: s.q.load, over part s : Sys whose Sys binds p.load = q.load, holds Sys's binding as well as P's asserts. A value the same in every instance — a literal, or arithmetic over literals the instance changes nothing of — keeps the feature's own name. A verify row prints a path read through an instance at that instance's value (bindings, and the evidence record's witness): q.m2 is −40 where Q's own m2 is 9; a value a binding carries into the instance prints in the unit the feature it fills declares (5000 g into a kg feature is 5 [SI::kg]), and no value stands where the reading finds none there (an expression with a unit literal) or where the row abstains. A requirement's subject that nothing binds, read in the requirement itself, is the generic instance of its type (the requirement is about any one); reached through a usage (r1.s, sys.ra.s, a nested requirement's r2.t) it is that usage's own, and a subject that says something of its own (subject s : P { assert constraint … }) is an instance of its own. --free and bounds --measure take an instance's symbol, or its dotted path.

A name the element it is written in does not declare is read as KerML resolves it there: through the namespaces that own that element, nearest first. part def A { attribute x = K; } in package Lex { attribute K = 7.0; … } reads Lex's K, on every surface — except where one feature nested below the element reading it is the only one of that name (A's part p : P with P's own K): that feature is read first, as before, where KerML reads Lex's K, and an asserted equation (below) takes no value from the name there: a known gap. Only an attribute is read so, and only by its bare name: a qualified Lex::K or a dotted name is not. A body is read as it is written, wherever it is read: A's x = K, read for part def H { attribute K = 70.0; part a : A; }'s a, reads no K where A sees none, nor where an import or an alias answers the name first (import Consts::*;, alias K for Consts::K; — such a name is not read), nor where something that specialises the element reading it declares a K of its own. A package's attribute is one value wherever it is read, unless it is a default that an assert other than the package's own names. An attribute of an enclosing definition or usage is read where it is declared only where it is one value in every instance of that owner: nothing that specialises the owner declares the name anew, no binding joins it, no assert names it where it is a default, and what its value reads is such a value too (R's y = 3.0 read by its nested part def Q { attribute z = y + K; }). Elsewhere a row that reads it is could not be evaluated, in a sentence naming the element that changes it — Q's p :>> load = L beside part q : Q { attribute :>> L = 50.0; } reads neither Q's 1 nor q's 50, for Q's own p or for q's. An asserted equation over a default reads such a name on its other side as a value of its own where it is a constant written with =: part p : P { assert constraint { x == L } } beside the package's L = 50.0 makes p's x 50 on every surface, and so does Q's assert constraint { p.x == L }. Where an assert in an instance around the feature names one that is not read so (an import answers it, or an instance gives it another value), the default gives way there and the feature is read as no value.

A requirement is read where its subject is bound. satisfy R by p and requirement r : R { subject s = p; } read R's clauses at p — s.m is p's m — as rows named R::c in R::p (or in R::r), each goal under its own assumptions, beside R's own reading at the subject's type, wherever p reads them otherwise: a value of its own, or an instance that holds more than R's subject does — an assert or value of p's own, a narrower type, an instance enclosing it (satisfy R by q1.p is q1's p), a relation of the model that reads it. A satisfier that holds exactly what the subject holds reads R as the subject does, and adds no row. refine reads a component's contract at the part that satisfies it.

The status column says what is stored, never what is true. open means nothing has been shown yet; no formal clause means the requirement is prose with no constraint body; not encodable means a gate refused the relation and names which. discharged and stale are read back from an evidence record, so nothing is ever discharged here today.

A requirement massOk : MassLimit; usage owns no clause of its own — the require constraint is on the definition it applies. contracts says so on the usage's row and files the clause once, on the definition; it is not counted as prose-only, and it does not appear under --missing.

A requirement that specialises another and writes a clause as well is the other half of that shape, and it is the one where a reader can be shown less than applies. requirement def StrictMassLimit :> MassLimit { require constraint { v.topSpeed <= 60 [m/s] } } promises what it wrote and what MassLimit wrote, so the row lists both and marks the second:

$ npm run sysprose -- contracts spec-inherit.sysml
  ...
  SpecInherit::StrictMassLimit  [RequirementDefinition]
    subject v : Vehicle (inherited)
    require v.topSpeed <= 60 [m/s]  [QF_LRA — linear real arithmetic]
    2 guarantee(s): 1 declared, 1 inherited from SpecInherit::MassLimit
    require v.mass <= 1500 [kg]  [QF_LRA — linear real arithmetic] (inherited)
    no satisfy, verify, derive or refine statement names it
    variables declared v.topSpeed (parameter)
  ...

The (inherited) is the same word the subject line has always carried, and it is a disclosure, not a filing: the inherited clause is still filed once, on the element whose body holds it, so the worklist, the obligation digests and the evidence keys are exactly what they were. The element named on the count line is the one that wrote the clauses of that role — down a chain of three, an inherited assume and an inherited require come from two different places and each line says its own. variables reads variables declared on such a row for the same reason: that list is the encoder's input and it holds what this requirement wrote, not what the clause above it reads.

Only a clause some contract in the same report files is disclosed. A general type the report left out — a #prose statement, or a case clause written outside an objective — has no row of its own, so its body is shown on nobody else's either. A case that specialises another does disclose the parent's objective clauses, because that is where a case's clauses are filed.

contracts --json carries the census beside the inventory — clauseInheritance counts the contracts that inherit a clause, split by whether the author wrote :> (Subclassification) or : (FeatureTyping), plus how many distinct inherited clauses are anonymous and how many named ones a nearer clause masks. Every example this repository ships, and every model in its test corpus, reads zero on all four.

obligations --missing is the one to run first on a real requirement set. It narrows the listing to exactly the rows this lane would not decide even with every solver installed, and prints the histogram of the gates that refused them. Expect a substantial fraction of a real programme's requirements to land there: prose-only requirements, temporal ones, °C arithmetic, collection-valued features. That is information about your model as much as about the tool, and it arrives before anyone waits for a proof.

Both take --element REF — an id, a qualified name, or a name unique in the model — to scope the report to one requirement or one package. A reference naming bundled library content is refused: every figure in both reports is about your model and excludes the library by construction.

Source of truth: src/semantics/contracts.ts, src/semantics/obligations.ts, src/api/verification.ts, and the plan these implement, 04-formal-verification-plan.md.

Writing a clause the tool will accept

Between the prose and the proof there is a step nothing above helps with: a requirement that says "shall sustain at least 45 minutes" has to become a relation a solver can read. Two subcommands stand there, and both of them ship before the clause reaches verify.

property-draft --element R hands you what you need to write one. The three FRETish fields that are mandatory (component, shall, response) filled in from the model; the three that are not (scope, condition, timing) printed as commented guidance with the reason each is unencodable; a data dictionary of every legal name in the subject's scope with its type, unit, dimension, value and whether it can stand in an arithmetic comparison; every #prompt that reaches the requirement or its subject, verbatim; a skeleton whose six fields are comments and whose last line carries <bound> for you to replace; and example clause shapes built from the dictionary, each of which passes the gates below as written.

$ npm run sysprose -- property-draft examples/uav-isr.sysml --element MassRequirement
examples/uav-isr.sysml: UAVSurveillanceSystem::MassRequirement — the encodable skeleton
  subject   uav : AirVehicle (declared)
  ...
  data dictionary — 19 legal name(s), always written through the subject
    uav.cruisePower                       ISQ::PowerValue  [W]  dim L²·M·T⁻³  claim literal  = 650.0
    uav.endurance                         ISQ::DurationValue  (no unit of its own)  dim T  claim consistent  = battery.capacity * usableEnergyFraction / cruisePower
    uav.mtow                              ISQ::MassValue  [kg]  dim M  claim literal  = 18.5
    ...
  meaning is not checked; read the back-translation.

Every name in that dictionary is written through the subject — uav.mtow, never a bare mtow. That is not decoration: the shipped example has two features called mass, a bare name resolves to whichever the scope walk reached first, and you would have no way to see which one you got.

property-check --element R --clause TEXT then judges the clause you wrote, at gate 0 and four gates after it, and refuses at the first one that says no:

Gate 0 refuses; it does not accept with a gap. A clause carrying a temporal field is one nothing downstream can decide, and "accepted, but the temporal part was ignored" would put an undecidable clause in your file with a tick beside it. The fields are written ahead of the body and separated from it by ;, in either spelling — scope: after; uav.mtow <= 25.0 [kg] or scope = after; …. The first is what property-draft's skeleton emits, so handing that skeleton back with its // markers removed reaches gate 0 rather than being refused as arithmetic.

$ npm run sysprose -- property-check examples/uav-isr.sysml \
    --element EnduranceRequirement --clause 'endurance >= 45 [min]'
examples/uav-isr.sysml: UAVSurveillanceSystem::EnduranceRequirement — refused at gate 2
  ...
  refused at gate 2: `endurance` does not resolve in the scope of `uav` — did you mean `uav.endurance`? ...

An accepted clause comes back with a back-translation into structured English and the insertion range — the line and column inside the requirement body where the clause goes, with the line already indented:

$ npm run sysprose -- property-check examples/uav-isr.sysml \
    --element MassRequirement --clause 'uav.mtow <= 25.0 [kg]'
examples/uav-isr.sysml: UAVSurveillanceSystem::MassRequirement — accepted
  ...
  back-translation
    uav shall satisfy: uav.mtow is at most 25.0 kg
  where it goes
    line 138, column 1
            require constraint { uav.mtow <= 25.0 [kg] }
  meaning is not checked; read the back-translation.

The range is zero-width and the indentation is copied from the body, so applying it is a splice and nothing is overwritten. Three shapes are worth knowing about. A requirement written entirely on one line has no body line to insert before, so the range points just inside its closing brace and the indent is a single space. A requirement usage with no body at all (requirement massReq : MassReq;) has nowhere inside it for a clause to live, so there is no range and the report says which of those it is rather than guessing. And on a case, the range points inside objective { … } — that is where a case's clauses are read from, and a clause outside it would parse and bind nothing.

Three things to take from that, and the last one matters most:

• Neither subcommand judges the model, so both obey the reporting exit contract: a refused clause is an answer about a string you passed, not a finding about your file, and it exits 0 with the verdict in the report (and in --json, under outcome, refusedAt and code). 2 is a usage error — a missing --clause, a REF that names no requirement.
• Gate 4 is syntactic non-triviality. The clause and its negation are checked satisfiable with no axioms asserted at all, so uav.mtow <= 25.0 [kg] is accepted over a model that pins mtow = 18.5 [kg]. It is true of the design as written and the gate does not care: what it refuses is a clause that is valid or unsatisfiable on its own. verify's tautology check and the vacuity report are what decide the other question, and the limit is printed on every report.
• The tool never says the clause means what the prose meant. Every report ends with "meaning is not checked; read the back-translation." — which is what the back-translation is printed for. Reading it is the one step nothing here can do for you.

Nothing is written back: property-check tells you where the clause goes and you (or your agent) put it there, then npm run check and the ordinary repair loop apply. examples/contract-authoring-prompts.sysml is a shipped model that writes the four authoring rules as #prompt statements at package level, so property-draft hands them to whoever works on any requirement in it.

Source of truth: src/api/property.ts, examples/contract-authoring-prompts.sysml, test/unit/property.test.ts, and §3.3 of 04-formal-verification-plan.md.

Whether it holds, and the two words that are not the same

verify is the one subcommand that reaches a verdict, and it is the one whose exit code you should read before anything else. It has its own exit-code contract, and it is not the other two: 0 every obligation discharged and there was at least one to discharge, 1 at least one obligation refuted, 2 usage, I/O, a degraded model, a model that states no obligation at all, or any inconclusive.

The summary line leads with the inconclusive count, on purpose: it is the figure that decides the exit code, and a line that opened with the green number read as a pass with a footnote.

$ npm run sysprose -- verify examples/uav-isr.sysml --engine literal
examples/uav-isr.sysml: 0 inconclusive, 2 discharged, 0 refuted — engine literal
  a point evaluation at the model's own values — `holds-at-values`, never `proved`
  UAVSurveillanceSystem::EnduranceRequirement  uav.endurance >= 45.0 [min]
    holds-at-values: holds at the model's values (no assumptions — the pass is unconditional at these values)
    bound: the model's own feature values, 1 of them; 0 free variables; compared as 2835.6923076923076 vs 2700 in T, coherent SI
    digest sha256:e4618d6f...
  ...
$ echo $?
0

That compared as … coherent SI clause is not decoration. uav.endurance is derived — the model computes it — so what it stores is 0.7877, the hours its own equation produced, with no declared unit, beside a requirement written in [min]. Read on its own that number looks like a refutation of the verdict it supports. The SI pair is what the comparison was actually made on, it is in the evidence record's bound.si, and every witness value in a record carries its role so a computed value is never mistaken for one you could edit.

holds-at-values is not proved, and the tool will not let the two words blur. The literal engine substitutes the values your file states and reads off the answer. That is worth having — it is what the Analyze button already computes, it needs nothing installed, and it is the first thing anyone wants — but it holds at one point of a design space that is infinite. proved is reserved for the solver showing that the negation of the obligation is unsatisfiable, and only the SMT engine can say it.

Three engines, and the one that is missing never goes green.

That last line is the rule to remember: with no solver present, the same file that is exit 0 under --engine literal is exit 2 under the default --engine auto. "No solver, nothing to report, exit 0" would be indistinguishable from a proof, so it does not happen.

Every claim this lane can make, and what each one costs you. A claim is the word in the evidence record; a verdict is the three-valued facet written back into the file, and only two claims are allowed to move it (proved ⇒ pass, refuted ⇒ fail). The exit code is the run's, not the row's: the strongest row wins, in the order refuted → design-admitted → undecided.

Two readings that table is defending. holds-at-values discharging a run is not a proof being rebranded: it is the reader naming a point evaluation on the command line and getting exactly that, which is why the same file is exit 2 the moment the engine is auto. And an empty run is exit 2, not 0 — a model that states no obligation has not been shown anything, and a build that went green because every requirement was deleted is the failure this lane exists to prevent.

What proved stands on. The engine asks four questions per obligation, and each of the last three exists to stop a proof that would be void rather than absent:

$ npm run sysprose -- verify examples/uav-isr.sysml --engine smt
examples/uav-isr.sysml: 0 inconclusive, 2 discharged, 0 refuted — engine smt
  negation-unsat under a satisfiable axiom set — `proved` means exactly that, at 5000 ms per check, with every feature value bound as the model states it
  UAVSurveillanceSystem::EnduranceRequirement  uav.endurance >= 45.0 [min]
    proved: A ∧ P ∧ ¬G unsat, QF_NRA, 4 fixed / 0 free, timeout 5000 ms; assumptions satisfiable
    bound: every feature at the value the model binds it to; 4 symbol(s), 0 free; compared as 2835.69… vs 2700 in T, coherent SI; decided by z3 Z3 5.1.0.0, seed 0
  ...
$ echo $?
0

• Is the model's own axiom set satisfiable? Asked once per run. If your file contradicts itself, every negation is unsat and every obligation would print as proved — so instead every row is verification/inconsistent-axioms with the colliding facts named, and nothing is decided.
• Is the negation unsatisfiable? Unsat ⇒ the obligation holds everywhere your axioms and assumptions allow. Sat ⇒ a counterexample, which is checked before it is printed (below).
• Can the assumptions all hold at once? If not, the obligation was discharged for free: verification/vacuous, exit 2, never a pass.
• Is the goal true of every model? panel.area == panel.area is honestly proved and honestly useless, so it is proved and flagged as a tautology.

A counterexample is re-checked before you see it. Every witness the solver returns is substituted back through this tool's own evaluator — over the exact rationals the solver answered with — and with nothing freed it must also read as violated on the numeric surface — a second, independent path. A witness that fails either gate is reported as inconclusive: witness not confirmed, never as a violation. That is what catches an encoder defect in the direction that matters.

Numbers are the decimals you wrote, on every surface. 0.1 + 0.2 == 0.3 holds and 0.1 + 0.2 > 0.3 does not — on the Problems panel, the numeric surface, verify --engine literal and --engine smt, consistency, bounds and refine alike. A strict bound is violated at its boundary (mass < 18.5 [kg] at 18.5 kg is refuted, exit 1, by both engines), and 1.0 + 0.00000000000000001 > 1.0 is true, although binary64 rounds that sum to 1.0. The point evaluators compute in binary64, but they decide every comparison by exact arithmetic over the decimals written — unit factors included — wherever it can be computed. Where it cannot (an operand computed by a fractional power), two sides within a relative 1e-9 of each other are undecided: not-evaluable, never forgiven, and never either verdict. Two readings are binary64 by definition: a numeral written with more than 15 significant digits is the double it parses to, and a unit factor that is no decimal (the hartley and the nat, whose factors are logarithms) is the double the registry holds. A value only a numeric solve produced is read at the solve's own tolerance: within it ==, <= and >= hold, and a strict ordering or a != is undecided — the solve does not know which side of the bound its value lies on.

Freeing a feature is a two-sided act. --free F releases a value so the solver may vary it — but this tool derives no domain axiom from a quantity kind. It does not know that a power is non-negative. Freeing uav.cruisePower under an assumption that only caps it from above lets a solver answer with −1 W, and the re-evaluation gate confirms that arithmetic, so it would print as a genuine refutation of a requirement nothing is wrong with. So a freed feature the assumptions do not confine on both sides is verification/free-variable-unbounded — inconclusive, exit 2, never refuted. Write the premise both ways round first:

assume constraint { uav.cruisePower >= 100.0 [W] and uav.cruisePower <= 600.0 [W] }

--timeout MS is a budget, not a switch. Every check in this lane is bounded (5000 ms by default) and there is no spelling for "no timeout": --timeout 0 and --timeout forever are refused rather than quietly replaced by the default, because a reader who asked for a bound the tool did not honour would read every unknown under a bound that was never in force. A solver that runs out of time reports verification/timeout, which says nothing about whether the requirement holds, and it is not retried with a weaker encoding.

--strict-vacuity is loud and inert. It raises a vacuous obligation from an info line to verification/vacuous-property, an error — and changes the exit code not at all. Vacuity is inconclusive and exits 2 with the flag and without it. Use it when a vacuity is something you want a build log to shout about rather than something to scroll past.

--why names the axioms the solver's own answer stood on — and says what that is not. When z3 answers unsat it can hand back an unsat core: the subset of the labelled assertions that is enough, on its own, for the contradiction. verify --engine smt --why prints that set under each proved row, member by member, with the kind each one was asserted under:

$ npm run sysprose -- verify examples/uav-isr.sysml --engine smt --why
  UAVSurveillanceSystem::EnduranceRequirement  uav.endurance >= 45.0 [min]
    proved: A ∧ P ∧ ¬G unsat, QF_NRA, 4 fixed / 0 free, timeout 5000 ms; assumptions satisfiable
    why: the core names 4 of this model’s 12 axiom(s), 1 side condition(s) and the goal — 6 label(s) in all
      axiom UAVSurveillanceSystem::AirVehicle::cruisePower
      axiom UAVSurveillanceSystem::AirVehicle::endurance
      axiom UAVSurveillanceSystem::AirVehicle::usableEnergyFraction
      axiom UAVSurveillanceSystem::BatteryPack::capacity
      goal UAVSurveillanceSystem::EnduranceRequirement::«ConstraintUsage»
      side UAVSurveillanceSystem::AirVehicle::endurance — a non-zero divisor or base the ENCODING asserts, not a fact the model states
    the set z3 returned is sufficient, not minimal: an axiom listed here may not have been needed, and an axiom NOT listed may still carry the claim

Read that last line before you read the list. A core is a sufficient reason, picked by the solver — not the set of facts your requirement depends on. Give a model three ways to settle one requirement and it will name one of them: with mtow = 18.5 [kg] capped at both 20 and 22, the core for mtow <= 25.0 [kg] names the 22 — the weakest of the three — and never mentions the value your file actually binds. Deleting an axiom that is not in the core can therefore break the proof, and that is why this tool will not print "the axioms this proof depends on" over a core, and why minimal is a word only consistency --minimize earns: that one runs a deletion loop, and this runs none.

The side member is worth knowing about. Where a relation divides by something your model can vary, the encoding asserts the divisor is non-zero — an assumption it added, not a fact you wrote — and labels it with the name of the row it guards. So the same qualified name can appear twice in one core, once as an axiom and once as a side condition, and both are real.

--why decides nothing: the claim, the code and the exit status are identical with the flag and without it, and nothing it prints reaches the evidence record. Only a proved row's core is published here — a point evaluation asks no solver anything — and a run that reached no proof says so rather than printing nothing. Two other cores are printed by this tool and neither is one of these: the one under verification/inconsistent-axioms is about the whole file's axiom set, and the one under verification/vacuous is about that obligation's premises. Both appear inside the sentence that reports them, because they answer other questions.

With --json, each obligation carries the core itself — on every run, with the flag and without it, since the flag gates the display and not the field — plus an axiom census: modelAxioms (every axiom row this run gathered, whether the encoder took it or refused it), footprintAxioms (the rows this obligation's read-closure kept, refused ones included, so a kept row can assert nothing), scriptAxioms (what those rows actually asserted, side conditions included) and coreAxioms. Read coreAxioms against footprintAxioms: that is the pair that says how far the solver's answer narrowed the read-closure the encoder already applies. The two other numbers do not bracket each other — scriptAxioms is 5 against a footprint of 4 on the endurance obligation above, where an axiom divides by a variable and the encoding asserts the divisor as well, and it is 1 against a footprint of 2 on a model whose read-closure kept an axiom the encoder refused. And nothing in the payload repeats the sufficiency sentence: a consumer that renders these members carries it itself.

What is inconclusive, and what a flag may forgive.

A vacuous requirement is reported as undecided, and that is a deliberate disagreement with the specification. Part 1 §9.2.14.2.8 gives a requirement check as allTrue(assumptions) implies allTrue(constraints), which makes a requirement with a false assumption true. A requirement discharged by an antecedent that does not hold tells you nothing, and it is the classic way a whole requirement set passes while meaning nothing — so this tool says vacuous, exits 2, and records the disagreement in CONFORMANCE.md.

--record PATH writes the evidence. One record per obligation: the claim, the engine, the tool and its version, the bound the claim holds within, the witness (your own values), the flags that changed what was shown, and two digests — one for the obligation's normal form, one for your model. Records carry no timestamp, so two runs over an unchanged file produce byte-identical files and a diff answers "did anything change?". The model digest is taken over qualified names rather than element ids, which are fresh on every load, so it survives a reparse and moves when you edit a literal. The shape is documented in schemas/evidence-record.schema.json.

--record refuses a model that did not load cleanly. A record is durable and diffable; one written over half a model would claim holds-at-values about a file the same run calls unreadable, bound to a digest taken over only what was salvaged. Fix the findings first, or read the verdict on stdout without --record.

--free F releases a feature value so a solver may vary it; a refutation obtained that way is a design your model admits, not a violation of it, and it is reported as design-admitted and exit 2 — never exit 1. A spelling that frees nothing is refused rather than ignored, because a name that quietly freed nothing would print a verdict under a bound the record then claims was in force — and there are three ways to free nothing, all three refused: a name that matches no element, a bare name that matches more than one (--free uav on the shipped example names three: the part usage and the subject uav of each requirement — write the qualified name of the one you mean), and a name that resolves to something no relation in the run reads. That last one is not hypothetical: --free UAVSurveillanceSystem::uav names the part usage, which is not a variable any relation reads, so it released nothing at all — and the run printed proved and exited 0 under a header reading "with uav released", where the intended --free uav.cruisePower is design-admitted and exits 2. The refusal names what could be freed here, so the next attempt is a copy-and-paste. The literal engine refuses the flag outright rather than accepting and ignoring it.

Source of truth: src/semantics/engines/literal.ts, src/semantics/engines/smt.ts, src/api/evidence.ts, src/api/verification.ts, and the golden verdict corpus in test/fixtures/verification/.

Whether the requirements can all hold at once

verify asks whether each requirement holds of the design your file describes. consistency asks the other question: could these requirements be met by any design at all? The two are different, and they disagree by construction — a file whose values break a requirement is refuted by the first and has a perfectly satisfiable requirement set according to the second. That is why they are two subcommands and not a flag.

$ npm run sysprose -- consistency examples/uav-isr.sysml --with-values
examples/uav-isr.sysml: 0 inconsistent, 0 inconclusive, 1 consistent — 2 requirement(s) on 1 subject(s)
  asked at the model's own values (`--with-values`): …
  subject UAVSurveillanceSystem::AirVehicle (as `uav`) — consistent
    2 requirement(s) can hold together at the model's own values (`--with-values`): QF_LRA,
    witness …::mtow = 18.5, …::cruisePower = 650 (stored magnitudes), re-read in
    process. 0 relations refused. …
$ echo $?
0

By default the numbers in your file do not get to answer. Every feature that carries a literal value is released, and only the structural axioms — assert constraint bodies, bind equalities and the defining equations of derived features — are kept. A requirement set is inconsistent when nothing can satisfy it, and answering that with whatever mtow happens to be today would be a question about one design point rather than about the requirements. The report says which values it let go and how many. --with-values re-pins them and asks the weaker question — "can these requirements hold together at the point this file states" — and every verdict line names which of the two it was computed in.

Each requirement is read as assume ⇒ require, and every verdict line says so. That is the reading the shipped library states (Requirements::RequirementCheck is allTrue(assumptions()) implies allTrue(constraints())) and the one verify uses on the same file. It matters most for mode- and phase-conditional requirements: assume { mode == cruise } against assume { mode == ferry } is not a conflict, because no single design point is ever required to meet both guarantees. Read as a conjunction they would be reported as contradictory, which is a false alarm on one of the commonest patterns in systems engineering.

The price of that reading is paid rather than hidden. A set of implications is satisfiable by falsifying every antecedent, so each requirement that carries assumptions is asked a second question — can it be engaged at a point the whole set admits? A set that holds only because one of its requirements never applies is not reported consistent: the row comes back inconclusive under verification/vacuous with the requirement and its assumptions named, exit 2, and no flag lowers it — the same rule verify applies to an obligation discharged by an antecedent nothing can satisfy. The witness is still printed, because the set is satisfiable; what is undecided is whether the requirements mean anything at that point.

Mutually exclusive modes pass that check — each is engaged at its own point — while two requirements under the same assumption whose guarantees collide fail it. So a conditional requirement is neither exempt from scrutiny nor falsely accused.

An inconsistency is only ever printed with a named subset. The engine asserts each requirement under its own tracking literal, so an unsat comes back with the labels that collided:

$ npm run sysprose -- consistency conflict.sysml --minimize
conflict.sysml: 1 inconsistent, 0 inconclusive, 0 consistent — 2 requirement(s) on 1 subject(s)
  subject ConsistencyConflict::AirVehicle (as `uav`) — inconsistent
    …a minimal conflicting subset is {R-UAV-002::mtowCeiling, R-UAV-004::mtowFloor}. 0 relations refused
    verification/inconsistent-requirements
    a minimal conflicting subset, 2 member(s):
      R-UAV-002  uav.mtow <= 25.0 [kg]  [guarantee: ConsistencyConflict::MassCeiling::mtowCeiling]
      R-UAV-004  uav.mtow >= 30.0 [kg]  [guarantee: ConsistencyConflict::MassFloor::mtowFloor]
$ echo $?
1

Exit 1 means the same kind of thing here as it does for verify: a decided finding about your model. verification/inconsistent-requirements is an error, and no flag forgives one.

"Minimal" is a word only --minimize can earn. A solver's unsat core is not minimal — it is a subset that collides — so the report calls it a conflicting subset. --minimize runs a deletion loop, one solver check per member, removing each in turn and keeping it only if the rest become satisfiable without it. Only a loop that ran to completion upgrades the phrase to a minimal conflicting subset; a timeout, or a core larger than --max-core (default 8), leaves the weaker phrase and says the budget was why.

"Consistent" always comes with the count of what was left out. A relation a gate refused — arithmetic on a °C scale, a %, a collection — is listed with its reason and is not asserted. That cuts both ways, and the asymmetry is why the count is printed every time: an inconsistency found without those relations is still an inconsistency (adding an assertion can only make a set harder to satisfy), but a set satisfiable without them might be excluded by the very relation that was refused — so a set that reaches one (its own clause, or a refused fact sharing a feature with it) is inconclusive, not consistent: verification/unsupported-construct, which --allow-inconclusive may forgive, where every such relation is the set's own and outside the fragment (as verify files it) and, under --with-values, none is false at the values (a violation verify refutes), and verification/not-evaluable otherwise. A requirement that states no relation at all is counted apart, on the same line: no gate refused it, and folding the two together would report a file of prose requirements as one whose relations this tool turned down.

A requirement set with nothing to check is never green. A subject whose requirements are all prose, or all outside the encodable fragment, comes back inconclusive — an empty conjunction is satisfiable and says nothing — and a run in which nothing was decided is exit 2 with --allow-inconclusive and without it. With no solver installed there is nothing to fall back to at all: satisfiability is not a question your model's own values can answer, so --engine literal has no counterpart here and an absent backend is verification/tool-absent, exit 2.

--subject REF narrows it, and a type answers for its subtypes: a requirement written about a Vehicle is a requirement about every air vehicle, so the air-vehicle set holds both — even when no requirement is written about the air vehicle itself. The REF may name the part usage your file writes after subject (--subject uav), which is narrowed through its declared type. A REF that resolves but is the subject of nothing, and conforms to nothing that is, is refused by name and exits 2 — not reported as a file that states no requirements. Requirements with no subject are grouped and answered together rather than dropped.

What this is not. It decides the satisfiability of static contracts — numbers, and the relations between them. Whether a reactive implementation could be built to meet a specification over time is a different question with a different answer, and this command does not answer it. Nothing here is about ordering, timing or behaviour.

Source of truth: src/semantics/consistency.ts, consistencyReport in src/api/verification.ts, and the L8 cases in test/campaign/verification.test.ts.

Whether the parts add up to the whole

verify and consistency are about requirements. refine is about an architecture: given a contract on a system and a contract on each of its parts, do the parts — together with the equalities your model actually states — entail the whole? It is Cimatti's Theorem 1, and the two obligations it checks are the ones that theorem names.

$ npm run sysprose -- refine examples/uav-power-budget.sysml --via composition
examples/uav-power-budget.sysml: 0 not refined, 0 vacuous, 0 inconclusive, 1 refined — 1 decomposition(s) over 5 contract(s)
  obligations are Cimatti's Theorem 1 in normal form (`nf(C) = ¬A ∨ G`), preceded by the satisfiability precondition step (0): …
  γ, the connection assertion: 2 bind equalities, 1 item flow(s); 1 connection(s) NOT encoded — a connection is not an equality; bind the attributes if they are one quantity
  UAVPowerBudget::PowerBudget on `UAVPowerBudget::PowerSystem` — refined
    refines: 4 obligation(s) proved over 4 sub-contract(s), 2 bind equalities and 1 item flow(s); 1 connection(s) not encoded as equalities. 0 relations refused. …
      obligation (3)  proved
      obligation (4) UAVPowerBudget::ComputerDraw  proved
      …
$ echo $?
0

A decomposition is read off satisfy, not guessed. A contract belongs to a part because your file says satisfy R by sys.part;. A contract whose part encloses the parts other contracts are satisfied by is a system contract, and those others are its components — with the nearest such enclosing part winning, so a three-level tree decomposes level by level rather than flattening. A file that states no such pair states no decomposition, and the run says so and exits 2 rather than reporting that everything is fine.

Encloses means containment and the part's own type, because that is how a SysML v2 file writes a tree. satisfy CellCharge by Pack::cell names a usage whose owner is the part definition Pack, and no contract is satisfied by Pack itself; part pack : Pack is what says where cell lives. Reading only containment would drop those leaf contracts from every decomposition — silently, with the run still exiting 0 over the level above them. test/fixtures/verification/models/refinement-three-level.sysml pins both levels.

The two obligations, in normal form. With nf(C) = ¬A ∨ G:

• (3) ⋀ nf(C′) ∧ γ ⊨ nf(C) — the components, plus the connections, entail the system contract.
• (4) for each component U: A ∧ ⋀_{S′≠U} nf(C′) ∧ γ ⊨ A_U — every component assumption is discharged by its siblings and the wiring.

Normal form is not a flourish. With bare guarantees the check is unsound under mutual support: take two components where each assumes exactly what the other guarantees, against a system contract that promises the same thing. The bare obligation G₁ ∧ G₂ ⊨ G is p ∧ p ⊨ p and passes — yet an implementation in which p is false satisfies both component contracts and breaks the system guarantee. In normal form each nf(Cᵢ) is ¬p ∨ p, which is ⊤, so the obligation becomes ⊤ ⊨ p and is refuted, with a witness. That is the case test/fixtures/verification/models/refinement-mutual-support.sysml pins.

Step (0) runs before every obligation. check(A ∧ ⋀ nf(C′) ∧ γ). Two sibling contracts of ⟨true, x > 10⟩ and ⟨true, x < 5⟩ over one bind class make the antecedent of obligation (3) unsatisfiable, so (3) holds vacuously — and without step (0) the tool would print "obligation (3) proved" over an architecture whose components cannot coexist and whose system guarantee is absurd. It comes back verification/contract-set-vacuous, never refined, exit 2, and no flag lowers it.

γ is what your model states, and what this tool already computes with. The connection assertion is built from bind / BindingConnector equalities and from the item flows value propagation already carries (target = source). Those are exactly the edges checkConstraints, the app and every existing report honour, so a proof here cannot rest on an equality the rest of the tool does not believe — and an item flow that does carry a voltage is not left out, which is how a downstream assumption ends up "not discharged" for no reason.

A bare connection is not an equality. It joins two features and states nothing about their values, so it is listed under notEncoded with the hint bind the attributes if they are one quantity, and it is counted on every verdict line — counted per decomposition, so a group reports the wiring it carries rather than the file's total. --connections-as-equalities opts into the OCRA reading in which it is an equality, and it opts into that for connect and nothing else: an allocate is a traceability mapping and an interface joins ports through connections of its own, so both stay listed under the flag, each with a hint naming what it is. When you use it, that fact is printed on every verdict line, because it changes what the verdict claims. Counter-evidence, recorded rather than buried: the one published SysML v2 → OCRA translation maps connect and bind alike, so the default here is a stricter reading than that path takes, not a consensus.

$ npm run sysprose -- refine rig.sysml
rig.sysml: 1 not refined, 0 vacuous, 0 inconclusive, 0 refined — 1 decomposition(s) over 3 contract(s)
  γ, the connection assertion: 0 bind equalities, 0 item flow(s); 1 connection(s) NOT encoded — …
      obligation (4) RefinementBareConnection::LoadDraw  refuted [verification/unconnected-assumption]
      witness: …::Load::supplyVoltage = 0, … (stored magnitudes)
$ echo $?
1

Exit 1 means the same kind of thing here as everywhere else in this lane: a decided finding about your model. A refuted obligation is verification/refinement-failed, or verification/unconnected-assumption when the quantity the assumption is about is reached by no connection at all — the second is a wiring problem and the first is a design one, which is why they are two codes. Both are errors and no flag forgives one.

refine publishes its own exit-code contract, not verify's. The two look alike at 1 — both mean a decided negative about the model — but verify's paragraph is written in terms of values: "with every feature at its model value", "a relation not evaluable at the model's values", "a refutation obtained under --free". A refinement obligation reads no value and there is no --free here, so quoting that paragraph under refine would publish three promises it cannot keep. refine --help and the command reference print the contract this command actually implements: 0 every decomposition shown to refine, 1 an obligation refuted with a confirmed counterexample, 2 anything undecided — including a vacuity and a clause a gate refused.

A clause the tool could not encode does not quietly shrink the question. It is listed with the gate that refused it, and where it sat decides what happens. On the system contract any refused clause stands the whole decomposition down as verification/refinement-undecided: nf(C) with a conjunct missing is a weaker goal, and a weaker goal is easier to entail. On a component the two halves of nf(C′) = ¬A ∨ G go opposite ways — a refused require conjunct only weakens that component's normal form, which a proof survives, while a refused assume conjunct strengthens it, and with every assume gone it collapses to a bare G, the axiom "this component promises its guarantee unconditionally" that your file never stated. So such a component is left out of the premise set and its own obligation (4) is undecided. Neither direction is ever reported as a refinement.

Nothing here is about ordering or time. This is the propositional and numeric shape of contract refinement, not OCRA's temporal one, and every verdict line says so. The tool never says "the architecture satisfies its requirements", never says refined while an obligation is undecided, and never says refined when the antecedent of (3) or (4) is unsatisfiable.

A refinement obligation does not read the values in your file. It is a claim about every implementation the contracts admit, so examples/uav-power-budget.sysml refines whether its design point draws 607 W or 6 W. That is the difference between refine and verify, and it is why --free has no meaning here.

--via names the family of edges, and there are three of them. composition is the question above. derive and refine ask the same question of a requirement somebody wrote down from another requirement, and all runs every family in one pass with each row naming the one it came from.

A derivation is checked with the orientation your file actually stores. The two spellings store their ends the opposite way round, and this is the one place where guessing would not fail loudly — it would check the mirror obligations and report "refines" for a chain written the other way up:

• derive requirement D from R; puts R on the source end, so R is the parent and D is written down from it.
• refine requirement X by Y; puts Y on the source end, uniform with satisfy, so X is the parent and Y is the one doing the refining.

The two obligations, over that orientation. With nf(C) = ¬A ∨ G as before:

• A_R ⊨ ⋀ A_D — the derived set assumes no more than its parent. A child that assumes more applies in fewer situations than the parent's guarantee is claimed in, so discharging the children would leave that gap unproved.
• A_R ∧ ⋀ nf(C_D) ⊨ G_R — the children, in normal form, entail what the parent promised. Two children that each carry part of a budget conjoin to imply the whole of it; one of them alone does not.

$ npm run sysprose -- refine derived.sysml --via derive
derived.sysml: 1 not refined, 0 vacuous, 0 inconclusive, 0 refined — 1 derivation chain(s) over 2 contract(s)
  a derivation chain is checked with the orientation the mapper stores: `derive requirement D from R` makes R the parent, …
  DerivationStrongerAssumption::MassBudget via derive — not-refined
    verification/derivation-not-refinement
      assumes no more: DerivationStrongerAssumption::BodyMass  refuted [verification/derivation-not-refinement]
      witness: DerivationStrongerAssumption::Vehicle::speed = 11 (stored magnitudes)
$ echo $?
1

A derivation group names no part, and the report says so rather than borrowing one: a derive edge joins two requirements and states nothing about who satisfies either of them — so a --via derive run prints no γ census either, with or without a solver. Its failures file verification/derivation-not-refinement rather than verification/refinement-failed, because the fix is an edit to a requirement and not to an architecture.

An edge whose other end is not a requirement forms no chain, and is counted. derive requirement Child from rig; names a part, so there is no obligation over two contracts to check. The run says how many such edges it found rather than reporting "this model states no derive chain at all" about a file that plainly writes one.

A refused clause on a derived requirement is read by which half it came from. A dropped conjunct of its guarantee makes nf(C_D) weaker, and a weaker premise is implied by the real one — so the child stays in the premise set and a proof under it is still a proof. A dropped conjunct of its assume strengthens nf(C_D) into an axiom the file does not state, so that child is kept out, files its own undecided row, and the composition row over what is left is never published as a refutation: the very clause that was dropped may exclude the design point it found.

Source of truth: src/semantics/refinement.ts, refinementReport in src/api/verification.ts, and the L8 cases in test/campaign/verification.test.ts.

The tightest value the model admits

verify asks whether a requirement holds; bounds asks a different question with no verdict in it — how far can this quantity actually go, given what my model says? It is z3's optimiser (νZ) over the model's axioms.

Which clauses are axioms, and which are not. The axiom set is exactly what obligations files as axiom: feature values, bind equalities and assert constraint bodies. A require clause is not one of them — a requirement is what is being checked, not a fact about the design — and neither is an assume, which is the guard a requirement applies under. That is why the answer below is unbounded above on a file that plainly states a 25 kg limit:

$ npm run sysprose -- bounds uav.sysml --measure uav.mtow --free all
uav.sysml: 0 not established, 1 decided — `BoundsUav::AirVehicle::mtow` over 2 assertion(s)
  the axiom set: feature values, `bind` equalities and `assert constraint` bodies; `require` and `assume` clauses excluded, because a requirement is what is being checked, not a fact
  max  unbounded
    max `BoundsUav::AirVehicle::mtow`: unbounded above — over 2 assertion(s) — …
$ echo $?
0

The exclusion is repeated on every verdict line rather than once in a header, because a reader who scrolls to a row has been handed a claim they have to be able to check. --with-requirements folds those bodies in — each as the implication assume ⇒ require the shipped library says a requirement is — and says so on the line:

$ npm run sysprose -- bounds uav.sysml --measure uav.mtow --free all --with-requirements
  max `BoundsUav::AirVehicle::mtow` = 25 (coherent SI; the feature declares no unit) exactly (linear optimum, optimality established by z3's νZ) … PLUS the `require` bodies … (`--with-requirements`)
$ echo $?
0

The parenthesis is not noise. The bound is reported in the magnitude the model STORES, with the unit the feature declares beside it — payload is 6 [kg] (6 in coherent SI) — and mtow declares no unit literal at all (its value is the expression emptyMass + payload), so what it stores is coherent SI already and the line says which of the two a reader is holding. A quantity whose unit you want named on the row is one the file should declare a unit for.

--free decides what may move. With nothing released every value the file states is an axiom, so the bound is the value in the file. Release a feature and the bound ranges over it; --free all releases every value the file states and keeps every equation that says how a quantity is computed — the same rule consistency releases under, so the two commands cannot answer over different design spaces.

Exact, or honest about not being exact. Four answers, and they are not the same sentence:

The last one is verification/optimality-not-established, and it exits 2. It is deliberately not one of the two codes --allow-inconclusive lowers — and bounds does not offer that flag at all — because presenting a non-optimal bound as the optimum is the one sentence this command may never write.

A refused axiom is a missing axiom, and the row says so instead of a number. A relation a gate could not encode was not asserted, and dropping one widens the design space — so the bound over what is left is looser than the model's, never tighter. When such a refusal shares a symbol with what the objective can reach, the row is verification/not-evaluable at exit 2 rather than a bound: a file whose only ceiling on a quantity is a relation the encoder refused would otherwise read unbounded above. A refusal in an unrelated corner of the file cannot move the answer and is listed rather than acted on — the same reach test verify applies before it publishes a refutation.

The point z3 stopped at is re-read before the number is published. Every design point this lane prints goes back through the tool's own evaluator first (§5's witness gate), and bounds is the surface with the least redundancy behind it — its answer is a number the encoder produced. A point this tool cannot reproduce is verification/not-evaluable, never a bound.

bounds publishes its own exit-code contract, and it has no 1. Every other judging subcommand spends its 1 on a decided negative about the model. A bound is not one: 0 is every bound decided, 2 is anything undecided, and there is no 1 to misread.

Two optimisers, named so they are never read as one. bounds reports a bound z3 proved; the optimize function in src/semantics/solver.ts is a coordinate descent with a golden-section line search that returns a point it found and proves nothing. The report says which is which, and the L8 corpus pins the direction of the difference: the heuristic never beats the proved bound.

Source of truth: src/semantics/bounds.ts, boundsReport in src/api/verification.ts, and the L8 cases in test/campaign/verification.test.ts.

Which contract failures break the top requirement

refine asks whether the parts add up to the whole. fault-tree asks the same question from the other side: which combinations of contract failures would break it? A basic event is "sub-contract i not honoured", and a set of them is a cut set when the refinement obligation fails with those guarantees withdrawn. It is the same obligation (3) refine --via composition proves, over the same normal form and the same γ — asked again with parts of the premise set taken away.

A decomposition that refines can still have a single point of failure. That is the whole reason this is a separate command, and the shipped power-budget example is the demonstration: refine exits 0 on it, and

$ npm run sysprose -- fault-tree examples/uav-power-budget.sysml
examples/uav-power-budget.sysml: 1 with a single point of failure, 1 with cut sets, 0 with none up to the bound, 0 vacuous, 0 not enumerated — 1 tree(s) over 5 contract(s)
  a basic event is "sub-contract not honoured", and a set of them is a CUT SET when obligation (3) — the same one `refine --via composition` proves — fails with those guarantees withdrawn
  UAVPowerBudget::PowerBudget on `UAVPowerBudget::PowerSystem` — cut-sets
    4 basic event(s); 4 minimal cut set(s) up to order 2: {BatterySupply}, {ComputerDraw}, {PropulsionDraw}, {RadioDraw}. there is a single point of failure … 6 check(s), all decided …
    order bound 2, from the default
      order 1  {BatterySupply}
        witness: …BatteryPack::availablePower = 0, …
$ echo $?
1

Four single points of failure in a decomposition whose obligations are all proved. Each load's draw is bounded by its own guarantee and by nothing else, so withdrawing any one of them frees a term of the sum the pack has to cover. Redundancy is what changes that answer, and it shows up as an order-2 cut set: with two supplies bound to one bus, neither is a cut set alone and the pair is — {PrimaryOutput, BackupOutput} in test/fixtures/verification/models/fault-tree-redundant.sysml.

Minimal, bounded, and counted. Sets are enumerated by increasing order and every superset of a cut set is pruned rather than checked — withdrawing more guarantees cannot restore an obligation that already failed — so the list is minimal. The enumeration costs the sum of C(n,k) solver checks and the report prints the count. And the bound travels with the answer: "no cut set up to order 2 — higher orders not explored" is the whole sentence, never the first half of it.

"Minimal" is withheld when a smaller set went undecided. Pruning removes the supersets of sets shown to be cut sets; it cannot remove the supersets of one the solver did not answer about, because that smaller set may itself be the cut set. Those supersets are still checked and still listed — each is a real cut set, confirmed against a counterexample — but the row says minimality not established and the head sentence drops the word. And any undecided check makes the run exit 2, whatever else it found: the enumeration is incomplete, and an undecided order-1 check is exactly the state a "no single point of failure" sentence may never be written over. There is no --allow-inconclusive here to lower it.

--max-order N, and the same number written in the model. The order bound is the one part of this analysis that is an assumption — how many independent failures you consider credible at once — rather than something the contracts state. A carrier puts it where a reviewer sees it, and the flag overrides one:

requirement def MissionPower {
    @SysproseVerification::FaultHypothesis { attribute maxOrder = 2; }
    subject sys : Avionics;
    require constraint { sys.bus.voltage >= 20.0 [V] }
}

Both spellings of the cell are read — { maxOrder = 2; } and { attribute maxOrder = 2; }. A cell this tool cannot read as a whole number is never guessed at, because inventing a bound would put a number nobody wrote onto every absence the command prints; instead the run says the carrier is there and was not read, and enumerates to the default.

The report says which of the four the number came from — --max-order, the carrier, an unreadable carrier, or the default.

A vacuous contract set is reported as vacuous, never as "no cut set". If the sub-contracts, the connections and the top requirement's assumption cannot hold together, obligation (3) can never fail, so no fault set could ever be a cut set. Enumerating over that would print this command's most reassuring sentence about its least trustworthy model, so step (0) runs first and the row reads inconclusive: contract set vacuous at exit 2. Nothing lowers it.

Nothing is claimed about a check that was not decided. "No single point of failure" is a statement about every order-1 check having been decided; a check that timed out is not a component shown to be harmless. One undecided order-1 check and the report says so instead — and there is no --allow-inconclusive here to forgive it.

The two safety lanes stay apart. A state machine passed as --element is measured, not enumerated: the command counts what a behavioural fault tree would need — failure-mode flags to inject and #exceptional states to aim at — prints the two numbers, and exits 2 under the row that names a state machine whose failure modes this command found none of:

$ npm run sysprose -- fault-tree examples/uav-isr.sysml --element FlightModes
examples/uav-isr.sysml: `UAVSurveillanceSystem::FlightModes` is a state machine whose failure modes this command found none of: 0 failure-mode flag(s), 0 `#exceptional` state(s) — the behavioural lane has no fault variable to inject here
  nothing was enumerated and no absence is claimed: this command injects failures into the CONTRACTS a `satisfy` attaches to the parts of a system, and a state machine carries none — its failure modes would be flags its guards read, which no lane in this build injects, so this run is exit 2
  this is contract-level fault-tree analysis over the refinement obligations, not a behavioural safety analysis: it says which contract failures break the top requirement, and nothing about ordering, time, rates or probabilities
  model sha256:…
$ echo $?
2

An empty cut-set list over a machine would read as a behaviour with no failure mode, which is the loudest false statement this command could make — so no list is printed, and no absence is claimed. Under --json the payload also carries a census over the whole file, faultTree.behaviouralLane (machines, machinesWithExceptionalStates, machinesWithFailureModeFlags, hazardsUnreachableFromTheContractLane): the measurement a behavioural fault tree is held behind, and it reads 0 on every shipped example and every verification fixture. A failure-mode flag is an attribute tagged with a FailureMode metadata definition; the shipped vocabulary does not declare one yet, so only a model that declares its own is counted — and a machine that carries one is answered with the other tail of the same row, whose failure modes this command found and does not inject: still exit 2, still no list. The command measures exactly the machines reach walks: name a state inside a machine (--element FlightModes::standby) and it is refused with the machine named — name the machine — rather than measured over the state's own descendants; name a state def whose states are joined only by successions and it is refused as owning no transition, the same answer reach gives over it, rather than counted as a machine the census did not. And every report says what it is: contract-level fault-tree analysis over the refinement obligations — nothing about ordering, time, rates or probabilities, and not a behavioural safety analysis.

Source of truth: src/semantics/fault-tree.ts, faultTreeReport in src/api/verification.ts, and the L8 cases in test/campaign/verification.test.ts.

The verdict in the file, and whether it still holds

A verdict that lives only in a terminal scrollback is a verdict nobody can review. evidence-attach writes the records of a verify run into the model as annotations on the requirements they are about, evidence-status says whether they still hold, and evidence-detach takes them back off. All three report; none of them judges. The judging was done once, by verify, and a verdict is not re-decided by being written down.

$ npm run sysprose -- verify examples/uav-isr.sysml --engine literal --record evidence.json
  …
  2 evidence record(s) written to evidence.json
$ npm run sysprose -- evidence-attach examples/uav-isr.sysml --from evidence.json --out examples/uav-isr.sysml
sysprose evidence-attach: 2 record(s) attached to 2 element(s), 0 already present, 0 skipped; 2 verdict facet(s) written
Wrote examples/uav-isr.sysml

The input file is never written unless you name it. The updated model goes to stdout; --out <path> writes it, and --out pointing back at the file you read is how you edit in place. Without it the command says, on stderr, that your file was not changed and prints the flag that would change it. A tool that rewrote somebody's source by default would be a tool you could not run to see what it would do.

What a record is, in the file. Each one is a @SysproseVerification::Evidence { … } annotation — the notation's §7.27 annotating form over the metadata definition the SysproseVerification package ships. That package is not written into your file: evidence-attach adds carriers and nothing else, so a model that carries evidence and neither declares nor imports SysproseVerification has an annotation whose type resolves nowhere, and no check in this tool objects to it. Paste the package (it is quoted in full above) into the file, or import it, if you want the file to stand on its own. Five readable scalars come first (claim, verdict, engine, tool, modelGraph) and the whole record follows as JSON in record. The scalars are a rendering; record is the datum, and it is the only half this tool reads back, because two readable copies of one number can disagree and the one that must win is the one a consumer parses.

The verdict facet is derived, never accepted. Beside the carrier, evidence-attach writes metadata RequirementMetadata { attribute verdict = …; } — and it writes it from the record's claim, by one rule: pass for proved, fail for refuted, inconclusive for everything else. A --engine literal record claims holds-at-values, so it writes inconclusive. There is no path through this command by which a point evaluation writes pass. A record file is JSON somebody can edit, and a record states a verdict of its own beside its claim; that field is never copied through. If the two disagree — "claim": "holds-at-values" beside "verdict": "pass" — the whole file is refused, naming the record and what its claim actually implies, rather than half-trusted.

A requirement with several obligations carries the worst of them. One run produces one record per clause, and the file holds one verdict facet: it is fail if any live obligation is refuted, inconclusive if any is undecided, and pass only when every one of them was proved. Re-recording one obligation supersedes that obligation and nothing else — the pair clause + obligationDigest is what identifies one — so a requirement whose second clause was just discharged still reads fail while its first clause stands refuted, and the answer does not change if you swap the two clauses in the source.

A reading in a context or an instance is one of those obligations. satisfy LoadReq by p1; makes verify read LoadReq in p1 as well as on its own row, and verify --record writes that reading as a sysprose-evidence/2 record naming the requirement and the reading ("instance": { "requirement": "H::LoadReq", "reading": "H::p1" }). The facet is the worst over the readings too, and so is the verdict of a verification case that verifies the requirement: a requirement refuted in one part makes the case fail in verify's report, with or without --case (which records the readings with the own row), and is written fail by the record and by the case, on every attach. A requirement usage typed by the definition (requirement massR : LoadReq; satisfy massR by p1;) owns none of the definition's clauses, so the clause is read once, on LoadReq's own row, and read again at each satisfier; the reading at p1 is written for the requirement the satisfy names, massR ("requirement": "H::massR", and the record's obligation.requirement reads H::massR in H::p1), and verify massR by VC judges it. The case over the definition keeps it too: verify LoadReq by VC is still judged over the reading satisfy massR by p1 refutes in LoadReq's clause, and evidence-attach writes that case's verdict the same way. The definition's own verdict facet is the worst over its carriers and over the readings moved onto the usages typed by it, so it stays fail, an attach of the same record again reports no verdict change, and evidence-status and evidence-detach read it the same way. A case that verifies both LoadReq and massR counts that reading once. verify's own report still prints the row as H::LoadReq in H::p1, and a satisfy LoadReq by p1 that names the definition (or a requirement definition that specializes it) keeps the record on LoadReq; only a requirement usage takes it. A record from an older build names a reading only as <requirement> in <reading>. evidence-attach refuses the whole --from file, with exit 2 and nothing written, when a sysprose-evidence/2 record has an empty instance.reading or instance.requirement (the schema requires at least one character). A record that passes the schema is held to the same checks in both versions before anything is written: the requirement must be a requirement of this model, the model must read it in that reading, and (for a sysprose-evidence/2 record) the facet and obligation.requirement must say the same thing; a record that fails one is skipped with the half that does not match named. A record written by an earlier build for such a usage, LoadReq in p1 in either version, is skipped, and the reason names the usage that carries the reading now (the model files LoadReq in p1 on H::massR); running verify --record again writes it there.

Evidence accumulates. A second run appends a carrier; nothing is overwritten and no earlier verdict is deleted, so the file keeps the history of what was claimed and when it changed. A record that is already there byte for byte is counted as already present rather than written twice, which is what makes the command safe to run again. Every verdict the run moved is printed on stderr with both claims — and a fail replaced by a pass is named as what it is.

Two refusals, and a third. A model that did not load cleanly is refused outright: writing a degraded model back would replace your source with what the tool managed to salvage. (That refusal is why evidence-attach and evidence-detach have no exit 1: the reporting contract's 1 means "the report is of what parsed", and these two never report over half a model. They exit 0 or 2.) A record naming an element under a declaration the parser could not read is refused with the same sentence the facet editors show, because the serializer re-emits that declaration verbatim and anything written underneath it is gone on the next save — at the command line you will meet the degraded refusal first, since a faulted declaration only exists after a parse error. And a record aimed at the bundled standard library is refused: a carrier written there is never saved with your file. Every one of these is raised before the first carrier is written, so a refused run leaves your model exactly as it found it.

Then edit one literal.

$ npm run sysprose -- evidence-status examples/uav-isr.sysml
examples/uav-isr.sysml: 2 stale, 0 current, 0 unrecorded — model sha256:196f8a85…
  a record is shown with the claim it was made under — `holds-at-values` is never shown as `proved`
  UAVSurveillanceSystem::MassRequirement  stale
      stale — recorded at sha256:4b48f0ed…, the model is now sha256:196f8a85…; 3 element(s)
      in this requirement's slice must be re-read, and the digest is over the whole model so
      this tool cannot say which of them moved. Re-run `verify --record`.
      slice: UAVSurveillanceSystem::uav, UAVSurveillanceSystem::EnduranceRequirement, UAVSurveillanceSystem::AirVehicle

You do not have to run evidence-status to be told: npm run check raises validation/stale-evidence as a warning on the ordinary path, because the next person to open the file runs the checker, not the verifier. A stale verdict only the verification lane could see would be a verdict that survived every edit made by anyone who did not know the lane existed.

An SMT proof is not re-run for an edit it could not have read. A record written by --engine smt carries what its proof stood on: the axiom rows the clause's read-closure reaches (its footprint), a digest over the whole axiom set the consistency check ran over, a digest over the requirement's own premises, and a digest over the clause itself — each of them over the relation AND the scale it is read at, so relabelling a feature from [Wh] to [J] is an edit the scope sees even though the expression tree is unchanged. npm run check compares those rather than the whole model, so an edit that moves none of them raises nothing. Measured on examples/uav-isr.sysml: of nineteen single edits, eight — a declaration with no value, a doc line, a state, an action, a part definition, a string facet, a renamed connection, a prose requirement — move the whole-model digest and nothing either proof reads, and the two records stay put. The other eleven are reported, and the sentence says which part moved:

budget.sysml:125:5: warning validation/stale-evidence  Evidence on UAVPowerBudget::ComputerDraw
was recorded over sha256:95da2919…; this model is sha256:aa014dc3…. The claim `proved` no longer
stands: stale — this proof's premises changed, so the satisfiable-assumptions check that
separated `proved` from `vacuous` was not the one that ran. Re-read this requirement's slice —
UAVPowerBudget::PowerSystem::flightComputer, UAVPowerBudget::PowerSystem::propulsion,
UAVPowerBudget::FlightController — then re-run `verify --record` and `evidence-attach`. The
comparison is scoped to what this proof stood on, so an edit elsewhere in the file is not
reported here.

The parts are different ways a proof dies, and most of them do not look like an edit to the proof. An axiom in the footprint changing what it says is the obvious one. A NEW axiom entering the footprint is the second — the proof never mentioned it, and it is now part of the context the negation is unsatisfiable under (or is not). The third is the axiom SET: proved means the negation is unsatisfiable under a satisfiable axiom set, and that second conjunct is a property of the whole file — one added assert can contradict another one and void every proof in the model, including proofs whose footprint never touches either. The fourth is the premises: the check that separates proved from vacuous is a check on them, and it is in none of the first three — on examples/uav-power-budget.sysml, raising one assume constraint { fc.supplyVoltage >= 20.0 [V] } to >= 200.0 [V] moves no axiom, no footprint member and no symbol, and takes the obligation from proved to vacuous. The fifth is the clause itself: the first four are all about a proof's CONTEXT, and tightening uav.mtow <= 25.0 [kg] to <= 24.0 [kg] moves none of them.

Only three of them can change the answer, and the report says which. The axiom-set digest is taken over every axiom row in the file, and the footprint is a subset of those same rows digested the same way — so a footprint digest cannot move without the axiom-set digest moving too, and a member cannot enter or leave the read-closure unless an axiom, a premise or the clause already moved. What the footprint parts buy is the SENTENCE: they are how a finding can name the axiom you have to re-read rather than telling you something in the file changed. The narrowing itself comes from the edits that touch no axiom at all — eight of the nineteen on examples/uav-isr.sysml.

What is NOT recorded, and why. The solver's unsat core — the axioms z3 named as a sufficient reason, which verify --why prints — is not written into a record. Its membership was measured to move with how warm the solver's context is: the same model, one seed, six labels from a fresh process and five from a worker that had already run many checks. A record is promised byte-identical across two runs over an unchanged file, and a digest over a set chosen that way could not honour it. The footprint is the encoder's own relevance walk over the MODEL, is a function of the model alone, and is what the core is a subset of.

A record with no scope keeps the whole-model comparison, and says so in the same words it always did: --engine literal writes no scope (a point evaluation has no axiom set and no non-vacuity step to speak of), and neither does a record written by a build older than this field.

evidence-status answers the other question, on purpose. It reports whether a record was taken over THIS model — a fact about the file, which any edit moves — while the checker reports whether the edit could have reached the proof. A file where evidence-status says stale and npm run check says nothing is a file where something moved and no proof in it could have read what moved. npm run check -- <file> --json publishes the reading per record, inside the report: {scoped, matched, wholeModelMoved, footprintContentMoved, footprintMembershipMoved, axiomSetMoved, premisesMoved, obligationMoved} and the sentence. matched is false where a record carries a scope but this model states no obligation to recompute it against — the clause was deleted, or two anonymous clauses share one qualified name — in which case the comparison falls back to the whole model and the sentence says so. A scope that did not move reads current within this proof's scope, never the bare word: the claim is scoped and the words are part of it. Bare current appears only on a record that carries no scope, where it means what it has always meant — the model still hashes to what the record names.

What the digest can and cannot say. It is taken over the whole user model — every element you wrote, canonicalised so that reformatting, reordering and reparsing leave it alone, and so that what a verification run itself wrote is excluded (or every record would be stale the instant it was attached). So the comparison knows that something moved and can never know what: it never saw the earlier model, only its hash. Naming the requirement's slice is the honest half of the answer — these are the declarations to re-read — and every stale line says the other half out loud rather than implying an attribution it cannot make. It catches model edits; it does not catch a hand-edited record, and nothing here pretends otherwise.

Two things this command calls out by name. A verdict facet with no record behind it is verification/claimed-without-evidence — info, not a defect: a verdict reached by inspection is ordinary requirements management, and the row says only that this tool has nothing standing behind it. A verdict = "pass" over a record whose claim is not proved is verification/verdict-overstates-evidence, and that one is an error: both artefacts are the tool's own, they contradict each other, and the contradiction is in the direction that overstates. evidence-attach cannot produce that state; a file in it was written by hand.

A claim is never upgraded on display. A record claiming holds-at-values is shown as holds-at-values in the terminal and in the Requirements table's Evidence column, never as proved; a stale record is never counted as discharged. The Verdict column beside it shows the facet, whose three values cannot tell a point evaluation from a proof — which is exactly why the claim word is on the row.

evidence-detach takes the facets with the carriers. A verdict left behind by a detach is a claim with nothing behind it, which is the very state verification/claimed-without-evidence exists to report — so the command that removes the evidence removes the verdict it wrote, and leaves a facet you wrote by hand alone.

What another tool makes of this is not something this page will claim. The verdict facet is an unbound tag holding a quoted string, where the standard has an enumeration on a different metaclass; a conforming SysML v2 reader is entitled to treat that line as an untyped annotation and ignore it. The round trip that matters is Sysprose → someone else's tool, and it has not been measured. Until it has, no claim is made about it.

Source of truth: src/api/evidence.ts, the stale-evidence rule in src/validation/rules.ts, and test/fixtures/agent-authoring/L8-evidence-stale.

Which states a machine can reach, and the choice a simulation hides

reach walks a state machine's configuration graph. It uses the same step relation the simulator uses — the one runStateMachine runs — with one difference that is the whole point: where the simulator fires the FIRST enabled transition, this walks every enabled one. That is how it can say something a simulation cannot.

$ npm run sysprose -- reach examples/uav-isr.sysml
examples/uav-isr.sysml: 1 state machine(s), 1 walked to exhaustion; 4 configuration(s) explored
  a bounded walk of what the interpreter would do — every figure below holds under the bounds printed beside it
  UAVSurveillanceSystem::FlightModes [StateDefinition]
    4 configuration(s) explored, depth 3 — exhaustive under {maxConfigs 10000, maxDepth 200, maxCompletion 64, alphabet no named trigger, store seeded from declared literal values — a guard over an attribute with no declared value is read as false}
    4 of 4 state(s) reachable; 5 of 5 transition(s) fired, 0 dead
    livelock     {manual, autonomous} — the chase goes round 2 configuration(s) on trigger-less transitions and the run ends where the budget stops it (no trigger is named); entered in 1 step(s) from standby
    choice       UAVSurveillanceSystem::FlightModes::autonomous: 2 enabled as completion transitions (no trigger); the simulator takes autonomous -> manual, never autonomous -> failsafe
  semantic profile (the reading every figure above holds under):
    ...
  verification/completion-livelock  `UAVSurveillanceSystem::FlightModes`: completion livelock — the interpreter's chase goes round {manual, autonomous} without coming to rest: …
  verification/nondeterministic-choice  `…::autonomous`: 2 transitions are enabled at once …

The finding on this machine is not the count. FlightModes declares four states and five transitions and every one of the five is trigger-less, so the machine runs on completion alone — and autonomous has two of them enabled at once. Declaration order decides which one a simulation takes, so failsafe is never entered in simulation while the model plainly admits it. That is verification/nondeterministic-choice, and it is the row worth reading. Note what the line does NOT contain: a trigger name. The machine names none, and a report that printed one would have invented it.

Every figure carries the reading it holds under. The semantic profile printed under each machine names six things every published formalisation of state machines disagrees about — run-to-completion (chasing is bounded at 64 steps), priority (innermost substate first), history (shallow, by parent map), regions (the interpreter concatenates them; a parallel machine is not explored here at all), deferred events (none — there is no event pool), and time (discrete after(n); the walk offers each after(n) label as an event rather than advancing a clock). A verdict about a machine is a verdict under a reading of those six, and one that does not say which reading is one you cannot check.

A bound stops the walk, and then the absence claims stop with it. Two sentences this command will only say after seeing the whole graph: "this state is unreachable" and "this transition is dead". Both are claims of ABSENCE, and a walk that was cut off cannot make one. So when --max-configs is spent, both lists come back empty — suppressed, not shortened — with verification/bound-exhausted saying so:

$ npm run sysprose -- reach examples/uav-isr.sysml --max-configs 2
…
    partial under {maxConfigs 2, …} — the configuration bound was reached; the unreachable and dead lists are lower bounds and are NOT reported as findings

A check-behaviour search can also come back short with no bound hit at all: the walk finished, but never offered a trigger the machine names, so a run that takes it was not searched. That is verification/trigger-not-offered, not bound-exhausted: the row names the triggers, exits 2, and says that no flag decides it, so --max-configs is not advised. The walk offers the whole alphabet wherever it can decide that the interpreter takes its next event, so a row under this code is a gap in the engine and not in the model.

The 64-step chase budget is not a bound: the walk follows it. The interpreter fires trigger-less transitions for at most 64 steps after each event, and then takes the next event wherever the chase stopped — so on a machine whose trigger-less transitions form a cycle (a ⇄ b, with a accept e then c), every run spends the budget and e still takes it to c. The walk does the same: where a chase reaches the budget with a trigger-less transition still due, it offers the machine's events right there, exactly as the simulator takes the next one. So c above is reachable and a -> c is not dead, and on a chain of trigger-less transitions longer than 64 the states past the 64th are unreachable — no run gets there — under the maxCompletion 64 the line prints. A transition still due where a chase stops is enabled there, so it is not dead and that state is not a no way out; but a set this walk could call inescapable is not claimed over such a machine, and the trap line says why.

A machine that names no trigger is walked as it states itself even when its trigger-less transitions cycle, like FlightModes above: a chase stopped there is followed by nothing, so the walk reaches the same states either way. What the budget does decide there is where a run ends — every run is the one chase from the opening, stopped after 64 steps wherever it is — so the two answers that are about where runs end are checked against those stopping points: check-behaviour's recoverable (below) and the every run? guaranteed line. Each is withheld where the run the budget stops would read differently.

A cycle the chase never leaves is a finding of its own. On FlightModes the simulator's chase goes standby -> manual -> autonomous -> manual -> … for its whole 64-step budget on every run — autonomous -> manual is declared first, so the chase never takes autonomous -> failsafe — and the machine never comes to rest. reach reports that as verification/completion-livelock, a warning, once per cycle of states: the livelock line above names the states the chase goes round, in order, and the shortest way in, and the finding says where declaration order decides (autonomous here, the choice row below it). It is decided over configurations and over the transition the interpreter fires at each one, not over states: a loop whose guard or whose store takes the chase out of it on its own is not reported, and a cycle that only another branch of a choice could leave is. Cycles that go round the same states under different values of the store are one row, and the row says how many it stands for. The way in is the simulator's own run wherever the walk holds one — here standby -> manual, the step simulate takes. Where only the walk's way in reaches the cycle, through a branch the simulator never takes, the line ends on a run of the walk, not of the simulator and the finding names the state where the two part: run simulate and it may never get there. On a machine that names a trigger only an event moves such a run on; FlightModes names none, so the run ends where the budget stops it, and the line says that instead. A trigger on one transition of the cycle, or a guard that is false where the machine should wait, is the fix. A guard on a trigger-less way out of the cycle that the walk could not evaluate withholds the row — a withheld line says so in its place — and check-behaviour files the same warning beside its verdicts on the machine it checks, without changing a verdict or the exit code. It files the published rows only: read a withheld one in reach. On --json every machine row carries livelocks and livelocksWithheld (empty on a machine with none, the second with the clause that withheld each), and totals.livelocks counts the published rows. A row names its states, the transitions the chase fires, the choices where declaration order keeps it on the cycle, its way in (entry, steps), whose run that way in is (entryBy: simulator, or walk with branchAt the state where it parts from the simulator) and how many store or history variants it stands for (cycles).

The other direction is deliberately loose, in one place: the walk offers each after(n) label as a named event rather than advancing a clock, so a state behind a dwell is treated as reachable. An over-approximation like that can only shrink an absence claim, never invent one. It is loose there and nowhere else — the walk branches on the declaration-order tie-break, taking every transition enabled at the innermost active level where a simulation takes the first, and it does not cross the priority rule. A transition an inner state always beats fires in no run at all, so a configuration reached through one is a configuration no run enters, and verification/deadlock and verification/nondeterministic-choice reported there would be invented rather than found.

A guard it could not evaluate is not a guard that is false. A bound is not the only thing that stops an absence claim. Ten lines that parse clean, with no diagnostics of their own:

part def Ctrl {
    attribute mode : Integer;          // no value, anywhere
    state def Modes {
        state idle;
        state hazard;
        transition idle if mode == 3 then hazard;
    }
}

The model does not say mode != 3; it says nothing about mode, so mode == 3 evaluates to nothing at all. A walk cannot fire that transition — it has to pick something, and it picks not firing — but "the walk did not fire it" is not "no run ever could". So reach withholds the two walk-wise absence lists for that machine (unreachable and dead), prints undetermined under {…} where it would otherwise print exhaustive, and raises verification/guard-undetermined naming the guard and the names nothing valued. A no-way-out row is withheld per CONFIGURATION rather than per machine: it goes only where the undecided guard is an edge out of the configuration the row is about (read over its whole active stack), and each row that goes leaves a withheld line in its place, so a short list is never read as a clean one. A sink elsewhere in the same machine that no guard was consulted about keeps its row and its finding. Here idle's only way out is the undecided guard, so its row is the one withheld:

    1 configuration(s) explored, depth 0 — undetermined under {maxConfigs 10000, …} — 1 guard(s) the walk could not evaluate; the unreachable and dead lists are WITHHELD and are NOT reported as findings, as is the no-way-out row for 1 configuration(s) whose only ways out are guards this walk could not decide
    undecided    idle -> hazard — guard `mode == 3`: no value for mode
    withheld     GuardProbe::Ctrl::Modes::idle — no enabled way out was found and none is reported: a guard the walk consulted decided nothing, so an edge the model states is absent from the relation
    the unreachable and dead lists are WITHHELD, and the no-way-out rows marked `withheld` above: a guard this walk could not evaluate is not a guard that is false
  verification/guard-undetermined  the guard `mode == 3` on transition `idle -> hazard` could not be evaluated — no value is in scope for `mode`. …

Write attribute mode : Integer = 3; (or = 4) and the walk decides it — and with = 4 you get the unreachable state and the dead transition back, because then the guard really is false.

A hidden-choice row is an existential claim — two transitions were enabled at once in a configuration the walk reached — so a bound never withholds one. A withheld edge is more delicate, and the narrow statement is the true one: removing a candidate beside a choice can only shrink it, but removing one inside it moves which level of the active stack the choice is read at, and that can invent a row. So a choice is withheld exactly where an undetermined guard sits strictly inside it, and reported everywhere else.

check-behaviour shares the gate: a property no bad prefix violated over a graph missing an edge nothing decided is inconclusive (exit 2), never pass and never vacuous, and its row is the same verification/guard-undetermined.

A set of configurations nothing leaves. Everything above is about where a run can get to. reach also asks the other half of the question — which configurations, once entered, no run ever leaves — and reports each such set as verification/unrecoverable-mode. A set nothing leaves is a bottom strongly-connected component of the walk's successor relation, and three kinds of them are exempted rather than reported: an ending (final states and done nodes are where the machine is meant to stop), a single configuration with no successor at all (that is already verification/deadlock, and one fact gets one row), and the component holding the opening configuration — which is the machine's own reachable core, not somewhere it can be trapped from. That last exemption is why FlightModes above prints nothing here: its four states form one component and standby is in it. A machine that is trapped looks like this:

$ npm run sysprose -- reach test/fixtures/verification/models/trap-probe.sysml
test/fixtures/verification/models/trap-probe.sysml: 1 state machine(s), 1 walked to exhaustion; 5 configuration(s) explored
  a bounded walk of what the interpreter would do — every figure below holds under the bounds printed beside it
  TrapProbe::Probe::Modes [StateDefinition]
    5 configuration(s) explored, depth 4 — exhaustive under {maxConfigs 10000, maxDepth 200, maxCompletion 64, alphabet no named trigger, store seeded from declared literal values — a guard over an attribute with no declared value is read as false}
    5 of 5 state(s) reachable; 6 of 6 transition(s) fired, 0 dead
    trap         {failsafe, failsafeHold} — 2 configuration(s) nothing leaves; entered in 3 step(s) from standby
    livelock     {alpha, beta} — the chase goes round 2 configuration(s) on trigger-less transitions and the run ends where the budget stops it (no trigger is named); entered in 1 step(s) from standby
    livelock     {failsafe, failsafeHold} — the chase goes round 2 configuration(s) on trigger-less transitions and the run ends where the budget stops it (no trigger is named); entered in 3 step(s) from standby, on a run of the walk, not of the simulator
    choice       TrapProbe::Probe::Modes::beta: 2 enabled as completion transitions (no trigger); the simulator takes beta -> alpha, never beta -> failsafe
  semantic profile (the reading every figure above holds under):
    ...
  verification/unrecoverable-mode  trap — 2 configuration(s) form a set nothing leaves: {failsafe, failsafeHold}. Entered in 3 step(s) from `standby`. every claim above is about this MACHINE's semantics — …
  verification/completion-livelock  `TrapProbe::Probe::Modes`: completion livelock — the interpreter's chase goes round {alpha, beta} without coming to rest: …
  verification/completion-livelock  `TrapProbe::Probe::Modes`: completion livelock — the interpreter's chase goes round {failsafe, failsafeHold} without coming to rest: …
  verification/nondeterministic-choice  `TrapProbe::Probe::Modes::beta`: 2 transitions are enabled at once …

Read the row for what it says and for what it does not. {failsafe, failsafeHold} names the states of every configuration in the set — the union of their active stacks, so a composite state is named as itself and never only by the leaf inside it — and entered in 3 step(s) from standby is the shortest way in. It does NOT say the machine cannot recover: escaping the set might need a trigger the real environment never offers, and this tool has no carrier for what an environment supplies. It does not say livelock — that the chase goes round {failsafe, failsafeHold} without coming to rest is the separate verification/completion-livelock row beside it, a claim about the chase rather than about the set, whose line ends on a run of the walk, not of the simulator for the reason the next sentence gives — and it does not say the machine is free of anything. And the sentence beside the finding is there because beta is a choice point: the walk explored both branches, simulate takes beta -> alpha every time, and a reader who tries to reproduce the trap with the simulator may never see it.

This is the first row reach publishes under the stricter gate, and it is emptied — never shortened — whenever the walk is not exact. The unreachable and dead lists are claims that can only shrink as edges are added, so a walk that offers more edges than the machine grants cannot invent one. No trap runs the other way: it gets easier to say as edges are added, and a missing edge invents a trap. So the trap list is published only where the walk finished inside every bound, met no construct this engine refuses, offers no after(n) dwell, names no trigger, consulted no guard it could not evaluate, and did not follow the interpreter through a chase its budget stops with a trigger-less transition still due — there a run rests where the budget leaves it, which is not an edge of the machine. On the latch machine (transition locked accept unlatch then nominal;) the walk supplies unlatch wherever it can decide that the interpreter takes its next event, so whether locked is inescapable is a question about the environment, and the report says so in place of the list:

    inconclusive: this machine names triggers this walk offers wherever it can decide that the interpreter takes its next event, so an escape it found may be one the environment never supplies and no absence of an escape is claimed; the environment offered every trigger this machine names wherever the walk could decide that the interpreter takes its next event (no completion transition due, or the chase budget spent), …

The same refusal, with its own sentence, prints for a dwell transition, for a guard the walk could not evaluate, and for a chase the budget stops (inconclusive: the interpreter’s chase budget stops a run of this machine …); a bound or an unsupported construct prints nothing extra, because the lines above already say every list is short. On --json the machine row carries trapCensus — how many components the walk had, how many nothing leaves, how many were exempted as endings, deadlocks or the core, and which clause refused the answer if one did — and, where the gate held and no trap was found, a sentence that names what was exempted rather than a bare all-clear. That sentence is never a text row.

Both spellings of an edge are one edge. Between two states the notation offers transition idle then active; and first active then done;, and a machine may mix them in one body:

state def Modes {
    state idle;
    state active;
    state done;
    transition idle then active;
    first active then done;
}

The walk follows both. It did not always: the step relation held TransitionUsage alone, so the succession was in no configuration and in no census, and the report called itself exhaustive while printing 1 of 1 transition(s) fired, done unreachable and active a state with no way out — two absence claims about an edge nothing had followed. A succession between two states carries neither trigger nor payload, so it is read as what it is: a completion transition. What stays outside is an edge with a PAYLOAD — a SuccessionFlow, or a succession carrying an item, which this tool already reads as the same thing — because the walk models no payload; it refuses the machine rather than walking a graph it knows is short of an edge.

Every edge under a machine is walked, or refused by name. That is a census, published on --json under census, and it is the durable half of the fix above. Four readers found four different ways the relation the walk retains differed from the machine somebody wrote, so the question is now asked the other way round: each edge-bearing element under the machine lands in exactly one bucket — walked (in the relation, leaving a node some configuration's stack can hold), opening (read by the machine's opening and never fired), refused (an unsupported construct names it), off-stack (neither end is a node the walk can stand on — a do action's own flow is under the machine and is not an edge of it), not-a-step (the element sequences nothing: state idle : Base; is a typing between two elements, connect a to b; a connection, and no run ever carries the control token along either) — and anything left over is unaccounted, which is a test failure and a refusal: verification/behaviour-unsupported-construct with the construct edge-not-walked, no absence list, and no exhaustive. The row names the edge and says why the relation does not hold it, so a spelling that sequences behaviour and that this engine cannot walk can no longer shrink a claim in silence.

Which nodes a configuration's stack can hold is computed, not guessed from a metaclass: the machine's states, plus everything the relation can land the walk on from one. So the edges leaving a decide node between two states are walked and counted, and an edge leaving the machine ROOT — which the walk never stands on, because it opens at the root's initial substate — is neither counted nor reported dead.

One thing the fix deliberately did not move: a state definition that owns no TransitionUsage at all is still not one of this tool's machines, and reach says so — this file declares no element that owns a transition, so there is no configuration graph to walk. That is an answer about what was looked for, not an absence claim about a graph: nothing is called unreachable and nothing is called exhaustive.

A state def written inside another state machine is a machine of its own, not a region of the one it sits in: reach walks the nested definition separately, so its states decide themselves. They are neither reported unreachable nor counted in the outer machine's totals, and the outer walk stops at the nested definition's boundary. A simulator run of the outer machine takes its states at the same boundary, so it starts where the walk opens: at the outer machine's own initial substate (where its own initial node leads, else its first declared state), also when the nested definition is written before it. The Simulation tab offers the outer machine's own events only, not the nested definition's, and lists a nested definition as a machine where no machine holds it: a state def whose only content is a nested definition is no machine, so the tab runs the nested one; a nested definition inside a machine is not listed beside it. A nested state def that owns no TransitionUsage is walked by nothing, and each of its states then reads not walked in the app rather than being called unreachable under a machine that does not contain it.

A transition that crosses that boundary — written in the outer machine and leading into one of the nested definition's states or to the definition itself, written in the nested definition and leading out of it, or written in one top-level machine and leading into another's state — has no meaning either walk defines, because each machine steps only by its own transitions. Walked anyway, the outer machine entered the inner state and found no way out of it, while the nested definition's walk followed its edge out to a state the outer walk had just called unreachable. So reach and check-behaviour alike refuse both machines the transition joins — the one it is written in, and the one whose state it names from outside: verification/behaviour-unsupported-construct with the construct machine-boundary, naming the transition — no absence list, no exhaustive, and every property about either machine inconclusive. Keep each transition inside the machine whose states it joins, or write the nested definition as a composite state (state Inner { … }) to make its states part of the outer machine. A specialisation or a typed usage that adds a transition over the states it inherits (state def Derived :> Base { transition … }, exhibit state m : Modes { transition … }) crosses the same way, and both machines are refused with the inheritance named: no walk here puts the two together, so write the machine you mean out whole, its states and every transition it steps by, in one definition. A simulator run still takes such a transition — into the far state, where it then stays, since none of that state's own transitions are the run's — which is what the Simulation tab shows, not a verdict.

check-behaviour --element Outer checks Outer itself, also when a state def written inside it makes it hold a second machine: a reference that is a machine names that machine. What Outer is checked against stops where its walk does: a property carried by the nested definition, or by one of its states, belongs to that definition and is counted and checked there only — and where that definition owns no transition, so is no machine and is walked by nothing, the property is counted on Outer and reported there as inconclusive, … — not checked, verification/behaviour-unsupported-construct, naming the definition: checked by nothing, and said so rather than dropped — and a property of Outer's that names one of the nested definition's states or transitions is refused as verification/unknown-atom, as one naming another machine's state is. A reference that only contains machines (the package, say) is still refused with the machines it holds, and a state is refused with the machine it belongs to — for a state of the nested definition, that definition, not the outer machine whose text holds it. In the app, the pick row such a refusal lists in the Checks tab (the machine's qualified name and its property count) selects that machine, and the next Run checks it.

What it may never say. Not "verified", not "deadlock-free", not "proved". verification/deadlock names a state with no enabled way out that is neither marked final nor a done node — a reading of one machine under one alphabet, never a statement that the system deadlocks. A machine that ends at done has ended, and is not reported. And reach reports rather than judges: a state nothing reaches is a fact about a machine, not a violated requirement, so it exits 0 with its findings in the report (--json publishes them under reach). A file that declares no machine at all exits 0 too and says so — nothing was misused and nothing failed to load. Exit 2 is for the command line: a --max-configs that is not a bound, or an --element that names something holding no machine.

In the app, the marks. Run Reachability on the State view and each state that answers a question carries one badge, in this precedence: unreachable (the published unreachable list), not decided (an unreached state of a machine whose lists were withheld — the SUPPRESSED or not-explored line says why), not walked (a state under no machine the walk covered), withheld (the leaf of a withheld no-way-out row), no way out (a published deadlock), trap (a member of a published trap), and choice (a published choice). A status panel in the canvas's top-left corner (behaviour-marks) says which, and the legend gains a Marks section (legend-marks) listing the words present. Every mark names a row in the Checks tab except not decided and not walked. A completion livelock is a Checks-tab row and a livelock line of the report, and puts no badge on the states it names.

In the app, the edge marks. A dead transition and a guard the walk could not decide are marked on the transition itself, not only as a Checks-tab row: the edge is drawn with a coloured, dashed stroke and a dead or undecided badge beside its label. They follow the same rule as the state marks — painted only while a current reach result is stored, on the State view, with the marks not hidden and no witness open — and the legend lists the edge words present (legend-edge-marks). A dead transition is one the walk proved never fires; an undecided guard is one it could not evaluate, so the edge may in truth be taken and this page is not claiming either way.

In the app, the witness. A fail or covered row turns its witness steps in the Checks tab into buttons (checks-witness-step, with Prev / Next / Close). A click paints the walk's run on the State view — the step's leaf, its stack, and the leaves already passed — and hides the reachability marks and the simulation glow until it is closed. The walk obeys run-to-completion and the chase budget, so every witness it found is one a run admits and every one is drawn; none stays plain text. Running the check again closes an open witness as the run begins, since the Checks tab hides the result, and with it the stepper, while the run lasts; Cancel keeps the earlier result, not the witness.

Source of truth: src/semantics/mc/config.ts (the step relation the interpreter and the walk share), src/semantics/mc/explore.ts and src/semantics/mc/profile.ts.

Whether a safety property holds on every configuration, and whether a situation can be reached

reach reports on a machine. check-behaviour judges a claim you made about one: a property pattern — a shape with holes in it — filled with atoms that name things the walk can observe. It walks the same configuration graph reach walks, looking for a bad prefix: a finite run that breaks the property. Finding one is a fail, printed as that run. Finding none over a graph the walk saw whole is a pass. One pattern, cover, asks the opposite question — can some run get here? — and the same search answers it the other way round: a run found is covered, printed as that run; none found over a graph seen whole is not covered. Everything else is said out loud.

$ npm run sysprose -- check-behaviour examples/uav-isr.sysml --element FlightModes \
    --pattern 'pattern=absence, scope=globally, p=state failsafe'
examples/uav-isr.sysml: UAVSurveillanceSystem::FlightModes — 1 property: 0 pass, 1 fail, 0 vacuous, 0 inconclusive, 0 covered, 0 not covered
  a pass is a claim about every configuration this walk reached, under the bounds printed beside it, and about nothing outside them; a covered is a claim that ONE run this walk saw reaches the situation named, and not covered that none it saw whole does: pass, fail, vacuous, inconclusive, covered, not covered are the six words this command reaches
  liveness (`existence`, `response`) is NOT decided here: a bad-prefix search finds no bad prefix for either, so both report inconclusive
  FAIL         `state failsafe` never holds, over the whole run
    from --pattern
    fail — witness trace of 3 step(s) …
    verification/refuted
    every run? potential — some run avoids it: the cycle manual → autonomous → manual never enters `failsafe` — every claim above is about this MACHINE's semantics — the walk explores both branches of a nondeterministic choice; the simulator takes the first declared one, so a run this verdict quantifies over may be a run `simulate` never produces
    3 product state(s) explored — exhaustive under {maxConfigs 10000, maxDepth 200, maxCompletion 64, alphabet no named trigger, store seeded from declared literal values — a guard over an attribute with no declared value is read as false} …
    witness — a run this semantics admits:
       0  start → UAVSurveillanceSystem::FlightModes::standby
       1  completion standby -> manual → UAVSurveillanceSystem::FlightModes::manual
       2  completion manual -> autonomous → UAVSurveillanceSystem::FlightModes::autonomous
       3  completion autonomous -> failsafe → UAVSurveillanceSystem::FlightModes::failsafe  [holds p]
  semantic profile (the reading every verdict above holds under):
    ...

This is reach's finding from the other side. reach says two completion transitions are enabled at autonomous and the simulator takes the first, so failsafe is never entered in simulation. Here that same fact refutes a property: the model admits a run that reaches failsafe, and the witness is that run, step by step. A tool that only simulated would have told you the opposite.

And the every run? line says whether that witness is one run or every run. potential means some run avoids the violation, and the line names it — here the cycle manual → autonomous → manual, which never enters failsafe. On a machine that names no trigger every run is one chase, so the cycle or the stopping point named is one such a run reaches inside the 64-step budget without the violation, and where none is, the line names the run the budget stops (the run the chase budget stops in `p64` never enters `v` ). guaranteed means every maximal run of the machine reaches it. Both are read off the same graph the witness was, and both are withheld as not decided, with the reason, whenever that graph is not the machine's: a walk that stopped at a bound, a machine that names a trigger the walk offers wherever it can decide that the interpreter takes its next event, a dwell the walk takes without advancing a clock, a guard over something the walk could not read, a chase the walk follows the interpreter's budget through — and, where the machine names no trigger, a guaranteed that a run the budget stops before it violates would contradict (not decided: the interpreter’s chase budget stops a run of this machine …) — and three refusals of the property itself, a stateful pattern or scope, a fires/trigger atom, an expression that needs the store. The tail of the line is there because this machine has a choice point: the walk explored both branches at autonomous, and the run the sentence names is one the simulator's declaration-order tie-break never takes. In --json the same answer is the row's modality field — value, sentence, failedClause, avoiding — and it changes no count and no exit code.

But if reaching failsafe is what you WANTED, that fail is the wrong colour. absence is red on the design that can get there and green on the one that cannot — the intent "can this design ever reach the situation I care about?" was, until cover, only expressible upside down. cover is the same search read the right way round:

$ npm run sysprose -- check-behaviour model.sysml --element Modes \
    --pattern 'pattern=cover, scope=globally, p=state failsafe'
model.sysml: CoverProbe::Reachable::Modes — 1 property: 0 pass, 0 fail, 0 vacuous, 0 inconclusive, 1 covered, 0 not covered
  …
  COVERED      `state failsafe` holds on some run, over the whole run
    from --pattern
    covered — witness trace of 2 step(s), a run this semantics admits: `state failsafe` holds on some run, over the whole run — the environment offered every trigger this machine names wherever the walk could decide that the interpreter takes its next event (no completion transition due, or the chase budget spent), so a witness that consumes `abort` is a claim about that environment and not about one that withholds it
    2 product state(s) explored — exhaustive under {maxConfigs 10000, maxDepth 200, maxCompletion 64, alphabet abort, store seeded from declared literal values — a guard over an attribute with no declared value is read as false} — the count beside it is the product states seen up to the witness, not the size of the product space
    witness — a run this semantics admits:
       0  start → CoverProbe::Reachable::Modes::idle
       1  completion idle -> armed → CoverProbe::Reachable::Modes::armed
       2  on `abort` armed -> failsafe on `abort` → CoverProbe::Reachable::Modes::failsafe  [holds p]

Exit 0, a witness, and the environment sentence beside it: the walk offers every trigger the machine names wherever it can decide that the interpreter takes its next event — at a configuration where no completion transition is due, or where the 64-step chase budget is spent with one still due — so a run that consumed abort is a claim about that environment and not about one that never sends it. Where a completion transition is due and the budget is not spent, the interpreter chases it before it takes any event, and so does the walk: no trigger is offered there. Nor where nothing is due but a trigger-less transition whose guard the walk could not evaluate: the interpreter reads that guard as false and takes its next event, while the walk cannot tell which it does and offers no trigger at all — it holds fewer runs there, not more, and verification/guard-undetermined withholds every absence on that machine. On the sealed twin — the same machine with the abort edge removed — the row reads NOT-COVERED, not covered under {…} — over 2 configuration(s), an info line verification/not-covered, and exit 2: a decided absence, a missing behaviour, and not a violated requirement. Nothing was refuted, so the 1 is not spent — unless you say the behaviour is required:

$ npm run sysprose -- check-behaviour model.sysml --element Modes \
    --pattern 'pattern=cover, scope=globally, p=state failsafe' --cover-required
…
  NOT-COVERED  `state failsafe` holds on some run, over the whole run
  …
  --cover-required: every not-covered row above is also an error below and spends the 1; the claim word is the same with the flag and without it
  error verification/cover-required  …
  info verification/not-covered  …

Exit 1 now — and the row still says NOT-COVERED, never FAIL, and the verification/not-covered line is still there under the added error. The flag moves the exit code and nothing else. Two more things the row tells you rather than leaving you to infer: --max-configs can hide a witness and can never invent one, so a covered found under a bound still stands (the bounds line says partial under {…}) while a not covered needs the whole graph, exactly as a pass does — below the bound the sealed twin is inconclusive: bound exhausted — the not-covered claim is not made. And a witness that crossed an after(n) dwell is a run the walk admits and the interpreter may never take, because this walk advances no clock; the row keeps the claim and re-words the warrant — covered — witness trace of 1 step(s), a run this WALK admits: step 1 fires after(10)(idle -> B onafter(10)), a dwell this engine offers as a named event without advancing a clock, so the interpreter may never take this trace — so the bare "a run this semantics admits" is never printed over a trace the semantics does not admit. On a machine where the walk explored a choice the simulator never takes, every covered also carries the simulator sentence: the claim is about the machine's semantics, and simulate may never produce the run.

And one question neither absence nor cover can ask: from every configuration the machine can be in, can it get back? absence says whether a run ever enters failsafe; cover says whether some run does; neither says whether the design can return from wherever it ends up. That is a branching-time question — AG EF p, from every reachable configuration, some continuation reaches p — and a bad-prefix search cannot answer it in either direction: no finite run breaks it, so the search would find nothing and print this command's strongest verdict for free. recovery is answered by a different algorithm on the same walk: the configurations that hold the state you name are collected, and the walk's own successor relation is followed backwards from them. Every configuration the backward pass reaches can get there; every one it does not is named.

$ npm run sysprose -- check-behaviour test/fixtures/verification/models/trap-probe.sysml \
    --element TrapProbe::Probe::Modes --pattern 'pattern=recovery, scope=globally, p=state standby'
test/fixtures/verification/models/trap-probe.sysml: TrapProbe::Probe::Modes — 1 property: 0 pass, 1 fail, 0 vacuous, 0 inconclusive, 0 covered, 0 not covered
  …
  FAIL         `state standby` is reachable from every reachable configuration, over the whole run
    from --pattern
    not recoverable: 4 configuration(s) cannot reach `state standby`: {alpha, beta, failsafe, failsafeHold}; the nearest is entered in 1 step(s) from `standby`. Of these, 2 form a set nothing leaves — `reach` reports them as `verification/unrecoverable-mode`.
    verification/refuted
    5 configuration(s) explored — exhaustive under {maxConfigs 10000, maxDepth 200, maxCompletion 64, alphabet no named trigger, store seeded from declared literal values — a guard over an attribute with no declared value is read as false}
  semantic profile (the reading every verdict above holds under):
    ...
  error verification/refuted  `TrapProbe::Probe::Modes`: `state standby` is reachable from every reachable configuration, over the whole run — not recoverable: 4 configuration(s) cannot reach `state standby`: …
  warning verification/completion-livelock  `TrapProbe::Probe::Modes`: completion livelock — the interpreter's chase goes round {alpha, beta} without coming to rest: …
  warning verification/completion-livelock  `TrapProbe::Probe::Modes`: completion livelock — the interpreter's chase goes round {failsafe, failsafeHold} without coming to rest: …

Read the two numbers for the two questions they answer. Four configurations cannot get back to standby — nothing in this machine returns there, so every configuration but the opening is on the list — and the row names them by the state each rests in and says how soon the first is entered. Two of those four are the set reach reports as a trap: {failsafe, failsafeHold} is the part nothing leaves at all, while alpha and beta cycle between themselves with a way out that leads only deeper. The trap row and this row are the same machine seen from two sides, and neither number is ever printed under the other's question. The two warnings after the error are not about this property: they are the machine's completion livelocks, filed after every property's finding in reach's words, and they move no count — the exit code stays 1. Note what the row is not: it is a fail — an assertion you wrote that the design does not meet, verification/refuted, exit 1 — but there is no witness trace under it, because a set is not a run; the count beside the bounds line is the machine's own configurations, not product states, because no product search ran. On the flagship machine the same property is withheld — inconclusive, exit 2 — although every configuration of FlightModes reaches standby along the transitions it states: none of them names a trigger, so a run is the one chase from standby, and the 64-step budget stops it in standby or in autonomous, from where the run gets back to nothing. On examples/views-tour.sysml, whose standby ⇄ flying every run is stopped in standby, the row reads PASS with recoverable: state standby is reachable from every reachable configuration, exit 0.

What the row refuses, and why it refuses both directions. recoverable is a claim that gets easier to make as edges are added, so it is withheld — never qualified — wherever the walk's relation is not the machine's: a bound the walk hit, a named trigger the walk offers wherever it can decide that the interpreter takes its next event, with no carrier for whether an environment would send it (the latch fixture: locked → nominal exists only because the walk supplies unlatch, and the draft of this feature printed recoverable about it), an after(n) dwell the walk takes without advancing a clock, a run the interpreter's chase budget stops away from p — the walk follows the budget there, or, on a machine that names no trigger, the relation follows the chase past where the run ends (the flagship above). That last refusal is filed under its own code, verification/recovery-budget-withheld (exit 2): the walk finished and no construct is outside the fragment, so it is neither a bound nor an unsupported construct, and no flag decides it — raising --max-configs is no advice for it. not recoverable gets easier as edges are removed, which is the opposite direction — and a guard over something the walk could not decide removes exactly one: on the trapguard fixture the escape degradedA if resetOk then nominal is absent from the relation because nothing valued resetOk, and a row that gated only the positive half would print not recoverable: 2 configuration(s) cannot reach state nominal at exit 1 about a design that states the way back. So one gate holds both halves, the row is inconclusive naming the clause, and nothing is shortened. Two more refusals are about the property rather than the walk: p must be a state or a node atom — a trigger or fires atom holds on a step and not at a configuration, and an expression reads a store this walk does not retain, so none of the three gives a target set to reverse from, and reading one anyway would earn a refutation from a tool limitation — and the scope must be globally. And the two atom kinds are read exactly as absence reads them: state X is X on the active stack, node X is X the active leaf, so on a composite state recovery p = state degraded holds from everywhere while recovery p = node degraded is a refutation with an empty target set — the same split absence shows on the same file, and the pattern never says vacuous for it: a state nothing reaches is a decided no, not an unopened antecedent.

The catalogue, and the half of it this engine will not decide.

A safety property is broken by a finite run, so a search for one either finds it or, having seen the whole graph, has not. A guarantee — cover is Manna–Pnueli's ◇β — is confirmed by a finite run, so the same search either finds one and prints it, or, having seen the whole graph, has not; it is the one pattern whose negative answer is a behaviour the design does not admit rather than a requirement it violates, which is why it has two words of its own and why not covered exits 2 by default. A branching-time property — recovery is AG EF p — is not a property of any run, so the search decides nothing about it; it is answered by reverse reachability over the same walk, in both directions, and only over a walk whose relation is the machine's. A liveness property is broken only by an infinite run that never delivers what it promised, and a bad-prefix search finds no bad prefix for one on any graph. Reporting "nothing found, so it holds" would print this command's strongest verdict for exactly the two properties it cannot decide, so both come back inconclusive: liveness not checked in-process — until a lasso search lands and a fairness assumption is named.

bounded-existence counts occurrences, not configurations. state Outer holds at every observation from the moment the machine enters Outer until it leaves — state X reads the whole active stack — so a composite entered once and never left has occurred once, however many steps happen inside it. That is Dwyer's reading (his at-most-n formula counts maximal intervals), and counting configurations instead would refute "at most once" about a machine that enters the state exactly once.

The five scopes, each naming where the property has to hold: globally, before R, after Q, between Q and R, after Q until R. The last two differ on one run and it matters: between speaks only about segments that actually close, so a Q never followed by an R says nothing at all (vacuous), while after … until is a weak until and the same run is a violation. Both are written over Q & !R, so an observation where the opening and closing atoms hold together opens no segment at all: there is nothing between a Q and an R that are the same observation. On a hierarchical machine that is not a corner case — a composite state and the substate its entry cascades into hold together at every observation.

The five atoms: state X (X is on the active stack), node N (N is the active leaf, which is how you name a done node), trigger t (the event offered on this step), fires T (a named transition fired), or an expression — read by the same parser your guards are read with, over the same store.

A property lives in the model, as §7.27 metadata. --pattern is for trying one out; the carrier is how a claim stays with the machine it is about, and it is checked beside whatever you type, never instead of it:

state def FlightModes {
    @SysproseVerification::PropertyPattern {
        attribute pattern = "absence";
        attribute scope = "globally";
        attribute p = "state failsafe";
    }
    state standby;
    …
}

One attribute per field, so the phrase-to-atom trace survives a save: a reader can see which pattern, over which scope, filled by which atom, without re-parsing a sentence.

What it refuses to say, and how each refusal reads.

A bound can hide a violation and can never invent one, which is why those rows are not symmetric — and why covered sits with fail on the witness side of the line and not covered with pass on the whole-graph side. --max-configs N that stops the walk turns a would-be pass into inconclusive; a violation found inside the same bound is still a violation. A vacuity is on the pass side of that line: "no run opens the scope" is a claim of absence, and a walk that stopped at a bound has not established one — so a partial walk that never reached the antecedent is inconclusive, not vacuous, and --strict-vacuity files nothing against the model for it.

Every witness is replayed through the interpreter before a row stands on it. A fail or covered row prints a run, and that run is driven through runStateMachine — the simulator itself — with the witness's events before the row is published: the interpreter must fire the witness's transitions in its order and enter the states it enters. The one choice the replay makes the witness's way is the declaration-order tie-break, where the walk explores both branches and the simulator takes the first declared one (the simulator sentence beside such a row says so); run-to-completion, the 64-step chase budget and the priority rule are the interpreter's own. A row whose witness does not replay is inconclusive under verification/witness-not-replayed, exit 2, with the step where the two parted — a defect in this engine, not in your model, and a row no flag lowers.

A property nobody could read is never dropped. A pattern outside the catalogue, a scope outside its five, a missing field — and a carrier attribute that is not a property field at all, which is the one a typo reaches: scope is the only field with a default, so a carrier written scpoe = "after" read without it would silently become a different property and be decided as if somebody had written it. Every one of them is verification/malformed-property ⇒ exit 2. So is a --pattern whose value expanded to nothing, for the same reason: dropping it would report on the carriers alone and look like a clean sweep.

An atom that names nothing is never read as false. absence of state failsafe would otherwise PASS the moment somebody misspelt failsafe — the loudest way this whole lane could print a green verdict that means nothing. A name the machine does not have is verification/unknown-atom, the row lists what the machine does offer, and the run exits 2.

Vacuity is surfaced and no flag launders it. A property whose antecedent never holds is true of your machine for a reason that has nothing to do with your machine. It is vacuous ⇒ exit 2, with --strict-vacuity and without it; the flag raises the row from a line to verification/vacuous-property, an error, and changes nothing else — including the exit code.

Source of truth: src/semantics/mc/patterns.ts (the catalogue, the monitor and the bad-prefix search), src/semantics/mc/atoms.ts (the five atom spellings), and src/semantics/mc/explore.ts for the walk they both stand on.

The keywords a file carries, including somebody else's

A #keyword in front of a declaration is the notation's own extension point: SysML v2 §7.27.4 makes the short name of a metadata def writable as a tag, and §7.27.1 says such a definition "simply acts as a user-defined syntactic tag on the annotated element". Sysprose reads those tags, keeps them exactly as you wrote them through a save, and — because a model annotated for another tool is a model you should still be able to open here — reads a handful of other people's spellings too.

contracts --keywords is the inventory. It says one of four things per keyword, and it changes nothing:

$ npm run sysprose -- contracts vocabulary.sysml --keywords
  keywords: 3 use(s) of 3 distinct keyword(s) — an inventory; nothing here changes an obligation
    sysprose vocabulary: #exceptional on P::failsafe → SysproseVerification::ExceptionalOutcome
    third-party spelling: #Exception read as `SysproseVerification::exceptional` on P::abort — not SysML v2, not a Sysprose keyword
    names nothing: #precondtion on P::launch resolves to no metadata definition in scope
  verification/foreign-keyword  ...
  verification/keyword-names-nothing  ...

Those two verification/* rows are information and they come from nowhere but this command — except verification/foreign-keyword, which obligations --from-keywords also raises, once per row a keyword filed. npm run check does not judge a keyword: a misspelt one costs you nothing but the tag you thought you had written.

"Names nothing" is not a bug — it is the notation. A keyword names a metadata def in scope, so it resolves inside the package that declares the definition, inside one that imports it, or when you write it qualified. The one vocabulary Sysprose ships is a package you paste into your own file:

package SysproseVerification {
    doc /* Four definitions SysML v2 does not express, carried over metadata definitions (SysML v2 7.27.1, 7.27.4). #exceptional says an outcome is a failure rather than an equally valid result. Evidence carries what a verification run showed, as an annotation on the requirement it is about. PropertyPattern carries a behavioural property — a pattern, a scope and the atoms that fill them — as an annotation on the machine it is about. FaultHypothesis carries the order bound a cut-set enumeration is run to, which is an assumption about how many failures are credible at once rather than something the contracts state. All four are Sysprose extensions, not standard vocabulary. */
    metadata def <exceptional> ExceptionalOutcome;
    metadata def Evidence;
    metadata def PropertyPattern;
    metadata def FaultHypothesis;
}

#exceptional says an outcome is a failure rather than an equally valid result — the one annotation in this whole lane that SysML v2 has no way to express, which is why it is shipped rather than borrowed. It is a Sysprose extension and this guide will not pretend otherwise. Two keywords you might expect are deliberately absent: #precondition and #postcondition, because assume constraint, require constraint and a case objective { … } already say both, three ways and two ways respectively.

Evidence in that same package is deliberately not a keyword. It ships with no short name, so there is nothing to write after a #. A keyword is a tag — it says one thing by being present — and an evidence record has a body: a claim, an engine, a tool version and a model digest. So it is written in §7.27's annotating form, @SysproseVerification::Evidence { attribute … = "…"; }, by evidence-attach, and a bare #Evidence that carried no record and claimed to be one is a spelling this package does not allow.

PropertyPattern is not a keyword either, and for the same reason. A behavioural property has a body — a pattern name, a scope, and the atoms that fill them — so it is written in the annotating form too, @SysproseVerification::PropertyPattern { attribute pattern = "absence"; … }, one attribute per field. check-behaviour reads it; nothing writes it, because a property is a claim you make about your machine and not one this tool invents for you.

The statement kinds are the exception, and the inventory says so. #prose, #prompt and #'requirement' are read from the spelling — that is what lets a tag work whether or not SysproseStatements is in your file — so the inventory names them as this tool's own and never as a keyword that names nothing:

    sysprose vocabulary: #prose on P::Why — read from the spelling; declare or import SysproseStatements to bind it

A tag this tool acted on is not a tag it failed to find.

Somebody else's spelling. Four third-party spellings are recognised, and each of them prints where it came from wherever it is used:

That last column is the important one. Without --from-keywords, a file full of another tool's vocabulary produces exactly the worklist the same file without it produces: the keywords are read, listed and kept, and they file nothing. With the flag, a #precondition on a plain constraint files a premise and a #postcondition files something to show — and every such row prints from #precondition — a third-party spelling read as … on its own line, so no premise ever appears without the word that put it there. A clause role you wrote yourself always wins: a keyword never reclassifies require constraint, and no keyword can ever add an axiom.

Source of truth: src/semantics/keywords.ts (the reader, the resolver and the alias table), src/semantics/verification-vocabulary.ts (the shipped package), and docs/CONFORMANCE.md §7 for the assessment behind which keyword ships.

Scripting it

Inside the browser, the SDK is on window.sysml (the API Console tab is a console over it) and diagram scoping is on window.sysprose.diagram. Outside it, every one of these engines is an importable function — checkText, modelMetrics, requirementSatisfaction, whereUsed, analysisReport, buildGrid, buildDSM, buildPlan — with no DOM anywhere in them.

An edit made through window.sysml — create, update, delete, reparent, a commit(fn) batch — is an edit like any other: the Explorer and Properties follow at once, and Problems, the diagram and the Text view with the next refresh. The model then reads unsaved: New, Open ▾ and Import ask before dropping it, and an attached Google Drive file shows unsaved changes. The one exception is text typed in the Text view and not applied, which an SDK edit never replaces (§5). An SDK edit is not an Undo step of its own. Nor does it put an element of yours inside the standard library: a create or a reparent with an owner there puts the element at the top level of the model, as the Explorer does (§5), and the strip says so.

Source of truth: src/ui/store.ts:3076-3258 (runValidation, solveParametric: the four buttons), 1985-2065 (afterSdkEdit: an SDK edit), src/api/analytics.ts:2408-2415 (feasible), src/ui/App.tsx:46-94 (window.sysml), scripts/sysprose.ts, scripts/sysml-check.ts.

7. Three kinds of statement

A model holds three quite different sorts of statement, and until you say which is which, the tool has to guess from the shape you wrote them in. A requirement binds: something has to satisfy it, and the coverage figure is about it. An explanation written for a person binds nothing. Guidance written for an agent binds nothing either — but it is addressed to a machine, so a machine ought to be able to find it.

The vocabulary is this project's own; the way you write it is not. The published SysML v2 specification has no enumeration of statement kinds. The one requirement-related kind it has — RequirementConstraintKind = assumption | requirement — classifies a membership inside a requirement body (assume / require), not an element, and the shipped library classifies requirements by subclassification instead (FunctionalRequirementCheck, PerformanceRequirementCheck, …). Nothing there separates an explanation from a rule, and nothing names guidance meant for a machine reader. What is borrowed is the mechanism: §7.27.1 of that specification says a metadata usage exists to add tool-specific information to a model, and that a metadata usage whose definition has no nested features of its own "simply acts as a user-defined syntactic tag on the annotated element"; §7.27.4 defines the user-defined keyword — #name written in front of a declaration — and the standard library ships exactly that shape for its own <derive> tag. So a kind here is a keyword over a metadata definition: no notation is invented, no grammar is changed, and a file carrying one is an ordinary file of the notation that any reader of it can still read.

Writing one

The keyword goes in front of the declaration:

#prose part note {
    doc /* Written for the reader. Nothing has to satisfy it. */
}

Three keywords, one of them awkward: #prose, #prompt and #'requirement'. The last is quoted because requirement is a hard keyword of the notation, and the notation's own escape for a name that collides with a keyword is the quoted form. #requirement does not parse.

Those keywords name three metadata definitions, and nothing in this tool binds a keyword to a definition — metadata is unvalidated here — so a tag works whether or not the definitions are in your file, and a misspelt #prosee is silently no kind at all rather than an error. If you want them declared, this is the package, and it is the text the tool itself ships:

package SysproseStatements {
    doc /* Statement kinds are a Sysprose extension, carried as user-defined keywords over metadata definitions (SysML v2 7.27.1, 7.27.4). Writing #'requirement', #prose or #prompt in front of a declaration says what the statement is for. */
    metadata def <'requirement'> RequirementStatement;
    metadata def <prose> ProseStatement;
    metadata def <prompt> PromptStatement;
}

Most statements need no keyword. An element with no tag still has a kind wherever its metaclass settles the question: a requirement reads as a requirement, a doc and a comment read as prose, and everything else — a part, a package, an action — has no kind at all, which is a different answer from having the default one. You write a keyword for the cases the shape gets wrong: the paragraph of commentary written as a requirement because that is where it belongs in the tree, and the guidance written for an agent.

Where a keyword cannot go. Prefix metadata belongs to a declaration, so connect a to b;, perform x;, a transition, an enumeration literal, a doc and a comment have nowhere to put one. The tool refuses rather than accepting a tag that would vanish on the next save: the Kind selector is absent on those elements and the writer throws. A doc and a comment still read as prose — they simply cannot be told to be anything else. The other way a kind can be invisible is the longer metadata form: @ProseStatement about p1; parses and round-trips, but it is not read as a kind, because reading it means resolving about against scope and this tool does not do that yet.

In the app the kind is Properties → Kind (prop-statement-kind), offered on every element that can carry one — not only on requirements, since guidance is most useful on a definition or a package. The blank entry is a real state, "no keyword is written here", and it says what the element reads as without one.

What it changes

Naming a kind is only worth doing if something acts on it. These do — and the last of them is the one that deliberately does not.

• Coverage counts requirements only. An explanation written in requirement shape used to enter the divisor and sit there with nothing satisfying it — nothing is supposed to satisfy an explanation — so a fully covered model read below 100% with a gap nobody could close. Tagged statements leave the divisor and are counted, beside the library and re-derived exclusions.
• The requirement rules skip them. requirement-subject asks what a requirement constrains, which is a fair question for a rule and a meaningless one for a paragraph, so it passes over prose and prompts. constraint-violation exempts only what you explicitly tagged: a plain constraint c { … } has no statement kind, and it is still checked exactly as it was.
• The Requirements view keeps the row and labels it in its Kind column, rather than hiding it — the one editable grid in the app is not the place a prose statement becomes uneditable.
• The terminal says which rows the ratio left out, instead of stating a figure the reader cannot reconcile with the rows above it.
• An untagged requirement is unaffected. The kind falls back to the metaclass, so every model written before any of this is counted and checked the way it always was.

Written out, all three kinds in one small model:

package Brakes {
    part def Vehicle;
    part vehicle : Vehicle;

    requirement <R1> stoppingDistance {
        doc /* The vehicle shall stop within 40 m from 100 km/h on dry asphalt. */
        subject v : Vehicle;
    }

    #prose requirement <N1> whyFortyMetres {
        doc /* Forty metres is the figure the customer specification quotes, repeated here so a reader need not open it. */
    }

    #prompt requirement <P1> beforeChangingTheFigure {
        doc /* Before changing a braking figure, re-run the deceleration analysis and record its verdict on R1. */
    }

    satisfy stoppingDistance by vehicle;
}

and what the report makes of it:

$ npm run sysprose -- requirements brakes.sysml
brakes.sysml: 1 of 1 requirement(s) satisfied (100%)
  [x] 1  stoppingDistance (R1) — satisfied by vehicle
  [-] 2  whyFortyMetres (N1) — prose: an explanation for the reader, not counted
  [-] 3  beforeChangingTheFigure (P1) — prompt: guidance for an agent, not counted
  24 bundled library requirement(s) and 0 re-derived copy/copies are not counted
  2 statement(s) tagged prose or prompt are not requirements and are not counted

Three statements, one ratio, and nothing hidden: [-] is a row that binds nothing, the last line says how many rows that was, and --kind requirement, --kind prose or --kind prompt narrows the listing to one of them. The filter deliberately does not move the headline ratio — coverage is a fact about the model, not about what you asked to see.

Writing a prompt

A prompt is the kind this tool is unusually placed to have. An agent driving the model can collect the guidance that applies to whatever it is working on, which is only worth writing if it is worth writing once: guidance repeated onto every part that needs it is guidance that rots.

So write it where it reaches. Asking what applies to an element walks two edge families out from it — what it is (its types) and where it sits (its owners) — transitively, and reports the prompts hanging on each scope and on that scope's direct children:

package Propulsion {
    #prompt part packageGuidance {
        doc /* Parts in this package follow the fuel-system conventions in DOC-114. */
    }

    part def Engine {
        #prompt part engineGuidance {
            doc /* Give an engine its fuel and exhaust ports before connecting it to anything. */
        }
    }

    part engine : Engine;
}

$ npm run sysprose -- prompts propulsion.sysml --element engine
propulsion.sysml: Propulsion::engine — 2 prompt(s) apply
  1  type   Propulsion::Engine::engineGuidance via Propulsion::Engine
      Give an engine its fuel and exhaust ports before connecting it to anything.
  1  owner  Propulsion::packageGuidance via Propulsion
      Parts in this package follow the fuel-system conventions in DOC-114.
  nearest first; guidance reaches an element from what it is, where it sits, and where what it is sits
  0 library element(s) dropped from the walk; 0 re-derived element(s) crossed but not reported; 0 declared type(s) this walk cannot follow

Neither prompt is written on engine, and both apply to it. What to know about that walk before you write one:

• Nearest first, by hop count, and at equal distance what the element is comes before where it sits — a type is more specific about it than an owner. Each prompt is reported once, at the nearest place it was found, so you can read down the list and stop.
• Direct children only, per scope. Guidance nested two levels down was written about the thing that owns it, and collecting whole subtrees would make every package-level question return the file.
• Owners of types count too. A part typed by a definition from another package is handed that package's guidance, because you used a definition from there. It is the same rule taken to its conclusion, and it means owner in that listing is not only your own containment chain.
• The bundled library is dropped at every hop and the count is printed. One unfiltered hop through a library type would turn the question into a walk of tens of thousands of elements. The tool's re-derived copies are the other way round: walked through so a walk can reach the definition behind a copy, and never reported.
• A type the walk cannot follow is counted, as the third figure on that line. An attribute typed by something outside ScalarValues — attribute mtow : ISQ::MassValue — keeps its type as text and gets no typing edge, so this walk cannot go down it. Zero there means nothing was hidden from you; a number means guidance may hang off a type this answer never reached.
• The words come from the doc body you write under the tagged element (or from a comment addressed to it). A prompt with a tag and no words says so on its own line rather than printing a blank one.

--json gives the same thing structurally — each prompt with its text, attachedTo, via and distance — which is the shape an agent should read. The question has no control in the app: Properties writes a kind, and nothing there collects what applies to a selection.

Two limits worth knowing. A kind classifies an element, not each sentence inside it: a doc body cannot be tagged separately from the requirement that owns it. And requirements --kind prompt lists only prompts written in requirement shape — the population of that report is what a requirements table holds — so a #prompt on a part or a package is found by prompts --element, not there.

Source of truth: src/semantics/statement-kind.ts (the vocabulary, the keyword, what can carry one), src/api/analytics.ts (promptsFor, and the nonNormativeExcluded figure in requirementSatisfaction), src/validation/rules.ts:562-579, 974-997 (the two rules that ask), scripts/sysprose.ts (requirements --kind, prompts), test/unit/semantics.statement-kind.test.ts.

8. What is kept, and what is not

Nothing here leaves your browser unless you sign in to Google Drive (§8.1) — then exactly the file you save goes to your own Google Drive, and nothing else. Nothing here is saved for you automatically.

Save takes no name and shows no confirmation. It writes over the current project name — and, with a Google Drive file attached that has unsaved changes, saves to that file too (which may first ask the strip's rewrite question, or meet a conflict). Save — the button, or Ctrl/⌘ + S from anywhere in the app, a field included (Appendix B) — stores the model, so text typed in the Text view and not yet applied is applied first, as Apply text → model does, and the save holds what is on screen, still under the current project name. Two kinds of typed text are kept back instead: the model is saved as it stands, the Text view still reads modified — not yet applied, and, when no Google Drive file is attached, the strip under the toolbar says so.

• A text with a syntax error. The parser's best guess at it is not what you see. The strip says Saved in this browser without the text typed in the Text view: it has a syntax error at line N. Fix it, then save again. — the line of the first error, which neither Problems nor the strip under the editor lists for a text not applied. An attached Drive file gets the text as typed (§8.1).
• Any typed text, in a collaboration room. Applying it replaces the room's model for everyone in it, and an edit a peer made after you began typing is not in your text: one Save would erase it. Apply text → model still does that when you choose to; Save does not, and the strip says Saved in this browser without the text typed in the Text view: in a collaboration room, Save does not replace the room's model with it.

The next save that holds the text takes the note down; × hides it.

Replacing a model with unsaved work asks first. New, Open ▾, Import, switching to a branch in the Versions tab and a merge there that resolves (it loads the merged model) each put another model in place of this one; joining a collaboration room lets the room's model change or replace it. When the model has work no save holds, the strip under the toolbar asks first — <project> has unsaved changes — with Save and continue (the project saved in this browser, text typed in the Text view applied first, then the command), Discard and continue (after New, Open ▾, Import or a branch switch, one Undo still brings the model back; before a room join it reads Join without saving) and Keep editing. Unsaved means that the Text view's text — typed and not yet applied, or not — differs from the text the model had when it was last saved, in this browser, to Google Drive or as a commit in the Versions tab, or opened: a project from Open ▾, a ?model= link, a Drive file, the branch the Versions tab loaded. New counts as saved, and so does the model the app starts with, so a first visit that touched nothing is never asked; Undo back to the saved model reads saved again. An import is not a save. A box moved by hand changes no text, so it is not asked about. A merge that meets conflicts (manual) loads nothing, and asks nothing. Save and continue is disabled while text typed in the Text view has a syntax error — this browser keeps models, not text: fix it, or discard it. A command given while the browser is still storing a Save waits for it; if the browser refuses the save (its storage full, or blocked for the site), the command waits, and the question says so. With a Google Drive file attached, the question is about that file's unsaved changes instead (§8.1). Closing or reloading the tab asks nothing about work unsaved in this browser, and the Versions tab's commits go with the tab; only an attached Drive file's unsaved changes raise the browser's question. Press Save before you leave.

If you want the model out of the browser, use Export ▾: SysML text, model JSON, OMG-API-shaped JSON, the diagram as SVG or PNG, or an FMI 3.0 FMU / modelDescription.xml for the selected block. The SysML text is the model's text — what the Text view shows when it reads in sync with model: your packages, without the standard library the app merges in, so Import opens it as the same model and the CLI reads it as it is. Text typed in the Text view and not yet applied is applied first, as Save applies it, so the file holds what is on screen: the export then changes the model, and spends one Undo step, as Apply text → model does. Save's two exceptions hold: a text with a syntax error, and any typed text in a collaboration room, are kept back — the file holds the model as it stands, the Text view still reads modified — not yet applied, and the strip under the toolbar says Exported without the text typed in the Text view, naming the line of the first syntax error, or the room. The next export that holds the text takes that note down. A save in this browser does not — the file still lacks the text — nor does an export take down a save's note; but a newer note of either kind replaces the older one, and a save to an attached Google Drive file takes either down. The two JSON exports write the model as it stands, without text not yet applied, and carry the merged library too, as a saved project does.

Source of truth: src/persistence/store.ts:88-135, src/branding.ts:48, src/ui/store.ts:786-804 (persistScenarios: the Regroup scenarios kept in this browser), 3449-3541 (newProject, listProjects: New, Save, Open and what they mark saved), 3783-3848 (commitVersion, switchBranch: a commit, and a branch head loaded), 4601-4611 (mergeLoads: a merge that loads), 4613-4722 (applyTypedTextToSave, sayWhatWasKept: typed text applied before a save or an export, or kept back and said so), src/ui/commands.ts:39-104 (Save, and Export ▾ → SysML), src/ui/store.drive.ts:422-434 (what reads unsaved), 1333-1398 (the question), src/api/versioning.ts:481-494, src/ui/panels/DriveStrip.tsx, src/ui/App.tsx:96-103, src/persistence/io.ts:45-86, test/e2e/persistence-reload.spec.ts, test/e2e/import-export.spec.ts, test/e2e/toolbar-lifecycle.spec.ts.

8.1 Google Drive (optional)

Where it is. Only on a site whose operator has set it up — a drive.json next to the app names their Google client (the README's Deploy section says how). There, Drive ▾ sits on the first toolbar row, beside Collaborate. A build that nobody configured ships the feature off: no button, and nothing in this section applies.

Nothing goes to Google until you ask. The app contacts Google only after you open Drive ▾, press Ctrl/⌘ + Shift + S, or follow a link to a Drive file — each of those loads Google's sign-in script, and signing in is a click of its own after that.

Signing in. Drive ▾ → Sign in to Google… (it reads Loading Google sign-in… for the moment the script takes). Google shows its account chooser — pick the school or the personal account you mean — then asks you to let the app use the Drive files you make or choose with it, and no others: the drive.file permission. The panel then reads Signed in as your address. A school account may meet Google's Access blocked page instead — a Google Workspace for Education account designated under 18 does, until the school allows the app, and so does any account missing from the test-user list while the site's Google project is still in testing. Closing that page leaves Sign-in was cancelled or blocked, with Privacy & data ↗ beside it: that page names the app's client ID, which is what your administrator needs (Admin console → Security → Access and data control → API controls → Manage third-party app access, add the app by its client ID; Limited access is enough).

Saving. Save to Drive as… asks for a name — the project's, with .sysml added — and writes a new file in the root of My Drive; the model is now attached to it, and the strip under the toolbar says saved to your Google Drive at the time. After an edit the strip reads unsaved changes, and Save to Drive — the strip's button, the panel's, or Ctrl/⌘ + Shift + S, from anywhere in the app, a field included — writes it. With a file attached, the toolbar's Save and Ctrl/⌘ + S write its unsaved changes to it as well, beside the copy they keep in this browser; if the browser refuses that copy (its storage full, or blocked for the site), the strip says so. What goes to Drive is the Text view's text: your packages, in this app's layout, and none of the standard library — nor the boxes you moved by hand on a diagram, which only the copy in this browser keeps. Text you typed and did not apply is applied first, because saving it means making it the model — except for the copy in this browser when that text has a syntax error: the parser's best guess at broken text is not what you see, so the browser keeps the model as it stood, while Drive gets your text as typed. Nothing goes to Drive by itself — there is no autosave — and closing or reloading the tab while a Drive file has unsaved changes raises the browser's own question whether to leave the page. Every row the strip can show, and every Drive control with its test id, is in Appendix A.

Opening. Signed in, the panel's Recent lists the files this app saved or opened for your account, newest first; one click opens one. Browse Drive… opens Google's file picker on your files and on those shared with you (on a site that configured the picker). The field under it takes a Drive share link — its resourcekey, which older link-shared files need, is kept and sent with every request for that file — a link to this app, or a bare file id. Opening replaces the model, and Undo starts over from the file; if the model has work no save holds (§8), the strip asks first (Open anyway, Keep editing). A model JSON file opens but is not attached: Save to Drive as… writes it as a .sysml file. With unsaved Drive changes, these commands ask first — New, Open, Import, switching to a branch or a merge that resolves in the Versions tab, joining a collaboration room, a Drive open, Close Drive file and Sign out — offering Save to Drive and continue, Discard and continue and Keep editing; each of them lets go of the file (a merge that meets conflicts loads nothing, keeps the file, and asks nothing). While a file is attached, only its unsaved changes are asked about — what Drive holds is not lost, whatever this browser holds. Without one, or with one gone from Drive (changes unsaved to it or not), the commands that replace the model ask the question in §8; Close Drive file and Sign out keep the model, and ask nothing more. While you are connected to a room, its peers change the model too, so no Drive file opens or attaches there: a Drive open and Save to Drive as… say Leave the collaboration room first, and a file attached while the room's relay was out of reach lets go when it connects.

Links and sharing. Copy link to this file copies a link to this app ending in ?drive= and the file's id (and its resourcekey, when it has one). Opening it shows a gate — This link opens a file from Google Drive — with Sign in and open and Skip. To share the model: Open in Google Drive ↗ → Share (Editor to let them save back, Viewer otherwise), then send the link Copy link to this file gives you. The first time, Drive will not let the app open a file somebody shared with you until you have chosen it once yourself in Google's picker: the gate says so and offers Browse Drive… on that one file — or, on a site without the picker, says the file cannot be opened there. Choosing it there grants it, and from then on the link opens directly. Pasting the file's Drive share link into the field beside it grants nothing — only the picker does — but the link carries the resourcekey some older link-shared files need. With view access only, the strip reads you have view access, and Save to Drive as… keeps your own copy.

When two people save one file. Just before a save, the app asks Drive whether the file's content changed since it last read or wrote it (by Drive's checksum of the content, so a rename or a new share does not count). If it did, nothing is written and the strip turns amber — changed in Drive since you opened it, with who and when — and offers Save as copy, Overwrite and Reload from Drive (one Undo step takes you back to your version). Drive keeps the previous version for about 30 days (up to 100 versions): Open in Google Drive ↗, then Manage versions; mark one Keep forever to keep it longer.

A file written by hand. The app writes files in its own layout: // comments go, while doc and comment bodies stay. The first time you save a file that was written by hand or by another tool, the strip asks once: Save anyway, Save as copy (the original stays as it is), or Cancel. Files the app wrote itself never ask. A file with a syntax error opens with its parse errors in Problems and keeps them through a save; what goes to Drive then is your text as typed.

Offline. The Drive commands that need Google — signing in, Save to Drive as…, Recent and its Refresh, Browse Drive…, opening a pasted link — are disabled, their tooltip reading Offline (if Google's sign-in script could not be fetched, the sign-in button reads Google sign-in did not load instead). If the attached file has unsaved changes, Save to Drive is disabled the same way, Ctrl/⌘ + Shift + S saves nothing and says you appear to be offline, and the strip says the changes stay in this tab: its Save keeps them in this browser — text typed in the Text view applied first — and Save to Drive works again once you are back online. With no Drive file attached, the key opens the Save to Drive as… form, whose save button is disabled offline as well. A ?drive= link opened offline says it needs Google Drive, and offers Skip.

The hour-long sign-in. A Google sign-in in the browser lasts about an hour, and there is nothing to renew it with silently. In its last two minutes, a strip showing unsaved changes adds sign-in expires soon, and after the hour sign-in expired; the next Drive command — the next Save to Drive, say — then opens a brief Google window — no account chooser — and carries on. If the browser blocks that window, the strip says so: allow pop-ups for the site and give the command again. If that window comes back signed in as another Google account — it can, once yours is no longer signed in to Google in this browser — the command does nothing: the strip says so, the Drive file is closed, the Recent list cleared, and the panel names the account now signed in. Google can also refuse a sign-in partway through a command — one revoked from another device, say. The app then opens the same brief window to renew it, and if that window is blocked or closed, the strip says Your Google sign-in expired, and Sign in and continue finishes what was interrupted.

Signing out. Drive ▾ → Sign out asks Google to revoke the app's access, then forgets the session, the Recent list and the attached file; the model stays on screen. If your sign-in had expired, it first asks Google for a fresh one in a brief window, because revoking needs one (should that window come back as another account, it is that account's access that is revoked, and the strip says so). When Google does not accept the request, the app says so and points to Google Account › Security › Third-party access, where you can remove the app yourself. After a sign-out, the next sign-in shows Google's permission screen again, and a file a classmate shared may need choosing once more.

What stays where. The sign-in lives in this page's memory only — the app never puts it in the browser's storage or in a URL — and is gone at sign-out, when it expires, or when the tab closes; Google's own picker receives it when you choose Browse Drive…. Your files travel between this browser and Google's servers. Whoever runs the site sees nothing of them: there is no server of theirs in between, only the host that serves the app's own files. A ?drive= link is an address like any other, though: opening one sends the file id in it — and its resourcekey, when it has one — to that host, and a file shared with anyone with the link is as open as that sharing makes it.

The CLI on a Drive file. With a file attached, the Copy command of the palette's checks names that file — as it is when its name is plain letters, digits, _, . and -. Any other name could be read as a command by some terminal (cmd.exe and PowerShell do not quote the way bash does), so the command names a stand-in instead — Swarm (copy).sysml becomes Swarm__copy_.sysml — and the note under the check says to save the file under that name. To have it in a terminal, download it — Open in Google Drive ↗ → Download, which works everywhere — or use Google Drive for desktop, which keeps My Drive in a folder on Windows and macOS (there is no Linux client). The file holds exactly the Text view's text, so the CLI reads what you saw: npm run sysprose -- stats Swarm.sysml. Export ▾ → SysML writes the model's text too, changes not yet saved to Drive included; text typed in the Text view and not yet applied is applied first, as Save does — one Undo step — unless it has a syntax error or a collaboration room is connected (§8). It names the file after the project, so save it under the name the command uses.

Source of truth: src/ui/store.drive.ts:493-573 (every sentence the feature says), 1149-1163 (the content check), src/persistence/drive/, src/ui/panels/DriveMenu.tsx, src/ui/panels/DriveStrip.tsx, test/e2e/drive.spec.ts (against faked Google services).

9. Limits

Stated plainly, because finding these out by surprise is worse.

• The library is a real download — the size is in §2. It is fetched and merged before the app is interactive, and re-merged a few hundred milliseconds after every Apply, Import, Open and branch switch; that second merge is why Problems and the text buffer refresh twice.
• Derived surfaces lag behind a burst of edits (§5).
• Undo is bounded and model-only. View changes, scoping and the theme are not undoable.
• PNG export is a white-background rasterisation of the SVG at 2×. Dark theme is not honoured. SVG and PNG export, and Auto-layout, are disabled off a graph view — the greyed control's tooltip says why.
• Collaboration needs a relay you start yourself (npm run collab), rooms are open with no permissions layer, and your identity is a random per-session name and colour.
• Google Drive, where a site offers it (§8.1): a sign-in lasts about an hour, and renewing it opens a window the browser must allow — so allow pop-ups for the site. One upload is at most 5 MB of text. Nothing is saved to Drive without you: there is no autosave. A tab holds one Drive file at a time. A file somebody shared with you opens here only after you have chosen it once in Google's picker, so a site without the picker cannot open it. The check for somebody else's save runs just before the upload, so two saves landing within the same second or two can still overwrite each other — Drive's version history keeps the other. Browse Drive… lists files by type — plain text, unknown binary (which a .sysml file often is to Drive) and JSON — and a file Drive typed otherwise does not appear in it. The resourcekey an older link-shared file needs is sent as a request header, and whether Google accepts that header from a browser page has so far been tried only against a stand-in for Google; if it does not, such a file will have to be opened through Browse Drive…. While connected to a collaboration room, no Drive file is opened or attached.
• Feasibility is approximate. The solver is penalty-driven; feasible means no known violated inequality, and unjudged relations are listed separately.
• The geometry view is massing, not CAD — primitive solids from attributes.
• One file at a time. No cross-file imports, no workspace.
• Ctrl+N is not a shortcut. New is a toolbar button only.

The verification lane's own register. These are not defects to be fixed later; they are the boundary of what this tool is allowed to say, and each one is a sentence it will refuse to print rather than a corner it will cut.

Source of truth: src/library/std/manifest.json, src/ui/store.ts:232 (UNDO_LIMIT: undo is bounded), 1682-1712 (RECOMPUTE_DEBOUNCE_MS: the derived surfaces lag), 4871-4989 (mergeLibrary, loadStandardLibraryAsync: the library merge), src/ui/panels/Toolbar.tsx:90-105, 273-313, src/api/analytics.ts:2408-2415 (feasible), src/ui/commands.ts:198-310.

10. Where to go next

• CLI-REFERENCE.md — every subcommand and flag, generated from the command table itself.
• DIAGNOSTIC-CODES.md — every finding code, what triggers it, and the repair it suggests. Branch on code, never on message.
• AGENT-AUTHORING-CAMPAIGN.md — how an agent is meant to write and repair models here, and the defects that campaign found.
• 02-omg-standard-reference.md — the language and API this tool implements a subset of.
• FEATURE-PARITY.md — what exists compared with other tools, with a test citation per row.
• ../examples/ — the shipped models.

Appendix A — every control, and the id a test can find it by

Every control carries a stable data-testid. The E2E suite drives the app by these ids, and so can you (or an agent) from a browser console. They are checked against the source by test/unit/user-guide.test.ts, so this table cannot quietly go stale.

Toolbar, row 1

Toolbar, row 2 — the view bar

Google Drive panel and strip

Present only on a deployment that configures Google Drive. The panel opens from Drive ▾; the strip is the line under the toolbar, there only while it has something to say; the gate is the loading screen a ?drive= link holds. (The strip's question about work no save holds, with no Drive file attached, is on every deployment: it is in the toolbar table above. So are two of its notes — that a save in this browser, or Export ▾ → SysML, kept typed text back, and that an element went to the top level of your model rather than into the standard library: see the Strip · error or note row.)

Panels

Bottom panel

The ▾ at the end of the tab strip folds the panel down to its tabs (bottom-collapse); ▴, or any tab, opens it again.

Appendix B — keyboard shortcuts

Plain keys are suppressed while you are typing in a field. So are the Ctrl/⌘ ones — except Ctrl/⌘ + S and, where the deployment has Google Drive, Ctrl/⌘ + Shift + S, which save from anywhere in the app, a field included: a Properties box, the Explorer search, the Text view's editor. The browser's own Save page dialog does not open. A box that applies what you type on Enter or on leaving it — Properties' Subject, Tags, Type and requirement attributes, a rename, a Requirements table cell — is applied first, as leaving it would, so the save holds what is on screen; the cursor stays where it was, except in a rename or a table cell, which close as Enter closes them. The focus then goes to the toolbar's Save button, as after a click on it, so the keys you press next do not delete anything: Backspace and Delete are ignored while a button has focus, where they would remove the selection — often the element you just renamed. The Requirements table's reference picker, which leaving cancels, stays open with what you typed in it, and nothing is linked. Every other key in a field stays the field's own.

Ctrl/⌘ + S also first applies what you typed in the Text view, as Apply text → model does, so the save holds the text on screen — unless the text has a syntax error, or a collaboration room is connected: then the browser keeps the model as it stood and the editor still reads modified — not yet applied; with no Drive file attached the strip under the toolbar says so, and an attached Drive file gets a faulted text as typed. A change applied from a field is an edit, though, and an edit replaces text typed in the Text view and not yet applied (§5): the save holds the field's change, not that text.

There is no Ctrl+N; New is a button only.

Source of truth: src/ui/commands.ts:39-104, 198-422, src/ui/App.tsx:143-148, src/ui/panels/RequirementsTable.tsx:569-606 (the reference picker).