stateright 0.29.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

//! Utilities for actor tests.

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

    pub struct PingPongActor { serve_to: Option<Id> }

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

    impl Actor for PingPongActor {
        type Msg = PingPongMsg;
        type State = u32; // count

        fn on_start(&self, _id: Id, 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
                })
        }
    }
}