Examples

1. Traffic Light (Simplest)

The minimal stateproof example — a 3-state machine with one context variable.

import { machine, verify, createRuntime, generateTLA, toMermaidStateDiagram } from '@stateproof/core'

const trafficLight = machine('TrafficLight')
  .states('red', 'yellow', 'green')
  .initial('red')
  .context({ count: 0 })
  .transition('toGreen', {
    from: 'red',
    to: 'green',
    action: (ctx) => {
      ctx.count += 1
    }
  })
  .transition('toYellow', { from: 'green', to: 'yellow' })
  .transition('toRed', { from: 'yellow', to: 'red' })
  .invariant('count non-negative', (ctx) => ctx.count >= 0)

// Generate TLA+ for model checking
const { spec, cfg } = generateTLA(trafficLight.build())
console.log(spec)
// ---- MODULE TrafficLight_Generated ----
// EXTENDS Integers, Sequences, FiniteSets, TLC
// VARIABLES state, count
// ...
// ====

// Run as a runtime state machine
const rt = createRuntime(trafficLight)
console.log(rt.state) // 'red'
rt.send('toGreen') // true
console.log(rt.state) // 'green'
rt.send('toYellow') // true
rt.send('toRed') // true
console.log(rt.state) // 'red'
console.log(rt.context.count) // 1

// Verify with TLC (requires Java + tla2tools.jar)
const result = await verify(trafficLight)
console.log(result.ok) // true (if TLC available)
console.log(result.distinctStates) // 3

// Generate Mermaid diagram
console.log(toMermaidStateDiagram(trafficLight))
// stateDiagram-v2
//   [*] --> red
//   red --> green: toGreen
//   green --> yellow: toYellow
//   yellow --> red: toRed

What this demonstrates:

machine() fluent builder with .states(), .initial(), .context(), .transition(), .invariant()
Guards and actions are plain TypeScript lambdas
generateTLA() compiles to TLA+ for formal verification
createRuntime() gives you a live state machine from the same spec
verify() runs TLC model checking
toMermaidStateDiagram() generates visual diagrams

2. Guarded Counter

Demonstrates guards (preconditions) and multiple invariants.

import { machine, createRuntime, generateTLA, generateTests } from '@stateproof/core'

const counter = machine('Counter')
  .states('counting', 'done')
  .initial('counting')
  .context({ value: 0 })
  .transition('increment', {
    from: 'counting',
    guard: (ctx) => ctx.value < 5, // Only increment when < 5
    action: (ctx) => {
      ctx.value += 1
    }
  })
  .transition('finish', {
    from: 'counting',
    to: 'done',
    guard: (ctx) => ctx.value >= 5 // Can only finish when value reaches 5
  })
  .invariant('value bounded', (ctx) => ctx.value <= 5)
  .invariant('done means five', (ctx) => ctx.state !== 'done' || ctx.value >= 5)

// Runtime: guards enforce bounds
const rt = createRuntime(counter)
for (let i = 0; i < 5; i++) rt.send('increment')
console.log(rt.context.value) // 5
console.log(rt.send('increment')) // false — guard blocks it
console.log(rt.send('finish')) // true
console.log(rt.state) // 'done'

// TLA+ includes guard compilations
const { spec } = generateTLA(counter.build())
console.log(spec)
// increment ==
//   /\ state = "counting"
//   /\ (value < 5)
//   /\ state' = state
//   /\ value' = value + 1

// Generate coverage traces
const traces = await generateTests(counter.build(), { strategy: 'coverage' })
console.log(`${traces.length} traces covering all transitions`)

What this demonstrates:

Guards compiled to TLA+ expressions: ctx.value < 5 → (value < 5)
Actions compiled to primed assignments: ctx.value += 1 → value' = value + 1
Multiple invariants checked in every reachable state
Self-transitions (increment stays in 'counting')
Test generation covers all transition paths

3. Agent Session (Full Specification)

A real-world spec: an AI agent's session lifecycle with 7 states, 12 transitions, invariants, and liveness properties.

import { machine, createRuntime, generateTLA, toMermaidStateDiagram } from '@stateproof/core'

