Skip to content

tla-compilation.md

Latest commit

 

History

History
86 lines (62 loc) · 1.96 KB

tla-compilation.md

File metadata and controls

86 lines (62 loc) · 1.96 KB

TLA+ Compilation

How JavaScript Compiles to TLA+

The compiler operates on function source strings (captured via .toString()). It tokenizes, parses into a simple AST, then translates node-by-node to TLA+ syntax.

Guards → TLA+ Boolean Expressions

// Input
ctx => ctx.toolsInFlight === 0 || ['working', 'shutting_down'].includes(ctx.state)

// Output
(toolsInFlight = 0) \/ (state \in {"working", "shutting_down"})

Actions → TLA+ Next-State Assignments

// Input
ctx => { ctx.messageQueue.shift(); ctx.contextSize += 1 }

// Output
messageQueue' = Tail(messageQueue)
contextSize' = contextSize + 1

Full Transition Example

.transition('startWork', {
  from: 'idle',
  to: 'working',
  guard: ctx => ctx.messageQueue.length > 0,
  action: ctx => { ctx.messageQueue.shift(); ctx.contextSize += 1 },
})

Compiles to:

startWork ==
  /\ state = "idle"
  /\ (Len(messageQueue) > 0)
  /\ state' = "working"
  /\ messageQueue' = Tail(messageQueue)
  /\ contextSize' = contextSize + 1
  /\ UNCHANGED <<toolsInFlight, shutdownRequested>>

Invariants → TLA+ Properties

.invariant('terminal states are clean',
  ctx => !['complete', 'error'].includes(ctx.state) || ctx.toolsInFlight === 0)

Compiles to:

terminal_states_are_clean == ~((state \in {"complete", "error"})) \/ (toolsInFlight = 0)

Liveness → TLA+ Temporal Properties

.liveness('shutdown completes', 'shutting_down', ['complete', 'error'])

Compiles to:

shutdown_completes == state = "shutting_down" ~> state \in {"complete", "error"}

Compilation Limits

The compiler deliberately rejects:

  • Closures and captured variables
  • Async/await
  • Arbitrary function calls (only .push(), .shift(), .includes(), .has(), Math.floor())
  • Loops (for, while)
  • Object spread/destructuring in complex forms

When something can't be compiled, use .rawTLA() or .temporal() escape hatches.