Handle unsupported syntax

The Solver covers a growing subset of SysML v2. When a model uses something outside that subset, the Solver does not fail the whole run: it analyzes what it can, skips what it cannot, and tells you exactly what was skipped and why. Nothing is guessed.

A partly analyzable model

Create mixed.sysml. The flow-rate check is fully supported. The diameter-match check relies on attributes whose type nothing in the model decides:

package Pump {
    private import ScalarValues::Integer;
    part pump [1] {
        attribute flowRate : Integer = 40;
        attribute inletDiameter;
        attribute outletDiameter;
        attribute matched = inletDiameter == outletDiameter;
    }
    assert constraint flowOk { pump.flowRate <= 50 }
    assert constraint portsMatched { pump.matched }
}

syside solver check -i mixed.sysml

{
  "result": {
    "subject": "Pump",
    "expression": "assertions[2]",
    "determination": "unknown",
    "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::portsMatched",
          "outcome": {
            "shape": "attainable_set",
            "attainable": { "values": [], "exhaustive": "unknown", "reason": "depends on 'Pump::pump.inletDiameter', ..." },
            "unattainable": { "values": [], "exhaustive": "unknown", "reason": "depends on 'Pump::pump.inletDiameter', ..." }
          }
        }
      ]
    },
    "causes": []
  },
  "warnings": [
    { "code": "Unimplemented", "span": null, "message": "'Pump::pump.inletDiameter' excluded from analysis ..." },
    { "code": "Unimplemented", "span": null, "message": "'Pump::pump.outletDiameter' excluded from analysis ..." }
  ],
  "fail_when": "false_attainable",
  "exit_code": 0
}

(The reason and message strings are shortened here. The real output carries them in full.)

How to read this:

  • flowOk was checked normally and holds (false is unattainable). Unsupported syntax elsewhere in the model did not block it.

  • portsMatched could not be analyzed: neither listing holds a value, and both have an exhaustive of "unknown". The reason says which element caused it and, where the Solver can tell, what to change (here: declare a type for the two diameters).

  • Each skipped element also appears in warnings, so skipped parts of the model are visible even when every remaining assertion holds.

  • determination is unknown: the run as a whole could not decide every assertion.

Changed in version 1.0.0: Before 1.0.0, such an assertion had a status of unanalyzable with a reason.

An assertion the Solver could not analyze is not a violation, so under the default --fail-when mode the exit code stays 0. If your CI should treat “could not check” as a failure, use the strict mode:

syside solver check -i mixed.sysml --fail-when not-exactly-true

This exits 1 unless every assertion must hold, so it fails the step when any assertion can be violated or could not be analyzed.

When the whole query is unsupported

If the expression you pass to evaluate --expr or check --predicate itself depends on an element the Solver could not analyze, the result has no values in either listing, both with an exhaustive of "unknown" and the same kind of reason, and result.causes carries an unanalyzable entry with the reasons. The exit code is 0 for evaluate, and for check under the default --fail-when mode:

syside solver evaluate -i mixed.sysml --expr "Pump::pump.matched"

{
  "result": {
    "subject": "Pump",
    "expression": "Pump::pump.matched",
    "determination": "unknown",
    "outcome": {
      "shape": "attainable_set",
      "attainable": { "values": [], "exhaustive": "unknown", "reason": "the query depends on 'Pump::pump.inletDiameter', ..." },
      "unattainable": { "values": [], "exhaustive": "unknown", "reason": "the query depends on 'Pump::pump.inletDiameter', ..." }
    },
    "causes": [
      {
        "unanalyzable": {
          "reasons": ["the query depends on 'Pump::pump.inletDiameter', ..."]
        }
      }
    ]
  },
  "warnings": [ "..." ],
  "exit_code": 0
}

(The reason strings are shortened and the warnings elided.)

Changed in version 1.0.0: Before 1.0.0, such a query printed an error object instead of a result and exited with code 2.

Common causes and fixes

  • Attribute has no declared type, and its uses do not decide one (as in the example above). Declare one: attribute inletDiameter : Real;.

  • A quantity attribute is missing its quantity type. Values with units need a declaration like : MassValue. See Compare values across units.

  • A package-level part usage without an explicit multiplicity. Write part rover [1] {...}, or see Add assumptions for the singular-usages override.

  • A transition with an effect (transition first Off do assign level := 1 then On;). The Solver does not analyze such a state machine yet. An answer that depends on an attribute the machine writes gets an exhaustive of "unknown", and the reason ends with “has an effect action (do ...), which is not supported”. Other machines in the model are still analyzed.

  • An assertion inside a state definition or a state. It is reported with the reason “asserts inside state definitions are not yet supported”, and every other assertion is still checked. Check that requirements hold lists the assertions the Solver checks.

  • The construct’s meaning is open in the specification. Some syntax the Solver refuses by default can be given a stated meaning with an override. Add assumptions lists them.