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

use std::collections::BTreeMap;
use std::fmt::Debug;
use std::hash::Hash;
use std::io::Write;
use std::time::Duration;

use crate::{DiscoveryClassification, Model, Path};

/// The data sent during a report event.
pub struct ReportData {
    /// The total number of states.
    pub total_states: usize,
    /// The number of unique states found.
    pub unique_states: usize,
    /// Maximum depth explored.
    pub max_depth: usize,
    /// The current duration checking has been running for.
    pub duration: Duration,
    /// Whether checking is done.
    pub done: bool,
}

/// A discovery found during the checking.
pub struct ReportDiscovery<M>
where
    M: Model,
{
    /// The path that led to the discovery.
    pub path: Path<M::State, M::Action>,
    /// The classification of the path.
    pub classification: DiscoveryClassification,
}

/// A reporter for progress during the model checking.
pub trait Reporter<M: Model> {
    /// Report a progress event.
    fn report_checking(&mut self, data: ReportData);

    /// Report the discoveries at the end of the checking run.
    fn report_discoveries(
        &mut self,
        model: &M,
        discoveries: BTreeMap<&'static str, ReportDiscovery<M>>,
    ) where
        M::Action: Debug + PartialEq,
        M::State: Debug + Hash + PartialEq;

    fn delay(&self) -> std::time::Duration {
        std::time::Duration::from_millis(1_000)
    }
}

pub struct WriteReporter<'a, W> {
    writer: &'a mut W,
}

impl<'a, W> WriteReporter<'a, W> {
    pub fn new(writer: &'a mut W) -> Self {
        Self { writer }
    }
}

impl<M, W> Reporter<M> for WriteReporter<'_, W>
where
    M: Model,
    W: Write,
{
    fn report_checking(&mut self, data: ReportData) {
        if data.done {
            let _ = writeln!(
                self.writer,
                "Done. states={}, unique={}, depth={}, sec={}",
                data.total_states,
                data.unique_states,
                data.max_depth,
                data.duration.as_secs(),
            );
        } else {
            let _ = writeln!(
                self.writer,
                "Checking. states={}, unique={}, depth={}",
                data.total_states, data.unique_states, data.max_depth
            );
        }
    }

    fn report_discoveries(
        &mut self,
        model: &M,
        discoveries: BTreeMap<&'static str, ReportDiscovery<M>>,
    ) where
        M::Action: Debug + PartialEq,
        M::State: Debug + Hash + PartialEq,
    {
        for (name, discovery) in discoveries {
            let _ = write!(
                self.writer,
                "Discovered \"{}\" {} {}",
                name, discovery.classification, discovery.path,
            );
            let _ = writeln!(
                self.writer,
                "Action index path: {}",
                discovery.path.encode(model)
            );
        }
    }
}