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//! This crate is part of the [SCAN statistical model checker](https://convince-project.github.io/scan/)
5//!
6//! [^1]: Baier, C., & Katoen, J. (2008). *Principles of model checking*. MIT Press.
7
8#![warn(missing_docs)]
9#![forbid(unsafe_code)]
10
11pub mod channel_system;
12mod grammar;
13mod oracle;
14pub mod program_graph;
15mod smc;
16mod time;
17mod tracer;
18mod transition_system;
19
20pub use grammar::*;
21use log::{info, trace};
22pub use oracle::*;
23use rayon::iter::{IntoParallelIterator, ParallelIterator};
24pub use smc::*;
25use std::{
26    fs::{File, create_dir, create_dir_all, rename},
27    path::PathBuf,
28    sync::{
29        Arc, Mutex,
30        atomic::{AtomicBool, AtomicU32, Ordering},
31    },
32    time::Instant,
33};
34use thiserror::Error;
35pub use time::*;
36pub use tracer::{TraceWriter, Tracer};
37pub use transition_system::{Atom, TransitionSystem, TransitionSystemRun};
38
39const TEMP: &str = ".temp";
40const SUCCESSES: &str = "successes";
41const FAILURES: &str = "failures";
42
43/// Errors that can be returned by a `[Scan]` method
44#[derive(Clone, Copy, Debug, Error)]
45pub enum ScanError {
46    /// Precision value is out-of-bounds
47    #[error("out-of-bounds precision value: {0}")]
48    OutOfBoundsPrecision(f64),
49    /// Confidence value is out-of-bounds
50    #[error("out-of-bounds confidence value: {0}")]
51    OutOfBoundsConfidence(f64),
52}
53
54/// Final report for a verification run.
55#[derive(Debug, Clone)]
56pub struct Report {
57    /// Total executions run (even partial).
58    pub runs: u32,
59    /// Successful executions.
60    pub successes: u32,
61    /// Failed executions.
62    pub failures: u32,
63    /// Breakdown of violations by property.
64    pub violations: Vec<u32>,
65}
66
67// The possible outcomes of a model execution:
68// - If the run was not completed (because the execution violated an assume), result is `None`.
69// - If the run succeeded, or failed by violating the guarantees, result is `Some(violations)`
70//   where the `violations` carries which (if any) guarantees were violated.
71type RunOutcome = Option<Vec<bool>>;
72
73/// The main type to interface with the verification capabilities of SCAN.
74/// [`Scan`] holds the model, properties and other data necessary to run the verification process.
75/// The type of properties is abstracted through the [`Oracle`] trait,
76/// to provide a unified interface.
77#[derive(Debug, Clone)]
78pub struct Scan<O> {
79    model: TransitionSystem,
80    oracle: O,
81    running: Arc<AtomicBool>,
82    successes: Arc<AtomicU32>,
83    failures: Arc<AtomicU32>,
84    violations: Arc<Mutex<Vec<u32>>>,
85}
86
87impl<O> Scan<O> {
88    /// Create new [`Scan`] object.
89    pub fn new(tsd: TransitionSystem, oracle: O) -> Self {
90        Scan {
91            model: tsd,
92            oracle,
93            running: Arc::new(AtomicBool::new(false)),
94            successes: Arc::new(AtomicU32::new(0)),
95            failures: Arc::new(AtomicU32::new(0)),
96            violations: Arc::new(Mutex::new(Vec::new())),
97        }
98    }
99
100    fn reset(&self) {
101        self.successes.store(0, Ordering::Relaxed);
102        self.failures.store(0, Ordering::Relaxed);
103        self.violations.lock().unwrap().clear();
104        self.running.store(true, Ordering::Relaxed);
105    }
106
107    /// Tells whether a verification task is currently running.
108    #[inline]
109    pub fn running(&self) -> bool {
110        self.running.load(Ordering::Relaxed)
111    }
112
113    /// Returns the number of successful executions in the current verification run.
114    #[inline]
115    pub fn successes(&self) -> u32 {
116        self.successes.load(Ordering::Relaxed)
117    }
118
119    /// Returns the number of failed executions in the current verification run.
120    #[inline]
121    pub fn failures(&self) -> u32 {
122        self.failures.load(Ordering::Relaxed)
123    }
124
125    /// Returns a vector where each entry contains the number of violations of the associated property in the current verification run.
126    #[inline]
127    pub fn violations(&self) -> Vec<u32> {
128        self.violations.lock().expect("lock").clone()
129    }
130}
131
132impl<O: Oracle + Clone> Scan<O> {
133    fn verification(&self, confidence: f64, precision: f64) {
134        assert!(0f64 < confidence && confidence < 1f64);
135        assert!(0f64 < precision && precision < 1f64);
136
137        let result = self
138            .model
139            .new_run()
140            .experiment(self.oracle.clone(), self.running.clone());
141        if let Some(guarantees) = result
142            && self.running.load(Ordering::Relaxed)
143        {
144            let local_successes;
145            let local_failures;
146            if guarantees.iter().all(|b| *b) {
147                local_successes = self.successes.fetch_add(1, Ordering::Relaxed);
148                local_failures = self.failures.load(Ordering::Relaxed);
149                // If all guarantees are satisfied, the execution is successful
150                trace!("runs: {local_successes} successes");
151            } else {
152                local_successes = self.successes.load(Ordering::Relaxed);
153                local_failures = self.failures.fetch_add(1, Ordering::Relaxed);
154                let violations = &mut *self.violations.lock().unwrap();
155                violations.resize(violations.len().max(guarantees.len()), 0);
156                guarantees
157                    .into_iter()
158                    .zip(violations.iter_mut())
159                    .filter(|(success, _)| !success)
160                    .for_each(|(_, violations)| {
161                        *violations += 1;
162                    });
163                // If guarantee is violated, we have found a counter-example!
164                trace!("runs: {local_failures} failures");
165            }
166            let runs = local_successes + local_failures;
167            // Division by 0 leads to Inf/NaN, which is not less than any other float number
168            // so this actually works as expected even for runs = 0.
169            let avg = local_successes as f64 / runs as f64;
170            if adaptive_bound(avg, confidence, precision) <= runs as f64 {
171                info!("adaptive bound satisfied");
172                self.running.store(false, Ordering::Relaxed);
173            }
174        }
175    }
176
177    /// Statistically verifies the provided [`TransitionSystem`] using adaptive bound and the given parameters.
178    pub fn adaptive(&self, confidence: f64, precision: f64) -> Result<Report, ScanError> {
179        if !(0f64 < confidence && confidence < 1f64) {
180            return Err(ScanError::OutOfBoundsConfidence(confidence));
181        }
182        if !(0f64 < precision && precision < 1f64) {
183            return Err(ScanError::OutOfBoundsPrecision(precision));
184        }
185
186        self.reset();
187
188        // WARN FIXME TODO: Implement algorithm for 2.4 Distributed sample generation in Budde et al.
189        info!("verification starting");
190        let start_time = Instant::now();
191
192        let runs = (0..)
193            .map(|_| self.verification(confidence, precision))
194            .take_while(|_| self.running.load(Ordering::Relaxed))
195            .count() as u32;
196
197        let elapsed = start_time.elapsed();
198        info!("verification completed in {elapsed:0.2?}");
199        Ok(Report {
200            runs,
201            successes: self.successes(),
202            failures: self.failures(),
203            violations: self.violations(),
204        })
205    }
206
207    /// Produces and saves the traces for the given number of runs,
208    /// using the provided [`Tracer`].
209    pub fn traces<T>(&self, runs: usize, path: PathBuf, model_data: &T::ModelData)
210    where
211        T: Tracer,
212    {
213        // WARN FIXME TODO: Implement algorithm for 2.4 Distributed sample generation in Budde et al.
214        info!("tracing starting");
215        let start_time = Instant::now();
216        create_traces_dirs_tree(path.clone());
217
218        (0..runs).for_each(|idx| {
219            self.trace::<T>(path.clone(), model_data, idx);
220        });
221
222        let elapsed = start_time.elapsed();
223        info!("tracing completed in {elapsed:0.2?}");
224    }
225
226    fn trace<T>(&self, mut path: PathBuf, model_data: &T::ModelData, idx: usize)
227    where
228        T: Tracer,
229    {
230        let mut ts = self.model.new_run();
231        let filename = PathBuf::new()
232            .with_file_name(format!("{idx:04}"))
233            .with_extension(T::EXTENSION);
234        path.push(TEMP);
235        path.push(&filename);
236        path.add_extension("gz");
237        let file = File::create_new(&path).expect("create file");
238        let writer = flate2::GzBuilder::new()
239            .filename(filename.to_str().expect("file name"))
240            .comment("Scan-generated execution trace")
241            .write(file, flate2::Compression::best());
242        let tracer = T::init(writer, model_data);
243        if let Some(verified) = ts.trace::<T, _>(self.oracle.clone(), tracer, model_data) {
244            let mut new_path = path.clone();
245            // pop file name
246            new_path.pop();
247            // pop temp folder
248            new_path.pop();
249            if verified.into_iter().all(|b| b) {
250                new_path.push(SUCCESSES);
251            } else {
252                new_path.push(FAILURES);
253            }
254            new_path.push(path.file_name().expect("file name"));
255            rename(&path, new_path).expect("renaming");
256        }
257    }
258}
259
260impl<O> Scan<O>
261where
262    O: Oracle + Clone + Sync,
263{
264    /// Statistically verifies the provided [`TransitionSystem`] using adaptive bound and the given parameters,
265    /// spawning multiple threads.
266    pub fn par_adaptive(&self, confidence: f64, precision: f64) -> Result<Report, ScanError> {
267        if !(0f64 < confidence && confidence < 1f64) {
268            return Err(ScanError::OutOfBoundsConfidence(confidence));
269        }
270        if !(0f64 < precision && precision < 1f64) {
271            return Err(ScanError::OutOfBoundsPrecision(precision));
272        }
273
274        self.reset();
275
276        // WARN FIXME TODO: Implement algorithm for 2.4 Distributed sample generation in Budde et al.
277        info!("verification starting");
278        let start_time = Instant::now();
279
280        let runs = (0..usize::MAX)
281            .into_par_iter()
282            .map(|_| self.verification(confidence, precision))
283            .take_any_while(|_| self.running.load(Ordering::Relaxed))
284            .count() as u32;
285
286        let elapsed = start_time.elapsed();
287        info!("verification completed in {elapsed:0.2?}");
288        Ok(Report {
289            runs,
290            successes: self.successes(),
291            failures: self.failures(),
292            violations: self.violations(),
293        })
294    }
295
296    /// Produces and saves the traces for the given number of runs,
297    /// using the provided [`Tracer`],
298    /// spawning multiple threads.
299    pub fn par_traces<T>(&self, runs: usize, path: PathBuf, model_data: &T::ModelData)
300    where
301        T: Tracer,
302        T::ModelData: Sync,
303    {
304        // WARN FIXME TODO: Implement algorithm for 2.4 Distributed sample generation in Budde et al.
305        info!("tracing starting");
306        let start_time = Instant::now();
307        create_traces_dirs_tree(path.clone());
308
309        (0..runs).into_par_iter().for_each(|idx| {
310            self.trace::<T>(path.clone(), model_data, idx);
311        });
312
313        let elapsed = start_time.elapsed();
314        info!("tracing completed in {elapsed:0.2?}");
315    }
316}
317
318fn create_traces_dirs_tree(mut path: PathBuf) {
319    create_dir_all(&path).expect("create base dir");
320    path.push(TEMP);
321    create_dir(&path).expect("create temp dir");
322    assert!(path.pop());
323    path.push(SUCCESSES);
324    create_dir(&path).expect("create successes dir");
325    assert!(path.pop());
326    path.push(FAILURES);
327    create_dir(&path).expect("create failures dir");
328}
scan_core/lib.rs

scan_core/
lib.rs
