Check that requirements hold

syside solver check answers a yes/no question: does a condition hold in every situation the model allows? It reports which truth values the condition can take. If false is impossible, the condition holds. If false is possible, the Solver hands you a witness for it, a concrete assignment of values under which the condition fails.

“Every situation the model allows” matters when the model leaves values open. If an attribute has no fixed value, the Solver does not pick one for you: the condition only holds if it holds no matter what that value turns out to be.

Checking the assertions written in the model

The most common way to use check is to write the conditions into the model as assert constraint elements. Create pump.sysml:

package Pump {
    private import ScalarValues::Integer;
    part pump [1] {
        attribute flowRate : Integer = 40;
        attribute pressure;
    }
    assert constraint flowOk { pump.flowRate <= 50 }
    assert constraint pressureOk { pump.pressure <= 10 }
}

Note the difference between the two attributes: flowRate is fixed at 40, but pressure is left open. The model says the pump has a pressure, not what it is.

Run:

syside solver check -i pump.sysml

{
  "result": {
    "subject": "Pump",
    "expression": "assertions[2]",
    "determination": "determined",
    "outcome": {
      "shape": "assertions",
      "assertions": [
        {
          "name": "Pump::flowOk",
          "outcome": {
            "shape": "attainable_set",
            "attainable": {
              "values": [
                {
                  "value": "true",
                  "witness": {
                    "values": [["Pump::pump.flowRate", "40"]],
                    "value": "true"
                  }
                }
              ],
              "exhaustive": "true"
            },
            "unattainable": { "values": ["false"], "exhaustive": "true" }
          }
        },
        {
          "name": "Pump::pressureOk",
          "outcome": {
            "shape": "attainable_set",
            "attainable": {
              "values": [
                {
                  "value": "false",
                  "witness": {
                    "values": [["Pump::pump.pressure", "11"]],
                    "value": "false"
                  }
                },
                {
                  "value": "true",
                  "witness": {
                    "values": [["Pump::pump.pressure", "0"]],
                    "value": "true"
                  }
                }
              ],
              "exhaustive": "true"
            },
            "unattainable": { "values": [], "exhaustive": "true" }
          }
        }
      ]
    },
    "causes": []
  },
  "warnings": [],
  "fail_when": "false_attainable",
  "exit_code": 1
}

  • flowOk holds: false is unattainable, because 40 is at most 50, always.

  • pressureOk can fail: false is attainable. Since the model never fixes pressure, nothing stops it from being 11, and the witness of false says exactly that. true is attainable too (a pressure of 0), so the condition is not necessarily violated either.

This is the check doing its job. A human reader might assume the pressure will be fine. The Solver points out that the model, as written, does not guarantee it. To fix it you would either give pressure a value in the model or constrain its range.

Changed in version 1.0.0: Before 1.0.0, each assertion carried a status (satisfied or violated) and a counterexample instead of its own outcome. See Read the solver’s output.

Checking one assertion, or an ad-hoc condition

To check a single assertion by its qualified name:

syside solver check -i pump.sysml --name Pump::flowOk

To check a condition you have not written into the model, pass it inline with --predicate:

syside solver check -i pump.sysml --predicate "Pump::pump::flowRate < 45"

With --predicate, result.outcome is the condition’s own attainable set over true and false, rather than a list of assertions.

--name and --predicate cannot be combined. Without either, every in-model assertion is checked.

A condition that reads an attribute written more than once by assign (in an action that runs its assignments in sequence) has no single truth value, so --predicate refuses it with exit code 2:

{
  "error": { "code": "Lowering", "span": null, "message": "the checked predicate reads the written scalar(s) Valve::cycle.opening bare, which has no single truth value across snapshots; wrap it in `snapshots->forAll { in s; ... }` (must hold at EVERY snapshot) or `snapshots->exists { in s; ... }` (must hold at SOME snapshot)" },
  "exit_code": 2
}

Write the condition into the model instead, as an assert constraint inside the action that says which snapshots it covers:

package Valve {
    private import ScalarValues::Integer;
    private import ControlFunctions::*;
    action cycle {
        attribute opening : Integer;
        assign opening := 0;
        assign opening := 80;
        assert constraint withinRange {
            snapshots->forAll { in s; (s as cycle).opening <= 100 }
        }
    }
}

Checked as written, this assertion lists false as attainable and exits 1: by default, the specification lets a snapshot between the two writes hold a value the model never states. Add --alt-semantics sticky-writes (part of free, see Add assumptions) to make each written value hold until the next write, and withinRange then holds.

Which assertions are checked New in v1.0.0

