#![allow(dead_code)]
use hegel::TestCase;
use std::cmp::min;
struct DieHard {
small: i32,
big: i32,
}
#[hegel::state_machine]
impl DieHard {
#[rule]
fn fill_small(&mut self, _tc: TestCase) {
self.small = 3;
}
#[rule]
fn fill_big(&mut self, _tc: TestCase) {
self.big = 5;
}
#[rule]
fn empty_small(&mut self, _tc: TestCase) {
self.small = 0;
}
#[rule]
fn empty_big(&mut self, _tc: TestCase) {
self.big = 0;
}
#[rule]
fn pour_small_into_big(&mut self, _tc: TestCase) {
let big = self.big;
self.big = min(5, self.big + self.small);
self.small -= self.big - big;
}
#[rule]
fn pour_big_into_small(&mut self, _tc: TestCase) {
let small = self.small;
self.small = min(3, self.small + self.big);
self.big -= self.small - small;
}
#[invariant]
fn physics_of_jugs(&mut self, _tc: TestCase) {
assert!(0 <= self.small && self.small <= 3);
assert!(0 <= self.big && self.big <= 5);
}
#[invariant]
fn die_hard_problem_not_solved(&mut self, tc: TestCase) {
tc.note(&format!("small / big = {0} / {1}", self.small, self.big));
assert!(self.big != 4);
}
}
#[hegel::test(test_cases = 2000)]
fn test_die_hard(tc: TestCase) {
let m = DieHard { small: 0, big: 0 };
hegel::stateful::run(m, tc);
}
fn main() {}