Solver v0.10.3 Labs

Experimental feature

The Solver is a Labs feature. Its interface and output format may change in future releases. See Labs Labs for what the Labs designation means.

The Solver is a command-line tool that answers two questions about a SysML v2 model:

  • Does my requirement actually hold? You have written a constraint in your model, and you want the tool to confirm it – or to show you a concrete scenario where it fails. That is syside solver check.

  • What values can this attribute take? Your model fixes some values and leaves others open, and you want to see what a computed value can come out to. That is syside solver evaluate.

Unlike evaluating an expression in Python (see Essentials), the Solver does not need every value to be filled in. If your model leaves a value open – a battery voltage nobody has set yet, a component that may or may not override a default – the Solver considers every possibility the model allows, and tells you what can happen across all of them.

Try it in five minutes

Create a file named rover.sysml and paste the following model. It is a rover with four wheels, a payload, and a mass budget written as an assertion:

package Rover {
    private import NumericalFunctions::sum;
    part def Wheel {
        attribute mass = 12;
    }
    part rover [1] {
        part wheels : Wheel [4];
        attribute payloadMass = 30;
        attribute totalMass = sum(wheels.mass) + payloadMass;
    }
    assert constraint massBudget { Rover::rover::totalMass < 100 }
}

Open a terminal in the directory containing the file and run:

syside solver check -i rover.sysml

The Solver checks every assert constraint in the model and prints its verdict as JSON:

{
  "result": {
    "subject": "Rover",
    "expression": "assertions[1]",
    "determination": "determined",
    "outcome": {
      "shape": "assertions",
      "assertions": [
        { "name": "Rover::massBudget", "status": "satisfied",
          "counterexample": null }
      ]
    },
    "causes": []
  },
  "warnings": [],
  "exit_code": 0
}

The line to read is the one with "status": the mass budget is satisfied. Four wheels of 12 each plus a payload of 30 gives 78, which is below 100.

Now make the payload heavier. Change payloadMass = 30 to payloadMass = 60 in rover.sysml, and run the same command again:

{
  "result": {
    "subject": "Rover",
    "expression": "assertions[1]",
    "determination": "determined",
    "outcome": {
      "shape": "assertions",
      "assertions": [
        {
          "name": "Rover::massBudget",
          "status": "violated",
          "counterexample": {
            "values": [
              ["Rover::rover::totalMass", "108"]
            ]
          }
        }
      ]
    },
    "causes": []
  },
  "warnings": [],
  "exit_code": 1
}

The budget is now violated, and the counterexample shows why: the total mass comes out to 108. The command also exits with code 1 instead of 0, so a script or CI job running the check fails automatically.

That is the core loop: write what must hold as an assert constraint in the model, run syside solver check, and read the status.

Note

In this release the Solver prints JSON only. Human-readable terminal output is planned; until then, Reading the Solver’s output shows which fields to read and gives copy-paste one-liners that reduce the output to a short summary.

Where to go next

Each page below starts from a question you might bring to the tool: