Check asserted constraints from Python

New in v0.11.0

A model can state what must hold as an assert constraint inside a definition. evaluation checks those statements against the instances that bind concrete values, from a script, and returns one verdict per instance and constraint. Use it when you want the check inside your own Python workflow: a report, a pre-commit hook, a test. The Solver answers the same question from the command line and, unlike this package, also covers values the model leaves open.

You need a model loaded with load_model and an assert constraint whose feature references resolve to values on the instance being checked.

Example

The model defines a wheel with a mass limit and a car with four wheels, three of which bind a mass. Save it as example_model.sysml:

package WheelBudget {
  private import ScalarValues::Real;

  part def Wheel {
    attribute mass : Real;
    assert constraint massLimit { mass < 20.0 }
  }

  part def Car {
    // Each wheel binds its own mass, so the constraint can be checked
    // for it.
    part frontLeft : Wheel {
      :>> mass = 12.0;
    }
    part spare : Wheel {
      :>> mass = 25.0;
    }
    part built : Wheel = new Wheel(mass = 7.0);

    // No value is bound, so nothing can be concluded for this wheel.
    part unknown : Wheel;
  }
}

Checking is one call. check_model evaluates every assertion against every usage it applies to and returns the results as a list. Save the script beside the model as check_constraints.py:

import pathlib

import syside
from syside import evaluation

EXAMPLE_DIR = pathlib.Path(__file__).parent
MODEL_FILE_PATH = EXAMPLE_DIR / "example_model.sysml"


def main() -> None:
    (model, diagnostics) = syside.load_model([MODEL_FILE_PATH])
    assert not diagnostics.contains_errors(warnings_as_errors=True)

    # Every `assert constraint`, checked against every instance it applies to.
    results = evaluation.check_model(model)

    for result in results:
        print(f"{result.verdict.name}: {result.usage.qualified_name}")


if __name__ == "__main__":
    main()

Run python check_constraints.py and it prints:

HOLDS: WheelBudget::Car::frontLeft
VIOLATED: WheelBudget::Car::spare
HOLDS: WheelBudget::Car::built
UNDECIDABLE: WheelBudget::Car::unknown

spare is reported because 25 is not below 20. built is checked through its constructor, new Wheel(mass = 7.0), so a value passed to new counts as bound. unknown binds nothing, and the verdict says so instead of passing it.

Reading a verdict

Each ConstraintResult carries the usage, the assertion, a verdict, the raw value the compiler returned, and a detail string that explains the verdict when it is not a plain yes or no. For unknown above, detail reads “cannot determine whether the constraint holds for all instances of WheelBudget::Car::unknown: ‘mass’ (has no value binding) …”.

Verdict	Meaning
HOLDS	The constraint evaluated to true for this instance.
VIOLATED	The constraint evaluated to false for this instance.
UNDECIDABLE	The constraint could not be reduced to a single boolean for this instance: a referenced feature has no value, or the expression is outside what Compiler.evaluate can compute. detail names the cause.
UNSUPPORTED	The usage both constructs a value with new and overrides it with bindings in its body. No single scope reflects the merged value, so the package refuses to guess.

A constraint is never reported as holding by default: anything the compiler cannot decide is UNDECIDABLE, so a script that only looks for VIOLATED should also count UNDECIDABLE results, or it will miss the constraints it did not check.

Checking one usage

check_usage takes a single usage and returns the results for the assertions that apply to it. It differs from check_model in one respect: an unsupported usage raises UnsupportedUsageError instead of producing an UNSUPPORTED result, so a caller that asked about one specific usage is told rather than handed a verdict it might overlook.

Limits

• The evaluable fragment is that of Compiler.evaluate: model-level evaluable expressions as the SysML v2 specification defines them. Constraints outside it come back UNDECIDABLE.

• Instances are checked one at a time with the values they bind. To ask whether a constraint holds for every value the model allows, use the Solver.

• check_model scans every usage in the model, so its cost grows with model size times the number of assertions. It is meant for whole-file checks, not for a loop that runs on every edit.