scan_core/smc.rs
1// An efficient statistical model checker for nondeterminism and rare events,
2// Carlos E. Budde, Pedro R. D’Argenio, Arnd Hartmanns, Sean Sedwards.
3// International Journal on Software Tools for Technology Transfer (2020) 22:759–780
4// https://doi.org/10.1007/s10009-020-00563-2
5
6/// Computes Okamoto bound for given confidence and precision.
7pub fn okamoto_bound(confidence: f64, precision: f64) -> f64 {
8 (2f64 / (1f64 - confidence)).ln() / (2f64 * precision.powf(2f64))
9}
10
11/// Computes adaptive bound for given confidence, precision and (partial) experimental results.
12pub fn adaptive_bound(avg: f64, confidence: f64, precision: f64) -> f64 {
13 4f64 * okamoto_bound(confidence, precision)
14 * (0.25f64 - ((avg - 0.5f64).abs() - (2f64 * precision / 3f64)).powf(2f64))
15}
16
17/// Computes precision for given experimental results and confidence
18/// deriving it from adaptive bound through quadratic equation.
19pub fn derive_precision(s: u32, f: u32, confidence: f64) -> f64 {
20 let n = s + f;
21 let avg = s as f64 / n as f64;
22 let k = 2f64 * (2f64 / (1f64 - confidence)).ln();
23 // Compute quadratic equation coefficients.
24 let a = (n as f64) + (4f64 * k / 9f64);
25 let b = -4f64 * k * (avg - 0.5f64).abs() / 3f64;
26 let c = k * ((avg - 0.5f64).powf(2f64) - 0.25f64);
27 // Take (larger positive) quadratic equation solution.
28 (-b + (b.powf(2f64) - 4f64 * a * c).sqrt()) / (2f64 * a)
29}