Command reference

Two commands read a .sysml file from a terminal. npm run check says whether the file is sound; npm run sysprose says what is in it. Each subcommand is a thin shell over the exported function named in its Backed by line, so a figure read here and the same figure computed from that import cannot differ. The app answers the same QUESTIONS, but several of its views draw their own projection rather than call the reporting function — the user guide and the README's capability table mark which, and say how the two can differ.

For what the answers mean — and for the app the commands mirror — read the user guide. For what a diagnostic code means, read the diagnostic-code catalogue.

npm run sysprose

npm run sysprose -- <subcommand> <file.sysml|-> [options]
cat model.sysml | npm run sysprose -- stats -
npm run sysprose -- --help                 # the subcommand list
npm run sysprose -- <subcommand> --help    # the flags of one subcommand

The exit-code contract is per subcommand, and there are 7 of them. Most subcommands report: stats, elements, requirements, trace, connectivity, where-used, orphans, prompts, contracts, obligations, property-draft, property-check, evidence-status, reach — for those, 0 clean · 1 the model did not load cleanly (the report is of what parsed) · 2 usage/IO error. verify and consistency judge, and their 1 means a decided negative — an obligation refuted with every feature at its model value, or one requirement set nothing can satisfy. refine judges an architecture and carries a contract of its own, because a refinement obligation reads no feature value and there is no --free for it: 0 every decomposition or derivation chain the --via family reads was shown to refine — for a decomposition, obligation (3) proved and every component assumption discharged; for a derive/refine chain, every derived requirement shown to assume no more than its parent and the set shown to entail the parent's guarantee — over a satisfiable contract set, and there was at least one of them to decide · 1 at least one obligation refuted, with a counterexample this tool re-read and confirmed: the component contracts admit an implementation that breaks the system contract, or the derived requirements admit one that breaks the requirement they were written from · 2 usage/IO error, a degraded model, a model that states no decomposition or derivation chain the --via family can read, or ANY undecided group — a timeout, an absent solver, a clause a gate refused, or a contract set that is vacuous, which is never laundered into a pass. A refinement obligation reads no feature value and there is no --free here. bounds DECIDES without judging — it reports the tightest value the model's axioms admit, and a number is not a violation — so its contract has no exit 1 in it at all: 0 every bound asked for was DECIDED — an optimum whose optimality z3's νZ established, an exact supremum or infimum it proved is approached and never attained, or an unboundedness it proved under the axioms that were asserted · 2 usage/IO error, a degraded model, or any bound that was not decided — a value νZ does not certify as the tightest (nonlinear), a timeout, an absent solver, an axiom set that cannot hold together, or a measure no relation in the model reads. There is no exit 1: a bound is what the axioms admit and not a verdict, and there is no --allow-inconclusive here. evidence-attach and evidence-detach write the file back, and they have no exit 1 at all: 0 written · 2 usage/IO error, or a model that did not load cleanly — a degraded model is refused rather than partially rewritten, so there is no exit 1. check-behaviour judges a machine and carries another, because there is no solver in that lane and no --free for it either: 0 every ASSERTION stated on this machine was shown to hold on every reachable configuration, over a graph this walk saw whole, and every cover stated on it was witnessed on a run this walk saw, and there was at least one of them to decide · 1 at least one property refuted, with a witness trace of a run this semantics admits — or a recovery assertion some reachable configuration cannot discharge, reported as that set rather than as a run — or, under --cover-required, a cover this walk did not witness on any run it saw whole · 2 usage/IO error, a degraded model, a machine that states no property at all, or ANY undecided property — a bound the walk hit, a trigger the machine names that the walk never offered with no bound hit (verification/trigger-not-offered), a construct this engine does not explore, a witness the interpreter does not take (verification/witness-not-replayed), a recovery withheld because the interpreter’s chase budget stops a run somewhere that does not hold p (verification/recovery-budget-withheld), a liveness pattern no bad-prefix search decides, a property that could not be read, an atom that names nothing, or a vacuous one, which is never laundered into a pass — or a cover property whose behaviour this walk did not find on any run it saw whole, which is a missing behaviour and not a violated requirement — --cover-required spends the 1 for it instead. There is no solver in this lane and no --free: the walk reads the model’s own values. fault-tree judges an architecture from the failure side and carries the last of them, because its 1 is a combination of contract failures rather than one refuted obligation — a decomposition that refines can still have a single point of failure: 0 every fault tree the model states was enumerated to its order bound and none of them has a single point of failure — every order-1 check decided and none of them broken — and there was at least one tree to enumerate · 1 at least one sub-contract whose failure ALONE breaks the top requirement, with a counterexample this tool re-read and confirmed, or a top event that is already open with every sub-contract honoured · 2 usage/IO error, a degraded model, a model that states no decomposition to inject a failure into, a state machine whose failure modes this command found none of (or found and does not inject), or ANY undecided check — a timeout, an absent solver, a clause a gate refused, or a contract set that is vacuous, which is reported as vacuous and never as "no cut set". A cut set of order 2 or above is what redundancy looks like from the failure side, so it does not spend the 1; every absence is bounded by the order it was checked to and higher orders are not explored. A cut set reads no feature value: there is no --free here, and no --allow-inconclusive either, because an undecided order-1 check is exactly the state a "no single point of failure" sentence may never be written over. Each section below states its own contract in full, and every section states which of the 7 it obeys.

