Diagnostic codes

Every finding Sysprose reports about a .sysml source file carries a code from this catalogue. Codes are stable: messages get reworded, codes do not, so automation should branch on code and never on message.

This is the reference half of the Agent Diagnostics Contract; the workflow that uses it is in AGENT-AUTHORING-CAMPAIGN.md.

The shape of a finding

{
  "id": "parse#0",
  "code": "parse/mismatched-token",   // stable catalogue id — branch on this
  "severity": "error",                 // error | warning | info
  "source": "parser",                  // lexer | parser | mapper | validation | import
  "message": "Expecting token of type '}' but found `def`.",
  "range": {                           // 1-based line/column, 0-based offset
    "start": { "line": 2, "column": 10, "offset": 25 },
    "end":   { "line": 2, "column": 13, "offset": 28 }
  },
  "expected": ["}"],                   // parser errors: what would have been legal
  "found": "def",                      // what was written instead
  "hint": "Expected `}` here, found `def`. …",
  "elementId": "…",                    // validation findings: the offending element
  "elementName": "Vehicle",
  "instances": {                       // per-instance roll-up findings: the counts
    "total": 12, "generic": 1, "satisfied": 10, "violated": 1, "unknown": 0, "unread": 0,
    "listed": ["H2P::q::p"]            // "atLeast": true beside a count that is a lower bound
  },
  "instance": "H2P::q::p",             // a single-instance finding names its instance
  "relation": "H2P::P::c"              // and the relation it is about
}

range is present on every finding derived from the source text. The one family that is NOT derived from source text is checks/*: those are the app's own status rows for a check (a result, its scope, whether it could run), so they carry a code and no range. The range rule of the contract is narrowed for this family alone, because no span of the file would name the thing the row is about; see the checks source in the campaign document.

elementId and elementName appear on validation findings. expected/found appear on lexer and parser errors. instances, instance and relation appear on per-instance findings: a roll-up carries the counts in instances, and a finding about one instance names it in instance.

Severity means

Lexical

The text could not be turned into tokens. Always an error; the file cannot be read as SysML until it is fixed.

lexer/illegal-char

• Severity: error
• Source: lexer
• Fires when: A character that cannot start any token appears in the source.
• Hint given: Remove the stray character {found}. SysML identifiers are letters, digits and underscore; quote a name containing anything else as 'like this'. A unit with a non-ASCII symbol must be quoted the same way: ['m²'], ['W⋅h'], ['°C'].

lexer/unterminated-string

• Severity: error
• Source: lexer
• Fires when: A double-quoted string literal is not closed before end of line/file.
• Hint given: Close the string with a matching double quote.

lexer/unterminated-comment

• Severity: error
• Source: lexer
• Fires when: A block comment opened with /* is not closed before end of file.
• Hint given: Close the block comment with */.

Syntactic

The tokens do not form a legal declaration. expected lists what would have been legal at that position and found is what was actually written.

parse/mismatched-token

• Severity: error
• Source: parser
• Fires when: The parser required one specific token and found another. The single most common agent mistake: a missing semicolon or brace.
• Hint given: Expected {expected} here, found {found}. Insert the expected token before {found}.

parse/no-viable-alt

