Examples¶
Annotated walkthroughs of the example scripts in the examples/ directory. Each example demonstrates a key module with detailed explanations.
| Example | Module | Description |
|---|---|---|
| RAG Pipeline Verification | algebra + verification + topology | End-to-end: 4-agent pipeline, deadlock detection, timeout fix, spectral analysis, CTL model checking |
| CSP Composition | algebra | All 13 CSP operators, LTS analysis, deadlock detection |
| Interrupt & Timeout | algebra | 5 agent-specific extensions with practical scenarios |
| Consensus Specification | algebra + specifications | 3-agent consensus modeled in CSP |
| Mesh Topology | topology | Spectral analysis, topology comparison |
| Protocol Verification | mpst | MPST global types, projection, well-formedness |
| Temporal Verification | verification | CTL model checking: safety, liveness, mutual exclusion |
| Probabilistic Verification | verification | DTMC reachability, steady-state, expected steps |
| Counterexample Generation | verification | Structured failure explanations for refinement/equivalence |
All examples are runnable: