Check asserted constraints from Python

New in v0.11.0

A model can state what must hold as an assert constraint inside a definition. syside.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 four wheels, three of which bind a mass:

package WheelBudget {
  private import ScalarValues::Real;

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

  // Each wheel binds its own mass, so the constraint can be evaluated
  // 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;
}

check_model evaluates every assertion against every non-library usage it applies to:

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)

    # One result per (instance, assertion) pair, in model order.
    results = evaluation.check_model(model)

    for result in results:
        print(
            f"{result.verdict.name:<11} {result.instance.qualified_name} "
            f"against {result.assertion.qualified_name}"
        )
        if result.detail:
            print(f"            {result.detail}")

    violated = [
        result
        for result in results
        if result.verdict is evaluation.Verdict.VIOLATED
    ]
    print(f"\n{len(violated)} violated constraint(s)")


if __name__ == "__main__":
    main()

The script prints:

HOLDS       WheelBudget::frontLeft against WheelBudget::Wheel::massLimit
VIOLATED    WheelBudget::spare against WheelBudget::Wheel::massLimit
HOLDS       WheelBudget::built against WheelBudget::Wheel::massLimit
UNDECIDABLE WheelBudget::unknown against WheelBudget::Wheel::massLimit
            cannot determine whether the constraint holds for all instances of WheelBudget::unknown: 'mass' (has no value binding) -- each can be redefined by a type that specializes WheelBudget::unknown, so the verdict here need not hold for every type that specializes it

1 violated constraint(s)

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 instance, the assertion, a verdict, the raw value the compiler returned, and a detail string that is filled in when the verdict is not a plain yes or no.

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 instance 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 instance

check_instance 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 instance raises UnsupportedInstanceError instead of producing an UNSUPPORTED result, so a caller that asked about one specific instance 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.