• Severity: error
• Source: parser
• Fires when: No grammar alternative matches at this point — usually a misspelled or misordered keyword.
• Hint given: No SysML declaration starts with {found} here. Check the keyword spelling and order, e.g. part def Name { not def part Name {.

parse/early-exit

• Severity: error
• Source: parser
• Fires when: A repetition that requires at least one occurrence found none.
• Hint given: A required element is missing before {found}.

parse/not-all-input-parsed

• Severity: error
• Source: parser
• Fires when: The file parsed to completion but text remains — typically one closing brace too many.
• Hint given: Unexpected {found} after the end of the model. Remove it, or check for an unbalanced closing brace.

parse/error

• Severity: error
• Source: parser
• Fires when: A parser error of a class this catalogue does not model specifically.
• Hint given: Syntax error at {found}. Compare the surrounding declaration with examples/vehicle.sysml.

parse/unknown-keyword

• Severity: error
• Source: parser
• Fires when: A word that no declaration starts with leads a member, so the parser stops on the token after it.
• Hint given: Unknown declaration keyword {found}; the declaration is kept as an unparsed element and re-emitted verbatim, so saving the file preserves this error instead of hiding it. Use a supported keyword such as part, attribute, port, action, state, requirement or connection.

parse/keyword-order

• Severity: error
• Source: parser
• Fires when: Declaration keywords appear in the wrong order, e.g. def part X;.
• Hint given: Keywords are in the wrong order. A definition is written <kind> def Name, e.g. part def Vehicle {, not def part Vehicle.

parse/bare-transition-arrow

• Severity: error
• Source: parser
• Fires when: A bare A -> B transition shorthand was used. It is rejected deliberately: it cannot be told apart from a -> function-operation expression.
• Hint given: Write the transition with its keyword: transition A -> B; (a bare A -> B is ambiguous with an expression and is not accepted).

parse/dangling-then

• Severity: error
• Source: mapper
• Fires when: A bare then X; appears with no preceding succession in the same scope to chain from.
• Hint given: A bare then X; continues the previous succession. Start the chain with first A then B;, or write this one in full.

parse/conflicting-direction

• Severity: warning
• Source: mapper
• Fires when: One feature declares two different directions, e.g. in port out x.
• Hint given: A feature has one direction. Remove {found} or the other one; the first direction written was kept.

Mapping

The tokens form a legal declaration, but the model this tool builds has nowhere to put it. The source text is preserved verbatim and re-emitted on save, so nothing is silently lost.

mapper/unsupported-keyword

• Severity: error
• Source: mapper
• Fires when: A declaration keyword the grammar accepts has no metaclass in this tool — the KerML type/feature family (namespace, class, feature, step, connector, …).
• Hint given: This KerML keyword {found} is not modelled; the declaration and its body are preserved verbatim and re-emitted unchanged on save. Rewrite it with a supported keyword such as part, attribute, item, port, action or state.

Reference resolution

A name did not resolve. These are WARNINGS: the textual name is preserved in the model, so the file still loads, but nothing is bound to it.

ref/unresolved-type

• Severity: warning
• Source: mapper
• Fires when: A type reference after : names nothing in scope or in the standard library.
• Hint given: Define the referenced type, import the package that declares it, or correct the spelling.

ref/unresolved-connection-end

• Severity: warning
• Source: mapper
• Fires when: A connect/connection endpoint names a feature that does not resolve.
• Hint given: Check the endpoint path: each dotted segment must name a feature of the preceding one, visible from the connection owner.

ref/unresolved-transition-end

• Severity: warning
• Source: mapper
• Fires when: A transition source or target names no state in scope.
• Hint given: Declare the state before referencing it, or correct the name.

ref/unresolved-specialization

• Severity: warning
• Source: mapper
• Fires when: A specialization/subsetting/redefinition target does not resolve.
• Hint given: Check the specialized name is declared and visible from here.

ref/unresolved-reference

• Severity: warning
• Source: mapper
• Fires when: A reference in a relationship statement (bind, disjoint, reference…) does not resolve.
• Hint given: Check the referenced name is declared and visible from here.

ref/unresolved-dependency-end

• Severity: warning
• Source: mapper
• Fires when: A dependency client or supplier does not resolve.
• Hint given: Declare the client/supplier element, or correct the name.

ref/unresolved-allocation-end

• Severity: warning
• Source: mapper
• Fires when: An allocation source or target does not resolve.
• Hint given: Declare the allocated element, or correct the name.

ref/unresolved-requirement

• Severity: warning
• Source: mapper
• Fires when: A satisfy/verify statement names a requirement or satisfier that does not resolve.
• Hint given: Declare the requirement and the satisfying element before the satisfy statement, or correct the names.

ref/unresolved-flow-end

• Severity: warning
• Source: mapper
• Fires when: A flow source or target does not resolve.
• Hint given: Check the flow endpoint names a visible feature.

ref/unresolved-alias-target

• Severity: warning
• Source: mapper
• Fires when: An alias names a target that does not resolve.
• Hint given: Declare the alias target, or correct the name.

ref/unresolved-import

• Severity: warning
• Source: mapper
• Fires when: An import names a package that is not loaded.
• Hint given: Check the imported package name; only the bundled standard library and packages declared in this file are visible.

Model validation

The file parsed, but the model it describes breaks a rule. Each code matches a rule id in src/validation/rules.ts.

validation/unresolved-import

• Severity: warning
• Source: validation
• Fires when: An import names a namespace that is not loaded, so it brings nothing into scope.
• Hint given: Check the imported namespace name. Only the bundled standard library and packages declared in this file are visible.

validation/split-declaration

• Severity: warning
• Source: validation
• Fires when: A declaration parsed to nothing but a keyword — no name, type, value, body or specialization — which happens when a misplaced word splits one declaration into two.
• Hint given: Check the declaration for a stray or repeated keyword. A port is written in port name : Type; (direction first, then the keyword).

validation/unknown-unit

• Severity: warning
• Source: validation
• Fires when: A value, a constraint body, a transition guard or an expression value carries a [unit] the engine does not know, so no dimensional check or unit conversion can be applied to it; a constraint using it answers unknown.
• Hint given: Use a registered unit symbol (SI units and their prefixes, the information units bit, B and o — these three also take the binary prefixes Ki..Yi — plus Sh, Hart, nat, Bd, Wh, Ah, min, h, °C, ft, lb, …), qualified or not ([kg], [SI::kg]). The information units take the MAGNIFYING prefixes only ([kB], [Mbit]), so [dB] is not one of them: the decibel is a logarithmic ratio, not a unit this engine can convert. Compound units are written as an expression — [m/s], [kg*m/s^2], [Mbit/s], [J/(kg*K)], [1/s] for a reciprocal — each atom taking its own qualifier ([m/SI::s]), or with the library spellings ⋅ and superscripts, which must be quoted because the grammar reads only ASCII names: ['W⋅h'], ['m²']. A library name resolves quoted and qualified ([SI::'watt hour'], [SI::'metre per second']); the worded forms per/squared/cubed are understood, longer ones are not — write the symbol. A symbol that is also a keyword is quoted (['in'] for the inch, in a value position). A value with an unknown unit is treated as a bare number in arithmetic, which is usually wrong; a constraint that reads one cannot be judged.

validation/derived-dimension-mismatch

• Severity: warning
• Source: validation
• Fires when: An expression-valued feature derives to a physical dimension that disagrees with its declared type — a Real computed from dimensioned quantities (usually a hand-rolled conversion such as … / power * 60.0), or an ISQ kind whose derivation has another dimension. The feature is excluded from unit-aware constraint evaluation, so a constraint reading it answers unknown.
• Hint given: Two repairs. (1) Type the feature by the ISQ kind its derivation has and drop the hand conversion — enduranceMin : Real = capacity / power * 60.0 becomes endurance : ISQ::DurationValue = capacity / power, and the comparison converts: endurance >= 45.0 [min]. (2) When the value really is a pure ratio, give the inlined constant its unit so the dimensions cancel: mtow / 25.0 becomes mtow / 25.0 [kg].

validation/connection-compatibility

• Severity: warning
• Source: validation
• Fires when: A connection joins two out (or two in) ports, or two ports whose port definitions share no ancestor.
• Hint given: Wire an out port to an in port (or use inout), and give both ends the same port definition — or a conjugated one (~PortDef) on the receiving side.

validation/duplicate-name

• Severity: error
• Source: validation
• Fires when: Two sibling elements in the same namespace declare the same name.
• Hint given: Rename one of them, or move it to a different owner. Sibling names must be unique.

validation/blank-name

• Severity: error
• Source: validation
• Fires when: A named element has an empty or whitespace-only name.
• Hint given: Give the element a name, or remove the empty quotes to leave it anonymous.

validation/unwritable-note-body

• Severity: error
• Source: validation
• Fires when: A doc/comment/rep body, or a requirement statement, contains the two characters that end a note — which the notation gives no way to escape.
• Hint given: Remove them from the text. Written into a note they would close it early, and everything after them would be read back as declarations instead of prose.

validation/dangling-endpoint

• Severity: error
• Source: validation
• Fires when: A relationship points at an element id that is not in the model.
• Hint given: A referenced element is missing; declare it, or remove the relationship.

validation/unresolved-type-ref

• Severity: error
• Source: validation
• Fires when: A type reference does not resolve to any declared or library type.
• Hint given: Declare the type, import the package that provides it, or correct the spelling.

validation/port-direction

• Severity: error
• Source: validation
• Fires when: A port has no direction, or one that is not in/out/inout.
• Hint given: Declare the port direction, e.g. in port fuelIn : FuelPort;.

validation/malformed-multiplicity

• Severity: error
• Source: validation
• Fires when: A multiplicity is not n, n..m, n..* or *.
• Hint given: Write the multiplicity as [1], [0..1], [1..*] or [*].

validation/connector-endpoints

• Severity: error
• Source: validation
• Fires when: A connection or connector has fewer than two endpoints.
• Hint given: Give the connection both ends, e.g. connect a.p to b.q;.

validation/requirement-subject

• Severity: warning
• Source: validation
• Fires when: A requirement has no subject: none declared, none inherited from its definition, and no satisfy/verify naming one.
• Hint given: Add a subject to the requirement, or a satisfy … by … statement naming what satisfies it.

validation/redefinition-target-missing

• Severity: error
• Source: validation
• Fires when: A redefinition, subsetting or reference-subsetting target is missing or unresolved.
• Hint given: Declare the redefined/subsetted feature, or correct the name after :>> / :>.

validation/containment-cycle

• Severity: error
• Source: validation
• Fires when: An element owns itself, directly or through a cycle.
• Hint given: Break the ownership cycle: an element cannot contain one of its own ancestors.

validation/specialization-cycle

• Severity: error
• Source: validation
• Fires when: Specialization relationships form a cycle.
• Hint given: Break the specialization cycle: a type cannot specialize itself, directly or indirectly.

validation/orphan-relationship

• Severity: warning
• Source: validation
• Fires when: A relationship element is not owned by any element.
• Hint given: Nest the relationship inside the element it belongs to.

validation/feature-typing-non-type

• Severity: error
• Source: validation
• Fires when: A feature is typed by something that is not a type.
• Hint given: Type the feature with a definition (part def, attribute def, port def…), not with a usage.

validation/connector-end-not-feature

• Severity: error
• Source: validation
• Fires when: A connector endpoint does not resolve to a feature.
• Hint given: Connect features (parts, ports, attributes), not definitions.

validation/value-type-mismatch

• Severity: warning
• Source: validation
• Fires when: A literal value is inconsistent with the declared type.
• Hint given: Make the literal match the declared type, e.g. a number for Real, true/false for Boolean.

validation/redefinition-conformance

• Severity: warning
• Source: validation
• Fires when: A redefining feature’s type does not conform to the redefined feature’s type.
• Hint given: Type the redefining feature with the redefined type or a specialization of it.

validation/constraint-violation

• Severity: warning
• Source: validation
• Fires when: A constraint or requirement expression is violated, or cannot be evaluated.
• Hint given: Check the constraint expression and the values it reads; an unevaluable constraint usually references a feature with no value, or compares two different physical dimensions — read the message, which names the actual fault.

validation/target-by-specialisation

• Severity: warning
• Source: validation
• Fires when: A target written over a measure that has no value where it is stated (Common::m >= 0.9) is read through a feature that subsets or redefines the measure in another context (LA::m :> Common::m): one finding per context, at that feature — a warning when its value misses the target, info when it meets it or cannot be read; past twenty contexts of one relation, one finding per verdict and cause, at the first context's feature, counting the rest. A context into whose reading a binding carries a value from another member (q’s :>> L = 50.0 through Q’s bind p.load = L, read by Q’s p.m2 >= 0.0) is validation/constraint-by-instance's instead.
• Hint given: A miss is a fact about the estimate, not a fault in the model: change the design if the target must be met, not the number to meet it. An info that could not be read names why — a context with two features that specialise the measure, a body that names a measure the context does not specialise, or a specialiser with no value and no asserted equation (the same equation required, or as a plain constraint, is a check of a value given elsewhere, not a definition).

validation/constraint-by-instance

• Severity: warning
• Source: validation
• Fires when: A relation whose reading a binding makes differ between instances — a definition’s constraint read in a usage several instances share (P’s load <= 10.0 in Q::p, read for Q’s own p and for q’s p), one written in such a usage, or one read in a context whose value reaches it through a binding — read once per instance: one finding per relation and usage of two or more instances counting the instances it holds in, is violated in, could not be read in (with the cause of each kind, at most three, and the first instance of each) and did not read past a cap (with the cap; a group of more instances than the tool reads is one info finding counting them all unread) (a warning when any is violated; past twenty usages of one relation, one finding for the relation, counting every instance and naming the 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), and one warning per violated instance, at most five, at the value that makes that instance differ, however few there are (a relation a usage owns, read in its one other instance, is that warning alone — or, where that instance could not be read, one info finding saying why). The roll-up is anchored at the relation; an instance’s or a context’s finding at the line that makes it differ: the member of its own stating the value a binding carries into it (q1’s attribute :>> L = 50.0), else the element the instance is read in (q2’s part :>> p { … }), else its innermost own usage (part q1 : Q) or definition (part def Q2 :> Q, for Q2’s own p), else the context itself — never the usage the instances share.
• Hint given: Change the value the binding carries into the named instance (the line the finding points at), or the relation — not the definition’s default, which a binding overrides in its context. Counts are in instances; an instance finding names its instance and relation. One that could not be read says why: no bound feature has a value, defaults differ, an enclosing assert constrains it (an inequality, an equation over values read elsewhere, or one that sets it equal to another default), enclosing asserted equations give it two values, more instances than the tool reads, the instance redefines the relation itself, a reference the relation is read through stands for another feature there, the tool cannot tell which element stands for the instance (one its path inherits twice, as from two types, neither redefining the other) or what it reads runs past the names the tool compares, its own element states a default that an asserted equation of its own constrains, the relation is read through a part a binding joins to another, the value a binding carries into it is of another dimension than the feature it fills, or the reading failed inside the tool (the sentence names the error). An instance whose own element states something the relation reads (a redefinition, a specialised type, a binding or a reference of its own on its path) is read in that element.

validation/dimensional-consistency

• Severity: warning
• Source: validation
• Fires when: A value’s unit has a different physical dimension than its quantity kind.
• Hint given: Use a unit of the declared quantity kind, e.g. a mass unit for a mass attribute.

validation/stale-evidence

• Severity: warning
• Source: validation
• Fires when: An attached evidence record no longer stands on this model. For a record that says what its proof stood on — what --engine smt writes — the comparison is SCOPED to that: the clause’s own relation, the axiom rows its read-closure reaches, the axiom set the consistency check ran over, and its own premises. An edit that moves none of them is not reported here at all, and the sentence names every part that did move. For a record with no scope — --engine literal, or one written before the field existed — the comparison is a digest over the whole user model, so the edit may be anywhere; either way the message names the requirement’s own slice, which is what has to be re-read.
• Hint given: Re-run npm run sysprose -- verify <file> --record evidence.json and evidence-attach, or take the stale record off with evidence-detach. A stale record is never counted as discharged, and the verdict facet beside it stands on nothing until it is re-recorded. npm run check -- <file> --json publishes, per record, which part of the proof’s scope moved.

Formal verification

The verification lane, and the severity splits it in two. Almost all of these are INFO because none of them is a defect in the model: they say that a relation is outside the fragment the lane encodes, that a contract has nothing to show, that a clause sits somewhere the standard does not admit it, or that a proof would be void rather than absent — each stated rather than left to be inferred from a silence. The ERRORS are the codes that say something about the MODEL — verification/refuted, the violation this lane exists to find, at their head — and the two a flag asks for: verification/vacuous-property, which exists only because --strict-vacuity asked for a vacuity to be loud, and verification/cover-required, which exists only because --cover-required asked for a decided absence to spend the 1.

verification/unsupported-expression

• Severity: info
• Source: verification
• Fires when: A relation is outside the fragment the verification lane encodes — a name that resolves to nothing, a body that does not parse, a dimension clash, arithmetic on an offset scale, a collection-valued feature, a remainder, a variable exponent or a non-numeric operand. refine also files a CONNECTOR here when it declines to read one as a value equality: a bare connection states that two features are joined and nothing about their values, and an allocate or an interface is not a connect at all, so neither enters the connection assertion γ.
• Hint given: The relation is listed with the gate that refused it and nothing is claimed about it. Check the names it reads, then rewrite it inside quantifier-free arithmetic over single-valued scalar features, or expect it in the obligations --missing histogram. For a connector the refusal is a modelling one rather than a fragment one: bind the attributes if they are one quantity, or add the item flow that carries the value — --connections-as-equalities opts into reading a bare connect as an equality, and reads only connect.

verification/contract-no-guarantee

• Severity: info
• Source: verification
• Fires when: A requirement states assumptions, guarantees nothing and inherits no guarantee either, so its contract has nothing to show. A requirement that inherits a require clause from a general type is not reported here: the clause applies to it and contracts lists it on its row.
• Hint given: Add a require constraint { … } stating what the requirement guarantees, or read the assumptions as context rather than as an obligation.

verification/nonstandard-clause-location

• Severity: info
• Source: verification
• Fires when: An assume or require clause is written in a body the standard's ActionBodyItem does not admit — an action definition, for instance. Sysprose parses it; the specification does not offer it there.
• Hint given: The standard writes a behaviour precondition as assert constraint precondition { … }, as a guard on the incoming transition, or as a requirement whose subject is the behaviour; contracts reads all three.

verification/foreign-keyword

• Severity: info
• Source: verification
• Fires when: A prefix keyword is a third-party spelling this tool recognises — #Exception, #exception, #precondition, #postcondition — read through the foreign-alias table rather than named by SysML v2 or shipped by Sysprose.
• Hint given: The line names the spelling and what it was read as. It is neither standard vocabulary nor a Sysprose keyword, and it files nothing unless obligations --from-keywords asked it to; write assume constraint / require constraint and no keyword is needed at all.

verification/keyword-names-nothing

• Severity: info
• Source: verification
• Fires when: A #keyword resolves to no metadata def in scope — a misspelling, or a vocabulary the file never declares or imports.
• Hint given: Declare or import the metadata def the keyword names — import SysproseVerification::*; for the one this tool ships — or correct the spelling. The keyword is kept in the file either way.

verification/vacuous-pass

• Severity: info
• Source: verification
• Fires when: A requirement is discharged by an antecedent that does not hold — its assume clause is false at the model’s values, or its premises are unsatisfiable. The standard reads allTrue(assumptions) implies allTrue(constraints), which makes such a requirement true; this tool reports it as undecided instead. That is a declared deviation, recorded in docs/CONFORMANCE.md.
• Hint given: Fix the assumption so it holds, or drop it: a requirement that only holds when something false is true says nothing about the design. The row exits 2 with and without --allow-inconclusive.

verification/not-evaluable

• Severity: info
• Source: verification
• Fires when: A relation this lane encodes could not be decided at the model’s own values — a feature it reads carries no value, a derived quantity cannot be compared as a bare number, or the expression did not evaluate to a boolean.
• Hint given: Give the features it reads values, or compare against a unit literal of the right dimension. --allow-inconclusive deliberately does NOT forgive this: an obligation nobody could evaluate is not an obligation that holds.

verification/unsupported-construct

• Severity: info
• Source: verification
• Fires when: An obligation is outside the fragment this lane encodes at all — a gate refused the relation, or the requirement carries prose and no constraint body, so there is nothing to decide.
• Hint given: Run npm run sysprose -- obligations <file> --missing for the histogram of what was refused and why, then rewrite the relation inside quantifier-free arithmetic over single-valued scalar features. This is one of the two codes --allow-inconclusive may lower to exit 0.

verification/tool-absent

• Severity: info
• Source: verification
• Fires when: The engine that was asked for could not run: --engine smt, or --engine auto with no solver backend to resolve to. Every obligation in the run is reported under this code.
• Hint given: Install the solver, or ask for --engine literal, which evaluates at the model’s own values and says holds-at-values — a point evaluation, never a proof. --allow-inconclusive never lowers this: a missing solver must never be a green build.

verification/design-admitted

• Severity: info
• Source: verification
• Fires when: An obligation was refuted only after --free released a feature value the model states. A = value is a binding, so the counterexample is a design the model admits, not a violation of it.
• Hint given: Read it as "the requirement fails if this feature is allowed to move", not as "the requirement fails". Re-run without --free for the verdict at the model’s values. It exits 2, never 1, and --allow-inconclusive does not lower it.

verification/timeout

• Severity: info
• Source: verification
• Fires when: A solver was asked and did not answer inside the time it was given — it returned unknown after the timeout rather than sat or unsat. It is the SMT engine’s undecided code and the second of the two --allow-inconclusive may lower.
• Hint given: Raise the budget with --timeout MS, narrow the obligation, or read the row as undecided — a solver that ran out of time has said nothing about whether the requirement holds. It exits 2 by default, and the row was not retried with a weaker encoding.

verification/refuted

• Severity: error
• Source: verification
• Fires when: A requirement does not hold with every feature at the value the model binds it to. Both engines file it: the literal one evaluates the relation and reads it as false, and the SMT one finds A ∧ P ∧ ¬G satisfiable and confirms the witness in process. check-behaviour files the same code for a behavioural property a bad-prefix search REFUTED: a run of the configuration graph that breaks the pattern, printed step by step — and for a recovery assertion some reachable configuration cannot discharge: not recoverable, naming the SET of configurations from which the named state is unreachable over a relation that is the machine’s own, with no run printed because a set is not a run. It is the one code on a DECIDED row, and the run exits 1.
• Hint given: Read the row’s detail for the two magnitudes the comparison was made on, and the witness for the assignment that breaks the requirement in the units the file stores — or, in the behaviour lane, the witness trace: a run this semantics admits, with the atoms that hold at each observation. A bound can hide a violation and can never invent one, so a refutation stands whether or not the walk finished. Fix the design or the requirement and re-run. --allow-inconclusive does not forgive a violation, and exit 1 outranks every undecided row in the same run.

verification/vacuous

• Severity: info
• Source: verification
• Fires when: The SMT engine found the premises unsatisfiable under the axioms — A ∧ P is unsat — so the obligation was discharged by an antecedent that no assignment satisfies. verification/vacuous-pass is the literal engine’s weaker sibling: an assumption false AT THE MODEL’S VALUES, rather than one nothing at all can satisfy.
• Hint given: Read the unsat core printed on the row for the facts that collide, then fix the assumption or drop it: an obligation discharged for free says nothing about the design. It is inconclusive and exits 2, no flag launders it, and --strict-vacuity raises it to verification/vacuous-property without changing the exit code.

verification/vacuous-property

• Severity: error
• Source: verification
• Fires when: --strict-vacuity was given and an obligation was vacuous. It is the same row as verification/vacuous or verification/vacuous-pass, raised from an info line to an error so a vacuity cannot be scrolled past. check-behaviour raises it from a third row, which carries no code of its own: a property whose scope no run of an exhaustively walked machine opens, or a precedence whose P never occurs.
• Hint given: The flag changes the code and the severity and NOTHING else: the claim stays vacuous, the row stays undecided, and the run exits 2 exactly as it does without the flag. Fix the antecedent so the obligation — or the behavioural property — stands on something that can hold.

verification/inconsistent-axioms

• Severity: info
• Source: verification
• Fires when: The once-per-run consistency check found the axiom set itself unsatisfiable — check(A) is unsat. Every obligation in the run is reported under this code, because a negation is unsat under a contradictory context whatever it says, and a proof from a contradiction is void.
• Hint given: Read the unsat core named on the row: it is the smallest set of the model’s own facts the solver found colliding. Nothing in the run was decided until they are reconciled. --allow-inconclusive never lowers this — proving everything is not the same as proving anything.

verification/inconsistent-requirements

• Severity: error
• Source: verification
• Fires when: No design point satisfies all the requirements on one subject at once: consistency asserted each of them under a tracking literal — as assume ⇒ require, the reading the shipped library states — and the solver answered unsat. The row names the conflicting subset the unsat core produced, by requirement and by the qualified name of each relation in it.
• Hint given: Removing or weakening any one member of the named subset is where a fix starts; --minimize reduces the subset by deletion until every member is needed, and only a loop that ran to completion may call it minimal. By default the question is asked with every feature value the file STATES released — a value expression that reads no other feature — so this is a conflict between the requirements themselves and not between a requirement and a value; --with-values re-pins them and asks the weaker question, and every line names the mode it was computed in. Requirements guarded by assume clauses that cannot both hold are NOT reported here: each requirement is read as an implication, so mode- and phase-conditional requirements never contradict each other. It is a decided finding about the model and the run exits 1; no flag forgives one.

verification/refinement-failed

• Severity: error
• Source: verification
• Fires when: A refinement obligation was refuted: the component contracts, together with the equalities the model states, admit an implementation that breaks the system contract (obligation (3)) or that fails a component’s own assumption (obligation (4)). The row carries a witness, re-read through this tool’s own evaluator before it was printed.
• Hint given: Read the witness: it is an implementation every component contract admits and the system contract forbids. The obligations are Cimatti’s Theorem 1 in NORMAL FORM (nf(C) = ¬A ∨ G), so a component whose assumption is false contributes nothing to the entailment — which is exactly why mutual support (A₁ = G₂, A₂ = G₁) cannot buy a verdict here. Strengthen a sibling’s guarantee, weaken the system guarantee, or state the connection that makes the two quantities one. It is a decided finding about the model and the run exits 1; no flag forgives one. Nothing in this verdict is about ordering or time.

verification/unconnected-assumption

• Severity: error
• Source: verification
• Fires when: A component assumption was not discharged, and NOTHING in the decomposition reaches the quantity it is about: no bind edge, no item flow, and no sibling contract mentions it. The structural half of a refuted obligation (4), separated from verification/refinement-failed because the fix is different — an assumption a sibling DOES constrain, just not strongly enough, is a design shortfall and is filed under that other code, since no bind can repair it.
• Hint given: A bare connection is not a value equality — it joins two features and says nothing about their values — so an assumption over a feature only a connect reaches is discharged by nothing. Bind the attributes if they are one quantity (bind a.v = b.v;), or state the item flow that carries the value. --connections-as-equalities opts into the OCRA reading in which a bare connect IS an equality, and the fact is then printed on every verdict line. It exits 1 like any other refuted obligation.

verification/refinement-undecided

• Severity: info
• Source: verification
• Fires when: A decomposition was not decided: a gate refused a clause of the system contract (dropping a conjunct of nf(C) would weaken the very goal being proved), a component’s assume clause was refused, the system contract states no guarantee this lane encodes, or no sub-contract states one.
• Hint given: Nothing is claimed about this decomposition — never read it as "refines". Run npm run sysprose -- contracts <file> to see what each contract states and obligations <file> --missing for what this lane cannot reach. --allow-inconclusive does NOT lower it: the flag is scoped to verification/timeout and verification/unsupported-construct, and this is neither.

verification/contract-set-vacuous

• Severity: info
• Source: verification
• Fires when: Step (0) of the refinement check found the antecedent unsatisfiable: the sub-contracts, the connection assertion and the system assumption cannot hold together. Every refinement obligation over them is entailed by a contradiction, so none of them is claimed.
• Hint given: Read the unsat core named on the row for the statements that collide — two sibling contracts over one bind class whose guarantees exclude each other are the usual cause. Without this step the tool would print "obligation (3) proved" over an architecture whose components cannot coexist. It is inconclusive, exits 2, and no flag lowers it; --strict-vacuity is a verify flag and does not change this code.

verification/derivation-not-refinement

• Severity: error
• Source: verification
• Fires when: A derive or refine chain the file states is not a refinement: the derived requirement assumes MORE than the one it was derived from (so it applies where the parent’s guarantee is not in force), or the derived requirements together do not entail what the parent promised. Both obligations are read with the orientation the mapper stores — derive requirement D from R puts R on the source end and refine requirement X by Y puts X on the target end, uniform with satisfy — and the row carries a witness this tool re-read before printing.
• Hint given: Read the witness: it satisfies every requirement written down from this one and breaks the one they were written from, or it satisfies the parent’s assumption and not the child’s. The two obligations are A_R ⊨ ⋀ A_D and A_R ∧ ⋀ nf(C_D) ⊨ G_R, in normal form (nf(C) = ¬A ∨ G), so mutual support cannot buy the verdict. Weaken the child’s assumption, strengthen its guarantee, add the sibling requirement that closes the gap, or correct the direction of the edge. It is a decided finding about the model and the run exits 1; no flag forgives one. Nothing in this verdict is about ordering or time.

verification/single-point-of-failure

• Severity: error
• Source: verification
• Fires when: A cut-set enumeration found a sub-contract whose failure ALONE breaks the top requirement: with that one guarantee withdrawn, the remaining sub-contracts and the connections admit an implementation the top requirement forbids. The row carries the counterexample, re-read through this tool’s own evaluator before it was printed. It is independent of whether the decomposition REFINES — an architecture whose obligation (3) is proved can have several single points of failure, and saying so is what this command is for.
• Hint given: Read the witness: it is the design the remaining contracts admit once this one stops delivering. A fix is redundancy — a second sub-contract guaranteeing the same quantity, which makes the set order 2 — a stronger sibling guarantee, or a weaker top requirement. It is a decided finding about the model and the run exits 1; there is no --allow-inconclusive on this command to forgive one. Cut sets of order 2 and above are NOT filed under this code: needing two failures at once is what redundancy looks like from the failure side. Nothing in this verdict is about ordering, time, rates or probabilities, and none of it is a behavioural safety analysis.

verification/optimality-not-established

• Severity: info
• Source: verification
• Fires when: z3 returned a bound for a measure and this tool will not call it the optimum: the script it optimised over is nonlinear in its bytes — a product or a quotient of two features — and νZ is complete for LINEAR real arithmetic only. The value is a bound the optimiser reached, not one it established as the tightest.
• Hint given: Read the row as the bound it is. Pinning the feature that makes the objective nonlinear (a divisor, or the second operand of a product) puts the question back inside the fragment νZ decides, and npm run sysprose -- obligations <file> shows which relation carries it. It exits 2 and no flag lowers it: presenting a non-optimal bound as the optimum is the one sentence this command may never write. The heuristic optimize in src/semantics/solver.ts searches for a point and proves nothing, so it is not a second opinion about optimality either.

verification/free-variable-unbounded

• Severity: info
• Source: verification
• Fires when: A feature released by --free is not confined on both sides by the axioms and premises the obligation stands on, so the solver may place a witness outside the physical domain. Reported instead of a refutation, never beside one.
• Hint given: Add a two-sided premise — assume constraint { x >= lo and x <= hi } — before freeing the feature. This tool derives no domain axiom from a quantity kind: it does not know that a power or a mass is non-negative, so a witness at a negative power is arithmetically confirmable and physically meaningless. It exits 2 and no flag lowers it.

verification/claimed-without-evidence

• Severity: info
• Source: verification
• Fires when: A requirement carries a verdict facet and no evidence record this tool can read — either none was ever attached, or the carriers present could not be parsed back.
• Hint given: This is not a defect: a verdict facet is ordinary requirements management, and a verdict reached by inspection is recorded there with no tool involved. The row says only that THIS tool has nothing standing behind it. Run verify --record then evidence-attach if you want one.

verification/verdict-overstates-evidence

• Severity: error
• Source: verification
• Fires when: A requirement states verdict = "pass" over an evidence record whose claim is not proved — holds-at-values, holds-within-bound, vacuous, inconclusive or anything else the engines can reach.
• Hint given: pass is written for one claim only, and a point evaluation is not a proof. Run evidence-attach --from again with the same records: it rewrites the facet from the claim even when every record is already present, which puts the file back where this tool would have left it. evidence-detach is the other repair, and takes the record off with the facet. evidence-attach cannot produce this state — every verdict it writes is derived from the claim, and a record file that says otherwise is refused — so a file in it was written by hand or by something that did not go through this tool.

verification/method-not-performed

• Severity: info
• Source: verification
• Fires when: A verification case declares a @VerificationCases::VerificationMethod { kind = …; } whose list contains no analyze — test, demo, inspect, or a spelling that names no VerificationMethodKind at all. This tool performs analysis only, so the case is not judged.
• Hint given: Read it as "not judged", never as "does not hold": an unjudged case is not a refutation, and the run exits 2 rather than 1. --allow-inconclusive does NOT lower it — the flag is scoped to verification/timeout and verification/unsupported-construct, and an unperformed method is neither, so there is no flag that forgives one. A case that says kind = (analyze, test) IS judged, on the analyze part, and reports the rest as not performed.

verification/no-property

• Severity: info
• Source: verification
• Fires when: A verification case has nothing to check: it names no requirement at all, or its verify statement points at something that is not a requirement — including an objective { verify X; } whose X names a part, an action or nothing, which never becomes a verification relationship at all and is read off containment instead. Prose splits two ways here. An UNTAGGED requirement that carries prose and no constraint body does NOT land here: it still raises an obligation row of its own (verification/unsupported-construct) and the case is judged inconclusive on that row, because there was a property to look for and looking for it is what failed. A requirement tagged #prose (or #prompt) contributes no row at all — the tag says it is deliberately informal — so a case that verifies nothing else DOES land here.
• Hint given: Point the case at a requirement with a formal clause — verify R by <case>; at member level, or objective { verify R; } inside the case. Both forms are read. A case with no property is inconclusive and exits 2: a case that checked nothing has not passed.

verification/verdict-changed

• Severity: info
• Source: verification
• Fires when: A requirement carries a verdict facet saying something other than what this run computed for the verification case that verifies it — for example pass in the file over a run that refuted the requirement, or inconclusive in the file over one that proved it.
• Hint given: This is a disagreement rather than a defect: a verdict facet is ordinary requirements management and may record a verdict reached by inspection with no tool involved. Nothing is rewritten by reporting it. verify --record then evidence-attach puts the facet back in step with the claim, and evidence-detach takes both off; a pass over a run that did not prove it is named as overstating on the row.

verification/temporal-field-unencodable

• Severity: info
• Source: verification
• Fires when: A drafted clause writes a FRETish field this lane cannot read: a scope other than global, a condition at all, or a timing other than always. All three describe WHEN a response is owed, and no in-process engine in phases 0–3 walks an execution or discharges a liveness claim, so the clause is refused at gate 0 rather than accepted with the temporal part quietly ignored.
• Hint given: Restate the clause as an invariant over the values the design admits and leave the three temporal fields unwritten — property-draft emits them as commented guidance for exactly that reason — fold a condition into the requirement as an assume constraint, or export the property to an engine that decides temporal logic (export, §3.11). "Accepted with the temporal field ignored" is not offered: nothing downstream could decide the clause that reached it.

verification/unresolved-name-in-property

• Severity: info
• Source: verification
• Fires when: A name in a drafted clause is not one the subject’s scope offers. A bare feature name is the commonest case: a property clause names its features THROUGH the subject (uav.endurance, never endurance), because a bare name in a requirement that states two subjects names whichever the walk reached first and a reader cannot see which.
• Hint given: Run npm run sysprose -- property-draft <file> --element REF for the data dictionary of every legal name with its type, unit and value, and write the dotted form. The row carries the nearest names it could find in expected.

verification/dimension-clash-in-property

• Severity: info
• Source: verification
• Fires when: Two operands of a drafted clause must share a physical dimension and do not — uav.endurance >= 45.0 [kg] compares a duration with a mass. It is the same gate the numeric surface applies, asked before the clause reaches a file rather than after.
• Hint given: Compare quantities of one dimension: read the feature’s dimension and unit in the property-draft dictionary and give the literal a unit of that dimension. A feature that is DERIVED and dimensioned cannot be compared as a bare number at all — it needs a unit literal on the other side.

verification/trivial-property

• Severity: info
• Source: verification
• Fires when: A drafted clause is valid on its own (uav.mtow <= uav.mtow — every assignment makes it true) or unsatisfiable on its own (no assignment does), checked under z3 with NO axioms asserted. Either way it says nothing about the design: proving the first is free, and the second can never be discharged.
• Hint given: State a bound the design has to meet, or check the relation’s direction. Note the gate’s scope: it is SYNTACTIC non-triviality, so a clause the model’s own feature values already satisfy passes it — uav.mtow <= 25.0 [kg] is accepted over a model that pins mtow = 18.5 [kg]. verify’s tautology check and the vacuity report decide that, and the limit is in the §6 register.

verification/nontriviality-unchecked

• Severity: info
• Source: verification
• Fires when: Gate 4 did not run: no z3 backend loaded (the package is optional, or SYSPROSE_NO_Z3 is set), or a check came back unknown inside its budget. The clause passed the first four gates and is accepted-with-gap.
• Hint given: Install the optional solver package — the absence sentence on the row names it and prints the install command — and re-run to close the gap. It is deliberately not reported as an accepted clause: an unchecked gate that printed "accepted" would be a missing tool producing a green answer, which is the failure this lane is written against.

verification/unreachable-state

• Severity: warning
• Source: verification
• Fires when: An EXHAUSTIVE walk of a machine’s configuration graph never entered a state. It is claimed only when four things hold at once: the walk finished inside its bounds, every trigger the machine names was offered, no unsupported construct was met, and every guard the walk consulted decided something. The interpreter’s completion-chase budget (64 steps) is not a bound here but part of what the walk follows: where a chase spends it with a completion transition still due, the interpreter takes the next event right there, and so does the walk — so a state only a chase longer than the budget would enter is one no run enters, under the maxCompletion printed beside the claim. On any bound hit, and over any guard the walk could not evaluate, the row is suppressed entirely rather than qualified.
• Hint given: Either a transition into the state is missing, or the guard on the one that is there can never hold. Read the bounds printed beside the claim: it is true under those and under no others, and reach --max-configs N widens them.

verification/dead-transition

• Severity: warning
• Source: verification
• Fires when: An EXHAUSTIVE walk never found a transition ENABLED in any reachable configuration — its source is unreachable, or its guard never holds where it is. Suppressed under the same four conditions as verification/unreachable-state. A completion transition still due where the chase budget stops a chase is enabled there, and is not reported, though no run fires it. Only transitions the walk could offer are counted at all: one leaving a node no configuration’s stack can hold is outside the census, not dead — the initial node’s edge, which the interpreter READS to decide where the machine opens, and an edge leaving the machine root, which the walk never stands on because it opens at the root’s initial substate.
• Hint given: Note the reading before acting on it: dead means never enabled, so a transition that an inner state’s priority always beats is enabled and is NOT reported here. Fix the guard, or the path into its source.

verification/deadlock

• Severity: warning
• Source: verification
• Fires when: A reachable configuration has no enabled outgoing transition — no completion transition, and none for any trigger the machine names — and its active leaf is neither marked final nor a done node. A configuration where the chase budget stops a chase is not one: a completion transition is still due there. Reachable means reached by a run of this semantics: a configuration only entered by firing a transition an inner state’s priority always beats is not explored, so nothing is reported there. It is an absence claim about one configuration’s outgoing edges, so it is WITHHELD wherever a guard the walk could not evaluate (verification/guard-undetermined) is an edge out of the configuration the row is about — read over its whole active stack, since an edge leaving a composite state is an edge out of every configuration inside it. That guard is an edge out nothing decided. A guard left undecided ELSEWHERE in the machine does not withhold it: the row is a claim about one configuration, and a question asked in another region is not an answer about this one. The report prints a withheld line in place of each row that went, so a short list is never read as a clean one. A bound does not withhold it: a bound stops the walk enqueueing successors and takes nothing away from a configuration it already dequeued and offered every input at.
• Hint given: Give the state a way out, or end the machine there properly — done finished; in the notation, or kind = "final" through the API. It is a reading of ONE machine under the printed alphabet: it says the machine cannot progress from there, never that the system deadlocks, and this tool never writes "deadlock-free".

verification/unrecoverable-mode

• Severity: warning
• Source: verification
• Fires when: A set of reachable configurations no run leaves — a bottom strongly-connected component of the walk’s successor relation — that is not where the machine is meant to stop. Three kinds of bottom component are exempted and never reported here: one made only of final states and done nodes (an ending); a single configuration with no successor at all, which is already verification/deadlock (one fact, one row); and the component holding the opening configuration, which is the machine’s own reachable core rather than somewhere it can be trapped FROM. The row names the states of every configuration in the set — the union of their active stacks, never the leaf alone — and the shortest path from the opening into it. It is published ONLY where the walk is exact: it 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 completion transition still due — a walk that does holds a resting point the budget makes where the machine states an edge. (A machine that names no trigger keeps the relation it states even where the budget stops its chase, and a set nothing leaves in that relation is a set no run leaves, so its rows stand.) Each of those is a way the retained relation can differ from the machine’s — a missing edge invents a set nothing leaves, and an edge the environment may never supply invents an escape from one — so under any of them the whole list is emptied, never shortened, and the report says which clause refused it. A machine with a nondeterministic choice carries the simulator sentence beside the row: the walk explores both branches, the simulator takes the first declared one.
• Hint given: Give one state in the set a transition to a state outside it, or end the machine there with done if stopping is the intent. This is a reading of ONE machine over a walk whose relation is the one the model states: it says no run of this machine leaves the set, and nothing about the system it models or about what an environment could do. A --json payload carries trapCensus beside the rows — how many components the walk had, how many nothing leaves, and how many were exempted as endings, deadlocks or the core — and, where no trap was found, a sentence that names what was exempted rather than a bare all-clear.

verification/completion-livelock

• Severity: warning
• Source: verification
• Fires when: A reachable cycle the interpreter’s completion chase goes round without coming to rest: a set of configurations the walk reached where a trigger-less transition is due at every one, and where the one the interpreter fires — the first enabled at the innermost level, by declaration order, the transition runStateMachine’s chase takes — leads to the next of them and round. A run that gets there goes round until its 64-step chase budget is spent, stops with a trigger-less transition still due, and moves on only on an event — on a machine that names no trigger, the run ends there; under run-to-completion the machine never rests there. It is decided over CONFIGURATIONS and over the interpreter’s chase, not over states and not over every branch: a guard that holds somewhere on the way round, or an effect that walks the store out of the loop, is a chase that leaves, and nothing is reported; a cycle that some OTHER enabled trigger-less transition could leave is still reported when declaration order keeps the chase on it, and the row names each state where that is so — the verification/nondeterministic-choice row beside it says the simulator never takes the other transition. Each configuration has one chase step, so two cycles never share a configuration; cycles that go round the same transitions and differ only in the store or history they carry are ONE row, which says how many it stands for — so a cycle of states is reported once, by reach and, on the machine it checks, by check-behaviour, where it moves no claim and no exit code (published rows only: a withheld one is a withheld line of reach, and is read there). The row names the machine, the states of the cycle’s configurations in the order the chase goes round them (the union of their active stacks), and the shortest way in from the opening: a run the simulator makes — each step the transition simulate takes, and the budget left to go round when it gets there — wherever the walk holds one; otherwise the walk’s own, which may take a branch of a choice the simulator never takes, and the row then says the way in is not one simulate makes and names the state where it parts from the simulator. Neither a bound nor a named trigger withholds it: every step it stands on is one the walk took from a configuration it dequeued, and a cycle through a configuration whose step a bound refused, or that is reached only where the budget stops a chase, is not found at all. It is WITHHELD — a withheld line in its place, naming the clause — where a guard the walk could not evaluate is a trigger-less transition out of one of the cycle’s configurations (whether the chase fires it and leaves was never decided), or where the step the chase takes is an after(n) dwell, which the walk takes without waiting it out.
• Hint given: Give the machine somewhere to rest: put a trigger on a transition of the cycle, so the run waits there for that event, or a guard that is false where it should wait — a configuration with no trigger-less transition enabled is where a chase stops. Where the row names a state with another trigger-less transition enabled, that choice is what decides whether the chase leaves; give the two transitions guards that cannot both hold. This is a reading of ONE machine under the printed bounds: it says the interpreter’s chase does not settle there and the budget is what stops it, never that the system the machine models loops.

verification/nondeterministic-choice

• Severity: warning
• Source: verification
• Fires when: Two or more transitions leaving the SAME state are enabled at once on one event, in a configuration a run of this semantics reaches, so which of them fires is decided by declaration order. The row names the one the simulator takes and the ones it never takes. Transitions enabled at different levels of the active stack are NOT reported: innermost-first is the profile’s stated priority rule, not an ambiguity. Nor is a row reported at a level a guard the walk could not evaluate sits strictly inside: that guard may have been the transition the priority rule would have picked, and the choice above it would then be one the withholding invented rather than one the walk found.
• Hint given: Declaration order is not a semantics. Give the transitions guards that cannot both hold, or different triggers; until then one of them is unreachable in simulation while the model admits both. A row on a trigger-less machine prints no trigger label, because there is none.

verification/guard-undetermined

• Severity: warning
• Source: verification
• Fires when: The walk consulted a transition’s guard and could not evaluate it — a name it reads has no value anywhere in scope or in the store (transition idle if mode == 3 then hazard; over attribute mode : Integer;), or the expression yielded no value for a reason that is not a missing name at all — a type error inside it, such as not mode over an Integer mode, a comparison between two different kinds of value, or arithmetic that is not finite. Raised once per transition, naming the guard text and the names that were missing, if any. It is NOT a guard that is false: the step relation does not fire an undetermined guard because it has to pick something, and that reading is right for a run and wrong for a report.
• Hint given: Read which of the two it is off the row: if it names missing names, give those features a value the walk can read (attribute mode : Integer = 3;) or drive the machine from a state whose effect assigns them; if it names none, every name resolves and the guard itself is the defect — most often that it is not a predicate. Until then the machine’s unreachable and dead lists are WITHHELD — they are absence claims, and nothing here established the absence — and the report says undetermined under {…} rather than exhaustive. A no-way-out row goes with them only where this guard is an edge out of the configuration that row is about; a configuration nothing undecided leaves keeps its row, and each row that does go is replaced by a withheld line naming why. check-behaviour is gated on the same condition and reports the property inconclusive rather than pass or vacuous. A hidden-choice row still stands where the withheld guard is at or outside the level the choice was read at — two transitions enabled at once is an existential claim, and removing a candidate beside them can only shrink it — but not where the withheld guard is strictly inside it, because that moves which level the choice is read at.

verification/bound-exhausted

• Severity: info
• Source: verification
• Fires when: A bound stopped the walk: the configuration bound (--max-configs) or the depth bound. The walk is partial. The 64-step completion-chase budget the interpreter runs under is not one of them — the walk follows it as the interpreter does, taking the next event where a chase spends it — and is named here only where a check-behaviour search that does not carry the chase position meets a run it would have to chase past the budget, and refuses that run rather than report on it: on a machine that names no trigger, whose walk keeps the relation it states, that is a monitor counting round a cycle of completion transitions. check-behaviour files it for a property whose search found no bad prefix over a graph it did not finish — for one whose scope no explored run opened, because “the antecedent is never met” is a claim of absence a partial walk has not established either — and for a recovery over a walk that did not finish, where neither “reachable from every configuration” nor its complement is a claim a partial relation supports: a frontier configuration looks like one nothing leaves.
• Hint given: The unreachable and dead lists are emptied rather than shortened, and the report says so: a partial walk cannot say what it never reached. In the behaviour lane the property is inconclusive rather than pass or vacuous, for the same reason. Only the configuration bound is a flag: raise --max-configs, or read the run as what it is. After the depth bound, or a chase past the budget, no re-run with a higher N decides the row, and the row says so instead of advising one. This is not a defect in the model.

verification/behaviour-unsupported-construct

• Severity: info
• Source: verification
• Fires when: A machine uses a construct this engine does not explore: parallel regions (attrs.parallel), a history state (attrs.history or a history pseudostate) — neither of which sysml.langium has a keyword for, so both are reachable only through the API — a step edge missing an endpoint, a step edge that crosses the machine’s boundary (machine-boundary: written in the machine and leading into a state def written inside it — to one of its states or to the definition itself — or out to another machine’s state, or written elsewhere and leading into or out of one of the machine’s states, a transition a specialisation or a typed usage adds over the states it inherits among them; each machine steps only by its own transitions, so the step has no meaning this engine defines, and both machines it joins are refused), or an edge under the machine that sequences behaviour and that the step relation does not hold (edge-not-walked): a spelling it does not read, or an edge carrying a payload it models nothing of. That last one is not an enumerated construct but whatever the edge census could not account for, so a kind nobody listed refuses the machine instead of quietly shrinking its absence lists. The machine is not walked and is never reported as exhaustively explored. check-behaviour also files it for a PROPERTY CLASS this engine does not decide: existence and response are liveness, violated only by an infinite run that never delivers what it promised, and a bad-prefix search finds no bad prefix for either — so a walk would answer “no violation found” on every graph and a pass drawn from that would be the strongest verdict the command has, printed for the two properties it cannot decide. And it files it for a recovery claim over a machine whose relation this walk cannot make exact — 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 supply it, or an after(n) dwell it takes without advancing a clock — because “reachable from every configuration” would then be a claim about escapes this walk invented, in either direction. And it files it for a property carried by a state def written inside a machine that owns no transition: that definition is no machine of its own, and the machine it is written in stops at it, so no walk stands on its states — the property is reported on the outer machine as checked by nothing rather than dropped from the run.
• Hint given: Nothing under such a machine is a claim of absence: no state is reported unreachable and no transition dead, and no liveness property is reported to hold. The row names the element and says why the relation does not hold it: give a step edge both of its endpoints, keep each transition inside the machine whose states it joins (or write a nested definition as a composite state, state Inner { … }, to make its states part of the outer machine; for a step a specialisation or a typed usage adds over inherited states, write the machine you mean out whole in one definition), put a property carried by a nested definition that owns no transition on the machine or the state it is about, take the payload off an edge that is meant to pass control rather than an item, model the behaviour with nested states and named triggers, write the safety half of what you meant (absence, universality, bounded-existence, precedence), or export the machine to an engine that decides it (§3.11). No flag lowers this row: --allow-inconclusive is scoped to verification/timeout and verification/unsupported-construct, and this is neither.

verification/trigger-not-offered

• Severity: info
• Source: verification
• Fires when: A check-behaviour search found no bad prefix (or no witness, for a cover) over a walk that no bound stopped, but the walk never offered a trigger the machine names at any configuration, so a run that takes it was not searched. It is the one clause of the exactness gate that is left when no bound was hit — the alphabet the walk offered is shorter than the alphabet the machine names. The walk offers the whole alphabet wherever it can decide that the interpreter takes its next event, so this row is a defect of the walk and not of the model, and a model that reaches it has no flag that decides it.
• Hint given: No bound was hit, so --max-configs re-runs the same walk and the row comes back the same: do not raise it. The row names the triggers the walk never offered. The property is inconclusive and exits 2, never pass, vacuous or not covered; --allow-inconclusive does not lower it. Report the model: a trigger the walk cannot offer is a gap in this engine.

verification/recovery-budget-withheld

• Severity: info
• Source: verification
• Fires when: A recovery property was withheld because the interpreter’s 64-step completion-chase budget decides the row, by either of two routes: the walk had to follow the budget instead of the edge the machine states (on a machine that names no trigger, the relation follows the chase past where the run ends), which withholds every recovery of the machine whatever p is; or a run comes to rest where the budget stops it, away from the named state, and gets back to nothing from there while the transitions the machine states lead on. Either way the run’s resting point and the relation’s answer part, and neither “reachable from every configuration” nor its complement is a claim made. It is raised by check-behaviour for recovery only, after the walk finished: no bound was hit and no construct is outside the fragment.
• Hint given: No flag decides it, and --max-configs is not advice for it: the budget is the interpreter’s own. Shorten the trigger-less chain to at most 64 steps, or remove the completion cycle, so that every run comes to rest inside the budget. Adding a named trigger does not decide the row: it moves it to verification/behaviour-unsupported-construct (the walk then cannot say whether an environment supplies the trigger), which is also undecided. The property is inconclusive and exits 2; --allow-inconclusive does not lower it.

verification/malformed-property

• Severity: info
• Source: verification
• Fires when: A behavioural property could not be read as one: a pattern outside the catalogue (absence, universality, bounded-existence, precedence, cover, recovery, existence, response), a scope outside its five, a field the pattern needs and did not get, a bounded-existence with no n, a --pattern that is not key=value, an expression atom that parses and is not a predicate, so it yielded a number (or nothing) where the walk needed a boolean — or a p whose atom kind this pattern cannot observe (recovery reads state and node only: 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 neither yields a target set to reverse from), or a recovery over any scope but globally, which this pattern gives no meaning to.
• Hint given: Write the property as pattern=absence, scope=globally, p=state failsafe — or pattern=cover, scope=globally, p=state failsafe to ask whether some run reaches the situation rather than whether none does — which is exactly the field set the @SysproseVerification::PropertyPattern carrier uses. A property nobody could read is never dropped from the run: it is inconclusive and exits 2, because a typo that silently removed a claim would look like a clean sweep.

verification/unknown-atom

• Severity: info
• Source: verification
• Fires when: A name in a property names nothing the machine has: state X for a state it does not declare, trigger t for a trigger no transition names, fires T for a transition with no such declared name, node N for no such node — or an expression reading a feature that is in no scope the walk offered. A name matching several elements lands here too, rather than resolving to whichever the walk reached first.
• Hint given: The row lists what the machine DOES offer, so a misspelling is one line from being fixed; on an ambiguous name, write the qualified one. This is never read as "the atom is false": absence of state failsafe would then PASS the moment failsafe were misspelt, which is the loudest way this lane could print a green verdict that means nothing.

verification/not-covered

• Severity: info
• Source: verification
• Fires when: A cover property — "can this design reach the situation I name?" — found no witness over a graph the walk saw whole: no explored run enters a configuration where its p atom holds inside an open scope segment. It is a DECIDED absence, published under the same five conditions a pass is (a bound hit or an undecided guard makes the row inconclusive instead, and the row says the not-covered claim is not made), and it is a missing behaviour rather than a violated requirement: the run exits 2, never 1, unless --cover-required is given.
• Hint given: Read the sentence as an answer, not a limit: the design as written admits no run into that situation within the printed bounds. If that situation is one the design must reach, add the transition or the trigger that gets there — or pass --cover-required, which makes the row exit 1 and adds verification/cover-required beside this line without changing the claim word. A witness that IS found prints as covered with the run step by step; the positive answer carries no code.

verification/cover-required

• Severity: error
• Source: verification
• Fires when: --cover-required was given and a cover property came back not covered. The flag spends the exit code’s 1 on a decided absence — a behaviour the author says this design MUST admit and it does not — and this error is ADDED beside the verification/not-covered info line, never in its place, so a flagged run and a plain run print the same claim word and the same info finding and differ only by this error and the exit code. The flag never re-grades a row that is inconclusive under verification/guard-undetermined: on every such cover the run says --cover-required not applied, counts how many of the cover’s unreached states sit behind a guard over an attribute with no declared value (which the walk read as false), and stays at exit 2, because an answer about an unbound model parameter is not an answer about a design that violates something.
• Hint given: The claim is still not-covered, not fail: nothing was refuted, and verification/refuted is never printed for a missing behaviour. Add the run the cover asks for, give the guarded attribute a value the walk can read if the row was withheld instead, or drop the flag and take exit 2 as the answer it is.

verification/witness-not-replayed

• Severity: info
• Source: verification
• Fires when: A check-behaviour search found a run that breaks a property (fail) or reaches the situation a cover names (covered), and the interpreter, driven with that run’s events, does not take it: at some step it fires another transition, or none, or enters another state. Every witness is replayed through runStateMachine before the row stands on it — with the declaration-order tie-break resolved the witness’s way, the one choice the semantic profile leaves open, and with run-to-completion, the 64-step chase budget, the priority rule and the events all the interpreter’s own. A run the interpreter does not take refutes nothing and witnesses nothing, so the row is inconclusive and exits 2, and the witness is not printed.
• Hint given: Nothing is claimed about the property, and nothing here is a defect in the model: the search and the interpreter disagree about one run, which is a defect in this engine. The row names the step where the two parted; drive the machine with the same events in the Simulation tab to see what the interpreter does there, and report the model. No flag lowers this row.

Input handling

Problems with the input itself rather than its content: wrong format, encoding normalisation, or a failure inside the checker.

import/not-text

• Severity: error
• Source: import
• Fires when: Content offered as SysML text is actually JSON (it starts with {).
• Hint given: This looks like JSON, not SysML textual notation. Import it as model JSON, or supply a .sysml source file.

import/malformed-json

• Severity: error
• Source: import
• Fires when: A file offered as model JSON does not parse as JSON.
• Hint given: Fix the JSON syntax, or supply the model as .sysml text instead.

import/wrong-extension

• Severity: warning
• Source: import
• Fires when: The source was given a file name whose extension is neither .sysml, .kerml nor .txt; the content was parsed as SysML text anyway. Text read from a pipe or a buffer carries a display name instead and is exempt.
• Hint given: Rename the file to .sysml so every tool recognises it.

import/bom-stripped

• Severity: info
• Source: import
• Fires when: A UTF-8 byte-order mark was removed before parsing.
• Hint given: Write .sysml files as UTF-8 without a BOM.

import/crlf-normalized

• Severity: info
• Source: import
• Fires when: Windows line endings were normalised to LF before parsing; reported positions are in the normalised text.
• Hint given: No action needed. Use LF line endings to keep reported positions identical to your file.

import/internal-error

• Severity: error
• Source: import
• Fires when: The checker itself failed. Reported as an error rather than a clean result so a failure is never mistaken for a valid model.
• Hint given: This is a tool defect, not a model error. Please report it with the input that triggered it.

Round-trip

Guards against the tool producing notation it cannot read back.

roundtrip/unparseable-serialization

• Severity: error
• Source: import
• Fires when: Text produced by this tool's own serializer does not parse back. A silent-misparse guard.
• Hint given: Tool defect: the serializer emitted notation the grammar rejects. See docs/AGENT-AUTHORING-CAMPAIGN.md "Open defects".

App checks

The palette's own status rows (src/ui/checks.ts). These are NOT derived from source text: a row is a fact about a CHECK — its result, its scope, whether it could run — so it carries a code and NO range, and the contract's range rule is narrowed for this family alone. They are catalogued here because automation reads them off the same Checks surface as every other finding and branches on the same codes; the closed set is CHECK_META_CODES, pinned to this family by test/unit/diagnostic-codes.test.ts.

checks/command-note

• Severity: info
• Source: checks
• Fires when: A solver check that cannot run in the page left a file or element name out of its copyable command, because the name has characters a terminal could read as commands, so the row says what the stand-in stands for.
• Hint given: Save the file under the plain name the command uses, or replace <qualified name> with the element it names — the note names which.

checks/degraded

• Severity: warning
• Source: checks
• Fires when: A reach or check-behaviour run was judged over a model that does not count as loading cleanly: a text a file of it can hold (what Save writes, or what Export ▾ SysML writes) has syntax errors, or validation finds errors on the user’s elements of the live model or of the model a text parses to, or the model cannot be written as text — so the same command exits 1 (reach) or 2 (check-behaviour) in a terminal. It is also raised, with its own message and no terminal exit code, when a text parses cleanly but to a model other than the one on screen (written back from its parse it reads otherwise: a field written back as typed closed its owner, added a declaration or turned the rest of its line into a comment), so a terminal given that file checks the other model; when validation of the model failed with an internal error; and when whether the text loads could not be checked (the background worker could not — it failed, stopped, could not load the standard library or said nothing for a minute — or the page has no worker and no standard library has loaded there). A text into which the serializer wrote, as typed, a value the grammar cannot read where it stands is not parsed: the row says how many such values it found.
• Hint given: Fix the syntax or validation errors the row counts, or open Export ▾ SysML and save the text it writes. A text that parses to another model holds a field written back as typed (a value, a type) that reaches past its own declaration: fix that field. When the load could not be checked, run the check again, or the command in a terminal; after a standard-library load failure, reload the page first. Nothing is judged over half a model.

checks/internal-error

• Severity: error
• Source: checks
• Fires when: A palette check threw instead of returning a verdict, so the failure is reported rather than read as a pass.
• Hint given: This is a tool defect, not a verdict on the model. Report it with the model that triggered it.

checks/not-here

• Severity: info
• Source: checks
• Fires when: A solver-backed check (verify, consistency, bounds, refine, fault-tree) cannot run in the page because it is not cross-origin-isolated, so the row is the terminal command to run instead of a verdict.
• Hint given: Copy the command and run it in a terminal, or open the app on a cross-origin-isolated page where z3 can load.

checks/not-walked

• Severity: info
• Source: checks
• Fires when: A state belongs to no state machine the reach walk covered, listed so it is not mistaken for a walked, reachable state.
• Hint given: Move the state into the machine that should contain it, or select that machine and re-run the walk. Nothing is claimed about a state the walk did not cover.

checks/pick-machine

• Severity: info
• Source: checks
• Fires when: A check-behaviour run could not tell which state machine the selection names — the selection is not a machine, or it holds several — so the machines a person can pick are listed.
• Hint given: Select one of the machines the row names (or a state inside it) and re-run, or name it with --element <qualified name> in a terminal.

checks/scoped

• Severity: info
• Source: checks
• Fires when: A contracts or obligations run narrowed to the selected element and what it contains, as --element narrows it in a terminal.
• Hint given: Nothing to repair: the row records the scope the result covers. Clear the selection to cover the whole model.

checks/whole-model

• Severity: info
• Source: checks
• Fires when: A contracts or obligations run covers the whole model because there is nothing to narrow to — no selection, a bundled library element, or an element that can hold no contract or obligation — and the message says which.
• Hint given: Select a package or definition to narrow the report, or read the figure as the whole model's; the message names the reason it could not narrow.

117 codes. Generated from src/text/langium/diagnostic-codes.ts.