Caelum¶
An LTL model checker.
Caelum reads .lum specification files describing finite-state transition systems
and checks whether declared LTL properties hold over all reachable states.
When a property fails, Caelum produces a counterexample trace.
Features¶
LTL model checking with always, eventually, next, and until operators
Counterexample generation showing exactly how a property fails
Three syntax modes: keyword (
always), ASCII ([]), and Unicode (□)Modular specifications with imports
JSON output for integration with other tools
Deterministic formatter for consistent code style
- Getting Started
- Tutorial
- Notation Primer
- Step 1: A Single Traffic Light
- Step 2: Adding Transitions
- Step 3: Safety Properties
- Step 4: Liveness Properties
- Step 5: Two Lights at an Intersection
- Step 6: Mutual Exclusion
- Step 7: Fairness Properties
- Step 8: Invalid Properties
- Running the Full Specification
- Summary of Language Features Used
- Language Guide
- CLI Reference
- Examples
- Full Specification