quint_connect/driver/
mod.rs

1mod nondet;
2mod state;
3mod step;
4
5pub use state::State;
6pub use step::Step;
7
8/// A convenience type alias for [`anyhow::Result`] used throughout this crate.
9///
10/// This type defaults to `Result<()>` when no type parameter is provided, making it
11/// ergonomic for functions that return success/failure without a value.
12pub type Result<A = ()> = anyhow::Result<A>;
13
14/// A static path used to navigate nested structures in Quint specifications.
15///
16/// Paths are represented as static string slices and are used in [`Config`] to specify
17/// where to find state and nondeterministic picks within the specification's state space.
18///
19/// # Examples
20///
21/// ```rust
22/// use quint_connect::Config;
23///
24/// let config = Config {
25///     state: &["global_var", "nested_record", "my_state"],
26///     nondet: &["nondet_choices"],
27/// };
28/// ```
29pub type Path = &'static [&'static str];
30
31/// Configuration for a [`Driver`] that specifies where to find state and nondeterministic
32/// picks within a Quint specification.
33///
34/// By default, both paths are empty (`&[]`). Empty paths indicate that:
35/// - State is extracted from the top level of the specification's state space
36/// - Nondeterministic picks are extracted from Quint's builtin `mbt::actionTaken` and
37///   `mbt::nondetPicks` variables
38///
39/// Override these paths when your specification nests the relevant state within a larger
40/// structure, or when tracking nondeterminism manually rather than using Quint's builtin
41/// variables.
42///
43/// # Examples
44///
45/// Specifying custom paths for nested state:
46///
47/// ```rust
48/// use quint_connect::{Driver, Config};
49/// # use quint_connect::{Step, Result, State};
50/// #
51/// # #[derive(Debug, PartialEq, serde::Deserialize)]
52/// # struct MyState;
53/// #
54/// # impl State<MyDriver> for MyState {
55/// #     fn from_driver(driver: &MyDriver) -> Result<Self> { Ok(MyState) }
56/// # }
57/// #
58/// # struct MyDriver;
59///
60/// impl Driver for MyDriver {
61///     type State = MyState;
62///
63///     fn config() -> Config {
64///         Config {
65///             state: &["global_var", "nested_record", "my_state"],
66///             nondet: &["global_var", "nondet_choices"],
67///         }
68///     }
69///
70///     fn step(&mut self, step: &Step) -> Result {
71///         // ...
72/// #       Ok(())
73///     }
74/// }
75/// ```
76#[derive(Default)]
77pub struct Config {
78    /// Path to the state within the Quint specification's state space.
79    ///
80    /// An empty path (`&[]`) indicates the state is at the top level.
81    pub state: Path,
82
83    /// Path to nondeterministic picks within the Quint specification's state space.
84    ///
85    /// An empty path (`&[]`) uses Quint's builtin `mbt::actionTaken` and `mbt::nondetPicks`
86    /// variables.
87    pub nondet: Path,
88}
89
90/// Core trait for connecting Rust implementations to Quint specifications.
91///
92/// Implementations of this trait define how to execute steps from a Quint trace against
93/// a Rust implementation, enabling model-based testing. The framework automatically
94/// generates traces from your Quint specification and replays them through your driver,
95/// verifying that the implementation state matches the specification state after each step.
96///
97/// See the [Quick Start](crate#quick-start) and [Examples](crate#examples) sections in the
98/// crate docs for examples.
99///
100/// # Associated Types
101///
102/// - [`State`]: The state type that can be extracted from both the driver implementation
103///   and the Quint specification for comparison.
104///
105/// # Required Methods
106///
107/// - [`step`](Driver::step): Processes a single step from the trace, typically by
108///   pattern-matching on the action name and nondeterministic picks, then executing the
109///   corresponding implementation code.
110///
111/// # Optional Methods
112///
113/// - [`config`](Driver::config): Returns configuration specifying where to find state
114///   and nondeterministic picks in the specification. Defaults to top-level paths.
115pub trait Driver: Sized {
116    /// The state type that can be extracted from both the driver and the specification.
117    ///
118    /// This type must implement [`State`] to provide state extraction and comparison logic.
119    /// Note that stateless drivers can set `State = ()` to disable state checking.
120    type State: State<Self>;
121
122    /// Processes a single step from a Quint trace.
123    ///
124    /// This method is called for each step in a generated trace. Implementations typically
125    /// use the [`switch!`](crate::switch) macro to pattern-match on the action name and
126    /// execute the corresponding implementation code.
127    fn step(&mut self, step: &Step) -> Result;
128
129    /// Returns configuration for this driver.
130    ///
131    /// Override this method to specify custom paths for extracting state and
132    /// nondeterministic picks from nested structures in the specification.
133    fn config() -> Config {
134        Config::default()
135    }
136}
quint_connect/driver/mod.rs

quint_connect/driver/
mod.rs
