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() * 0.5f64 / precision.powi(2)
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 okamoto_bound(confidence, precision)
14 * precision
15 .mul_add(-2f64 / 3f64, (avg - 0.5f64).abs())
16 .powi(2)
17 .mul_add(-4f64, 1f64)
18}
19
20/// Computes precision for given experimental results and confidence
21/// deriving it from adaptive bound through quadratic equation.
22pub fn derive_precision(s: u32, f: u32, confidence: f64) -> f64 {
23 let n = s + f;
24 let avg = s as f64 / n as f64;
25 let k = 2f64 * (2f64 / (1f64 - confidence)).ln();
26 // Compute quadratic equation coefficients.
27 let a = k.mul_add(4f64 / 9f64, n as f64);
28 let b = -(4f64 / 3f64) * k * (avg - 0.5f64).abs();
29 let c = k * (avg.powi(2) - avg);
30 // Take (larger positive) quadratic equation solution.
31 (a.mul_add(-4f64 * c, b.powi(2)).sqrt() - b) / (2f64 * a)
32}