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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132

//! Utilities for actor tests.

/// A pair of actors that send messages and increment message counters.
pub mod ping_pong {
    use crate::actor::*;
    use crate::*;

    pub struct PingPongActor {
        serve_to: Option<Id>,
    }

    #[derive(Eq, Ord, PartialEq, PartialOrd, Clone, Debug, Hash)]
    pub enum PingPongMsg {
        Ping(u32),
        Pong(u32),
    }

    impl Actor for PingPongActor {
        type Msg = PingPongMsg;
        type State = u32; // count
        type Timer = ();
        type Random = ();
        type Storage = ();
        fn on_start(
            &self,
            _id: Id,
            _storage: &Option<Self::Storage>,
            o: &mut Out<Self>,
        ) -> Self::State {
            if let Some(id) = self.serve_to {
                o.send(id, PingPongMsg::Ping(0));
            }
            0
        }

        fn on_msg(
            &self,
            _id: Id,
            state: &mut Cow<Self::State>,
            src: Id,
            msg: Self::Msg,
            o: &mut Out<Self>,
        ) {
            match msg {
                PingPongMsg::Pong(msg_value) if **state == msg_value => {
                    o.send(src, PingPongMsg::Ping(msg_value + 1));
                    *state.to_mut() += 1;
                }
                PingPongMsg::Ping(msg_value) if **state == msg_value => {
                    o.send(src, PingPongMsg::Pong(msg_value));
                    *state.to_mut() += 1;
                }
                _ => {}
            }
        }
    }

    pub struct PingPongCfg {
        pub maintains_history: bool,
        pub max_nat: u32,
    }

    pub type PingPongHistory = (u32, u32); // (#in, #out)

    impl PingPongCfg {
        pub fn into_model(self) -> ActorModel<PingPongActor, PingPongCfg, PingPongHistory> {
            ActorModel::new(self, (0, 0))
                .actor(PingPongActor {
                    serve_to: Some(1.into()),
                })
                .actor(PingPongActor { serve_to: None })
                .record_msg_in(|cfg, history, _| {
                    if cfg.maintains_history {
                        let (msg_in_count, msg_out_count) = *history;
                        Some((msg_in_count + 1, msg_out_count))
                    } else {
                        None
                    }
                })
                .record_msg_out(|cfg, history, _| {
                    if cfg.maintains_history {
                        let (msg_in_count, msg_out_count) = *history;
                        Some((msg_in_count, msg_out_count + 1))
                    } else {
                        None
                    }
                })
                .within_boundary(|cfg, state| {
                    state
                        .actor_states
                        .iter()
                        .all(|count| **count <= cfg.max_nat)
                })
                .property(Expectation::Always, "delta within 1", |_, state| {
                    let max = state.actor_states.iter().max().unwrap();
                    let min = state.actor_states.iter().min().unwrap();
                    **max - **min <= 1
                })
                .property(Expectation::Sometimes, "can reach max", |model, state| {
                    state
                        .actor_states
                        .iter()
                        .any(|count| **count == model.cfg.max_nat)
                })
                .property(Expectation::Eventually, "must reach max", |model, state| {
                    state
                        .actor_states
                        .iter()
                        .any(|count| **count == model.cfg.max_nat)
                })
                .property(
                    Expectation::Eventually,
                    "must exceed max",
                    |model, state| {
                        // this one is falsifiable due to the boundary
                        state
                            .actor_states
                            .iter()
                            .any(|count| **count == model.cfg.max_nat + 1)
                    },
                )
                .property(Expectation::Always, "#in <= #out", |_, state| {
                    let (msg_in_count, msg_out_count) = state.history;
                    msg_in_count <= msg_out_count
                })
                .property(Expectation::Eventually, "#out <= #in + 1", |_, state| {
                    let (msg_in_count, msg_out_count) = state.history;
                    msg_out_count <= msg_in_count + 1
                })
        }
    }
}