Compare values across units

Real models mix units: one supplier quotes a motor mass in grams, the frame is specified in kilograms, and the budget is in kilograms. The Solver converts between units of the same quantity automatically. You write each value in whatever unit is natural, and comparisons and sums come out right.

Create drone.sysml:

package Drone {
    private import ISQ::*;
    private import SI::*;
    part def Motor {
        attribute mass : MassValue = 250 [g];
    }
    part drone [1] {
        part motorA : Motor [1];
        part motorB : Motor [1];
        attribute frameMass : MassValue = 1 [kg];
        attribute totalMass : MassValue =
            motorA.mass + motorB.mass + frameMass;
    }
    assert constraint underLimit { drone.totalMass < 2 [kg] }
}

Grams and kilograms appear in the same sum and the same comparison. Run:

syside solver check -i drone.sysml
{
  "result": {
    "subject": "Drone",
    "expression": "assertions[1]",
    "determination": "determined",
    "outcome": {
      "shape": "assertions",
      "assertions": [
        {
          "name": "Drone::underLimit",
          "outcome": {
            "shape": "attainable_set",
            "attainable": {
              "values": [
                {
                  "value": "true",
                  "witness": {
                    "values": [
                      ["Drone::drone.frameMass", "1000"],
                      ["Drone::drone.totalMass", "1500"],
                      ["Drone::drone.motorA.mass", "250"],
                      ["Drone::drone.motorB.mass", "250"]
                    ],
                    "value": "true"
                  }
                }
              ],
              "exhaustive": "true"
            },
            "unattainable": { "values": ["false"], "exhaustive": "true" }
          }
        }
      ]
    },
    "causes": []
  },
  "warnings": [],
  "fail_when": "false_attainable",
  "exit_code": 0
}

The assertion holds (false is unattainable): 250 g + 250 g + 1 kg = 1.5 kg, which is under 2 kg.

Two things the example depends on:

  • Declare the quantity type. Each attribute is declared : MassValue (from the standard ISQ library). Without the type declaration the Solver cannot tell a mass from a bare number. It skips the attribute with a warning, and an assertion that depends on it gets an exhaustive of "unknown" with a reason that says to declare a type (see Handle unsupported syntax).

  • Import the unit libraries. ISQ provides the quantity types (MassValue), SI provides the units (g, kg).

Numbers in the output are in a common base unit

When a value with units appears in the output (in an attainable set or in a witness), it has been converted to a common base unit for the quantity. Evaluating the total mass of the drone:

syside solver evaluate -i drone.sysml --expr "Drone::drone.totalMass"
{
  "values": [
    {
      "value": "1500",
      "witness": {
        "values": [
          ["Drone::drone.frameMass", "1000"],
          ["Drone::drone.totalMass", "1500"],
          ["Drone::drone.motorA.mass", "250"],
          ["Drone::drone.motorB.mass", "250"]
        ],
        "value": "1500"
      }
    }
  ],
  "exhaustive": "true"
}

(Output truncated to the outcome.attainable part.)

Here everything is reported in grams: the 1 kg frame prints as 1000 and the total as 1500. The output does not currently name the unit, so when you read a number out of the Solver, check it against a value you know (as with the frame here) to confirm the scale.

Prefixed unit expressions like [milli * s]

The SysML v2 specification does not define what a prefix-and-unit chain such as 500 [milli * s] means, so by default the Solver refuses to guess. It skips any value that depends on one, with a warning, and an answer that depends on it gets an exhaustive of "unknown" whose reason names the override below. If your model uses this style, the prefix-scaling override gives it the reading you almost certainly intend (milli times second, i.e. milliseconds):

syside solver check -i model.sysml --alt-semantics prefix-scaling

See Add assumptions for how overrides work.