Checking that requirements hold

syside solver check answers a yes/no question: does a condition hold in every situation the model allows? If yes, the check is satisfied. If no, the Solver reports it as violated and hands you a counterexample – 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 check only passes if the condition 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::pump::flowRate <= 50 }
    assert constraint pressureOk { Pump::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", "status": "satisfied",
          "counterexample": null },
        {
          "name": "Pump::pressureOk",
          "status": "violated",
          "counterexample": {
            "values": [
              ["Pump::pump::pressure", "11"]
            ]
          }
        }
      ]
    },
    "causes": []
  },
  "warnings": [],
  "exit_code": 1
}

• flowOk is satisfied: 40 is at most 50, always.

• pressureOk is violated: since the model never fixes pressure, nothing stops it from being 11 – and the counterexample says exactly that.

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 the violation you would either give pressure a value in the model or constrain its range.

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"

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

Exit codes

check is built to run in scripts and CI pipelines:

• 0 – every checked assertion is satisfied

• 1 – at least one assertion is violated

• 2 – the model could not be loaded or the query could not be analyzed

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

check asks whether a condition holds in every allowed situation. If instead you want to see which outcomes are possible – for example, “can this expression ever be true, and can it ever be false, and show me an example of each” – use syside solver evaluate with the same expression. See Evaluating possible values.