tla_connect/
lib.rs

1//! tla-connect: TLA+/Apalache integration for model-based testing.
2//!
3//! Provides three complementary approaches for connecting TLA+ formal
4//! specifications to Rust implementations:
5//!
6//! 1. **Approach 1 (Apalache -> ITF -> replay)**: Batch trace generation + replay.
7//!    Apalache generates ITF traces from TLA+ specs, which are replayed against
8//!    a Rust `Driver`. Direct equivalent of the Quint/quint-connect workflow.
9//!    Requires features: `replay`, `trace-gen`.
10//!
11//! 2. **Approach 2 (Apalache JSON-RPC)**: Interactive symbolic testing.
12//!    Step-by-step symbolic execution via Apalache's explorer server, interleaved
13//!    with Rust implementation execution. Requires feature: `rpc`.
14//!
15//! 3. **Approach 3 (Rust -> NDJSON -> Apalache)**: Post-hoc trace validation.
16//!    Record Rust execution traces as NDJSON, then validate against a TLA+
17//!    TraceSpec using Apalache. Requires feature: `trace-validation`.
18//!
19//! Approaches 1 & 2 catch "implementation doesn't handle a case the spec allows."
20//! Approach 3 catches "implementation does something the spec doesn't allow."
21//!
22//! # Feature Flags
23//!
24//! - `replay` (default): ITF trace replay against a Driver
25//! - `trace-gen` (default): Apalache CLI trace generation
26//! - `trace-validation` (default): Post-hoc NDJSON trace validation
27//! - `rpc`: Interactive symbolic testing via Apalache JSON-RPC
28//! - `parallel`: Parallel trace replay using rayon
29//! - `full`: Enable all features
30//!
31//! # Quick Start (Approach 1)
32//!
33//! ```ignore
34//! use tla_connect::*;
35//!
36//! #[derive(Debug, PartialEq, Deserialize)]
37//! struct MyState { /* TLA+ vars to compare */ }
38//!
39//! impl State for MyState {}
40//!
41//! impl ExtractState<MyDriver> for MyState {
42//!     fn from_driver(driver: &MyDriver) -> Result<Self, DriverError> { /* ... */ }
43//! }
44//!
45//! struct MyDriver { /* Rust type under test */ }
46//!
47//! impl Driver for MyDriver {
48//!     type State = MyState;
49//!     fn step(&mut self, step: &Step) -> Result<(), DriverError> {
50//!         switch!(step {
51//!             "init" => { /* init */ Ok(()) },
52//!             "action1" => { /* ... */ Ok(()) },
53//!         })
54//!     }
55//! }
56//!
57//! let traces = generate_traces(&ApalacheConfig {
58//!     spec: "../../formal/tla/MySpec.tla".into(),
59//!     ..Default::default()
60//! })?;
61//! replay_traces(|| MyDriver::default(), &traces.traces)?;
62//! ```
63
64mod builder;
65pub mod driver;
66pub mod error;
67
68#[cfg(feature = "replay")]
69pub mod replay;
70
71#[cfg(feature = "rpc")]
72pub mod rpc;
73
74#[cfg(feature = "trace-gen")]
75pub mod trace_gen;
76
77#[cfg(feature = "trace-validation")]
78pub mod trace_validation;
79
80mod util;
81
82// Re-export core types (always available)
83pub use driver::{debug_diff, Driver, ExtractState, State, Step};
84pub use error::{BuilderError, DriverError, Error, TlaResult};
85
86#[cfg(any(feature = "trace-gen", feature = "trace-validation"))]
87pub use error::ApalacheError;
88#[cfg(any(feature = "replay", feature = "trace-gen"))]
89pub use error::DirectoryReadError;
90#[cfg(feature = "replay")]
91pub use error::ReplayError;
92#[cfg(feature = "trace-gen")]
93pub use error::TraceGenError;
94#[cfg(feature = "trace-validation")]
95pub use error::ValidationError;
96#[cfg(any(feature = "replay", feature = "rpc"))]
97pub use error::{StepContext, StepError};
98
99// Re-export replay types
100#[cfg(feature = "replay")]
101pub use replay::{
102    replay_trace_str, replay_traces, replay_traces_with_progress, ReplayProgress, ReplayProgressFn,
103    ReplayStats,
104};
105
106#[cfg(feature = "parallel")]
107pub use replay::replay_traces_parallel;
108
109// Re-export RPC types
110#[cfg(feature = "rpc")]
111pub use error::RpcError;
112#[cfg(feature = "rpc")]
113pub use rpc::{
114    interactive_test, interactive_test_with_progress, ApalacheRpcClient, InteractiveConfig,
115    InteractiveConfigBuilder, InteractiveProgress, InteractiveProgressFn, InteractiveStats,
116    RetryConfig,
117};
118
119// Re-export trace generation types
120#[cfg(feature = "trace-gen")]
121pub use trace_gen::{generate_traces, ApalacheConfig, ApalacheConfigBuilder, ApalacheMode, GeneratedTraces};
122
123// Re-export trace validation types
124#[cfg(feature = "trace-validation")]
125pub use trace_validation::{validate_trace, StateEmitter, TraceResult, TraceValidatorConfig, TraceValidatorConfigBuilder};
126#[cfg(feature = "trace-validation")]
127#[doc(hidden)]
128pub use trace_validation::ndjson_to_tla_module;
tla_connect/lib.rs

tla_connect/
lib.rs
