Read the solver’s output

In this release the Solver prints JSON to the terminal. A human-readable format is planned. Until it lands, this page tells you which fields to read and gives one-liners that reduce the output to a short summary.

The fields that matter

Every successful run prints one JSON object with these fields:

• result.outcome is the answer itself. Its shape field says how to read the rest:

  • "attainable_set" (from evaluate, and from check --predicate): the values the expression can take, in the two listings described below.

  • "approximated" (from a model with behavior that can run forever): the same two listings, computed within the explored depth. See Explore state machine reachability.

  • "assertions" (from check without --predicate): a list of assertions, each with its name and its own outcome in one of the two shapes above. An assertion’s outcome lists which of true and false the assertion can take.

• attainable and unattainable are the two listings in every outcome. Each has values, exhaustive and, when the Solver gave up, a reason:

  • attainable.values lists every value known to be possible, each with a witness (the values of the model’s features that produce it). On a model with behavior over time, a value carries a trace instead (the run that reaches it, snapshot by snapshot).

  • unattainable.values lists every value known to be impossible. For a boolean expression this is how “must be true” reads: an assertion that holds in every allowed situation has false in unattainable.values.

  • exhaustive says whether a listing is complete. "true" means no other value belongs in it. "false" means the listing is not complete, for example because --max-values cut it off or because the values cannot all be listed. "undetermined" means the method does not settle completeness, such as the bounded depth of a state machine exploration. "unknown" means the Solver gave up (for example, at a --solver-limit or --timeout, see Check that requirements hold), or the answer depends on part of the model it could not analyze, and reason says which.

• result.determination says whether the model pins the answer down. determined means the model has a single answer. undetermined means the answer varies with values the model leaves open. inconsistent means the model allows no situation at all, so there is no value to list. unknown means the Solver could not decide enough to say.

• result.causes names what kept the answer from being a single determined value. An unanalyzable entry carries the reasons a part of the model could not be analyzed (see Handle unsupported syntax). An unknown entry New in v1.0.0 names open values whose effect on the answer the Solver could not decide, with the reason, for example {"unknown": {"names": ["Battery::battery.cellB.voltage"], "reason": "solver limit exhausted: the check exceeded --solver-limit 1"}}.

• warnings lists the parts of the model the Solver had to skip, with reasons.

• alt_semantics appears when you pass --alt-semantics, and records every active override with its description. See Add assumptions.

• fail_when (from check) echoes the --fail-when mode that decided the exit code. See Check that requirements hold.

• exit_code is also the process exit code: 0 for an answer that passes, 1 for a check that fails its --fail-when mode, 2 for a model or query that could not be loaded.

A few fields appear only in specific outputs:

• A witness of a sum over a collection can carry a partitions field, listing for each collection how its members are grouped (members in one group are the same individual).

• A witness can carry an order field, listing the snapshots of a feature written more than once in the order they occur.

• A witness of a requirement can carry an unwritten_members entry, naming an open require or assume side whose unwritten members take the listed value.

• An outcome on a model with behavior over time carries integral, which says whether every listed value is an integer.

Changed in version 1.0.0: Before 1.0.0, a check assertion carried a status (satisfied, violated or unanalyzable) with a counterexample or a reason, and check --predicate used a "predicate" shape with a single status. An attainable set listed its values in values (or proven, for a state machine) and had no unattainable listing. A former satisfied is now false in unattainable.values. A former violated is false in attainable.values, and its witness replaces the counterexample. A former unanalyzable is an exhaustive of "unknown" with a reason.

Getting a short summary with jq

jq is a widely used command-line tool for slicing JSON. On Windows, install it with winget install jqlang.jq. On macOS, use brew install jq. On Linux, it is in every major package manager.

On Windows, set PYTHONUTF8 before piping the output into another program, so that the program receives UTF-8 text. In PowerShell, run $env:PYTHONUTF8 = "1". In Command Prompt, run set PYTHONUTF8=1. The setting lasts until you close that window.

The attainable truth values of each assertion, one line per assertion (works on any check run without --predicate):

syside solver check -i pump.sysml | jq -r \
    '.result.outcome.assertions[]
     | "\(.name): \(.outcome.attainable.values | map(.value) | join(","))"'

Pump::flowOk: true
Pump::pressureOk: false,true

An assertion that lists false can fail.

The witness of every assertion that can fail:

syside solver check -i pump.sysml | jq -r \
    '.result.outcome.assertions[] | .name as $n
     | .outcome.attainable.values[] | select(.value == "false")
     | .witness.values[] | "\($n): \(.[0]) = \(.[1])"'

Pump::pressureOk: Pump::pump.pressure = 11

Just the values from an evaluate run:

syside solver evaluate -i battery.sysml \
    --expr "Battery::battery.totalVoltage" | jq -r \
    '.result.outcome.attainable.values[].value'

-9
-8
-7
-6
-5
-4
-3
-2
-1
0

Without jq: PowerShell

Windows PowerShell can parse JSON with no extra installation. Run $env:PYTHONUTF8 = "1" first:

syside solver check -i pump.sysml | ConvertFrom-Json |
    ForEach-Object { $_.result.outcome.assertions } |
    Select-Object name, @{ Name = "attainable"; Expression = {
        ($_.outcome.attainable.values | ForEach-Object { $_.value }) -join "," } }

name             attainable
----             ----------
Pump::flowOk     true
Pump::pressureOk false,true

Keeping the full output

The JSON is a complete record of the run. For an audit trail, redirect it to a file and summarize from there:

syside solver check -i pump.sysml > check-result.json