Skip to main content

hegel/
stateful.rs

1//! Stateful (model-based) testing support.
2//!
3//! State machines are defined using the [`state_machine`](crate::state_machine) attribute macro.
4//! Methods annotated with `#[rule]` become rules (actions applied to the state machine) and
5//! methods annotated with `#[invariant]` become invariants (checked after each successful rule
6//! application). Rules must have signature `fn(&mut self, tc: TestCase)` and invariants must have
7//! signature `fn(&self, tc: TestCase)`.
8//!
9//! To run a state machine, call [`run()`] inside a Hegel test.
10//!
11//! Example:
12//! ```rust
13//! use hegel::TestCase;
14//! use hegel::generators as gs;
15//!
16//! struct IntegerStack {
17//!     stack: Vec<i32>,
18//! }
19//!
20//! #[hegel::state_machine]
21//! impl IntegerStack {
22//!     #[rule]
23//!     fn push(&mut self, tc: TestCase) {
24//!         let integers = gs::integers::<i32>;
25//!         let element = tc.draw(integers());
26//!         self.stack.push(element);
27//!     }
28//!
29//!     #[rule]
30//!     fn pop(&mut self, _: TestCase) {
31//!         self.stack.pop();
32//!     }
33//!
34//!     #[rule]
35//!     fn pop_push(&mut self, tc: TestCase) {
36//!         let integers = gs::integers::<i32>;
37//!         let element = tc.draw(integers());
38//!         let initial = self.stack.clone();
39//!         self.stack.push(element);
40//!         let popped = self.stack.pop().unwrap();
41//!         assert_eq!(popped, element);
42//!         assert_eq!(self.stack, initial);
43//!     }
44//!
45//!     #[rule]
46//!     fn push_pop(&mut self, tc: TestCase) {
47//!         let initial = self.stack.clone();
48//!         let element = self.stack.pop();
49//!         tc.assume(element.is_some());
50//!         let element = element.unwrap();
51//!         self.stack.push(element);
52//!         assert_eq!(self.stack, initial);
53//!     }
54//! }
55//!
56//! #[hegel::test]
57//! fn test_integer_stack(tc: TestCase) {
58//!     let stack = IntegerStack { stack: Vec::new() };
59//!     hegel::stateful::run(stack, tc);
60//! }
61//! ```
62
63use crate::TestCase;
64use crate::generators::integers;
65use crate::runner::Mode;
66use crate::test_case::{ASSUME_FAIL_STRING, STOP_TEST_STRING};
67use std::cmp::min;
68use std::collections::HashMap;
69use std::panic::{AssertUnwindSafe, catch_unwind, resume_unwind};
70
71/// A rule that can be applied to the state machine during testing.
72pub struct Rule<M: ?Sized> {
73    pub name: String,
74    pub apply: fn(&mut M, TestCase),
75}
76
77impl<M> Rule<M> {
78    /// Create a new rule with a name and an apply function.
79    pub fn new(name: &str, apply: fn(&mut M, TestCase)) -> Self {
80        Rule {
81            name: name.to_string(),
82            apply,
83        }
84    }
85}
86
87/// A pool of previously generated values.
88pub struct Variables<T> {
89    pool_id: i64,
90    tc: TestCase,
91    values: HashMap<i64, T>,
92}
93
94impl<T> Variables<T> {
95    fn pool_generate(&self, consume: bool) -> i64 {
96        match self
97            .tc
98            .with_data_source(|ds| ds.pool_generate(self.pool_id, consume))
99        {
100            Ok(id) => id,
101            Err(_) => {
102                panic!("{}", STOP_TEST_STRING);
103            }
104        }
105    }
106
107    /// Returns true if no variables are in the pool.
108    pub fn is_empty(&self) -> bool {
109        self.values.is_empty()
110    }
111
112    /// Number of variables currently in the pool.
113    pub fn len(&self) -> usize {
114        self.values.len()
115    }
116
117    /// Add a value to the pool.
118    pub fn add(&mut self, v: T) {
119        let variable_id: i64 = match self.tc.with_data_source(|ds| ds.pool_add(self.pool_id)) {
120            Ok(id) => id,
121            Err(_) => {
122                panic!("{}", STOP_TEST_STRING); // nocov
123            }
124        };
125        if self.values.contains_key(&variable_id) {
126            panic!("unexpected variable id in map"); // nocov
127        }
128        self.values.insert(variable_id, v);
129    }
130
131    /// Draw a reference to a value from the pool (without removing it).
132    ///
133    /// Calls `assume(false)` if the pool is empty.
134    pub fn draw(&self) -> &T {
135        self.tc.assume(!self.is_empty());
136        let variable_id = self.pool_generate(false);
137        self.values.get(&variable_id).unwrap()
138    }
139
140    /// Remove and return a value from the pool.
141    ///
142    /// Calls `assume(false)` if the pool is empty.
143    pub fn consume(&mut self) -> T {
144        self.tc.assume(!self.is_empty());
145        let variable_id = self.pool_generate(true);
146        self.values.remove(&variable_id).unwrap()
147    }
148}
149
150/// Create a new variable pool for stateful tests.
151pub fn variables<T>(tc: &TestCase) -> Variables<T> {
152    let pool_id = match tc.with_data_source(|ds| ds.new_pool()) {
153        Ok(id) => id,
154        Err(_) => {
155            panic!("{}", STOP_TEST_STRING); // nocov
156        }
157    };
158    Variables {
159        pool_id,
160        tc: tc.clone(),
161        values: HashMap::new(),
162    }
163}
164
165/// Trait for defining a stateful test.
166///
167/// Implement this to define the rules (actions) and invariants (assertions)
168/// of your state machine. Use `#[hegel::state_machine]` for a more
169/// ergonomic way to define state machines.
170pub trait StateMachine {
171    /// The rules (actions) that can be applied to this state machine.
172    fn rules(&self) -> Vec<Rule<Self>>;
173    /// Invariants checked after each successful rule application.
174    fn invariants(&self) -> Vec<Rule<Self>>;
175}
176
177// TODO: factor out (shared with runner.rs)
178fn panic_message(payload: &Box<dyn std::any::Any + Send>) -> String {
179    if let Some(s) = payload.downcast_ref::<&str>() {
180        s.to_string() // nocov
181    } else if let Some(s) = payload.downcast_ref::<String>() {
182        s.clone()
183    } else {
184        "Unknown panic".to_string() // nocov
185    }
186}
187
188fn check_invariants(m: &mut impl StateMachine, tc: &TestCase) {
189    let invariants = m.invariants();
190    for invariant in invariants {
191        let inv_tc = tc.child(2); // nocov
192        (invariant.apply)(m, inv_tc); // nocov
193    }
194}
195
196/// Execute a stateful test by repeatedly applying random rules and checking invariants.
197pub fn run(mut m: impl StateMachine, tc: TestCase) {
198    let rules = m.rules();
199    if rules.is_empty() {
200        panic!("Cannot run a machine with no rules."); // nocov
201    }
202
203    let rule_index = integers::<usize>().min_value(0).max_value(rules.len() - 1);
204
205    tc.note("Initial invariant check.");
206    check_invariants(&mut m, &tc);
207
208    let is_single = tc.mode() == Mode::SingleTestCase;
209
210    let step_cap = if is_single {
211        i64::MAX
212    } else {
213        let max_steps = 50;
214        let unbounded_step_cap = tc.draw_silent(integers::<i64>().min_value(1));
215        min(unbounded_step_cap, max_steps)
216    };
217
218    let mut steps_run_successfully = 0;
219    let mut steps_attempted = 0;
220    let mut step = 0;
221
222    while steps_run_successfully < step_cap
223        && (is_single
224            || steps_attempted < 10 * step_cap
225            || (steps_run_successfully == 0 && steps_attempted < 1000))
226    {
227        step += 1;
228        let rule = &rules[tc.draw_silent(&rule_index)];
229        tc.note(&format!("Step {}: {}", step, rule.name));
230
231        // We only need this because AssertUnwindSafe expects a closure.
232        let rule_tc = tc.child(2);
233        let thunk = || (rule.apply)(&mut m, rule_tc);
234        let result = catch_unwind(AssertUnwindSafe(thunk));
235
236        steps_attempted += 1;
237        match result {
238            Ok(()) => {
239                steps_run_successfully += 1;
240                check_invariants(&mut m, &tc);
241            }
242            Err(e) => {
243                let msg = panic_message(&e);
244                if msg == STOP_TEST_STRING {
245                    // Backend ran out of data — this test case is done.
246                    break;
247                } else if msg != ASSUME_FAIL_STRING {
248                    tc.note("Rule stopped early due to violated assumption.");
249                    resume_unwind(e);
250                }
251            }
252        };
253    }
254}