scan_core/
lib.rs

1//! Implementation of *program graphs* (PG) and *channel systems* (CS) formalisms[^1]
2//! for use in the SCAN model checker.
3//!
4//! [^1]: Baier, C., & Katoen, J. (2008). *Principles of model checking*. MIT Press.
5
6#![warn(missing_docs)]
7#![forbid(unsafe_code)]
8
9pub mod channel_system;
10mod cs_model;
11mod dummy_rng;
12mod grammar;
13mod oracle;
14mod pg_model;
15pub mod program_graph;
16mod smc;
17mod transition_system;
18
19use core::marker::Sync;
20pub use cs_model::{Atom, CsModel, CsModelRun};
21use dummy_rng::DummyRng;
22pub use grammar::*;
23use log::{info, trace};
24pub use oracle::*;
25pub use pg_model::{PgModel, PgModelRun};
26use rayon::iter::{IntoParallelIterator, ParallelIterator};
27pub use smc::*;
28use std::{
29    sync::{
30        Arc, Mutex,
31        atomic::{AtomicBool, AtomicU32, Ordering},
32    },
33    time::Instant,
34};
35pub use transition_system::{Tracer, TransitionSystem, TransitionSystemGenerator};
36
37/// The type that represents time.
38pub type Time = u32;
39
40/// The possible outcomes of a model execution.
41#[derive(Debug, Clone)]
42pub enum RunOutcome {
43    /// The run was not completed because the execution violated an assume.
44    Incomplete,
45    /// The run failed by violating the guarantees corresponding to the given index (if any).
46    Verified(Vec<bool>),
47}
48
49/// The main type to interface with the verification capabilities of SCAN.
50/// [`Scan`] holds the model, properties and other data necessary to run the verification process.
51/// The type of models and properties is abstracted through the [`TransitionSystem`] and [`Oracle`] traits,
52/// to provide a unified interface.
53#[derive(Debug, Clone)]
54pub struct Scan<TsG, O> {
55    tsd: TsG,
56    oracle: O,
57    running: Arc<AtomicBool>,
58    successes: Arc<AtomicU32>,
59    failures: Arc<AtomicU32>,
60    violations: Arc<Mutex<Vec<u32>>>,
61}
62
63impl<TsG, O> Scan<TsG, O> {
64    /// Create new [`Scan`] object.
65    pub fn new(tsd: TsG, oracle: O) -> Self {
66        Scan {
67            tsd,
68            oracle,
69            running: Arc::new(AtomicBool::new(false)),
70            successes: Arc::new(AtomicU32::new(0)),
71            failures: Arc::new(AtomicU32::new(0)),
72            violations: Arc::new(Mutex::new(Vec::new())),
73        }
74    }
75
76    fn reset(&self) {
77        self.successes.store(0, Ordering::Relaxed);
78        self.failures.store(0, Ordering::Relaxed);
79        self.violations.lock().unwrap().clear();
80        self.running.store(true, Ordering::Relaxed);
81    }
82
83    /// Tells whether a verification task is currently running.
84    #[inline]
85    pub fn running(&self) -> bool {
86        self.running.load(Ordering::Relaxed)
87    }
88
89    /// Returns the number of successful executions in the current verification run.
90    #[inline]
91    pub fn successes(&self) -> u32 {
92        self.successes.load(Ordering::Relaxed)
93    }
94
95    /// Returns the number of failed executions in the current verification run.
96    #[inline]
97    pub fn failures(&self) -> u32 {
98        self.failures.load(Ordering::Relaxed)
99    }
100
101    /// Returns a vector where each entry contains the number of violations of the associated property in the current verification run.
102    #[inline]
103    pub fn violations(&self) -> Vec<u32> {
104        self.violations.lock().expect("lock").clone()
105    }
106}
107
108impl<TsG: TransitionSystemGenerator, O: Oracle> Scan<TsG, O> {
109    fn verification(&self, confidence: f64, precision: f64, duration: Time) {
110        let local_successes;
111        let local_failures;
112        let mut ts = self.tsd.generate();
113
114        let result = ts.experiment(duration, self.oracle.clone(), self.running.clone());
115        if !self.running.load(Ordering::Relaxed) {
116            return;
117        }
118        match result {
119            RunOutcome::Verified(guarantees) => {
120                if guarantees.iter().all(|b| *b) {
121                    local_successes = self.successes.fetch_add(1, Ordering::Relaxed);
122                    local_failures = self.failures.load(Ordering::Relaxed);
123                    // If all guarantees are satisfied, the execution is successful
124                    trace!("runs: {local_successes} successes");
125                } else {
126                    local_successes = self.successes.load(Ordering::Relaxed);
127                    local_failures = self.failures.fetch_add(1, Ordering::Relaxed);
128                    let violations = &mut *self.violations.lock().unwrap();
129                    violations.resize(violations.len().max(guarantees.len()), 0);
130                    guarantees.iter().zip(violations.iter_mut()).for_each(
131                        |(success, violations)| {
132                            if !success {
133                                *violations += 1;
134                            }
135                        },
136                    );
137                    // If guarantee is violated, we have found a counter-example!
138                    trace!("runs: {local_failures} failures");
139                }
140            }
141            RunOutcome::Incomplete => return,
142        }
143        let runs = local_successes + local_failures;
144        // Avoid division by 0
145        let avg = if runs == 0 {
146            0.5f64
147        } else {
148            local_successes as f64 / runs as f64
149        };
150        if adaptive_bound(avg, confidence, precision) <= runs as f64 {
151            info!("adaptive bound satisfied");
152            self.running.store(false, Ordering::Relaxed);
153        }
154    }
155
156    /// Statistically verifies the provided [`TransitionSystem`] using adaptive bound and the given parameters.
157    pub fn adaptive(&self, confidence: f64, precision: f64, duration: Time) {
158        // Cannot return as a T::Err, don't want to include anyhow in scan_core
159        assert!(0f64 < confidence && confidence < 1f64);
160        assert!(0f64 < precision && precision < 1f64);
161
162        self.reset();
163
164        // WARN FIXME TODO: Implement algorithm for 2.4 Distributed sample generation in Budde et al.
165        info!("verification starting");
166        let start_time = Instant::now();
167
168        let _ = (0..usize::MAX)
169            .map(|_| self.verification(confidence, precision, duration))
170            .take_while(|_| self.running.load(Ordering::Relaxed))
171            .count();
172
173        let elapsed = start_time.elapsed();
174        info!("verification time elapsed: {elapsed:0.2?}");
175        info!("verification terminating");
176    }
177
178    #[inline]
179    fn trace<'a, T>(&'a self, tracer: T, duration: Time)
180    where
181        T: Tracer<<<TsG as TransitionSystemGenerator>::Ts<'a> as TransitionSystem>::Event>,
182    {
183        let mut ts = self.tsd.generate();
184        ts.trace(duration, self.oracle.clone(), tracer)
185    }
186
187    /// Produces and saves the traces for the given number of runs,
188    /// using the provided [`Tracer`].
189    pub fn traces<'a, T>(&'a self, runs: usize, tracer: T, duration: Time)
190    where
191        T: Clone + Tracer<<<TsG as TransitionSystemGenerator>::Ts<'a> as TransitionSystem>::Event>,
192    {
193        // WARN FIXME TODO: Implement algorithm for 2.4 Distributed sample generation in Budde et al.
194        info!("tracing starting");
195        let start_time = Instant::now();
196
197        (0..runs).for_each(|_| self.trace::<T>(tracer.clone(), duration));
198
199        let elapsed = start_time.elapsed();
200        info!("tracing time elapsed: {elapsed:0.2?}");
201        info!("tracing terminating");
202    }
203}
204
205impl<TsG, O> Scan<TsG, O>
206where
207    TsG: TransitionSystemGenerator + Sync,
208    O: Oracle + Sync,
209{
210    /// Statistically verifies the provided [`TransitionSystem`] using adaptive bound and the given parameters,
211    /// spawning multiple threads.
212    pub fn par_adaptive(&self, confidence: f64, precision: f64, duration: Time) {
213        assert!(0f64 < confidence && confidence < 1f64);
214        assert!(0f64 < precision && precision < 1f64);
215
216        self.reset();
217
218        // WARN FIXME TODO: Implement algorithm for 2.4 Distributed sample generation in Budde et al.
219        info!("verification starting");
220        let start_time = Instant::now();
221
222        let _ = (0..usize::MAX)
223            .into_par_iter()
224            .map(|_| self.verification(confidence, precision, duration))
225            .take_any_while(|_| self.running.load(Ordering::Relaxed))
226            .count();
227
228        let elapsed = start_time.elapsed();
229        info!("verification time elapsed: {elapsed:0.2?}");
230        info!("verification terminating");
231    }
232
233    /// Produces and saves the traces for the given number of runs,
234    /// using the provided [`Tracer`],
235    /// spawning multiple threads.
236    pub fn par_traces<'a, T>(&'a self, runs: usize, tracer: T, duration: Time)
237    where
238        T: Clone
239            + Sync
240            + Tracer<<<TsG as TransitionSystemGenerator>::Ts<'a> as TransitionSystem>::Event>,
241    {
242        // WARN FIXME TODO: Implement algorithm for 2.4 Distributed sample generation in Budde et al.
243        info!("tracing starting");
244        let start_time = Instant::now();
245
246        (0..runs)
247            .into_par_iter()
248            .for_each(|_| self.trace::<T>(tracer.clone(), duration));
249
250        let elapsed = start_time.elapsed();
251        info!("tracing time elapsed: {elapsed:0.2?}");
252        info!("tracing terminating");
253    }
254}
scan_core/lib.rs

scan_core/
lib.rs