Under the reporting contract, exit 1 is about the model, not the report: those subcommands report and do not judge, so finding four unused definitions is an answer and exits 0. A model that did not load cleanly still produces a report — of what error recovery salvaged — with a degraded banner on stderr saying so. Under the judging contract a degraded model is exit 2: a verdict over half a model is not a verdict.

stdout carries the report; stderr carries everything about the file, for every exit code, so a pipeline gets the data and a person gets the warnings.

Two refusals, each replacing an answer that would read as true: a file that parsed and produced no elements exits 2 rather than reporting an empty success, and an element reference matching several elements exits 2 with the candidates rather than reporting on the first one.

The subcommands

Options every subcommand takes

--no-library and --include-library are two different knobs. --no-library skips binding: it changes the model, and library types then report as unresolved. --include-library changes reporting: the library is bound and then listed alongside your model. Only elements can honour the second one — every other report excludes the library by construction and states its own excluded count — so it is refused elsewhere rather than accepted and quietly ignored.

Subcommands in detail

stats

How big is this model, and what shape is it?

npm run sysprose -- stats <file.sysml|-> [options]

No flags of its own.

Computed by modelMetrics + countByMetaclass (src/api/analytics.ts). With --json the answer is published under stats, beside ok and file.

Exit codes. 0 clean · 1 the model did not load cleanly (the report is of what parsed) · 2 usage/IO error.

elements

What is in it?

npm run sysprose -- elements <file.sysml|-> [options]

Computed by buildGrid (src/diagram/grid.ts). With --json the answer is published under elements, beside ok and file.

Exit codes. 0 clean · 1 the model did not load cleanly (the report is of what parsed) · 2 usage/IO error.

requirements

Are my requirements covered, and by what?

npm run sysprose -- requirements <file.sysml|-> [options]

Computed by requirementSatisfaction (src/api/analytics.ts) + buildRequirementsTable (src/diagram/requirements-table.ts). With --json the answer is published under requirements, beside ok and file.

Exit codes. 0 clean · 1 the model did not load cleanly (the report is of what parsed) · 2 usage/IO error.

trace

What satisfies, allocates, verifies, refines, derives or traces what?

npm run sysprose -- trace <file.sysml|-> [options]

Computed by traceabilityMatrix (src/api/analytics.ts). With --json the answer is published under trace, beside ok and file.

