Evaluate 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:
syside solver evaluate -i rover.sysml --expr "Rover::rover.totalMass"
{
"result": {
"subject": "Rover",
"expression": "Rover::rover.totalMass",
"determination": "determined",
"outcome": {
"shape": "attainable_set",
"attainable": {
"values": [
{
"value": "78",
"witness": {
"values": [
["Rover::rover.payloadMass", "30"],
["Rover::rover.totalMass", "78"]
],
"value": "78"
}
}
],
"exhaustive": "true"
},
"unattainable": { "values": [], "exhaustive": "false" }
},
"causes": []
},
"warnings": [],
"exit_code": 0
}
One value, 78, and "exhaustive": "true" in the attainable listing: this list is
complete, so no other value is possible. The unattainable listing names values
known to be impossible. It is empty and not exhaustive here, because the impossible values
(every number other than 78) cannot all be listed. Read the solver’s output describes
both listings.
Changed in version 1.0.0: Before 1.0.0, the values sat directly in outcome.values, with no unattainable
listing.
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, and 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",
"attainable": {
"values": [
{
"value": "-2",
"witness": {
"values": [
["Battery::battery.cellA.voltage", "3"],
["Battery::battery.totalVoltage", "-2"],
["Battery::battery.cellB.voltage", "-5"]
],
"value": "-2"
}
},
{
"value": "-1",
"witness": { "...": "..." }
},
{
"value": "0",
"witness": { "...": "..." }
}
],
"exhaustive": "false"
},
"unattainable": { "values": [], "exhaustive": "undetermined" }
},
"...": "..."
},
"warnings": [],
"exit_code": 0
}
(Output truncated; the two elided witnesses have the same shape as the first.)
Two things to notice:
"exhaustive": "false"inattainable: the listing was cut off by the cap, not complete. Nothing in the model bounds the unset voltage, sototalVoltagehas infinitely many possible values.Each value’s
witnessshows a way to get it: the first says “if the unset voltage were -5, the total would be -2”.
Note
Values are exact numbers, so a value that is not an integer prints as a fraction, never
as a decimal: 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:
{
"attainable": {
"values": [
{
"value": "false",
"witness": {
"values": [
["Battery::battery.cellA.voltage", "3"],
["Battery::battery.totalVoltage", "2"],
["Battery::battery.cellB.voltage", "-1"]
],
"value": "false"
}
},
{
"value": "true",
"witness": {
"values": [
["Battery::battery.cellA.voltage", "3"],
["Battery::battery.totalVoltage", "42"],
["Battery::battery.cellB.voltage", "39"]
],
"value": "true"
}
}
],
"exhaustive": "true"
},
"unattainable": { "values": [], "exhaustive": "true" }
}
(Output truncated to the outcome.attainable and outcome.unattainable parts.)
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:
both report the same attainable set, but evaluate exits 0 either way, while
check --predicate exits 1 when the set fails its --fail-when mode (by default,
when false is attainable). See Check that requirements hold.
Integer attributes hold whole numbers New in v1.0.0
An attribute typed Integer holds only whole numbers, and the Solver never lists a
fraction for it or uses one in a witness.
Changed in version 1.0.0: Earlier releases let an Integer attribute take fractional values, so a listing could
include values such as -3/2 and a check could fail only because of a fractional
witness.
This follows the SysML v2 specification: the values of an Integer attribute are
integers, and / on two integers returns a Rational. Writing a division of two
integers into an Integer attribute, as a binding (attribute h : Integer = v / 2;)
or as an assignment (assign h := v / 2;), is refused when the model loads, as a type
error.
What can go in --expr
The expression goes in --expr (-e). It is written over qualified names from the
model (see How Solver queries name features for what a qualified name means in a query):
a single attribute:
Rover::rover.totalMassarithmetic:
+,*,/over attributes and literalsa sum over a collection:
sum(Rover::rover::wheels.mass)comparisons and
not:Rover::rover.totalMass < 100
--max-values N (-m N) caps how many values are listed (10 by default). The other
options are shared with check and listed in Check that requirements hold.