To avoid testing known invalid states (like integer underflow), maintain a model_count in your TestState. Use next_state to track the expected value, op_generators to filter available operations, and preconditions_met to ensure the framework only attempts valid operations.
// 1. Update state to track model
struct TestState {
model_count: usize,
}
// 2. Update model in next_state
fn next_state(&mut self, op: &Self::Operation) {
match op {
CounterOp::Inc => self.model_count += 1,
CounterOp::Dec => self.model_count -= 1,
}
}
// 3. Use model to filter generators
fn op_generators(&self) -> Vec<Self::OperationStrategy> {
let mut ops = vec![Just(CounterOp::Inc).boxed()];
if self.model_count > 0 {
ops.push(Just(CounterOp::Dec).boxed());
}
ops
}
// 4. Use model for preconditions
fn preconditions_met(&self, op: &Self::Operation) -> bool {
match op {
CounterOp::Inc => true,
CounterOp::Dec => self.model_count > 0,
}
}
