timed_panic/
timed_panic.rs

1//! Example of a system that panics after some time.
2//!
3//! The inherent property verification should show that
4//! the panic is reached after counter goes to 7
5//! and the value is loaded from the input. In the next step,
6//! it will be detected that the value is 3.
7
8#[machine_check::machine_description]
9mod machine_module {
10    use ::machine_check::Unsigned;
11    use ::std::{
12        clone::Clone,
13        cmp::{Eq, PartialEq},
14        fmt::Debug,
15        hash::Hash,
16    };
17
18    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
19    pub struct Input {
20        value: Unsigned<2>,
21    }
22
23    impl ::machine_check::Input for Input {}
24
25    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
26    pub struct State {
27        counter: Unsigned<3>,
28        value: Unsigned<2>,
29    }
30
31    impl ::machine_check::State for State {}
32
33    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
34    pub struct System {}
35
36    impl ::machine_check::Machine for System {
37        type Input = Input;
38        type State = State;
39
40        #[allow(unused_variables)]
41        fn init(&self, input: &Input) -> State {
42            State {
43                counter: Unsigned::<3>::new(0),
44                value: Unsigned::<2>::new(0),
45            }
46        }
47
48        fn next(&self, state: &State, input: &Input) -> State {
49            if state.value == Unsigned::<2>::new(3) {
50                ::std::panic!("Value must not be 3");
51            }
52
53            let next_counter = state.counter + Unsigned::<3>::new(1);
54            let mut next_value = state.value;
55            if state.counter == Unsigned::<3>::new(7) {
56                next_value = input.value;
57            }
58            State {
59                counter: next_counter,
60                value: next_value,
61            }
62        }
63    }
64}
65
66/// Main entry point of the executable.
67fn main() {
68    // Construct the system. This one has no unchanging data.
69    let system = machine_module::System {};
70    // Run machine-check with the constructed system.
71    machine_check::run(system);
72}
timed_panic/timed_panic.rs

timed_panic/
timed_panic.rs
