die_hard/
die_hard.rs

1#![allow(dead_code)]
2
3use hegel::TestCase;
4use std::cmp::min;
5
6struct DieHard {
7    small: i32,
8    big: i32,
9}
10
11#[hegel::state_machine]
12impl DieHard {
13    #[rule]
14    fn fill_small(&mut self, _tc: TestCase) {
15        self.small = 3;
16    }
17
18    #[rule]
19    fn fill_big(&mut self, _tc: TestCase) {
20        self.big = 5;
21    }
22
23    #[rule]
24    fn empty_small(&mut self, _tc: TestCase) {
25        self.small = 0;
26    }
27
28    #[rule]
29    fn empty_big(&mut self, _tc: TestCase) {
30        self.big = 0;
31    }
32
33    #[rule]
34    fn pour_small_into_big(&mut self, _tc: TestCase) {
35        let big = self.big;
36        self.big = min(5, self.big + self.small);
37        self.small -= self.big - big;
38    }
39
40    #[rule]
41    fn pour_big_into_small(&mut self, _tc: TestCase) {
42        let small = self.small;
43        self.small = min(3, self.small + self.big);
44        self.big -= self.small - small;
45    }
46
47    #[invariant]
48    fn physics_of_jugs(&mut self, _tc: TestCase) {
49        assert!(0 <= self.small && self.small <= 3);
50        assert!(0 <= self.big && self.big <= 5);
51    }
52
53    #[invariant]
54    fn die_hard_problem_not_solved(&mut self, tc: TestCase) {
55        tc.note(&format!("small / big = {0} / {1}", self.small, self.big));
56        assert!(self.big != 4);
57    }
58}
59
60#[hegel::test(test_cases = 2000)]
61fn test_die_hard(tc: TestCase) {
62    let m = DieHard { small: 0, big: 0 };
63    hegel::stateful::run(m, tc);
64}
65
66fn main() {}
die_hard/die_hard.rs

die_hard/
die_hard.rs
