stateright 0.31.0

A model checker for implementing distributed systems.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114

//! Implements [`SequentialSpec`] for "write-once register" operational semantics.

use super::SequentialSpec;
use std::fmt::Debug;

/// A simple register used to define reference operational semantics via
/// [`SequentialSpec`].
#[derive(Clone, Default, Debug, Hash, PartialEq, serde::Serialize)]
pub struct WORegister<T>(pub Option<T>);

/// An operation that can be invoked upon a [`WORegister`], resulting in a
/// [`WORegisterRet`]
#[derive(Clone, Debug, Hash, PartialEq, serde::Serialize)]
pub enum WORegisterOp<T> {
    Write(T),
    Read,
}

/// A return value for a [`WORegisterOp`] invoked upon a [`WORegister`].
#[derive(Clone, Debug, Hash, PartialEq, serde::Serialize)]
pub enum WORegisterRet<T> {
    WriteOk,
    WriteFail,
    ReadOk(Option<T>),
}

impl<T: Clone + Debug + PartialEq> SequentialSpec for WORegister<T> {
    type Op = WORegisterOp<T>;
    type Ret = WORegisterRet<T>;
    fn invoke(&mut self, op: &Self::Op) -> Self::Ret {
        match (op, &self.0) {
            (WORegisterOp::Write(v), None) => {
                self.0 = Some(v.clone());
                WORegisterRet::WriteOk
            }
            // If something has already been written succeed if equal
            (WORegisterOp::Write(v), Some(vp)) if *v == *vp => {
                self.0 = Some(v.clone());
                WORegisterRet::WriteOk
            }
            (WORegisterOp::Write(_), Some(_)) => WORegisterRet::WriteFail,
            (WORegisterOp::Read, _) => WORegisterRet::ReadOk(self.0.clone()),
        }
    }
    fn is_valid_step(&mut self, op: &Self::Op, ret: &Self::Ret) -> bool {
        // Override to avoid unnecessary `clone` on `Read`.
        match (op, ret, &self.0) {
            (WORegisterOp::Write(v), WORegisterRet::WriteOk, None) => {
                self.0 = Some(v.clone());
                true
            }
            (WORegisterOp::Write(v), WORegisterRet::WriteOk, Some(vp)) if *v == *vp => true,
            (WORegisterOp::Write(v), WORegisterRet::WriteFail, Some(vp)) if *v != *vp => true,
            (WORegisterOp::Read, WORegisterRet::ReadOk(v), _) => &self.0 == v,
            _ => false,
        }
    }
}

#[cfg(test)]
mod test {
    use super::*;

    #[test]
    fn models_expected_semantics() {
        let mut r = WORegister(None);
        assert_eq!(r.invoke(&WORegisterOp::Write('A')), WORegisterRet::WriteOk);
        assert_eq!(
            r.invoke(&WORegisterOp::Read),
            WORegisterRet::ReadOk(Some('A'))
        );
        assert_eq!(
            r.invoke(&WORegisterOp::Write('B')),
            WORegisterRet::WriteFail
        );
        assert_eq!(
            r.invoke(&WORegisterOp::Read),
            WORegisterRet::ReadOk(Some('A'))
        );
    }

    #[test]
    fn accepts_valid_histories() {
        let none_char: Option<char> = None;
        assert!(WORegister(none_char).is_valid_history(vec![]));
        assert!(WORegister(none_char).is_valid_history(vec![
            (WORegisterOp::Read, WORegisterRet::ReadOk(None)),
            (WORegisterOp::Write('A'), WORegisterRet::WriteOk),
            (WORegisterOp::Read, WORegisterRet::ReadOk(Some('A'))),
            (WORegisterOp::Write('B'), WORegisterRet::WriteFail),
            (WORegisterOp::Read, WORegisterRet::ReadOk(Some('A'))),
            (WORegisterOp::Write('C'), WORegisterRet::WriteFail),
            (WORegisterOp::Read, WORegisterRet::ReadOk(Some('A'))),
        ]));
    }

    #[test]
    fn rejects_invalid_histories() {
        let none_char: Option<char> = None;
        assert!(!WORegister(Some('A')).is_valid_history(vec![
            (WORegisterOp::Read, WORegisterRet::ReadOk(Some('A'))),
            (WORegisterOp::Write('B'), WORegisterRet::WriteOk),
        ]));
        assert!(!WORegister(none_char).is_valid_history(vec![
            (WORegisterOp::Read, WORegisterRet::ReadOk(Some('A'))),
            (WORegisterOp::Write('A'), WORegisterRet::WriteOk),
        ]));
        assert!(!WORegister(none_char).is_valid_history(vec![
            (WORegisterOp::Read, WORegisterRet::ReadOk(None)),
            (WORegisterOp::Write('A'), WORegisterRet::WriteOk),
            (WORegisterOp::Write('B'), WORegisterRet::WriteOk),
        ]));
    }
}