Explore state machine reachability

For a model with behavior over time (a state machine writing to attributes), evaluate answers reachability questions: which values can an attribute take as the machine runs? Each reachable value comes with a trace: the step-by-step run that reaches it, so you can see how the machine got there.

Create thermostat.sysml. A two-state machine starts in Idle and flips a flag whenever it enters Heating:

package Thermostat {
    private import ScalarValues::Integer;
    part thermostat [1] {
        attribute heaterOn : Integer := 0;
        exhibit state behavior {
            entry; then Idle;
            state Idle;
            state Heating {
                entry assign heaterOn := 1;
            }
            transition Idle then Heating;
            transition Heating then Idle;
        }
    }
    assert constraint heaterCanRun { thermostat.heaterOn == 1 }
}

Can heaterOn become 1? Ask for its reachable values. Two extra options come into play:

  • --depth (-d) bounds how many steps of the machine’s run evaluate explores. The machine here can loop forever, so the listing of reachable values needs a horizon. (check does not need one. See below.)

  • --alt-semantics free reads the model closed-world: values change only when the machine writes them, and nothing outside the model interferes. Without it, the specification’s default reading lets an unwritten snapshot hold any value, which buries the answer in irrelevant possibilities. See Add assumptions.

syside solver evaluate -i thermostat.sysml \
    --expr "Thermostat::thermostat.heaterOn" \
    --depth 3 --alt-semantics free

{
  "result": {
    "subject": "Thermostat",
    "expression": "Thermostat::thermostat.heaterOn",
    "determination": "undetermined",
    "outcome": {
      "shape": "approximated",
      "attainable": {
        "values": [
          {
            "value": "0",
            "trace": [
              { "index": 0,
                "values": [["Thermostat::thermostat.heaterOn", "0"]] },
              { "index": 1,
                "values": [["Thermostat::thermostat.heaterOn", "1"]] },
              { "index": 2,
                "values": [["Thermostat::thermostat.heaterOn", "1"]] },
              { "index": 3,
                "values": [["Thermostat::thermostat.heaterOn", "1"]] }
            ]
          },
          {
            "value": "1",
            "trace": [
              { "index": 0,
                "values": [["Thermostat::thermostat.heaterOn", "0"]] },
              { "index": 1,
                "values": [["Thermostat::thermostat.heaterOn", "1"]] },
              { "index": 2,
                "values": [["Thermostat::thermostat.heaterOn", "1"]] },
              { "index": 3,
                "values": [["Thermostat::thermostat.heaterOn", "1"]] }
            ]
          }
        ],
        "exhaustive": "undetermined"
      },
      "unattainable": { "values": [], "exhaustive": "undetermined" },
      "integral": true
    },
    "causes": []
  },
  "alt_semantics": [ "..." ],
  "warnings": [],
  "exit_code": 0
}

(The alt_semantics section, elided here, spells out every override that free switched on.)

How to read this:

  • The shape is "approximated": for a machine that can run forever, the Solver reports the values it found reachable within the explored depth, rather than claiming a complete set.

  • attainable.values lists the values: 0 (the initial value, before the machine first enters Heating) and 1 (after it does). Both are genuinely reachable.

  • Each value’s trace is a run of the machine, snapshot by snapshot: heaterOn starts at 0 at step 0 and is 1 from step 1 on, because the machine took the Idle then Heating transition on its first step.

  • "exhaustive": "undetermined" is honest bookkeeping: within depth 3 nothing beyond 0 and 1 was reached, but the Solver does not claim that a longer run could never produce more. The unattainable listing is empty for the same reason.

Changed in version 1.0.0: Before 1.0.0, the reachable values were listed in proven, with no unattainable listing.

Checking a reachability assertion

The same model carries an assertion, heaterCanRun. check reads a condition on a machine’s attributes at every snapshot of a run, and a run may end after any snapshot, including the first. At the first snapshot heaterOn is still 0, so false is attainable for heaterCanRun, its trace is the one-snapshot run, and the check exits 1, while the reachability answer is yes:

syside solver check -i thermostat.sysml --alt-semantics free

{
  "name": "Thermostat::heaterCanRun",
  "outcome": {
    "shape": "approximated",
    "attainable": {
      "values": [
        {
          "value": "true",
          "trace": [
            { "index": 0,
              "values": [["Thermostat::thermostat.heaterOn", "0"]] },
            { "index": 1,
              "values": [["Thermostat::thermostat.heaterOn", "1"]] }
          ]
        },
        {
          "value": "false",
          "trace": [
            { "index": 0,
              "values": [["Thermostat::thermostat.heaterOn", "0"]] }
          ]
        }
      ],
      "exhaustive": "true"
    },
    "unattainable": { "values": [], "exhaustive": "true" },
    "integral": false
  }
}

