Evaluating possible values

syside solver evaluate reports every value an expression can take across the situations your model allows. Each reported value comes with a witness: a concrete assignment of the model’s open values that produces it, so you can see not just that a value is possible but how.

When every value is fixed

If the model pins down everything the expression depends on, the answer is a single value. Using the rover model from Solver v0.10.3 Labs:

syside solver evaluate -i rover.sysml --expr "Rover::rover::totalMass"

{
  "result": {
    "subject": "Rover",
    "expression": "Rover::rover::totalMass",
    "determination": "determined",
    "outcome": {
      "shape": "attainable_set",
      "values": [
        {
          "value": "78",
          "witness": {
            "values": [
              ["Rover::rover::payloadMass", "30"],
              ["Rover::rover::totalMass", "78"]
            ],
            "value": "78"
          }
        }
      ],
      "exhaustive": "true"
    },
    "causes": []
  },
  "warnings": [],
  "exit_code": 0
}

One value, 78, and "exhaustive": "true": this list is complete, no other value is possible.

When the model leaves a value open

Now a model that does not fix everything. Create battery.sysml:

package Battery {
    private import ScalarValues::Integer;
    part def Cell {
        attribute voltage : Integer;
    }
    part battery [1] {
        part cellA : Cell [1] {
            attribute redefines voltage = 3;
        }
        part cellB : Cell [1];
        attribute totalVoltage = cellA::voltage + cellB::voltage;
    }
}

cellA has its voltage set to 3; cellB does not. What can totalVoltage be? Ask, capping the listing at three values to keep the output short:

syside solver evaluate -i battery.sysml \
    --expr "Battery::battery::totalVoltage" --max-values 3

{
  "result": {
    "subject": "Battery",
    "expression": "Battery::battery::totalVoltage",
    "determination": "undetermined",
    "outcome": {
      "shape": "attainable_set",
      "values": [
        {
          "value": "3/2",
          "witness": {
            "values": [
              ["Battery::Cell::voltage", "-3/2"],
              ["Battery::battery::cellA::voltage", "3"],
              ["Battery::battery::totalVoltage", "3/2"]
            ],
            "value": "3/2"
          }
        },
        {
          "value": "2",
          "witness": { "...": "..." }
        },
        {
          "value": "3",
          "witness": { "...": "..." }
        }
      ],
      "exhaustive": "false"
    },
    "causes": [
      {
        "free_data": {
          "names": ["Battery::Cell::voltage"],
          "span": { "start_line": 4, "start_col": 9,
                    "end_line": 4, "end_col": 37 }
        }
      }
    ]
  },
  "warnings": [],
  "exit_code": 0
}

(The two elided witnesses have the same shape as the first.)

Three things to notice:

• "exhaustive": "false" – the listing was cut off by the cap, not complete. Nothing in the model bounds the unset voltage, so totalVoltage has infinitely many possible values.

• Each value’s witness shows a way to get it: the first says “if the unset voltage were -3/2, the total would be 3/2”.

• causes points at why the answer is not a single value: Battery::Cell::voltage is free, and the span gives the exact file location (line 4) of the declaration that left it open. This is where to edit the model if you expected a single answer.

Note

Values are exact numbers, so non-integers print as fractions: 3/2 means 1.5.

Probing for one specific value

With an infinite (or merely long) list, “is value X possible?” is better asked directly. Evaluate a comparison instead:

syside solver evaluate -i battery.sysml \
    --expr "Battery::battery::totalVoltage == 42"

A comparison is an expression like any other – its possible values are drawn from true and false, and each comes with a witness:

{
  "values": [
    {
      "value": "false",
      "witness": {
        "values": [
          ["Battery::Cell::voltage", "38"],
          ["Battery::battery::cellA::voltage", "3"],
          ["Battery::battery::totalVoltage", "41"]
        ],
        "value": "false"
      }
    },
    {
      "value": "true",
      "witness": {
        "values": [
          ["Battery::Cell::voltage", "39"],
          ["Battery::battery::cellA::voltage", "3"],
          ["Battery::battery::totalVoltage", "42"]
        ],
        "value": "true"
      }
    }
  ],
  "exhaustive": "true"
}

(Output truncated to the outcome.values part.)

Both true and false are attainable, so the answer to “can the total be 42?” is: yes, if the unset voltage is 39 – but it is not guaranteed.

This is also the difference between evaluate and check on a boolean expression: evaluate reports which truth values are possible (and exits 0 either way), while check --predicate demands the expression be true in every allowed situation (and exits 1 otherwise). See Checking that requirements hold.

What can go in --expr

An expression is written over qualified names from the model:

• a single attribute: Rover::rover::totalMass

• arithmetic: +, *, / over attributes and literals

• a sum over a collection: sum(Rover::rover::wheels.mass)

• comparisons and not: Rover::rover::totalMass < 100