Example for syside solver evaluate for the battery example has errors

For the battery.sysml example used in syside solver evaluate example on the Evaluating possible values — Syside webpage. Values are produced that are not correct for SysML v2 syntax and datatypes.

Given (from the Sensmetry web page):

(Note the corrected naming notation for cellA & cell B voltage)

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;
    }
}

Using the syside solver evaluate command, the results are:

CMD> 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": {
            "values": [
              ["Battery::Cell::voltage", "-1"],
              ["Battery::battery::cellA::voltage", "3"],
              ["Battery::battery::totalVoltage", "2"]
            ],
            "value": "2"
          }
        },
        {
          "value": "3",
          "witness": {
            "values": [
              ["Battery::Cell::voltage", "0"],
              ["Battery::battery::cellA::voltage", "3"],
              ["Battery::battery::totalVoltage", "3"]
            ],
            "value": "3"
          }
        }
      ],
      "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 following errors occur for the witness values, as voltage is typed as an Integer, the values indicated as witness values are in error (An Integer specializes Rational, so every Integer is a Rational, but not the reverse. The number 3/2 is a Rational that is not an Integer, so it can’t be a value of an Integer-typed attribute.)

To make evaluate work, the specification has to be rewritten to have the correct syntax and typing. Note line 4 for the default or the “:=” operator and line 11 for explicit typing.

Corrected specification:

As written on the webpage, evaluate incorrectly attempts to override a binding feature value on line 8 for cellA.voltage, which should have been reported as an unknown value for cellB.voltage; hence, evaluate should have reported an invalid computation on line 11 (i.e., unknown result).

Given the corrected specification, evaluate reports valid witness values.

V/r,
@Richard_Wallace

Thanks for noticing this. It will be fixed in v1.0.0.

Adam Layne, PhD