Exit codes. 0 clean · 1 the model did not load cleanly (the report is of what parsed) · 2 usage/IO error.

connectivity

Which ports are wired, and which are left dangling?

npm run sysprose -- connectivity <file.sysml|-> [options]

Computed by connectivityReport + signatureCensus (src/api/analytics.ts). With --json the answer is published under connectivity, beside ok and file.

Exit codes. 0 clean · 1 the model did not load cleanly (the report is of what parsed) · 2 usage/IO error.

where-used

What breaks if I change this element?

npm run sysprose -- where-used <file.sysml|-> [options]

Computed by impactClosure (src/api/analytics.ts). With --json the answer is published under whereUsed, beside ok and file.

Exit codes. 0 clean · 1 the model did not load cleanly (the report is of what parsed) · 2 usage/IO error.

orphans

What did I declare and never use?

npm run sysprose -- orphans <file.sysml|-> [options]

No flags of its own.

Computed by orphanReport (src/api/analytics.ts). With --json the answer is published under orphans, beside ok and file.

Exit codes. 0 clean · 1 the model did not load cleanly (the report is of what parsed) · 2 usage/IO error.

prompts

What guidance applies to the element I am working on?

npm run sysprose -- prompts <file.sysml|-> [options]

Computed by promptsFor (src/api/analytics.ts). With --json the answer is published under prompts, beside ok and file.

Exit codes. 0 clean · 1 the model did not load cleanly (the report is of what parsed) · 2 usage/IO error.

contracts

What does each requirement assume and guarantee, on which subject, honoured by which part?

npm run sysprose -- contracts <file.sysml|-> [options]

Computed by contractReport (src/api/verification.ts). With --json the answer is published under contracts, beside ok and file.

Exit codes. 0 clean · 1 the model did not load cleanly (the report is of what parsed) · 2 usage/IO error.

obligations

What must be shown, over which axioms, and what do the unit gates refuse?

npm run sysprose -- obligations <file.sysml|-> [options]

Computed by obligationsReport (src/api/verification.ts). With --json the answer is published under obligations, beside ok and file.

Exit codes. 0 clean · 1 the model did not load cleanly (the report is of what parsed) · 2 usage/IO error.

property-draft

How do I write a clause this tool will accept, over which names?

npm run sysprose -- property-draft <file.sysml|-> [options]

Computed by propertyDraft (src/api/property.ts). With --json the answer is published under propertyDraft, beside ok and file.

Exit codes. 0 clean · 1 the model did not load cleanly (the report is of what parsed) · 2 usage/IO error.

property-check

Would this clause pass the gates, and what does it actually say?

npm run sysprose -- property-check <file.sysml|-> [options]

Computed by propertyCheck (src/api/property.ts). With --json the answer is published under propertyCheck, beside ok and file.

Exit codes. 0 clean · 1 the model did not load cleanly (the report is of what parsed) · 2 usage/IO error.

verify

Does each obligation hold, by which engine, and under what bound?

npm run sysprose -- verify <file.sysml|-> [options]

Computed by verifyModel (src/api/verification.ts). With --json the answer is published under verify, beside ok and file.

Exit codes. 0 every obligation discharged non-vacuously by the engine that was asked for — or every requirement set shown satisfiable — and there was at least one of them to decide · 1 at least one obligation refuted with every feature at its model value, or one requirement set nothing can satisfy · 2 usage/IO error, a degraded model, a model that states nothing to decide at all, or ANY inconclusive — a timeout, an unsupported construct, a relation not evaluable at the model's values, a vacuous obligation, an absent solver, or a refutation obtained under --free, which is a design the model admits rather than a violation of it.

consistency

Can all the requirements on this subject hold at once — and if not, which conflict?

npm run sysprose -- consistency <file.sysml|-> [options]

Computed by consistencyReport (src/api/verification.ts). With --json the answer is published under consistency, beside ok and file.

