Requirement Satisfaction Evaluation

Hello,

I’m currently testing how to use the syside python commands to evaluate the satisfaction of a requirement by one of the PartUsages of the model.

I have taken the OMG example code (very slightly modified):

private import SI::*;
package 'OMG Requirement Example' {
    part def Vehicle {
        attribute dryMass : MassValue;
        attribute fuelMass : MassValue;
        attribute fuelFullMass : MassValue;
    }
    part vehicle_c1 : Vehicle {
        attribute :>> dryMass = 1500 [kg];
        attribute :>> fuelMass = 20 [kg];
        attribute :>> fuelFullMass = 40 [kg];
        satisfy vehicleSpecification;
    }
    requirement vehicleSpecification {
        doc
        /* Overall vehicle requirements group */
        subject vehicle : Vehicle;
        require fullVehicleMassLimit;
        require emptyVehicleMassLimit;
    }
    requirement def MassLimitationRequirement {
        doc
        /* The actual mass shall be less than or equal to the required mass. */
        attribute massActual : MassValue;
        attribute massReqd : MassValue;
        require constraint { massActual <= massReqd }
    }
    requirement def <'1'> VehicleMassLimitationRequirement :> MassLimitationRequirement {
        doc
        /* The total mass of a vehicle shall be less than or equal to the required mass. */
        subject vehicle : Vehicle;
        attribute :>> massActual = vehicle.dryMass + vehicle.fuelMass;
        assume constraint { vehicle.fuelMass > 0 [kg] }
    }
    requirement <'1.1'> fullVehicleMassLimit : VehicleMassLimitationRequirement {
        subject vehicle : Vehicle;
        attribute :>> massReqd = 2000 [kg];
        assume constraint {
            doc
            /* Fuel tank is full. */
            vehicle.fuelMass == vehicle.fuelFullMass
        }
    }
    requirement <'1.2'> emptyVehicleMassLimit : VehicleMassLimitationRequirement {
        subject vehicle : Vehicle;
        attribute :>> massReqd = 1500 [kg];
        assume constraint {
            doc
            /* Fuel tank is empty. */
            vehicle.fuelMass == 0 [kg]
        }
    }
}

Is there a way to verify the SatisfyRequirementUsage in the part vehicle_C1:

‘OMG Requirement Example’::vehicle_c1::(anonymous SatisfyRequirementUsage)

with a Boolean (true/false) result?

Hi,

It is possible but there is currently no high-level interface for this.

  1. As SatisfyRequirementUsage does not have a bound subject and semantic rules don’t require this, it needs to be changed to satisfy vehicleSpecification by vehicle_c1;. This will bind inherited vehicle used in constraint expressions to vehicle_c1.

  2. Nested requirements do not implicitly receive parent subject, these need to be overridden as

    requirement vehicleSpecification {
        doc
        /* Overall vehicle requirements group */
        subject param : Vehicle;
        require fullVehicleMassLimit { in sub = param; }
        require emptyVehicleMassLimit { in sub = param; }
    }
    

    Due to name resolution rules, parent requirement cannot use vehicle and use it as value in nested requirement as vehicle would instead resolve to inherited feature. Additionally, grammar does not allow subjects in such requirement usages, likely an oversight from the spec. Lastly, that seems like it may work but it is a library feature and the spec does not have special handling for it unlike self.

  3. Syside does not yet support user-functions so result expressions need to be evaluated manually. Additionally, quantities require experimental_quantities flag to evaluate.

The full script:

import syside

model, _ = syside.load_model(
    sysml_source="""\
private import SI::*;
package 'OMG Requirement Example' {
    part def Vehicle {
        attribute dryMass : MassValue;
        attribute fuelMass : MassValue;
        attribute fuelFullMass : MassValue;
    }
    part vehicle_c1 : Vehicle {
        attribute :>> dryMass = 1500 [kg];
        attribute :>> fuelMass = 20 [kg];
        attribute :>> fuelFullMass = 40 [kg];
        satisfy vehicleSpecification by vehicle_c1;
    }
    requirement vehicleSpecification {
        doc
        /* Overall vehicle requirements group */
        subject param : Vehicle;
        require fullVehicleMassLimit { in sub = param; }
        require emptyVehicleMassLimit { in sub = param; }
    }
    requirement def MassLimitationRequirement {
        doc
        /* The actual mass shall be less than or equal to the required mass. */
        attribute massActual : MassValue;
        attribute massReqd : MassValue;
        require constraint { massActual <= massReqd }
    }
    requirement def <'1'> VehicleMassLimitationRequirement :> MassLimitationRequirement {
        doc
        /* The total mass of a vehicle shall be less than or equal to the required mass. */
        subject vehicle : Vehicle;
        attribute :>> massActual = vehicle.dryMass + vehicle.fuelMass;
        assume constraint { vehicle.fuelMass > 0 [kg] }
    }
    requirement <'1.1'> fullVehicleMassLimit : VehicleMassLimitationRequirement {
        subject vehicle : Vehicle;
        attribute :>> massReqd = 2000 [kg];
        assume constraint {
            doc
            /* Fuel tank is full. */
            vehicle.fuelMass == vehicle.fuelFullMass
        }
    }
    requirement <'1.2'> emptyVehicleMassLimit : VehicleMassLimitationRequirement {
        subject vehicle : Vehicle;
        attribute :>> massReqd = 1500 [kg];
        assume constraint {
            doc
            /* Fuel tank is empty. */
            vehicle.fuelMass == 0 [kg]
        }
    }
}
"""
)


