State Machines¶

GUIDE · STATE MACHINES

Syscribe models state-based behaviour with StateDef / State elements, faithful to SysMLv2 §7.18. A state machine is a composite state whose subStates: are connected by transitions; the tool validates it for completeness (dead/trap states, missing or duplicate initials, non-determinism, illegal cross-region transitions, and unresolved references, incomplete transitions) with the W070–W079 and W929 checks. All of these are draft-suppressed and gateable with --deny W07x (and --deny W929).

A flat state machine¶

A StateDef lists its substates under subStates:. Exactly one substate is the initial state (isInitial: true); final states are marked isFinal: true. Each substate's transitions: carry it to a target:.

---
type: StateDef
name: FlightStates
subStates:
  - name: disarmed
    isInitial: true
    transitions:
      - target: armed
        accept: { payload: Items::ControlCommand }
        guard: "armStatus == ArmStatus::disarmed and gps.fixQuality >= 1"
  - name: armed
    transitions:
      - target: takingOff
        accept: Items::ControlCommand
        guard: "armStatus == ArmStatus::armed"
        effect: { name: startTakeoff, typedBy: Behavior::TakeoffAction }
  - name: takingOff
    entryAction: Behavior::TakeoffAction
    transitions:
      - target: flying
        guard: "altitudeM >= targetAltitudeM"
  - name: flying
    doAction: Behavior::MissionExecution
    transitions:
      - target: disarmed
        guard: "altitudeM <= 0.1"
---

The canonical transition schema (§8.8.3)¶

A transition is defined by one consistent vocabulary, taken from the SysMLv2 textual form transition first <source> accept <trigger> if <guard> do <effect> then <target>:

Transitions may be authored either nested under a substate (source implicit) or at the StateDef top level (with an explicit source:); both yield the same edge model.

isInitial: true and isFinal: true are the shorthands for the SysMLv2 entry; then … (initial) and then done (final) pseudostates.

Completeness checks (flat machines)¶

A decision transition (two or more guarded transitions from the same source) is a legitimate branch and does not raise W072 — guards are what disambiguate.

Parallel (orthogonal) regions¶

Set isParallel: true to make a state's direct substates concurrent regions. Each region is itself a composite with its own subStates: and its own initial state; the regions run at the same time.

---
type: StateDef
name: Vehicle
isParallel: true
subStates:
  - name: Motion          # region 1
    subStates:
      - { name: stopped, isInitial: true, transitions: [{ target: moving, accept: Go }] }
      - { name: moving,  transitions: [{ target: stopped, accept: Stop }] }
  - name: Lights          # region 2 — runs concurrently with Motion
    subStates:
      - { name: off, isInitial: true, transitions: [{ target: on, accept: Switch }] }
      - { name: on,  transitions: [{ target: off, accept: Switch }] }
---

W073/W074 are then checked per region (each region needs exactly one initial). Two further rules apply to the parallel parent:

• W077 — a transition that connects substates in two different regions (SysMLv2 forbids transitions between the substates of a parallel state).
• W078 — an isParallel: true state with fewer than two regions.

Composite (hierarchical) states¶

A substate is composite when it carries typedBy: (a reference to another StateDef) or an inline subStates: list. The checks recurse: each level is validated, a composite substate is treated as a single node in its parent's graph, and inline-subStates: interiors are checked as their own region (findings name the enclosing region). A typedBy: substate is a node only — the referenced StateDef is validated as its own element.

subStates:
  - name: Active
    isInitial: true
    subStates:                      # inline nested machine (composite-by-containment)
      - { name: warmup,  isInitial: true, transitions: [{ target: running }] }
      - { name: running, isFinal: true }
    transitions:
      - target: Done                # Active's own (parent-level) transition
  - name: Done
    isFinal: true

SysMLv2 conformance¶

Syscribe follows SysMLv2's streamlined state-machine model: composite + parallel states, entry/do/exit actions, accept/guard/effect transitions, and decision transitions for branching. It deliberately omits UML's pseudostate zoo (choice / junction / fork / join / history) — those are not part of SysMLv2.

