evaluation

Description

syside.evaluation: evaluate asserted constraints at the usages of a model.

This package checks whether the assert constraint { ... } constraints in a model actually hold for the usages that should satisfy them. It is built on syside.Compiler.evaluate(), which defines exactly which constraints can be checked; a constraint it cannot evaluate is reported Verdict.UNDECIDABLE rather than silently passed.

The public surface is small:

• check_model(): check every constraint against every usage in the user model (a usage in whose scope some value the constraint reads has no = binding, declared or inherited, is reported UNDECIDABLE, not skipped).

• check_usage(): check the constraints applying to one usage.

• evaluate_assertion(): evaluate one assertion in an explicit scope.

• ConstraintResult / Verdict: the result type (HOLDS, VIOLATED, UNDECIDABLE, or UNSUPPORTED).

Index

Classes

ConstraintResult		One (usage, assertion) pair and the verdict for it.
UnsupportedUsageError		Raised for a usage whose value this module cannot yet evaluate without risk of a wrong verdict.

Functions

check_usage		Check every constraint that applies to a single usage.
check_model		Check every constraint assertion in the user model, library packages included.
evaluate_assertion		Evaluate one assert constraint against scope and classify the result.

Enumerations

Verdict

The outcome of evaluating one asserted constraint against one usage.

---

Functions

check_usage(usage: syside.Usage, *, compiler: syside.Compiler | None = None) → list[syside.evaluation.ConstraintResult]

Check every constraint that applies to a single usage.

The evaluation scope is chosen so the usage’s bindings are native:

• if usage is written new Def(...) (its feature value is a syside.ConstructorExpression), the constructor is evaluated to its constructed object and that object’s scope is used;

• otherwise the usage’s own scope is used, where declarative bindings (redefinitions, feature values) already resolve.

Returns one ConstraintResult per applicable assertion. A usage with no applicable assertions yields an empty list. If a new Def(...) value cannot itself be evaluated, each of the definition’s assertions is reported Verdict.UNDECIDABLE rather than skipped.

Raises:

UnsupportedUsageError – if usage both constructs a value and overrides it with declarative bindings in its body, a shape whose merged effective value this module cannot yet evaluate without risk of a wrong verdict (see UnsupportedUsageError). Raising, rather than returning a verdict, prevents a silently wrong result.

Cost is linear in the usage’s feature count to find the applicable assertions, plus one syside.Compiler.evaluate() per assertion (and one more to evaluate the constructor, if any); the evaluate calls dominate.

check_model(model: syside.Model, *, compiler: syside.Compiler | None = None) → list[syside.evaluation.ConstraintResult]

Check every constraint assertion in the user model, library packages included.

Iterates every usage in the user model, the contents of the workspace’s own library package namespaces included, so an assertion in your own library is checked like any other. The SysML/KerML standard libraries are outside the scanned documents and are not checked. For each usage this evaluates the assertions that apply to it via check_usage(). Usages that carry no applicable assertion contribute nothing. The result is flat, in model-traversal order; callers typically filter for Verdict.VIOLATED to report problems and Verdict.UNDECIDABLE to report what could not be checked.

Unlike check_usage(), this never raises UnsupportedUsageError: a usage with an unsupported shape is recorded as Verdict.UNSUPPORTED (one result per applicable assertion) so a single such usage does not abort the scan or discard the verdicts already collected.

Note

This scans all usages, so cost is linear in model size times the per- usage evaluation cost. It is intended for whole-file checking (e.g. an on-save lint), not for hot loops.

evaluate_assertion(assertion: syside.AssertConstraintUsage, scope: syside.Type, *, compiler: syside.Compiler, usage: syside.Usage | None = None) → syside.evaluation.ConstraintResult

Evaluate one assert constraint against scope and classify the result.

scope must be a type in which the constraint’s feature references resolve to bound values: typically a constructed object (see check_usage()) or a usage carrying declarative bindings.

usage is the usage recorded on the result as the subject being checked. It is distinct from scope because the scope of a new Def(...) usage is the ephemeral constructed object, not the usage the modeller wrote; pass the original usage so the result points back at the source. When omitted it defaults to scope (correct for the declarative path, where the usage is its own scope).

The result is one of Verdict.HOLDS, Verdict.VIOLATED, or Verdict.UNDECIDABLE (never Verdict.UNSUPPORTED, which only check_model() records). A body the compiler cannot reduce, or one that reduces to anything other than a single bool (for example a collection, a number, or None), is Verdict.UNDECIDABLE, never reported as holding. assert not negation is applied to a concrete boolean only.

Cost is one syside.Compiler.evaluate() call, which dominates; the surrounding classification is O(1).

Enumerations

class Verdict

The outcome of evaluating one asserted constraint against one usage.

HOLDS ¶	The outcome of evaluating one asserted constraint against one usage.
VIOLATED ¶	The outcome of evaluating one asserted constraint against one usage.
UNDECIDABLE ¶	The outcome of evaluating one asserted constraint against one usage.
UNSUPPORTED ¶	The outcome of evaluating one asserted constraint against one usage.