machine_ir_json

Purpose

verified-tsm.machine.v1 is the machine IR used by tin tooling. YAML is the recommended hand-authored form; JSON is the canonical automation artifact for generators, diagram exporters, validation, replay fixtures, and integrations.

Use YAML for compact reviews, JSON when another tool produces or consumes the machine, and C++ or the .hsm DSL when behavior should live directly in source.

Top-Level Shape

schema: verified-tsm.machine.v1
machine:
  initial: Booting
 
# States and events are inferred from transition rows.
transitions: [
  {Booting, BootComplete, Running},
  {Running, OvervoltageFault, SafeHold}
]

YAML comments use # and are discarded before validation or generation.

# States and events are inferred from transition rows.
transitions:
  - source: Booting
    event: BootComplete
    target: Running

Optional top-level fields currently used by examples include:

• copyright
• license
• states
• events
• target
• transports
• runtime
• evidence

The validator requires schema, machine.initial, and transitions. If machine.name is omitted, the CLI derives it from the source filename. If states or events are omitted, the CLI infers them from transition sources, targets, and event names.

Machine

machine declares the initial state. name and namespace are optional generator metadata.

machine:
  name: SurgicalRobotSupervisor
  namespace: surgical_robot
  initial: Offline
  description: Supervisor state machine for a surgical robot scenario.

namespace is dotted in JSON and lowers to C++ namespace separators when a C++ skeleton is generated.

States

Flat states only need a name:

{ "name": "Offline" }

Composite states name an initial child. Children name their parent. Dotted names encode hierarchy:

{ "name": "Operational", "initial": "Operational.TeleopReady" },
{ "name": "Operational.TeleopReady", "parent": "Operational" },
{ "name": "Operational.Teleoperating", "parent": "Operational" }

Supported state metadata:

• name: required state identifier;
• parent: parent state for hierarchical states;
• initial: initial child selected when a composite state is entered;
• kind: normal, choice, fork, or join;
• region: orthogonal-region metadata for tooling;
• entry: entry callback name;
• exit: exit callback name.

Events

Payload-free events only need a name:

{ "name": "PowerOn" }

Payload events declare fields. Current generator field types are bool, int32, uint32, float32, float64, string, and bytes.

{
  "name": "Fault",
  "payload": [
    { "name": "code", "type": "uint32" }
  ]
}

Transitions

Each transition row names source state, event, target state, and optional behavior hooks.

source: Operational.TeleopReady
event: FootPedalPressed
target: Operational.Teleoperating
guard: console_ready
action: begin_motion
kind: external

For payload-free transitions with no hooks, YAML can use a compact three-token row. The order is source, event, target:

transitions: [
  {Operational.TeleopReady, FootPedalPressed, Operational.Teleoperating}
]

Supported transition metadata:

• source: required source state;
• event: required event;
• target: required target state;
• kind: external, local, or internal;
• guard: guard callback name;
• action: action callback name.

The legacy JSON spellings from and to are still accepted on input. Code generation normalizes authoring notes away and uses only semantic fields.

JSON Comments

YAML should use normal # comments. JSON has no comment syntax, so comment and comments fields are allowed at the top level, on machine, on explicit state/event declarations, and on transition rows. They are intentionally ignored by code generators.

{
  "schema": "verified-tsm.machine.v1",
  "machine": { "initial": "Booting" },
  "comment": "Keep ISR details out of the behavior model.",
  "transitions": [
    {
      "source": "Running",
      "event": "OvervoltageFault",
      "target": "SafeHold",
      "comment": "Emitted by the voltage monitor task."
    }
  ]
}

Runtime Metadata

The optional runtime object documents the intended runtime configuration for generators and review tools.

{
  "dispatch_model": "queued",
  "queue": {
    "storage": {
      "kind": "static_storage",
      "capacity": 8
    },
    "overflow": "reject_newest"
  }
}

The current C++ generator treats this as metadata. Production code still selects concrete runtime policies in C++.

Supported runtime vocabulary:

• dispatch_model: direct, queued, or per_region_queued;
• queue.storage.kind: static_storage, target_storage, freertos_queue, or zephyr_queue;
• queue.storage.capacity: positive integer queue capacity;
• queue.overflow: reject_newest, drop_oldest, or overwrite_latest;
• task_count: non-negative integer task count;
• timer_slots: non-negative integer timer slot count.

Target Metadata

The optional target object records the deployment profile and compile-time configuration a generated artifact is intended to match.

{
  "profile": "host-linux",
  "architecture": "x86_64",
  "platform": "linux",
  "compiler": "gcc",
  "abi": "gnu",
  "tick": {
    "rep": "std::uint64_t",
    "period": "std::micro"
  },
  "constraints": {
    "no_heap_runtime": true,
    "exceptions_disabled": true,
    "rtti_disabled": true
  }
}

profile names the tin platform profile. tick.rep and tick.period mirror the TSM_TICK_REP and TSM_TICK_PERIOD compile-time configuration. Constraint values are boolean review flags that target adapters and CI checks can inspect.

Transport Metadata

The optional transports array describes external handoff points that tools or adapters can inspect.

{
  "name": "patient_side_m2m_bus",
  "family": "m2m",
  "direction": "bidirectional",
  "events": ["ConsoleHandshake", "Fault", "Reset"],
  "link": {
    "kind": "can",
    "profile": "example-supervisory-frame"
  },
  "delivery": "acked"
}

Validation checks that transport event names refer to declared events and that local transport metadata uses a local link.

Evidence Metadata

The optional evidence object gives verification and trace tooling a place to record obligations.

{
  "obligations": [
    {
      "name": "all-supervisor-transitions-covered",
      "kind": "transition_coverage",
      "target": "*"
    }
  ]
}

Minimal Complete Example

{
  "schema": "verified-tsm.machine.v1",
  "machine": {
    "name": "Motor",
    "namespace": "examples.motor",
    "initial": "Disabled"
  },
  "states": [
    { "name": "Disabled" },
    { "name": "Running" },
    { "name": "Faulted" }
  ],
  "events": [
    { "name": "Enable" },
    {
      "name": "Fault",
      "payload": [
        { "name": "code", "type": "uint32" }
      ]
    },
    { "name": "Reset" }
  ],
  "transitions": [
    { "from": "Disabled", "event": "Enable", "to": "Running" },
    { "from": "Running", "event": "Fault", "to": "Faulted", "action": "latch_fault" },
    { "from": "Faulted", "event": "Reset", "to": "Disabled", "guard": "can_reset" }
  ]
}