Exit codes. 0 every obligation discharged non-vacuously by the engine that was asked for — or every requirement set shown satisfiable — and there was at least one of them to decide · 1 at least one obligation refuted with every feature at its model value, or one requirement set nothing can satisfy · 2 usage/IO error, a degraded model, a model that states nothing to decide at all, or ANY inconclusive — a timeout, an unsupported construct, a relation not evaluable at the model's values, a vacuous obligation, an absent solver, or a refutation obtained under --free, which is a design the model admits rather than a violation of it.

refine

Do the component contracts entail the system contract, and is every component assumption discharged?

npm run sysprose -- refine <file.sysml|-> [options]

Computed by refinementReport (src/api/verification.ts). With --json the answer is published under refinement, beside ok and file.

Exit codes. 0 every decomposition or derivation chain the --via family reads was shown to refine — for a decomposition, obligation (3) proved and every component assumption discharged; for a derive/refine chain, every derived requirement shown to assume no more than its parent and the set shown to entail the parent's guarantee — over a satisfiable contract set, and there was at least one of them to decide · 1 at least one obligation refuted, with a counterexample this tool re-read and confirmed: the component contracts admit an implementation that breaks the system contract, or the derived requirements admit one that breaks the requirement they were written from · 2 usage/IO error, a degraded model, a model that states no decomposition or derivation chain the --via family can read, or ANY undecided group — a timeout, an absent solver, a clause a gate refused, or a contract set that is vacuous, which is never laundered into a pass. A refinement obligation reads no feature value and there is no --free here.

bounds

What is the tightest value this measure can take under the model’s axioms?

npm run sysprose -- bounds <file.sysml|-> [options]

Computed by boundsReport (src/api/verification.ts). With --json the answer is published under bounds, beside ok and file.

Exit codes. 0 every bound asked for was DECIDED — an optimum whose optimality z3's νZ established, an exact supremum or infimum it proved is approached and never attained, or an unboundedness it proved under the axioms that were asserted · 2 usage/IO error, a degraded model, or any bound that was not decided — a value νZ does not certify as the tightest (nonlinear), a timeout, an absent solver, an axiom set that cannot hold together, or a measure no relation in the model reads. There is no exit 1: a bound is what the axioms admit and not a verdict, and there is no --allow-inconclusive here.

fault-tree

Which combinations of contract failures break the top requirement?

npm run sysprose -- fault-tree <file.sysml|-> [options]

Computed by faultTreeReport (src/api/verification.ts). With --json the answer is published under faultTree, beside ok and file.

Exit codes. 0 every fault tree the model states was enumerated to its order bound and none of them has a single point of failure — every order-1 check decided and none of them broken — and there was at least one tree to enumerate · 1 at least one sub-contract whose failure ALONE breaks the top requirement, with a counterexample this tool re-read and confirmed, or a top event that is already open with every sub-contract honoured · 2 usage/IO error, a degraded model, a model that states no decomposition to inject a failure into, a state machine whose failure modes this command found none of (or found and does not inject), or ANY undecided check — a timeout, an absent solver, a clause a gate refused, or a contract set that is vacuous, which is reported as vacuous and never as "no cut set". A cut set of order 2 or above is what redundancy looks like from the failure side, so it does not spend the 1; every absence is bounded by the order it was checked to and higher orders are not explored. A cut set reads no feature value: there is no --free here, and no --allow-inconclusive either, because an undecided order-1 check is exactly the state a "no single point of failure" sentence may never be written over.

evidence-status

What was shown, by which tool, over which model — and is it still valid?

npm run sysprose -- evidence-status <file.sysml|-> [options]

No flags of its own.

Computed by evidenceStatus (src/api/evidence.ts). With --json the answer is published under evidenceStatus, beside ok and file.

Exit codes. 0 clean · 1 the model did not load cleanly (the report is of what parsed) · 2 usage/IO error.

