rust_formal_verification/algorithms/
bmc.rs

1// ************************************************************************************************
2// use
3// ************************************************************************************************
4
5use std::{
6    thread,
7    time::{Duration, Instant},
8};
9
10use crate::{
11    formulas::{literal::VariableType, CNF},
12    models::FiniteStateTransitionSystem,
13    solvers::sat::{Assignment, SatResponse, StatelessSatSolver},
14};
15
16// ************************************************************************************************
17// enum
18// ************************************************************************************************
19
20pub enum BMCResult {
21    NoCTX {
22        depth_reached: i32,
23    },
24    CTX {
25        assignment: Assignment,
26        depth: VariableType,
27    },
28}
29
30enum TimedSatResult {
31    TimeOut,
32    NoTimeOut { response: SatResponse },
33}
34
35// ************************************************************************************************
36// struct
37// ************************************************************************************************
38
39pub struct BMC<T: StatelessSatSolver> {
40    verbose: bool,
41    solver: T,
42}
43
44// ************************************************************************************************
45// impl
46// ************************************************************************************************
47
48impl<T: StatelessSatSolver + std::marker::Send + 'static + std::marker::Sync + Clone> BMC<T> {
49    // ********************************************************************************************
50    // helper functions
51    // ********************************************************************************************
52
53    fn timed_sat_call(
54        &self,
55        sat_formula: CNF,
56        start_instant: &Instant,
57        timeout_duration: Duration,
58    ) -> TimedSatResult {
59        let solver = self.solver.to_owned();
60        let join_handle = thread::spawn(move || solver.solve_cnf(&sat_formula));
61
62        // wait until sat call finished or timeout has passed
63        let mut sleep_duration_in_millis = 1;
64        while !join_handle.is_finished() && (start_instant.elapsed() < timeout_duration) {
65            thread::sleep(Duration::from_millis(sleep_duration_in_millis));
66            // exponential increase no more than 1 second.
67            if sleep_duration_in_millis < 1000 {
68                sleep_duration_in_millis *= 2;
69            }
70        }
71
72        if join_handle.is_finished() {
73            // the sat call has stopped
74            let response = join_handle.join().unwrap();
75            TimedSatResult::NoTimeOut { response }
76        } else {
77            // let thread run until completion
78            TimedSatResult::TimeOut
79        }
80    }
81
82    // ********************************************************************************************
83    // api functions
84    // ********************************************************************************************
85
86    pub fn new(verbose: bool) -> Self {
87        Self {
88            solver: T::default(),
89            verbose,
90        }
91    }
92
93    pub fn search(
94        &self,
95        fin_state: &FiniteStateTransitionSystem,
96        search_depth_limit: u32,
97        timeout_duration: Duration,
98    ) -> BMCResult {
99        let start = Instant::now();
100        // I
101        let initial = fin_state.get_initial_relation();
102        // println!("initial = {}", initial);
103        // !P
104        let mut not_p0 = fin_state.get_unsafety_property().to_cnf();
105        not_p0.append(&fin_state.get_state_to_safety_translation());
106        // println!("not_p0 = {}", not_p0);
107        // Tr
108        let tr = fin_state.get_transition_relation();
109        // println!("tr = {}", tr);
110
111        // loop for wanted depth
112        for depth in 0..(search_depth_limit + 1) {
113            if self.verbose {
114                println!(
115                    "BMC running - depth = {}, elapsed time = {}",
116                    depth,
117                    start.elapsed().as_secs_f32()
118                );
119            }
120            if start.elapsed() > timeout_duration {
121                let depth: i32 = depth.try_into().unwrap();
122                return BMCResult::NoCTX {
123                    depth_reached: (depth - 1),
124                };
125            }
126
127            let mut sat_formula = initial.to_owned().to_cnf();
128            for unroll_depth in 0..depth {
129                sat_formula.append(&fin_state.add_tags_to_relation(&tr, unroll_depth));
130            }
131            sat_formula.append(&fin_state.add_tags_to_relation(&not_p0, depth));
132
133            let timed_response = self.timed_sat_call(sat_formula, &start, timeout_duration);
134            match timed_response {
135                TimedSatResult::NoTimeOut { response } => match response {
136                    SatResponse::Sat { assignment } => return BMCResult::CTX { assignment, depth },
137                    SatResponse::UnSat => {}
138                },
139                TimedSatResult::TimeOut => {
140                    let depth: i32 = depth.try_into().unwrap();
141                    return BMCResult::NoCTX {
142                        depth_reached: (depth - 1),
143                    };
144                }
145            }
146        }
147        BMCResult::NoCTX {
148            depth_reached: search_depth_limit.try_into().unwrap(),
149        }
150    }
151}
rust_formal_verification/algorithms/bmc.rs

rust_formal_verification/algorithms/
bmc.rs
