todc_utils/specifications/
register.rs

1//! A sequential specification of a [register](https://en.wikipedia.org/wiki/Shared_register).
2use std::fmt::Debug;
3use std::hash::Hash;
4use std::marker::PhantomData;
5
6use crate::specifications::Specification;
7
8/// An operation for a [register](https://en.wikipedia.org/wiki/Shared_register).
9#[derive(Debug, Copy, Clone)]
10pub enum RegisterOperation<T> {
11    /// Read a value of type `T` from the register.
12    ///
13    /// If the return value of the operation is not-yet-known, then this can be
14    /// represented as `Read(None)`.
15    Read(Option<T>),
16    /// Write a value of type `T` to the register.
17    Write(T),
18}
19
20use RegisterOperation::*;
21
22/// A sequential specification of a [register](https://en.wikipedia.org/wiki/Shared_register).
23pub struct RegisterSpecification<T: Default + Eq> {
24    data_type: PhantomData<T>,
25}
26
27impl<T: Clone + Debug + Default + Eq + Hash> Specification for RegisterSpecification<T> {
28    type State = T;
29    type Operation = RegisterOperation<T>;
30
31    fn init() -> Self::State {
32        T::default()
33    }
34
35    fn apply(operation: &Self::Operation, state: &Self::State) -> (bool, Self::State) {
36        match operation {
37            Read(value) => {
38                let value = value
39                    .as_ref()
40                    .expect("Cannot apply `Read` with unknown return value");
41                (value == state, state.clone())
42            }
43            Write(value) => (true, value.clone()),
44        }
45    }
46}
47
48#[cfg(test)]
49mod test {
50    use super::*;
51
52    type Spec = RegisterSpecification<u32>;
53
54    mod init {
55        use super::*;
56
57        #[test]
58        fn initializes_state_to_default() {
59            assert_eq!(Spec::init(), 0);
60        }
61    }
62
63    mod apply {
64        use super::*;
65
66        #[test]
67        fn read_is_valid_if_value_is_current_state() {
68            let (is_valid, _) = Spec::apply(&Read(Some(0)), &Spec::init());
69            assert!(is_valid);
70        }
71
72        #[test]
73        fn read_is_not_valid_if_value_is_not_current_state() {
74            let (is_valid, _) = Spec::apply(&Read(Some(1)), &Spec::init());
75            assert!(!is_valid);
76        }
77
78        #[test]
79        fn read_does_not_affect_state() {
80            let old_state = Spec::init();
81            let (_, new_state) = Spec::apply(&Read(Some(0)), &old_state);
82            assert_eq!(old_state, new_state);
83        }
84
85        #[test]
86        fn write_is_always_valid() {
87            let (is_valid, _) = Spec::apply(&Write(1), &Spec::init());
88            assert!(is_valid);
89        }
90
91        #[test]
92        fn write_sets_new_state_to_written_value() {
93            let value = 123;
94            let (_, new_state) = Spec::apply(&Write(value), &Spec::init());
95            assert_eq!(value, new_state);
96        }
97    }
98}
todc_utils/specifications/register.rs

todc_utils/specifications/
register.rs
