Getting Started

Prerequisites

Installation

git clone https://github.com/dhilst/caelum.git
cd caelum
cargo build --release

The binary is at target/release/caelum.

Your First Specification

Create a file called counter.lum:

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)
}

Run it:

caelum counter.lum

Both properties should pass. The counter wraps around from max back to 0, so it always returns to zero and always stays in range.

Understanding Output

On success, Caelum prints a summary and exits with code 0:

checking counter.lum
  in_range ........... PASS
  returns_to_zero .... PASS

On failure, Caelum shows which property failed and exits with code 1. Use --show-trace to see the counterexample trace.

Next Steps