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
56
57
58
59
60
61
62
63
64
65
66

use anyhow::anyhow;
use clap::Parser;
use scan_core::{Oracle, Scan, Time, Tracer, TransitionSystem, TransitionSystemGenerator};

const ALL_PROPS_ERR: &str =
    "the --all flag is incompatible with individually-specified properties.\n
Examples:
'scan PATH/TO/MODEL trace' executes the model once and writes the trace to disk
'scan PATH/TO/MODEL verify PROPERTY_1 PROPERTY_2' executes the model once and writes the trace to disk, classifying it according to verification outcome of the properties PROPERTY_1 and PROPERTY_2 together over the model
'scan PATH/TO/MODEL verify --all' executes the model once and writes the trace to disk, and classifying it according to verification outcome of all specified properties together over the model";

/// Produce execution traces.
#[derive(Debug, Clone, Parser)]
#[deny(missing_docs)]
pub(crate) struct TraceArgs {
    /// Space-separated list of properties to verify while tracing.
    pub(crate) properties: Vec<String>,
    /// Verify all properties found in the model specification while tracing.
    /// It is equivalent to listing all of the properties.
    #[arg(short, long)]
    pub(crate) all: bool,
    /// Number of traces to save.
    #[arg(long, default_value_t = 1)]
    pub(crate) traces: usize,
    /// Max duration of execution (in model-time).
    #[arg(short, long, default_value_t = 10000)]
    pub(crate) duration: Time,
    /// Run the model execution on a single thread.
    ///
    /// By default, SCAN uses multi-threading.
    /// Use this flag to run the model on a single thread.
    ///
    /// WARNING: only the running of the model is single-threaded.
    /// Other related functionalities, including model parsing and building, etc.,
    /// might still be running multiple threads.
    #[arg(long)]
    pub(crate) single_thread: bool,
    // /// TODO: Do not compress the saved traces.
    // #[arg(long)]
    // pub(crate) uncompressed: bool,
}

impl TraceArgs {
    pub(crate) fn validate(&self) -> anyhow::Result<()> {
        if !self.properties.is_empty() && self.all {
            Err(anyhow!(ALL_PROPS_ERR))
        } else {
            Ok(())
        }
    }

    pub(crate) fn trace<'a, D, Od, Tr>(&self, scan: &'a Scan<D, Od>, tracer: Tr)
    where
        D: TransitionSystemGenerator + Sync + 'a,
        Od: Oracle + Sync + 'a,
        Tr: Clone
            + Sync
            + Tracer<<<D as TransitionSystemGenerator>::Ts<'a> as TransitionSystem>::Event>,
    {
        if self.single_thread {
            scan.traces::<Tr>(self.traces, tracer, self.duration);
        } else {
            scan.par_traces::<Tr>(self.traces, tracer, self.duration);
        }
    }
}