const agentSession = machine('AgentSession')
  .states('idle', 'working', 'streaming', 'compacting', 'complete', 'error', 'shutting_down')
  .initial('idle')
  .context({
    messageQueue: [] as string[],
    contextSize: 0,
    toolsInFlight: 0,
    shutdownRequested: false
  })
  // Messages can arrive in most active states
  .transition('receiveMessage', {
    from: ['idle', 'working', 'streaming', 'compacting'],
    guard: (ctx) => ctx.messageQueue.length < 100,
    action: (ctx) => {
      ctx.messageQueue.push('msg')
    }
  })
  // Process queued messages
  .transition('startWork', {
    from: 'idle',
    to: 'working',
    guard: (ctx) => ctx.messageQueue.length > 0,
    action: (ctx) => {
      ctx.messageQueue.shift()
      ctx.contextSize += 1
    }
  })
  // Begin streaming response
  .transition('startStreaming', {
    from: 'working',
    to: 'streaming',
    guard: (ctx) => ctx.toolsInFlight === 0
  })
  // Tool call during streaming
  .transition('toolCallReceived', {
    from: 'streaming',
    to: 'working',
    guard: (ctx) => ctx.toolsInFlight < 3,
    action: (ctx) => {
      ctx.toolsInFlight += 1
      ctx.contextSize += 1
    }
  })
  // Tool completes
  .transition('toolCallComplete', {
    from: 'working',
    guard: (ctx) => ctx.toolsInFlight > 0,
    action: (ctx) => {
      ctx.toolsInFlight -= 1
      ctx.contextSize += 1
    }
  })
  // Context too large — compact
  .transition('triggerCompaction', {
    from: 'working',
    to: 'compacting',
    guard: (ctx) => ctx.contextSize >= 50 && ctx.toolsInFlight === 0
  })
  .transition('compactionComplete', {
    from: 'compacting',
    to: 'working',
    action: (ctx) => {
      ctx.contextSize = Math.floor(ctx.contextSize / 2)
    }
  })
  // Stream finishes
  .transition('streamComplete', {
    from: 'streaming',
    to: 'working',
    action: (ctx) => {
      ctx.contextSize += 1
    }
  })
  // All work done
  .transition('complete', {
    from: 'working',
    to: 'complete',
    guard: (ctx) => ctx.toolsInFlight === 0 && ctx.messageQueue.length === 0 && !ctx.shutdownRequested
  })
  // Error recovery
  .transition('fail', {
    from: ['working', 'streaming', 'compacting'],
    to: 'error',
    action: (ctx) => {
      ctx.toolsInFlight = 0
    }
  })
  // Graceful shutdown
  .transition('shutdownRequested', {
    from: ['idle', 'working', 'streaming', 'compacting'],
    to: 'shutting_down',
    action: (ctx) => {
      ctx.shutdownRequested = true
    }
  })
  .transition('shutdownDrain', {
    from: 'shutting_down',
    to: 'complete',
    guard: (ctx) => ctx.toolsInFlight === 0
  })
  // Safety invariants
  .invariant(
    'tools only when working',
    (ctx) => ctx.toolsInFlight === 0 || ['working', 'shutting_down'].includes(ctx.state)
  )
  .invariant('queue bounded', (ctx) => ctx.messageQueue.length <= 100)
  .invariant(
    'terminal states are clean',
    (ctx) => !['complete', 'error'].includes(ctx.state) || ctx.toolsInFlight === 0
  )
  // Liveness: these must eventually happen
  .liveness('compaction converges', 'compacting', ['working', 'error'])
  .liveness('shutdown completes', 'shutting_down', ['complete', 'error'])

// Runtime: simulate a session
const rt = createRuntime(agentSession)
rt.send('receiveMessage') // idle → idle (queue: 1)
rt.send('startWork') // idle → working
rt.send('startStreaming') // working → streaming
rt.send('toolCallReceived') // streaming → working (tools: 1)
rt.send('toolCallComplete') // working → working (tools: 0)
rt.send('complete') // working → complete
console.log(rt.state) // 'complete'

// TLA+ with compiled guards, actions, invariants, and liveness
const { spec, cfg } = generateTLA(agentSession.build())
// cfg includes:
//   SPECIFICATION Spec
//   INVARIANT tools_only_when_working
//   INVARIANT queue_bounded
//   INVARIANT terminal_states_are_clean
//   PROPERTY compaction_converges
//   PROPERTY shutdown_completes

What this demonstrates:

Multi-from transitions: from: ['idle', 'working', 'streaming', 'compacting']
Complex guards: ctx.contextSize >= 50 && ctx.toolsInFlight === 0
Array operations compiled to TLA+: push → Append, shift → Tail, .length → Len
Math.floor(x/y) compiled to integer division \div
Liveness properties: 'compacting' ~> 'working' \/ 'error'
Full lifecycle from idle through work to completion or shutdown