Without --name or --predicate, check reports every assertion it finds in the model:

  • assert constraint with a body, at package level or inside a definition or usage.

  • assert constraint typed by a constraint definition, such as assert constraint typedOk : FlowLimit { in limit = 50; }. The Solver checks the definition’s expression with the parameters the usage binds. A parameter the usage leaves unbound is open.

  • assert not constraint, which must be false.

  • assert constraint inside a requirement definition, reported once for that definition and once for every requirement definition that specializes it.

  • An assertion declared in a part definition, reported once for the definition and once for every specializing definition and every part usage typed by it, each named by its context. For example, an assertion flowOk in part def Pump, inherited by part bigPump : Pump [1], appears as both Pumps::Pump::flowOk and Pumps::bigPump.flowOk, and --name Pumps::bigPump.flowOk checks only the second.

An assertion inside a state definition or a state is reported with an exhaustive of "unknown" and the reason “asserts inside state definitions are not yet supported”, and listed in warnings. Any other assertion the Solver cannot analyze is reported the same way, with its own reason, while every other assertion in the run is still checked (see Handle unsupported syntax).

Choosing what fails the check New in v1.0.0

By default check fails when false is attainable, that is, when the condition can be violated. --fail-when picks a different rule:

  • false-attainable (the default): fails when the condition can be violated.

  • not-exactly-true: fails when the condition is not known to hold in every situation the model allows, including when the Solver leaves a truth value undecided and when the model is inconsistent.

  • true-unattainable: fails only when the condition is necessarily violated, so true is impossible.

  • true-not-proven-attainable: fails when the condition is not known to be possible, including when the Solver leaves a truth value undecided and when the model is inconsistent.

For example, pressureOk above can fail, but it is not necessarily violated:

syside solver check -i pump.sysml --name Pump::pressureOk \
    --fail-when true-unattainable

This exits 0, and the output records the mode as "fail_when": "true_unattainable".

Use not-exactly-true in CI when an assertion the Solver could not analyze should fail the build as well (see Handle unsupported syntax).

Exit codes

check is built to run in scripts and CI pipelines:

  • 0: no checked condition fails the --fail-when mode

  • 1: at least one checked condition fails the --fail-when mode

  • 2: the model or the query could not be loaded

An assertion the Solver could not analyze does not by itself exit 1 under the default mode (see Handle unsupported syntax).

Options

check and evaluate share these options:

  • -i PATH, --input PATH: a SysML v2 model file, or a directory that contributes every .sysml and .kerml file at or below it. Repeat the option to load several inputs. All inputs load as one model.

  • -a LIST, --alt-semantics LIST: comma-separated assumptions (see Add assumptions).

  • -d N, --depth N: exploration depth for a model with an unbounded loop (see Explore state machine reachability).

  • --solver-limit N: the amount of work each solver step may use before the Solver stops it (see below).

  • --timeout SECONDS: a time limit for the whole run (see below).

check adds -n (--name), -p (--predicate) and -f (--fail-when). syside solver check --help lists them all.

Limiting how long a run takes New in v1.0.0

Some questions take the Solver a long time, or more work than it can finish. Two options stop it, and both apply to check and evaluate:

  • --solver-limit N caps the work of each individual solver step. The default is 10000000, and 0 removes the limit. The limit counts work, not time, so the same model and command give the same answers on any machine, for a given Solver release.

  • --timeout SECONDS caps the wall-clock time of the whole run, in seconds with up to three decimals (at least 0.001). Without it, there is no time limit. Results can differ between faster and slower machines, or on a machine under load.

When both are given, each step stops at whichever is reached first: its own --solver-limit, or what remains of the --timeout.

A step that is stopped never turns into a value. The listings it would have decided get an exhaustive of "unknown", with a reason naming the limit:

syside solver check -i pump.sysml --solver-limit 1

{
  "name": "Pump::flowOk",
  "outcome": {
    "shape": "attainable_set",
    "attainable": {
      "values": [],
      "exhaustive": "unknown",
      "reason": "solver limit exhausted: the check exceeded --solver-limit 1"
    },
    "unattainable": {
      "values": [],
      "exhaustive": "unknown",
      "reason": "solver limit exhausted: the check exceeded --solver-limit 1"
    }
  }
}

(Output truncated to the first assertion.)

With --timeout, the reason reads time limit of 0.001 s reached, with the time you gave. As for any assertion the Solver could not decide, the exit code stays 0 under the default --fail-when mode, and --fail-when not-exactly-true turns it into exit 1.

A value the options cannot take is a usage error with exit code 2, for example:

syside solver check: error: argument --timeout: must be at least 0.001 (1 ms); omit --timeout for no time limit

“Can it fail?” versus “which values are possible?”

check and evaluate report the same attainable set for a boolean expression. The difference is the exit code: evaluate exits 0 either way, while check exits by its --fail-when mode. Use evaluate to explore what is possible, and check to gate a script on it. See Evaluate possible values.