counter/
counter.rs

1//! An example of a very simple machine-check system.
2//!
3//! The used structs and implementations must be enclosed
4//! within a module on which the machine_description macro
5//! is applied.
6
7#[machine_check::machine_description]
8mod machine_module {
9    // Currently, all used non-global paths must be imported
10    // within the machine_description macro.
11    //
12    // Only machine-check types and traits, plus a few std
13    // traits, can be used.
14    use ::machine_check::{BitvectorArray, Ext, Unsigned};
15    use ::std::{
16        clone::Clone,
17        cmp::{Eq, PartialEq},
18        fmt::Debug,
19        hash::Hash,
20    };
21
22    // It is required to derive the following traits
23    // on the structs that will be used for machine-check
24    // verification.
25    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
26    pub struct Input {
27        increment: Unsigned<1>,
28        unused: BitvectorArray<16, 8>,
29    }
30
31    // Input implementation signifies that the struct
32    // can be used as input to a system implementing Machine.
33    impl ::machine_check::Input for Input {}
34
35    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
36    pub struct State {
37        value: Unsigned<8>,
38        unused: BitvectorArray<16, 8>,
39    }
40
41    // State implementation signifies that the struct
42    // can be used as state of a system implementing Machine.
43    impl ::machine_check::State for State {}
44
45    // The system can contain data that will be unchanging,
46    // but usable within the machine-stepping functions.
47    //
48    // This one does not contain any such data.
49    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
50    pub struct System {}
51
52    // Machine implementation makes it possible to formally
53    // verify the system.
54    impl ::machine_check::Machine for System {
55        // The type of inputs to the finite-state machine.
56        type Input = Input;
57        // The type of states of the finite-state machine.
58        type State = State;
59
60        // Machine initialization. Given an input, a state is generated.
61        // The function must be pure, i.e. give the same result with the
62        // same parameters.
63        //
64        // Here, the value is initialized to zero, and the unused array
65        // is taken from the input, i.e. can have any values.
66        fn init(&self, input: &Input) -> State {
67            State {
68                value: Unsigned::<8>::new(0),
69                unused: Clone::clone(&input.unused),
70            }
71        }
72
73        // Machine step. Given a state and an input, the next state is generated.
74        // Again, the function must be pure.
75        //
76        // Here, the value is incremented if input increment field is 1.
77        // If it reaches 157, it is immediately reset to 0. The unused array
78        // is again taken from the input, i.e. can have any values, and the
79        // values do not have to match the previous ones.
80        fn next(&self, state: &State, input: &Input) -> State {
81            // The increment is extended to 8 bits (zero-extension because
82            // it is Unsigned), then added to the value in the current state.
83            // Currently, it must be called using associated function call,
84            // i.e. Ext::<8>::ext(a), rather than method call input.increment.ext()
85            let mut next_value = state.value + Ext::<8>::ext(input.increment);
86            // If the next value is 157, it is immediately set to 0.
87            if next_value == Unsigned::<8>::new(157) {
88                next_value = Unsigned::<8>::new(0);
89            }
90
91            // The clone function is one of the few std functions supported
92            // by machine-check. Currently, the functions can only be called
93            // using associated function call, i.e. Clone::clone(&a),
94            // rather than the usually used method call a.clone().
95            let unused = Clone::clone(&input.unused);
96
97            // The new state is constructed with the new value and unused fields.
98            State {
99                value: next_value,
100                unused,
101            }
102        }
103    }
104}
105
106// Main entry point of the executable.
107fn main() {
108    // Construct the system. This one has no unchanging data.
109    let system = machine_module::System {};
110    // Run machine-check with the constructed system.
111    machine_check::run(system);
112}
counter/counter.rs

counter/
counter.rs
