use crate::TestCase;
use crate::control::{AssumeFailed, hegel_internal_assert};
use crate::generators::{Generator, integers};
use crate::runner::Mode;
use crate::test_case::raise_for_rc;
use std::cell::RefCell;
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 Pool<T> {
pool_id: i64,
tc: TestCase,
values: HashMap<i64, T>,
}
fn pool_generate(tc: &TestCase, pool_id: i64, consume: bool) -> i64 {
match tc.with_ctc(|ctc| ctc.pool_generate(pool_id, consume)) {
Ok(id) => id,
Err(rc) => raise_for_rc(rc),
}
}
impl<T> Pool<T> {
pub fn is_empty(&self) -> bool {
self.values.is_empty()
}
pub fn len(&self) -> usize {
self.values.len()
}
pub fn add(&mut self, v: T) {
let variable_id: i64 = match self.tc.with_ctc(|ctc| ctc.pool_add(self.pool_id)) {
Ok(id) => id,
Err(rc) => raise_for_rc(rc), };
if self.values.contains_key(&variable_id) {
panic!("unexpected variable id in map"); }
self.values.insert(variable_id, v);
}
pub fn values_reusable(&self) -> ValuesReusable<'_, T> {
ValuesReusable {
pool_id: self.pool_id,
values: &self.values,
}
}
pub fn values_consumed(&mut self) -> ValuesConsumed<'_, T> {
ValuesConsumed {
pool_id: self.pool_id,
values: RefCell::new(&mut self.values),
}
}
}
pub struct ValuesReusable<'a, T> {
pool_id: i64,
values: &'a HashMap<i64, T>,
}
impl<'a, T> Generator<&'a T> for ValuesReusable<'a, T> {
fn do_draw(&self, tc: &TestCase) -> &'a T {
tc.assume(!self.values.is_empty());
let variable_id = pool_generate(tc, self.pool_id, false);
self.values.get(&variable_id).unwrap()
}
}
pub struct ValuesConsumed<'a, T> {
pool_id: i64,
values: RefCell<&'a mut HashMap<i64, T>>,
}
impl<T> Generator<T> for ValuesConsumed<'_, T> {
fn do_draw(&self, tc: &TestCase) -> T {
tc.assume(!self.values.borrow().is_empty());
let variable_id = pool_generate(tc, self.pool_id, true);
self.values.borrow_mut().remove(&variable_id).unwrap()
}
}
pub fn pool<T>(tc: &TestCase) -> Pool<T> {
let pool_id = match tc.with_ctc(|ctc| ctc.new_pool()) {
Ok(id) => id,
Err(rc) => raise_for_rc(rc), };
Pool {
pool_id,
tc: tc.clone(),
values: HashMap::new(),
}
}
pub trait StateMachine {
fn rules(&self) -> Vec<Rule<Self>>;
fn invariants(&self) -> Vec<Rule<Self>>;
}
fn check_invariants<M: StateMachine>(m: &mut M, invariants: &[Rule<M>], tc: &TestCase) {
for invariant in invariants {
let inv_tc = tc.child(2); (invariant.apply)(m, inv_tc); }
}
pub fn run<M: StateMachine>(mut m: M, tc: TestCase) {
let rules = m.rules();
let rule_names: Vec<&str> = rules.iter().map(|r| r.name.as_str()).collect();
let invariants = m.invariants();
let invariant_names: Vec<&str> = invariants.iter().map(|r| r.name.as_str()).collect();
let machine_id = match tc.with_ctc(|ctc| ctc.new_state_machine(&rule_names, &invariant_names)) {
Ok(id) => id,
Err(rc) => raise_for_rc(rc),
};
tc.note("Initial invariant check.");
check_invariants(&mut m, &invariants, &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_index = match tc.with_ctc(|ctc| ctc.state_machine_next_rule(machine_id)) {
Ok(i) => i,
Err(rc) => raise_for_rc(rc),
};
hegel_internal_assert!(
(0..rules.len() as i64).contains(&rule_index),
"state_machine_next_rule returned out-of-range rule index {rule_index}"
);
let rule = &rules[rule_index as usize];
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, &invariants, &tc);
}
Err(e) if e.downcast_ref::<AssumeFailed>().is_some() => {
tc.note("Rule stopped early due to violated assumption.");
}
Err(e) => resume_unwind(e),
};
}
}