Reading 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:

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

    • "assertions" (from check): a list of assertions, each with a status of satisfied, violated (with a counterexample), or unanalyzable (with a reason; see Handling unsupported syntax).

    • "predicate" (from check --predicate): a single status – satisfied, violated (with a trace when the model has behavior over time), or unknown when the Solver could neither prove nor refute the predicate (see Exploring state machine reachability).

    • "attainable_set" (from evaluate): a list of values, each with a witness, plus exhaustive saying whether the list is complete.

    • "approximated" (from evaluate on a model with time-varying behavior): values proven reachable within the explored depth; see Exploring state machine reachability.

  • result.determination – 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; unknown means the Solver could not analyze enough of the model to say.

  • result.causes – when the answer is not a single determined value, this names the open values responsible, with file/line spans pointing at the declarations that left them open.

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

  • exit_code – also the process exit code: 0 for a clean answer, 1 for a violated check, 2 for a model or query that could not be analyzed.

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, brew install jq; on Linux, it is in every major package manager.

One line per assertion (works on any check run):

syside solver check -i pump.sysml | jq -r \
    '.result.outcome.assertions[] | "\(.status)\t\(.name)"'

satisfied   Pump::flowOk
violated    Pump::pressureOk

Just the counterexample of every violated assertion:

syside solver check -i pump.sysml | jq -r \
    '.result.outcome.assertions[] | select(.status == "violated")
     | .counterexample.values[] | "\(.[0]) = \(.[1])"'

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.values[].value'

3/2
2
3

Without jq: PowerShell

Windows PowerShell can parse JSON with no extra installation:

syside solver check -i pump.sysml | ConvertFrom-Json |
    ForEach-Object { $_.result.outcome.assertions } |
    Format-Table name, status

name             status
----             ------
Pump::flowOk     satisfied
Pump::pressureOk violated

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