State Machines

Paradox includes first-class finite state machine support via the Machine type in the standard library. Define your states, events, and transitions in .dox files, and Paradox generates idiomatic state machine code for eleven target languages — with compile-time verification of structural properties.

Core Types

The state machine types are defined in machine.dox within the std package. Import them with import std.

Guard

A guard condition on a transition. Evaluates context to Boolean.

type Guard c
  name: Text
  check: (c. Boolean)?

The check field is an optional function from the context type to Boolean. When present, the transition only fires if the guard evaluates to true.

Transition

A transition between states, optionally guarded.

type Transition s e c
  event: e
  target: s
  guard: Guard c?

StateConfig

Configuration for a single state — its outgoing transitions and a human-readable label.

type StateConfig s e c
  transitions: [Transition s e c]
  label: Text

Machine

A complete finite state machine, parameterized over state (s), event (e), and context (c) types.

type Machine s e c
  name: Text
  initial: s
  context: c
  finals: {s}
  states: {s: StateConfig s e c}
Field Description

name

Machine identifier (used in generated code)

initial

The starting state

context

Initial context value

finals

Set of accepting/terminal states (empty for non-terminating machines)

states

Map from state to its configuration (transitions and label)

Defining a Machine

Define your states as a union, events as a union, and context as a product type. Then declare a Machine constant:

import std

union TurnstileState
  locked
  unlocked

union TurnstileEvent
  coin
  push

type TurnstileContext
  coins: Integer
  pushes: Integer

defaultContext: TurnstileContext
  coins: 0
  pushes: 0

Because Machine is a parameterized type, you must use the TypeName: prefix syntax for product literals. Nested product literals cannot appear directly inside arrays, so extract transitions and configs as named constants:

lockedCoinTransition: Transition TurnstileState TurnstileEvent TurnstileContext
  Transition:
    event: TurnstileEvent.coin
    target: TurnstileState.unlocked
    guard: ()

lockedPushTransition: Transition TurnstileState TurnstileEvent TurnstileContext
  Transition:
    event: TurnstileEvent.push
    target: TurnstileState.locked
    guard: ()

lockedConfig: StateConfig TurnstileState TurnstileEvent TurnstileContext
  StateConfig:
    transitions: [lockedCoinTransition, lockedPushTransition]
    label: ""

unlockedPushTransition: Transition TurnstileState TurnstileEvent TurnstileContext
  Transition:
    event: TurnstileEvent.push
    target: TurnstileState.locked
    guard: ()

unlockedCoinTransition: Transition TurnstileState TurnstileEvent TurnstileContext
  Transition:
    event: TurnstileEvent.coin
    target: TurnstileState.unlocked
    guard: ()

unlockedConfig: StateConfig TurnstileState TurnstileEvent TurnstileContext
  StateConfig:
    transitions: [unlockedPushTransition, unlockedCoinTransition]
    label: ""

turnstile: Machine TurnstileState TurnstileEvent TurnstileContext
  Machine:
    name: "turnstile"
    initial: TurnstileState.locked
    context: defaultContext
    finals: {}
    states: {TurnstileState.locked: lockedConfig, TurnstileState.unlocked: unlockedConfig}
Product literals for parameterized types like Machine s e c require the TypeName: prefix form. The sugar form (indented fields without a prefix) only works with non-parameterized types.

Verification

Paradox automatically verifies structural properties of every machine at compile time:

Determinism

For each (state, event) pair, at most one unguarded transition exists.

Reachability

Every declared state is reachable from the initial state via BFS traversal.

Deadlock freedom

Every non-final state has at least one outgoing transition.

Complete event coverage

Every non-final state handles every event with at least one transition.

Liveness

From every non-final state, a final state is eventually reachable. Skipped when finals is empty (non-terminating machine by design).

Verification errors appear as strap diagnostics with source positions pointing to the offending states.

Code Generation

When you run paradox generate, any Machine constants in your specification are automatically detected and generate a standalone state machine module alongside the normal type codegen. Each generated module includes:

  • State enum/union type

  • Event enum/union type

  • Context struct/record

  • A transition function implementing the state machine logic

Supported Targets

State machine code generation supports eleven languages:

Target Flag Generated Output

TypeScript

--typescript

String literal union types, interface, switch-based transition function

Haskell

--haskell

ADTs, pattern-matching transition function

Rust

--rust

Enums, structs, match-based transition function

Python

--python

String enums, dataclass, if/elif transition function

C++

--cpp

Enum class, struct, switch-based transition function

Elixir

--elixir

Atoms, struct, multi-clause function heads

Scala

--scala

Sealed trait, case class, pattern-matching transition

OCaml

--ocaml

Variant types, record, match-based transition

Nix

--nix

Attribute sets, conditional transition function

Bash

--bash

Case statements, associative arrays

C#

--csharp

Enums, record, switch expression

Example Output

For the turnstile example above, paradox generate --typescript produces:

// Generated FSM: turnstile

export type TurnstileState = "locked" | "unlocked";

export type TurnstileEvent = "coin" | "push";

export interface TurnstileContext {
  coins: number;
  pushes: number;
}

export type TurnstileTransitionResult = {
  target: TurnstileState;
  context: TurnstileContext;
} | null;

export function transition(
  state: TurnstileState,
  event: TurnstileEvent,
  context: TurnstileContext
): TurnstileTransitionResult {
  switch (state) {
    case "locked":
      switch (event) {
        case "coin":
          return { target: "unlocked", context };
        case "push":
          return { target: "locked", context };
      }
      break;
    case "unlocked":
      switch (event) {
        case "push":
          return { target: "locked", context };
        case "coin":
          return { target: "unlocked", context };
      }
      break;
  }
  return null;
}

See Also