def source_of(element: syside.Element) -> str:
    if (text_doc := element.document.text_document) and (cst := element.cst_node):
        with text_doc.lock() as source_text:
            return cst.text(source_text.text)
    return str(element)


def evaluate_satisfaction(vehicle: syside.PartUsage) -> None:
    req = vehicle.children.elements[-1].cast(syside.SatisfyRequirementUsage)
    compiler = syside.Compiler()

    for mem in req.feature_memberships.collect():
        if not isinstance(mem, syside.RequirementConstraintMembership):
            continue

        outer = mem.owned_constraint
        assert outer, "Invariant violated"
        print(f"#. {outer}")

        # Syside does not yet support user-functions thus we need to evaluate
        # result expressions manually within correct scope. However, doing it
        # this way will lose invoked function scope, therefore we manually
        # override parameters to correct values and use the invoked function as
        # the scope.
        outer.children.elements[0].cast(
            syside.Usage
        ).feature_value_member.set_member_element(syside.FeatureReferenceExpression)[
            1
        ].referent_member.set_member_element(vehicle)

        for inner in outer.feature_memberships.collect():
            if not isinstance(inner, syside.RequirementConstraintMembership):
                continue

            constraint = inner.owned_constraint
            assert constraint, "Invariant violated"

            expr = constraint.result_expression
            if not expr:
                continue

            value, report = compiler.evaluate(
                expr, scope=outer, experimental_quantities=True
            )

            if not report:
                print(f"  - `{source_of(expr)}` failed: {report.diagnostics}")
                continue
            print(f"  - `{source_of(expr)}` -> {value}")


with model.user_docs[0].lock() as doc:
    evaluate_satisfaction(
        doc.root_node["OMG Requirement Example"]
        .cast(syside.Namespace)["vehicle_c1"]
        .cast(syside.PartUsage)
    )

outputs:

#. 'OMG Requirement Example'::vehicleSpecification::fullVehicleMassLimit
  - `vehicle.fuelMass == vehicle.fuelFullMass` -> False
  - `vehicle.fuelMass > 0 [kg]` -> True
  - `massActual <= massReqd` -> True
#. 'OMG Requirement Example'::vehicleSpecification::emptyVehicleMassLimit
  - `vehicle.fuelMass == 0 [kg]` -> False
  - `vehicle.fuelMass > 0 [kg]` -> True
  - `massActual <= massReqd` -> False

Hello Daumantas,

many thanks for the quick repply.

Unfortunately the flag “experimental_quantities=True” is not working on my side. Using it leads to the following error:

File "/Users/alejandronietocuatenta/Documents/sysmlv2_omg_introduction/omg_requirements_example/syside_full_reply.py", line 103, in evaluate_satisfaction
    value, report = compiler.evaluate(
                    ~~~~~~~~~~~~~~~~~^
        expr, scope=outer, experimental_quantities=True
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
        # expr, scope=outer
        ^^^^^^^^^^^^^^^^^^^
    )
    ^
TypeError: evaluate(): incompatible function arguments. The following argument types are supported:
    1. evaluate(self, expr: syside.core.Expression, stdlib: syside.core.Stdlib | None = None, scope: syside.core.Type | None | None = None) -> tuple[int | float | bool | syside.core.Infinity | str | range | syside.core.Element | syside.core.BoundMetaclass | None | list[int | float | bool | syside.core.Infinity | str | range | syside.core.Element | syside.core.BoundMetaclass | None] | None | None, syside.core.CompilationReport]

Invoked with types: syside.core.Compiler, syside.core.OperatorExpression, kwargs = { scope: syside.core.ConstraintUsage, experimental_quantities: bool }

I can simply remove it and the script wiil now work,

value, report = compiler.evaluate(
                # expr, scope=outer, experimental_quantities=True
                expr, scope=outer
            )

but then I’ll got a different kind of error in the output. The one associated with unsupported-operators:

#. 'OMG Requirement Example'::vehicleSpecification::fullVehicleMassLimit
  - `vehicle.fuelMass == vehicle.fuelFullMass` failed: [<source>:10:34: error (unsupported-operator): Operator '[' is not model-level evaluable]
  - `vehicle.fuelMass > 0 [kg]` failed: [<source>:10:34: error (unsupported-operator): Operator '[' is not model-level evaluable]
  - `massActual <= massReqd` failed: [<source>:9:33: error (unsupported-operator): Operator '[' is not model-level evaluable]
#. 'OMG Requirement Example'::vehicleSpecification::emptyVehicleMassLimit
  - `vehicle.fuelMass == 0 [kg]` failed: [<source>:10:34: error (unsupported-operator): Operator '[' is not model-level evaluable]
  - `vehicle.fuelMass > 0 [kg]` failed: [<source>:10:34: error (unsupported-operator): Operator '[' is not model-level evaluable]
  - `massActual <= massReqd` failed: [<source>:9:33: error (unsupported-operator): Operator '[' is not model-level evaluable]

The experimental_quantities flag was added in 0.8.2 (Compiler), before then quantity expressions will not be evaluated.

Hello Daumantas,

thank you again for the clarication. Not using the flag and deleting all instances of quantity expression I was able to get the same results as in your first response (I have marked it as the Solution).

Maybe a silly question from my side, you said the flag "experimental_quantities”was added in 0.8.2. In my case I see that the flag is still not implemented even though I have the latest Modeler release 0.8.3. Is there something I’m missing here to update?

Perhaps your python package is not updated.

python -c "import syside; print(syside.__version__)"

should print 0.8.2 or greater.

It is either

pip install syside --upgrade

or

uv sync -P syside

Perfect, now is fully updated and working. Many thanks!