use crate::TestCase;
use crate::control::{AssumeFailed, hegel_internal_assert};
use crate::generators::Generator;
use crate::test_case::{labels, raise_for_rc};
use std::cell::RefCell;
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: crate::ffi::PoolHandle,
tc: TestCase,
values: HashMap<i64, T>,
}
fn pool_generate(tc: &TestCase, pool: &crate::ffi::PoolHandle, consume: bool) -> i64 {
match tc.with_ctc(|ctc| ctc.pool_generate(pool, 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)) {
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: &self.pool,
values: &self.values,
}
}
pub fn values_consumed(&mut self) -> ValuesConsumed<'_, T> {
ValuesConsumed {
pool: &self.pool,
values: RefCell::new(&mut self.values),
}
}
}
pub struct ValuesReusable<'a, T> {
pool: &'a crate::ffi::PoolHandle,
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, false);
self.values.get(&variable_id).unwrap()
}
}
pub struct ValuesConsumed<'a, T> {
pool: &'a crate::ffi::PoolHandle,
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, true);
self.values.borrow_mut().remove(&variable_id).unwrap()
}
}
pub fn pool<T>(tc: &TestCase) -> Pool<T> {
let pool = match tc.with_ctc(|ctc| ctc.new_pool()) {
Ok(handle) => handle,
Err(rc) => raise_for_rc(rc), };
Pool {
pool,
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 = match tc.with_ctc(|ctc| ctc.new_state_machine(&rule_names, &invariant_names)) {
Ok(handle) => handle,
Err(rc) => raise_for_rc(rc),
};
tc.note("Initial invariant check.");
check_invariants(&mut m, &invariants, &tc);
let mut steps_attempted: i64 = 0;
loop {
tc.start_span(labels::STATEFUL_RULE);
let rule_index = match tc.with_ctc(|ctc| ctc.state_machine_next_rule(&machine)) {
Ok(Some(i)) => i,
Ok(None) => break,
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 {}: {}", steps_attempted + 1, 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(()) => {
tc.stop_span(false);
check_invariants(&mut m, &invariants, &tc);
}
Err(e) if e.downcast_ref::<AssumeFailed>().is_some() => {
if let Err(rc) = tc.with_ctc(|ctc| ctc.state_machine_rule_rejected(&machine)) {
raise_for_rc(rc);
}
tc.stop_span(true);
tc.note("Rule stopped early due to violated assumption.");
}
Err(e) => {
tc.stop_span(false);
resume_unwind(e)
}
};
}
}