See also¶

• Element Types · Frontmatter
• Full schema: syscribe spec (§8.8) · rule reference: Validation Rules

Executing a machine¶

A machine that declares variables: or uses after, when, done, internal, assign or initialEffect is executable. syscribe compile lowers it to an IR and syscribe simulate runs it; the semantics and where each rule comes from are in docs/design/state-machine-execution-semantics.md. Type and unit errors in the expressions (a guard comparing metres with a plain number, a non-boolean guard, an assignment of the wrong dimension) are found without running anything and reported as E935; names that are not variables, such as event payload fields, are never errors (docs/design/static-typing.md).

type: StateDef
name: Door
variables:
  - {name: obstructions, value: "0"}
subStates:
  - name: Closed
    isInitial: true
    transitions:
      - {target: Opening, accept: Cmd::Open}
  - name: Opening
    transitions:
      - {target: Open, accept: {after: "3 s"}, guard: "obstructions == 0"}
      - {target: Closed, accept: {when: "obstructions > 2"}}
  - name: Open
    transitions:
      - {internal: true, accept: Cmd::Obstruct, assign: "obstructions := obstructions + 1"}
      - {target: Closed, accept: Cmd::Close}

Feature parameters in a machine¶

A guard, an assignment, a variable's initial value or a duration can use a feature parameter, written as a placeholder ({{Features::GridProfile.reconnectDelayS}}, see Variability). simulate, compile, mutate and inject take --config <Configuration> and run on that product, with the placeholder replaced by the Configuration's binding, else the parameter's fixed or default value. validate checks the symbolic base model at the parameters' defaults. A parameter with no value: or default: (the usual isRequired: true profile value) has nothing to check at, so its expressions are checked with a stand-in of the parameter's type (the lower bound of range: or 0, false, the empty string, or the first enumValues entry, with the unit after a |unit placeholder) and the parameter is reported once as W248, naming the machines that use it (not for a bindingTime: runtime or a derived/bindTo: parameter). validate --config <Configuration> checks the machines at that product's bound values instead, and --all-configs does so for each Configuration at its own bindings; suspect links and baselines still read the symbolic text. A value, bound or stand-in, is substituted as written, so quote a string or enum placeholder yourself: '{{Features::GridProfile.region}}' == 'US'. Without --config a run sees the written placeholder and reports it as an expression error.

accept: {after: "{{Features::GridProfile.reconnectDelayS}} s"}
guard: "s.v > {{Features::GridProfile.overVoltagePu}}"

Virtual time is kept on a grid of one nanosecond, so a delay split into parts (99 ms then 1 ms) reaches a timer exactly like the whole (100 ms) at any absolute time; durations finer than 1 ns are rounded.

Strict mode¶

simulate --strict turns silent tie-breaking into errors, so a run that depends on document order cannot pass unnoticed:

• an event no transition accepts;
• two enabled transitions out of one state, even when both go to the same target (their effects or assignments can differ, and only one runs);
• two transitions in different parallel regions whose exit sets overlap, for example one region leaving the parallel state while another reacts to the same event; a deeper source preempting an ancestor's is a defined priority and is not reported;
• two transitions taken together that assign the same variable, since the final value would depend on where the regions sit in the file. This is reported even for commutative updates such as n := n + 1; give each region its own variable.

Without --strict document order decides and nothing is reported.

Deviations from SCXML, deliberately: no history, fork/join, invoke, external send or multi-event transitions (none exist in the SysML v2 model); typed, unit-checked expressions instead of ECMAScript; a virtual clock instead of delayed sends; an expression error stops the run instead of raising error.execution; equal-priority conflicts (including two regions' transitions that exit the same states, which only document order would rank) and unhandled events are reported in strict mode; change triggers are SysML v2 one-shot observations, not SCXML level-triggered eventless transitions; behaviour references (effect: Pkg::Action, entryAction: Pkg::Action) are recorded in the trace but not executed.