Exploring 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::thermostat::heaterOn == 1 }
}

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

• --depth 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 Adding 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",
      "proven": [
        {
          "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",
      "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 what it proved reachable within the explored depth, rather than claiming a complete set.

• proven 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 – 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.

Checking a reachability assertion

The same model carries an assertion, heaterCanRun. Remember from Checking that requirements hold that check asks a universal question – “does this hold in every allowed run?” – which is the wrong shape for “can the heater run?”. A machine that never leaves Idle is an allowed run, so the universal claim fails while the reachability answer is yes.

For a “can it happen?” question, use evaluate as above and look for the value among proven. Use check for the mirror-image question, “is this always true?” – for example an invariant like “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": "predicate", "status": "satisfied" },
    "causes": []
  },
  "warnings": [],
  "exit_code": 0
}

(The alt_semantics section is elided.)

check verdicts hold at any depth

Note what just happened: no --depth, on a machine that can run forever – and the verdict is determined, not an approximation. A check verdict on a state machine is not “satisfied as far as we looked”:

• satisfied means the Solver proved the condition for runs of any length, including runs longer than anything it explicitly explored. This works even when the values themselves grow without bound: for a machine that increments a counter forever, check --predicate "... ticks + 1 > 0" still comes back satisfied.

• violated comes with a finite trace – a concrete run reaching the violation – which is a complete proof by itself, however deep it lies. Asking the incrementing counter whether ticks < 5 always holds returns violated with the run that reaches 5, with no depth setting.

• unknown is the honest third verdict: the Solver could neither prove the condition for all runs nor find a violating run. The exit code stays 0; determination is unknown. Treat it like an unanalyzable assertion (see Handling unsupported syntax): the tool is telling you it does not know, not that the model is fine.

evaluate 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 simply will not appear in proven); a larger depth explores more and runs longer. Start small, and increase the depth if a value you expect to be reachable is missing.