quint-connect 0.1.0

A model-based testing framework that connects Quint specifications with Rust applications
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136

mod nondet;
mod state;
mod step;

pub use state::State;
pub use step::Step;

/// A convenience type alias for [`anyhow::Result`] used throughout this crate.
///
/// This type defaults to `Result<()>` when no type parameter is provided, making it
/// ergonomic for functions that return success/failure without a value.
pub type Result<A = ()> = anyhow::Result<A>;

/// A static path used to navigate nested structures in Quint specifications.
///
/// Paths are represented as static string slices and are used in [`Config`] to specify
/// where to find state and nondeterministic picks within the specification's state space.
///
/// # Examples
///
/// ```rust
/// use quint_connect::Config;
///
/// let config = Config {
///     state: &["global_var", "nested_record", "my_state"],
///     nondet: &["nondet_choices"],
/// };
/// ```
pub type Path = &'static [&'static str];

/// Configuration for a [`Driver`] that specifies where to find state and nondeterministic
/// picks within a Quint specification.
///
/// By default, both paths are empty (`&[]`). Empty paths indicate that:
/// - State is extracted from the top level of the specification's state space
/// - Nondeterministic picks are extracted from Quint's builtin `mbt::actionTaken` and
///   `mbt::nondetPicks` variables
///
/// Override these paths when your specification nests the relevant state within a larger
/// structure, or when tracking nondeterminism manually rather than using Quint's builtin
/// variables.
///
/// # Examples
///
/// Specifying custom paths for nested state:
///
/// ```rust
/// use quint_connect::{Driver, Config};
/// # use quint_connect::{Step, Result, State};
/// #
/// # #[derive(Debug, PartialEq, serde::Deserialize)]
/// # struct MyState;
/// #
/// # impl State<MyDriver> for MyState {
/// #     fn from_driver(driver: &MyDriver) -> Result<Self> { Ok(MyState) }
/// # }
/// #
/// # struct MyDriver;
///
/// impl Driver for MyDriver {
///     type State = MyState;
///
///     fn config() -> Config {
///         Config {
///             state: &["global_var", "nested_record", "my_state"],
///             nondet: &["global_var", "nondet_choices"],
///         }
///     }
///
///     fn step(&mut self, step: &Step) -> Result {
///         // ...
/// #       Ok(())
///     }
/// }
/// ```
#[derive(Default)]
pub struct Config {
    /// Path to the state within the Quint specification's state space.
    ///
    /// An empty path (`&[]`) indicates the state is at the top level.
    pub state: Path,

    /// Path to nondeterministic picks within the Quint specification's state space.
    ///
    /// An empty path (`&[]`) uses Quint's builtin `mbt::actionTaken` and `mbt::nondetPicks`
    /// variables.
    pub nondet: Path,
}

/// Core trait for connecting Rust implementations to Quint specifications.
///
/// Implementations of this trait define how to execute steps from a Quint trace against
/// a Rust implementation, enabling model-based testing. The framework automatically
/// generates traces from your Quint specification and replays them through your driver,
/// verifying that the implementation state matches the specification state after each step.
///
/// See the [Quick Start](crate#quick-start) and [Examples](crate#examples) sections in the
/// crate docs for examples.
///
/// # Associated Types
///
/// - [`State`]: The state type that can be extracted from both the driver implementation
///   and the Quint specification for comparison.
///
/// # Required Methods
///
/// - [`step`](Driver::step): Processes a single step from the trace, typically by
///   pattern-matching on the action name and nondeterministic picks, then executing the
///   corresponding implementation code.
///
/// # Optional Methods
///
/// - [`config`](Driver::config): Returns configuration specifying where to find state
///   and nondeterministic picks in the specification. Defaults to top-level paths.
pub trait Driver: Sized {
    /// The state type that can be extracted from both the driver and the specification.
    ///
    /// This type must implement [`State`] to provide state extraction and comparison logic.
    /// Note that stateless drivers can set `State = ()` to disable state checking.
    type State: State<Self>;

    /// Processes a single step from a Quint trace.
    ///
    /// This method is called for each step in a generated trace. Implementations typically
    /// use the [`switch!`](crate::switch) macro to pattern-match on the action name and
    /// execute the corresponding implementation code.
    fn step(&mut self, step: &Step) -> Result;

    /// Returns configuration for this driver.
    ///
    /// Override this method to specify custom paths for extracting state and
    /// nondeterministic picks from nested structures in the specification.
    fn config() -> Config {
        Config::default()
    }
}