(Output truncated to the one assertion.)

For a “can it happen?” question, use evaluate as above and look for the value in attainable.values. Use check for the mirror-image question, “is this true at every snapshot?”, for example “the flag is never 2”:

syside solver check -i thermostat.sysml \
    --predicate "not (Thermostat::thermostat.heaterOn == 2)" \
    --alt-semantics free

{
  "result": {
    "subject": "Thermostat",
    "expression": "not Thermostat::thermostat.heaterOn == 2",
    "determination": "determined",
    "outcome": {
      "shape": "approximated",
      "attainable": {
        "values": [
          {
            "value": "true",
            "trace": [
              { "index": 0,
                "values": [["Thermostat::thermostat.heaterOn", "0"]] }
            ]
          }
        ],
        "exhaustive": "true"
      },
      "unattainable": { "values": ["false"], "exhaustive": "true" },
      "integral": false
    },
    "causes": []
  },
  "alt_semantics": [ "..." ],
  "warnings": [],
  "fail_when": "false_attainable",
  "exit_code": 0
}

(The alt_semantics section is elided.)

false is in unattainable.values: no snapshot of any run, however long, has the flag at 2. true is attainable, with the shortest run that shows it, and the answer is determined. The check exits 0 under every --fail-when mode. evaluate with the same expression reports the same listings and determination.

Changed in version 1.0.0: Before 1.0.0, a condition on a machine was reported as a status of satisfied, violated or unknown instead of two listings.

Conditions over snapshots New in v1.0.0

Inside a model, an assertion can say which snapshots it covers with snapshots->forAll (every snapshot) or snapshots->exists (some snapshot). Because a run may end after any snapshot, a condition that only a later snapshot meets can fail on a shorter run. Create counter.sysml:

package Counter {
    private import ScalarValues::Integer;
    private import ControlFunctions::*;
    action counter {
        attribute ticks : Integer := 0;
        loop { assign ticks := ticks + 1; }
        assert constraint reachesThree {
            snapshots->exists { in s; (s as counter).ticks == 3 }
        }
    }
}

syside solver check -i counter.sysml --alt-semantics free

reachesThree lists both truth values: true with the run that counts up to 3, and false with the one-snapshot run that ends at ticks 0. The check exits 1 under the default --fail-when mode. To ask “can ticks reach 3?”, evaluate Counter::counter.ticks instead and look for 3 in attainable.values.

check results hold at any depth

Note what the thermostat check did: no --depth, on a machine that can run forever, and still a firm answer rather than an approximation. A check result on behavior that runs forever is not “it holds as far as we looked”. Using the counter above:

  • false in unattainable.values means the condition must hold at every snapshot of runs of any length, including runs longer than anything the Solver explicitly explored. This works even when the values themselves grow without bound: check -i counter.sysml --predicate "Counter::counter.ticks + 1 > 0" --alt-semantics free lists false as unattainable and exits 0.

  • false in attainable.values comes with a finite trace (a concrete run reaching the violation), which settles the answer by itself, however deep it lies. Asking whether Counter::counter.ticks < 5 always holds lists false with the run that reaches 5, and exits 1, with no depth setting.

  • When the Solver could neither show that the condition holds for all runs nor find a violating run (for example, because it reached a limit set with --solver-limit or --timeout, see Check that requirements hold), neither listing settles false, and exhaustive is "unknown" with a reason. The exit code stays 0 under the default --fail-when mode. Treat it like an assertion the Solver could not analyze (see Handle unsupported syntax): the tool is telling you it does not know, not that the model is fine. --fail-when not-exactly-true turns it into exit 1.

counter.sysml needs --alt-semantics free (or simultaneous-expressions): the loop’s assign ticks := ticks + 1 reads ticks, and the specification does not say which snapshot that read refers to. Without the override, the Solver reports ticks as unknown with a reason that names the override.

evaluate on an attribute that is not boolean is different: a reachable-value listing for a machine that can run forever is always an approximation ("exhaustive": "undetermined"), and --depth sets how far it explores. A too-small depth can miss values that need more steps to reach (they will not appear in attainable.values). A larger depth explores more and runs longer. Start small, and increase the depth if a value you expect to be reachable is missing.

A machine whose transitions carry an effect (do ...) is not analyzed yet. See Handle unsupported syntax.