Examples

Counter

A simple modular counter that wraps around.

module examples.counter

const max = 3

let x ∈ 0..max

init {
  x = 0
}

transition step {
  x' = (x + 1) mod (max + 1)
}

property in_range {
  □ (x >= 0 ∧ x <= max)
}

property returns_to_zero {
  □ ◇ (x = 0)
}

Properties:

• in_range: The counter always stays within 0..max. Passes because the domain enforces it.

• returns_to_zero: The counter always eventually returns to zero. Passes because it cycles.

Failing Invariant

Demonstrates a property that fails with a counterexample.

module examples.failing_invariant

let x ∈ 0..2

init {
  x = 0
}

transition step {
  x' = (x + 1) mod 3
}

property never_two {
  □ (x ≠ 2)
}

The property never_two claims x is never 2, but the counter reaches 2 on the third step. Run with --show-trace to see the counterexample:

caelum --show-trace examples/failing_invariant.lum

Implication and Equivalence

let x ∈ 0..1

init { x = 0 }

transition toggle { x' = 1 - x }

property implies_example {
  □ (x = 0 → ◯ x = 1)
}

property iff_example {
  □ (x = 0 ↔ ◯ x = 1)
}

Both properties pass: when x = 0, the next state always has x = 1, and vice versa.

Crossroad Traffic Light

Two traffic lights sharing a named Color type, with mutual exclusion and fairness properties. This example demonstrates the type keyword for reusable enum domains.

type Color = enum { red, green, yellow }

let traf1 ∈ Color
let traf2 ∈ Color
let timer ∈ 0..5

init {
  traf1 = green ∧ traf2 = red ∧ timer = 5
}

transition tick {
  timer > 0 ∧ timer' = timer - 1 ∧ traf1' = traf1 ∧ traf2' = traf2
}

transition traf1_to_yellow {
  traf1 = green ∧ timer = 0 ∧ traf1' = yellow ∧ traf2' = red ∧ timer' = 2
}

transition swap_to_traf2 {
  traf1 = yellow ∧ timer = 0 ∧ traf1' = red ∧ traf2' = green ∧ timer' = 5
}

transition traf2_to_yellow {
  traf2 = green ∧ timer = 0 ∧ traf2' = yellow ∧ traf1' = red ∧ timer' = 2
}

transition swap_to_traf1 {
  traf2 = yellow ∧ timer = 0 ∧ traf2' = red ∧ traf1' = green ∧ timer' = 5
}

property mutual_exclusion {
  □ ¬ (traf1 = green ∧ traf2 = green)
}

property traf1_eventually_green {
  □ ◇ (traf1 = green)
}

invalid both_green {
  ◇ (traf1 = green ∧ traf2 = green)
}

Properties:

• mutual_exclusion: Both lights are never green simultaneously.

• traf1_eventually_green: Traffic light 1 always eventually gets a green phase.

• both_green (invalid): Claims both lights are eventually green at once — correctly fails because the transitions prevent it.

See examples/crossroad_traffic_light.lum for the full specification with all safety, liveness, and fairness properties. The Tutorial walks through building this example step by step.