4. WorktreeBinding (Concurrent Composition)

Multiple agents competing for limited worktrees — demonstrates concurrent composition.

import {
  machine,
  concurrent,
  createRuntime,
  generateConcurrentTLA,
  concurrentToMermaidStateDiagram
} from '@stateproof/core'

// Single worktree lifecycle
const worktreeBinding = machine('WorktreeBinding')
  .states('free', 'acquiring', 'bound', 'working', 'committing', 'releasing')
  .initial('free')
  .context({ owner: null as string | null, branch: null as string | null })
  .transition('acquire', {
    from: 'free',
    to: 'acquiring',
    action: (ctx) => {
      ctx.owner = 'agent'
      ctx.branch = 'main'
    }
  })
  .transition('lockGranted', { from: 'acquiring', to: 'bound' })
  .transition('lockDenied', {
    from: 'acquiring',
    to: 'free',
    action: (ctx) => {
      ctx.owner = null
      ctx.branch = null
    }
  })
  .transition('startWork', { from: 'bound', to: 'working' })
  .transition('commit', { from: 'working', to: 'committing' })
  .transition('commitDone', { from: 'committing', to: 'working' })
  .transition('release', {
    from: ['working', 'bound', 'committing'],
    to: 'releasing'
  })
  .transition('released', {
    from: 'releasing',
    to: 'free',
    action: (ctx) => {
      ctx.owner = null
      ctx.branch = null
    }
  })
  .invariant('exclusive ownership', (ctx) => ctx.state === 'free' || ctx.owner !== null)

// Concurrent: 2 worktrees
const multiAgent = concurrent('MultiAgentWorktrees')
  .instances('worktree', worktreeBinding, { count: 2 })
  .shared('assignments', 0)
  .invariant(
    'no double allocation',
    '\\A i \\in Worktrees: \\A j \\in Worktrees: ' +
      'i # j => (worktree_owner[i] # "null" /\\ worktree_owner[j] # "null" ' +
      '=> worktree_owner[i] # worktree_owner[j]) ' +
      '\\/ worktree_owner[i] = "null" \\/ worktree_owner[j] = "null"'
  )

// Generate concurrent TLA+
const { spec, cfg } = generateConcurrentTLA(multiAgent.build())
console.log(spec)
// ---- MODULE MultiAgentWorktrees_Generated ----
// EXTENDS Integers, Sequences, FiniteSets, TLC
//
// CONSTANT NumWorktree
// Worktrees == 1..NumWorktree
//
// VARIABLES worktree_state, worktree_owner, worktree_branch, assignments
//
// Init ==
//   /\ worktree_state = [i \in Worktrees |-> "free"]
//   /\ worktree_owner = [i \in Worktrees |-> "null"]
//   ...
//
// worktree_acquire(i) ==
//   /\ i \in Worktrees
//   /\ worktree_state[i] = "free"
//   /\ worktree_state' = [worktree_state EXCEPT ![i] = "acquiring"]
//   ...
//
// Next ==
//   \/ \E i \in Worktrees: worktree_acquire(i)
//   \/ \E i \in Worktrees: worktree_lockGranted(i)
//   ...
// ====

// Single instance still works as a runtime
const rt = createRuntime(worktreeBinding)
rt.send('acquire')
rt.send('lockGranted')
rt.send('startWork')
rt.send('commit')
rt.send('commitDone')
rt.send('release')
rt.send('released')
console.log(rt.state) // 'free'

// Mermaid diagram for the concurrent composition
console.log(concurrentToMermaidStateDiagram(multiAgent.build()))
// stateDiagram-v2
//   state "worktree (×2)" as worktree {
//     [*] --> worktree_free
//     worktree_free --> worktree_acquiring: acquire
//     ...
//   }

What this demonstrates:

concurrent() builder composes machine instances
Indexed TLA+ variables: worktree_state[i], worktree_owner[i]
EXCEPT notation for indexed updates
Existential quantification: \E i \in Worktrees: worktree_acquire(i)
Shared state across instances
Concurrent invariants as raw TLA+ (quantified over all instances)
Single-machine specs still work standalone as runtimes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Examples

1. Traffic Light (Simplest)

2. Guarded Counter

3. Agent Session (Full Specification)

4. WorktreeBinding (Concurrent Composition)

FilesExpand file tree

examples.md

Latest commit

History

examples.md

File metadata and controls

Examples

1. Traffic Light (Simplest)

2. Guarded Counter

3. Agent Session (Full Specification)

4. WorktreeBinding (Concurrent Composition)