tla_connect/
error.rs

1//! Typed errors for tla-connect.
2//!
3//! Provides structured error types instead of anyhow for better
4//! library ergonomics and pattern matching.
5
6#[cfg(any(feature = "replay", feature = "trace-gen", feature = "trace-validation", feature = "rpc"))]
7use std::path::PathBuf;
8use thiserror::Error;
9
10/// Shared error for Apalache CLI execution failures.
11///
12/// Used by both `TraceGenError` and `ValidationError` to avoid duplication.
13#[cfg(any(feature = "trace-gen", feature = "trace-validation"))]
14#[derive(Debug, Error)]
15#[non_exhaustive]
16pub enum ApalacheError {
17    /// Apalache execution failed with a non-zero exit code.
18    #[error("Apalache failed (exit code: {exit_code:?}): {message}")]
19    Execution { exit_code: Option<i32>, message: String },
20
21    /// Apalache binary not found or not executable.
22    #[error("Failed to execute Apalache. Is it installed and on PATH? {0}")]
23    NotFound(String),
24
25    /// Apalache timed out after the specified duration.
26    #[error("Apalache timed out after {duration:?}")]
27    Timeout { duration: std::time::Duration },
28}
29
30/// Shared error for directory read failures.
31///
32/// Used by both `ReplayError` and `TraceGenError` to avoid duplication.
33#[cfg(any(feature = "replay", feature = "trace-gen"))]
34#[derive(Debug, Error)]
35#[error("Failed to read directory {path}: {reason}")]
36pub struct DirectoryReadError {
37    pub path: PathBuf,
38    pub reason: String,
39}
40
41/// Context for a step-level error, identifying where in a test run the error occurred.
42#[cfg(any(feature = "replay", feature = "rpc"))]
43#[derive(Debug, Clone)]
44pub enum StepContext {
45    Replay { trace: usize, state: usize },
46    Rpc { run: usize, step: usize },
47}
48
49#[cfg(any(feature = "replay", feature = "rpc"))]
50impl std::fmt::Display for StepContext {
51    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
52        match self {
53            StepContext::Replay { trace, state } => write!(f, "Trace {trace}, state {state}"),
54            StepContext::Rpc { run, step } => write!(f, "Run {run}, step {step}"),
55        }
56    }
57}
58
59/// Shared error for step-level failures during replay or interactive testing.
60///
61/// Consolidates the duplicated error variants from `ReplayError` and `RpcError`.
62#[cfg(any(feature = "replay", feature = "rpc"))]
63#[derive(Debug, Error)]
64pub enum StepError {
65    /// Failed to execute action on driver.
66    #[error("{context}: failed to execute action '{action}': {reason}")]
67    StepExecution { context: StepContext, action: String, reason: String },
68
69    /// Failed to deserialize spec state.
70    #[error("{context}: failed to deserialize spec state: {reason}")]
71    SpecDeserialize { context: StepContext, reason: String },
72
73    /// Failed to extract driver state.
74    #[error("{context}: failed to extract driver state: {reason}")]
75    DriverStateExtraction { context: StepContext, reason: String },
76
77    /// State mismatch between spec and driver.
78    #[error("State mismatch at {context} (action: '{action}'):\n{diff}")]
79    StateMismatch { context: StepContext, action: String, diff: String },
80}
81
82/// Top-level error type for tla-connect operations.
83#[derive(Debug, Error)]
84#[non_exhaustive]
85pub enum Error {
86    /// Error during ITF trace replay.
87    #[cfg(feature = "replay")]
88    #[error("Replay error: {0}")]
89    Replay(#[from] ReplayError),
90
91    /// Error during Apalache trace generation.
92    #[cfg(feature = "trace-gen")]
93    #[error("Trace generation error: {0}")]
94    TraceGen(#[from] TraceGenError),
95
96    /// Error during trace validation.
97    #[cfg(feature = "trace-validation")]
98    #[error("Trace validation error: {0}")]
99    Validation(#[from] ValidationError),
100
101    /// Error during RPC communication with Apalache server.
102    #[cfg(feature = "rpc")]
103    #[error("RPC error: {0}")]
104    Rpc(#[from] RpcError),
105
106    /// Error during a step (shared between replay and RPC).
107    #[cfg(any(feature = "replay", feature = "rpc"))]
108    #[error("Step error: {0}")]
109    Step(#[from] StepError),
110
111    /// Error in driver step execution.
112    #[error("Driver error: {0}")]
113    Driver(#[from] DriverError),
114
115    /// Error during configuration building.
116    #[error("Builder error: {0}")]
117    Builder(#[from] BuilderError),
118
119    /// IO error.
120    #[error("IO error: {0}")]
121    Io(#[from] std::io::Error),
122
123    /// JSON serialization/deserialization error.
124    #[error("JSON error: {0}")]
125    Json(#[from] serde_json::Error),
126}
127
128/// Error during ITF trace replay.
129#[cfg(feature = "replay")]
130#[derive(Debug, Error)]
131#[non_exhaustive]
132pub enum ReplayError {
133    /// Failed to extract MBT variables from ITF state.
134    #[error("Trace {trace}, state {state}: failed to extract MBT vars: {reason}")]
135    MbtVarExtraction {
136        trace: usize,
137        state: usize,
138        reason: String,
139    },
140
141    /// ITF state is not a record.
142    #[error("Expected ITF state to be a Record, got: {found}")]
143    InvalidStateType { found: String },
144
145    /// Failed to parse ITF trace.
146    #[error("Failed to parse ITF trace: {0}")]
147    Parse(String),
148
149    /// Directory read error.
150    #[error(transparent)]
151    DirectoryRead(#[from] DirectoryReadError),
152}
153
154/// Error during Apalache trace generation.
155#[cfg(feature = "trace-gen")]
156#[derive(Debug, Error)]
157#[non_exhaustive]
158pub enum TraceGenError {
159    /// TLA+ spec file not found.
160    #[error("TLA+ spec not found: {0}")]
161    SpecNotFound(PathBuf),
162
163    /// Failed to create temp directory.
164    #[error("Failed to create temp directory: {0}")]
165    TempDir(String),
166
167    /// Apalache CLI error.
168    #[error(transparent)]
169    Apalache(#[from] ApalacheError),
170
171    /// No ITF traces found in output.
172    #[error("No ITF traces found in Apalache output directory: {0}")]
173    NoTracesFound(PathBuf),
174
175    /// Failed to parse ITF trace file.
176    #[error("Failed to parse ITF trace {path}: {reason}")]
177    TraceParse { path: PathBuf, reason: String },
178
179    /// Directory read error.
180    #[error(transparent)]
181    DirectoryRead(#[from] DirectoryReadError),
182}
183
184/// Error during trace validation (Approach 3).
185#[cfg(feature = "trace-validation")]
186#[derive(Debug, Error)]
187#[non_exhaustive]
188pub enum ValidationError {
189    /// TraceSpec file not found.
190    #[error("TraceSpec not found: {0}")]
191    TraceSpecNotFound(PathBuf),
192
193    /// Trace file not found.
194    #[error("Trace file not found: {0}")]
195    TraceFileNotFound(PathBuf),
196
197    /// Trace file is empty.
198    #[error("Trace file is empty: {0}")]
199    EmptyTrace(PathBuf),
200
201    /// Invalid JSON in trace file.
202    #[error("Invalid JSON on line {line}: {reason}")]
203    InvalidJson { line: usize, reason: String },
204
205    /// State must serialize to a JSON object.
206    #[error("State must serialize to a JSON object, got: {found}")]
207    NonObjectState { found: String },
208
209    /// Inconsistent record schema across trace lines.
210    #[error("Inconsistent record schema: line {line} has keys {found:?}, expected {expected:?}")]
211    InconsistentSchema {
212        line: usize,
213        expected: Vec<String>,
214        found: Vec<String>,
215    },
216
217    /// Unsupported JSON value type.
218    #[error("Unsupported JSON value type at line {line}, field '{field}': {reason}")]
219    UnsupportedType {
220        line: usize,
221        field: String,
222        reason: String,
223    },
224
225    /// Float values not supported (TLA+ uses Int).
226    #[error("Float value not supported at line {line}, field '{field}': {value}")]
227    FloatNotSupported {
228        line: usize,
229        field: String,
230        value: f64,
231    },
232
233    /// Failed to convert to TLA+ record.
234    #[error("Failed to convert line {line} to TLA+ record: {reason}")]
235    TlaConversion { line: usize, reason: String },
236
237    /// Apalache CLI error.
238    #[error(transparent)]
239    Apalache(#[from] ApalacheError),
240
241    /// Failed to create work directory.
242    #[error("Failed to create work directory: {0}")]
243    WorkDir(String),
244
245    /// Failed to copy spec files.
246    #[error("Failed to copy spec file {path}: {reason}")]
247    FileCopy { path: PathBuf, reason: String },
248
249    /// IO error during validation.
250    #[error("IO error: {0}")]
251    Io(#[from] std::io::Error),
252
253    /// Cannot emit after StateEmitter has been finished.
254    #[error("Cannot emit after StateEmitter has been finished")]
255    EmitterFinished,
256
257    /// Inconsistent array element types.
258    #[error("Inconsistent array element types at field '{field}': expected {expected}, got {found}")]
259    InconsistentArrayType {
260        field: String,
261        expected: String,
262        found: String,
263    },
264}
265
266/// Error during RPC communication with Apalache server.
267#[cfg(feature = "rpc")]
268#[derive(Debug, Error)]
269#[non_exhaustive]
270pub enum RpcError {
271    /// Failed to create HTTP client.
272    #[error("Failed to create HTTP client: {0}")]
273    ClientCreation(String),
274
275    /// Failed to send request to Apalache server.
276    #[error("Failed to send request to {url}. Is the Apalache server running? {reason}")]
277    RequestFailed { url: String, reason: String },
278
279    /// Failed to parse JSON-RPC response.
280    #[error("Failed to parse JSON-RPC response: {0}")]
281    ResponseParse(String),
282
283    /// JSON-RPC error from server.
284    #[error("Apalache JSON-RPC error {code}: {message}")]
285    JsonRpc { code: i64, message: String },
286
287    /// Missing result in response.
288    #[error("JSON-RPC response missing 'result' field")]
289    MissingResult,
290
291    /// Failed to deserialize result.
292    #[error("Failed to deserialize JSON-RPC result: {0}")]
293    ResultDeserialize(String),
294
295    /// Spec file not found.
296    #[error("Spec file not found: {0}")]
297    SpecNotFound(PathBuf),
298
299    /// Failed to read spec file.
300    #[error("Failed to read spec file {path}: {reason}")]
301    SpecRead { path: PathBuf, reason: String },
302
303    /// Init transition disabled.
304    #[error("Run {run}: Init transition is disabled")]
305    InitDisabled { run: usize },
306
307    /// Constants unsatisfiable.
308    #[error("Run {run}: Constant constraints are unsatisfiable")]
309    ConstantsUnsatisfiable { run: usize },
310
311    /// Trace missing states.
312    #[error("Trace has no states")]
313    EmptyTrace,
314
315    /// Trace missing states array.
316    #[error("Trace missing 'states' array")]
317    MissingStates,
318
319    /// Failed to convert state.
320    #[error("Failed to convert state to ITF Value: {0}")]
321    StateConversion(String),
322}
323
324/// Error during configuration building.
325#[derive(Debug, Error)]
326#[non_exhaustive]
327pub enum BuilderError {
328    /// A required field was not set.
329    #[error("Required field '{field}' was not set on {builder}")]
330    MissingRequiredField { builder: &'static str, field: &'static str },
331}
332
333/// Error during driver step execution.
334#[derive(Debug, Error)]
335#[non_exhaustive]
336pub enum DriverError {
337    /// Unknown action encountered.
338    #[error("Unknown action: {0}")]
339    UnknownAction(String),
340
341    /// Action execution failed.
342    #[error("Action '{action}' failed: {reason}")]
343    ActionFailed { action: String, reason: String },
344
345    /// State extraction failed.
346    #[error("Failed to extract state: {0}")]
347    StateExtraction(String),
348}
349
350/// Result type alias using tla-connect's Error.
351pub type TlaResult<T> = std::result::Result<T, Error>;
tla_connect/error.rs

tla_connect/
error.rs
