Playground

A full-page editor for experimenting with Caelum. Unlike the inline editors scattered through these docs (see Trying Caelum in Your Browser), this is a blank scratchpad with room to work and the ability to load and share specifications by URL. It is seeded with a small modular counter. Edit anything and press Check ▶ (or Ctrl-Enter) to re-run the model checker.

Note

The checker is caelum-kernel compiled to WebAssembly, using the pure-Rust varisat backend. Your spec never leaves the page — everything runs locally in your browser.

Load

Note

Load and share specs by URL. Paste any URL into the box above and press Load to open that .lum file — a staged example such as _static/examples/traffic_light.lum, or an absolute link like a raw GitHub file. The address updates to playground.html?q=<url>, so that link is itself shareable: send it to anyone and the playground loads the spec automatically. (Cross-origin hosts must allow it via CORS; raw GitHub does.)

Tip

When a property fails, the results pane shows a counterexample trace — one row per state, with the transition taken between states and, for a liveness (□ ◇) property, a ⟲ marker on the state the infinite loop returns to. A parse or type error is underlined inline at the offending location.