evidence-attach

Write the records of a verify run into the file, as annotations on what they are about

npm run sysprose -- evidence-attach <file.sysml|-> [options]

Computed by attachEvidence (src/api/evidence.ts). With --json the answer is published under evidenceAttach, beside ok and file.

Exit codes. 0 written · 2 usage/IO error, or a model that did not load cleanly — a degraded model is refused rather than partially rewritten, so there is no exit 1.

evidence-detach

Take every evidence record back off the file, and the verdict facets with them

npm run sysprose -- evidence-detach <file.sysml|-> [options]

No flags of its own.

Computed by detachEvidence (src/api/evidence.ts). With --json the answer is published under evidenceDetach, beside ok and file.

Exit codes. 0 written · 2 usage/IO error, or a model that did not load cleanly — a degraded model is refused rather than partially rewritten, so there is no exit 1.

reach

Which states are reachable, which transitions are dead, where did the simulator hide a choice?

npm run sysprose -- reach <file.sysml|-> [options]

Computed by reachReport (src/semantics/mc/explore.ts). With --json the answer is published under reach, beside ok and file.

Exit codes. 0 clean · 1 the model did not load cleanly (the report is of what parsed) · 2 usage/IO error.

check-behaviour

Does this behaviour pattern hold on every reachable configuration, and can this design reach the situation I name?

npm run sysprose -- check-behaviour <file.sysml|-> [options]

Computed by behaviourReport (src/semantics/mc/patterns.ts). With --json the answer is published under behaviour, beside ok and file.

Exit codes. 0 every ASSERTION stated on this machine was shown to hold on every reachable configuration, over a graph this walk saw whole, and every cover stated on it was witnessed on a run this walk saw, and there was at least one of them to decide · 1 at least one property refuted, with a witness trace of a run this semantics admits — or a recovery assertion some reachable configuration cannot discharge, reported as that set rather than as a run — or, under --cover-required, a cover this walk did not witness on any run it saw whole · 2 usage/IO error, a degraded model, a machine that states no property at all, or ANY undecided property — a bound the walk hit, a trigger the machine names that the walk never offered with no bound hit (verification/trigger-not-offered), a construct this engine does not explore, a witness the interpreter does not take (verification/witness-not-replayed), a recovery withheld because the interpreter’s chase budget stops a run somewhere that does not hold p (verification/recovery-budget-withheld), a liveness pattern no bad-prefix search decides, a property that could not be read, an atom that names nothing, or a vacuous one, which is never laundered into a pass — or a cover property whose behaviour this walk did not find on any run it saw whole, which is a missing behaviour and not a violated requirement — --cover-required spends the 1 for it instead. There is no solver in this lane and no --free: the walk reads the model’s own values.

trace relationship presets

A preset names the relationship kinds only. The row and column metaclasses are read off the model's own edges, because satisfy links a PartUsage to a RequirementDefinition in one model and to a RequirementUsage in the next, and a matrix that silently reports zero rows for the second shape is worse than no command at all. --from / --to override the derived axes; an override naming a metaclass the model has none of is refused rather than honoured into an empty matrix.

npm run check

npm run check -- <file.sysml> [more files…] [options]
cat model.sysml | npm run check -- -

Exit codes: 0 clean · 1 at least one file has findings (errors, or warnings with --strict) · 2 usage/IO error — and this is NOT sysprose's contract. check judges: a file that parsed perfectly and broke one validation rule loaded cleanly and still exits 1. sysprose reports, so its exit 1 is about the model, not the findings.

Parses each file, binds the bundled standard library, and runs the validation rules; - reads stdin, as with sysprose. Every finding carries a stable code, a source range (line, column and offset, start and end) and a one-line hint; parser errors also carry expected and found. Branch on code, never on message — see DIAGNOSTIC-CODES.md.

22 subcommands. Generated from scripts/lib/sysprose-spec.ts.