dsl-reference.md

DSL Reference

machine(name: string)

Creates a new machine specification builder.

.states(...names: string[])

Declare possible states. Required.

.initial(state: string)

Set the initial state. Must be in the states list. Required.

.context<C>(defaults: C)

Define extended state (context). Each key becomes a TLA+ variable. Types are inferred from default values.

Supported types: number, string, boolean, null, arrays, Maps.

.transition(name, def)

Define a named transition.

.transition('name', {
  from: 'state' | ['state1', 'state2'],  // Required
  to?: 'targetState',                      // Optional (self-transition if omitted)
  guard?: (ctx) => boolean,                // Optional precondition
  action?: (ctx) => void,                  // Optional state mutation
})

.invariant(name, predicate)

Safety invariant — must hold in every reachable state.

.invariant('bounded', ctx => ctx.count <= 10)

.liveness(name, from, to)

Liveness property — from condition eventually leads to target condition.

// State-based
.liveness('completes', 'working', ['done', 'error'])

// Predicate-based
.liveness('drains', ctx => ctx.queue.length > 0, ctx => ctx.queue.length === 0)

.temporal(name, tlaExpression)

Raw TLA+ temporal property (escape hatch).

.rawTLA(tla: string)

Include raw TLA+ in the generated spec.

.build()

Validate and return the MachineAST.

---

concurrent(name: string)

Creates a concurrent composition builder.

.instances(name, machine, { count })

Add a group of machine instances.

.shared(name, initial)

Declare shared state between instances.

.interaction(name, bodyOrTLA?)

Define an interaction between instance groups.

.invariant(name, predicateOrTLA)

Concurrent invariant (TLA+ string or function).

.fairness('weak' | 'strong')

Set fairness level (default: 'weak').

.build()

Validate and return the ConcurrentAST.

---

Constrained JS Subset

Guards and actions must use only:

JavaScript	TLA+
ctx.x === 0	x = 0
ctx.x !== 0	x # 0
ctx.x < 10	x < 10
ctx.arr.length	Len(arr)
ctx.arr.push(x)	arr' = Append(arr, x)
ctx.arr.shift()	arr' = Tail(arr)
[...].includes(ctx.x)	x \in {...}
ctx.map.has(key)	key \in DOMAIN map
Math.floor(x / y)	x \div y
ctx.x += 1	x' = x + 1
a && b	a /\ b
a || b	a \/ b
!a	~a
c ? a : b	IF c THEN a ELSE b