use crate::TestCase;
use crate::generators::integers;
use crate::runner::Mode;
use crate::test_case::{ASSUME_FAIL_STRING, STOP_TEST_STRING};
use std::cmp::min;
use std::collections::HashMap;
use std::panic::{AssertUnwindSafe, catch_unwind, resume_unwind};
pub struct Rule<M: ?Sized> {
pub name: String,
pub apply: fn(&mut M, TestCase),
}
impl<M> Rule<M> {
pub fn new(name: &str, apply: fn(&mut M, TestCase)) -> Self {
Rule {
name: name.to_string(),
apply,
}
}
}
pub struct Variables<T> {
pool_id: i128,
tc: TestCase,
values: HashMap<i128, T>,
}
impl<T> Variables<T> {
fn pool_generate(&self, consume: bool) -> i128 {
match self
.tc
.with_data_source(|ds| ds.pool_generate(self.pool_id, consume))
{
Ok(id) => id,
Err(_) => {
panic!("{}", STOP_TEST_STRING);
}
}
}
pub fn empty(&self) -> bool {
self.values.is_empty()
}
pub fn add(&mut self, v: T) {
let variable_id: i128 = match self.tc.with_data_source(|ds| ds.pool_add(self.pool_id)) {
Ok(id) => id,
Err(_) => {
panic!("{}", STOP_TEST_STRING); }
};
if self.values.contains_key(&variable_id) {
panic!("unexpected variable id in map"); }
self.values.insert(variable_id, v);
}
pub fn draw(&self) -> &T {
self.tc.assume(!self.empty());
let variable_id = self.pool_generate(false);
self.values.get(&variable_id).unwrap()
}
pub fn consume(&mut self) -> T {
self.tc.assume(!self.empty());
let variable_id = self.pool_generate(true);
self.values.remove(&variable_id).unwrap()
}
}
pub fn variables<T>(tc: &TestCase) -> Variables<T> {
let pool_id = match tc.with_data_source(|ds| ds.new_pool()) {
Ok(id) => id,
Err(_) => {
panic!("{}", STOP_TEST_STRING); }
};
Variables {
pool_id,
tc: tc.clone(),
values: HashMap::new(),
}
}
pub trait StateMachine {
fn rules(&self) -> Vec<Rule<Self>>;
fn invariants(&self) -> Vec<Rule<Self>>;
}
fn panic_message(payload: &Box<dyn std::any::Any + Send>) -> String {
if let Some(s) = payload.downcast_ref::<&str>() {
s.to_string() } else if let Some(s) = payload.downcast_ref::<String>() {
s.clone()
} else {
"Unknown panic".to_string() }
}
fn check_invariants(m: &mut impl StateMachine, tc: &TestCase) {
let invariants = m.invariants();
for invariant in invariants {
let inv_tc = tc.child(2); (invariant.apply)(m, inv_tc); }
}
pub fn run(mut m: impl StateMachine, tc: TestCase) {
let rules = m.rules();
if rules.is_empty() {
panic!("Cannot run a machine with no rules."); }
let rule_index = integers::<usize>().min_value(0).max_value(rules.len() - 1);
tc.note("Initial invariant check.");
check_invariants(&mut m, &tc);
let is_single = tc.mode() == Mode::SingleTestCase;
let step_cap = if is_single {
i64::MAX
} else {
let max_steps = 50;
let unbounded_step_cap = tc.draw_silent(integers::<i64>().min_value(1));
min(unbounded_step_cap, max_steps)
};
let mut steps_run_successfully = 0;
let mut steps_attempted = 0;
let mut step = 0;
while steps_run_successfully < step_cap
&& (is_single
|| steps_attempted < 10 * step_cap
|| (steps_run_successfully == 0 && steps_attempted < 1000))
{
step += 1;
let rule = &rules[tc.draw_silent(&rule_index)];
tc.note(&format!("Step {}: {}", step, rule.name));
let rule_tc = tc.child(2);
let thunk = || (rule.apply)(&mut m, rule_tc);
let result = catch_unwind(AssertUnwindSafe(thunk));
steps_attempted += 1;
match result {
Ok(()) => {
steps_run_successfully += 1;
check_invariants(&mut m, &tc);
}
Err(e) => {
let msg = panic_message(&e);
if msg == STOP_TEST_STRING {
break;
} else if msg != ASSUME_FAIL_STRING {
tc.note("Rule stopped early due to violated assumption.");
resume_unwind(e);
}
}
};
}
}