recovery/
recovery.rs

1//! A configurable system where the recovery property holds or not depending on a command-line argument.
2//!
3//! This system keeps the maximum value of the input `value` in its state.
4//! If the command-line argument `--system-enable-reset` is given, it can reset the maximum value
5//! to zero based on the input `reset`.
6//!
7//! We can verify whether the *recovery* property `AG![EF![max_value == 0]]` holds, i.e. considering that
8//! we are in any reachable state, we can reach the state where `max_value` equals zero. To complicate
9//! things a bit, there is an unused state field `unused` that is loaded in each cycle from the input
10//! `unused` and a free-running counter `free_counter` that does not interact with `max_value`.
11//!
12//! Without the command-line argument `--system-enable-reset`, **machine-check** will quickly determine
13//! the recovery property does not hold. When using the argument, it will not be able to determine it
14//! quickly unless `--strategy decay` is used, which lets it ignore the free-running counter.
15//!
16use clap::Args;
17use machine_check::Bitvector;
18
19#[machine_check::machine_description]
20mod machine_module {
21    use ::machine_check::{Bitvector, Unsigned};
22    use ::std::{
23        clone::Clone,
24        cmp::{Eq, PartialEq},
25        fmt::Debug,
26        hash::Hash,
27    };
28
29    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
30    pub struct Input {
31        /// A value input that we track the maximum value of.
32        value: Unsigned<4>,
33        /// A reset signal. May or may not be actually enabled.
34        reset: Bitvector<1>,
35        /// An unused input.
36        unused: Bitvector<4>,
37    }
38
39    impl ::machine_check::Input for Input {}
40
41    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
42    pub struct State {
43        /// The maximum value of the input `value`.
44        ///
45        /// Can be reset by the input `reset` if `enable_reset` is chosen.
46        max_value: Unsigned<4>,
47        /// An unused value.
48        unused: Bitvector<4>,
49        /// An irrelevant free-running counter.
50        free_counter: Unsigned<4>,
51    }
52
53    impl ::machine_check::State for State {}
54
55    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
56    pub struct System {
57        pub enable_reset: Bitvector<1>,
58    }
59
60    impl ::machine_check::Machine for System {
61        type Input = Input;
62        type State = State;
63        #[allow(non_snake_case)]
64        fn init(&self, _input: &Input) -> State {
65            State {
66                max_value: Unsigned::<4>::new(0),
67                unused: Bitvector::<4>::new(0),
68                free_counter: Unsigned::<4>::new(0),
69            }
70        }
71
72        fn next(&self, state: &State, input: &Input) -> State {
73            let input_value = input.value;
74
75            // If the maximum value is smaller than the input value,
76            // update it to the input value.
77            let mut next_max = state.max_value;
78            if next_max < input_value {
79                next_max = input_value;
80            }
81            // If the reset input is asserted and it is actually enabled in the system,
82            // reset the maximum value to zero.
83            if (input.reset & self.enable_reset) == Bitvector::<1>::new(1) {
84                next_max = Unsigned::<4>::new(0);
85            }
86
87            // Increment the free-running counter. It will wrap around eventually.
88            let free_counter = state.free_counter + Unsigned::<4>::new(1);
89            State {
90                max_value: next_max,
91                unused: input.unused,
92                free_counter,
93            }
94        }
95    }
96}
97
98#[derive(Args)]
99struct SystemArgs {
100    #[arg(long = "system-enable-reset")]
101    enable_reset: bool,
102}
103
104fn main() {
105    let (run_args, system_args) = machine_check::parse_args::<SystemArgs>(std::env::args());
106    if system_args.enable_reset {
107        println!("Reset input is enabled");
108    } else {
109        println!("Reset input is disabled");
110    }
111    let enable_reset = Bitvector::<1>::new(system_args.enable_reset as u64);
112    machine_check::execute(machine_module::System { enable_reset }, run_args);
113}
recovery/recovery.rs

recovery/
recovery.rs
