smc_scan 0.1.0

Statistical model checker for large concurrent 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

use scan_core::Time;
use serde::Serialize;
use std::{collections::HashMap, fmt::Display};

#[derive(Serialize)]
pub(crate) struct Report {
    pub(crate) model: String,
    pub(crate) precision: f64,
    pub(crate) confidence: f64,
    pub(crate) duration: Time,
    pub(crate) rate: f64,
    pub(crate) runs: u32,
    pub(crate) successes: u32,
    pub(crate) failures: u32,
    pub(crate) property_failures: HashMap<String, u32>,
}

impl Report {
    pub(crate) fn print(&self, json: bool) {
        if json {
            let report = serde_json::ser::to_string_pretty(&self).expect("report serialization");
            println!("{report}");
        } else {
            // Print final report
            println!("{self}");
        };
    }
}

impl Display for Report {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        // Magnitude of precision, to round results to sensible number of digits
        let mag = (self.precision.log10().abs().ceil() as usize).max(2);
        writeln!(
            f,
            "Completed {} runs with {} successes and {} failures",
            self.runs, self.successes, self.failures
        )?;
        for (property, &violations) in self.property_failures.iter() {
            write!(
                f,
                "Property {property} success rate: {0:.1$}",
                ((self.runs - violations) as f64) / (self.runs as f64),
                mag,
            )?;
            if violations > 0 {
                writeln!(f, " ({violations} fails)")?;
            } else {
                writeln!(f)?;
            }
        }
        write!(f, "Overall success rate: {:.1$}", self.rate, mag)?;
        Ok(())
    }
}