diff --git a/synth/src/studies/mod.rs b/synth/src/studies/mod.rs index 797cb13..b2b1790 100644 --- a/synth/src/studies/mod.rs +++ b/synth/src/studies/mod.rs @@ -1 +1,6 @@ +// Copyright 2023-2024 The Regents of the University of California +// released under BSD 3-Clause License +// author: Kevin Laeufer + +pub mod unrolling; pub mod windowing; diff --git a/synth/src/studies/unrolling.rs b/synth/src/studies/unrolling.rs new file mode 100644 index 0000000..55b487c --- /dev/null +++ b/synth/src/studies/unrolling.rs @@ -0,0 +1,5 @@ +// Copyright 2024 The Regents of the University of California +// released under BSD 3-Clause License +// author: Kevin Laeufer +// +// we study how the length of unrolling affects the basic synthesis approach diff --git a/synth/src/studies/windowing.rs b/synth/src/studies/windowing.rs index c9c3a6d..7c5a0d5 100644 --- a/synth/src/studies/windowing.rs +++ b/synth/src/studies/windowing.rs @@ -32,14 +32,20 @@ pub struct Windowing<'a, S: Simulator, E: TransitionSystemEncoding> { snapshots: HashMap, } +// possible outcomes: +// 1. no repair found +// 2. no correct repair found + #[derive(Debug, Serialize)] struct Stats { - /// time it took to sample the first minimal repair - minimal_repair_candidate_ns: Option, - /// number of minimal repairs sampled before we found a correct repair - correct_repair_tries: Option, - /// time to find a correct repair - correct_repair_ns: Option, + /// minimum number of changes, None if no repair found + min_repair_size: Option, + /// number of minimal repairs that were samples + min_repairs_samples: u64, + /// whether a correct repair was found + success: bool, + /// overall time in ns + time_ns: u128, } #[derive(Debug, Serialize)] @@ -167,7 +173,6 @@ where // generate one minimal repair let r = generate_minimal_repair(&mut self.rctx, step_range.start, Some(step_range.end))?; - let minimal_repair_candidate_ns = start.elapsed().as_nanos(); let mut failures_at = Vec::new(); if let Some((r0, num_changes)) = r { @@ -181,11 +186,12 @@ where .first_fail_at { None => { - let correct_repair_ns = Some(start.elapsed().as_nanos()); + let time_ns = start.elapsed().as_nanos(); let stats = Stats { - minimal_repair_candidate_ns: Some(minimal_repair_candidate_ns), - correct_repair_tries: Some((failures_at.len() + 1) as u64), - correct_repair_ns, + min_repair_size: Some(num_changes as u64), + min_repairs_samples: (failures_at.len() + 1) as u64, + success: true, + time_ns, }; return Ok((stats, make_result(Some(repair), window))); } @@ -215,18 +221,22 @@ where }; } // no correct repair found + let time_ns = start.elapsed().as_nanos(); let stats = Stats { - minimal_repair_candidate_ns: Some(minimal_repair_candidate_ns), - correct_repair_tries: None, - correct_repair_ns: None, + min_repair_size: Some(num_changes as u64), + min_repairs_samples: failures_at.len() as u64, + success: false, + time_ns, }; Ok((stats, make_result(None, window))) } else { // no repair found + let time_ns = start.elapsed().as_nanos(); let stats = Stats { - minimal_repair_candidate_ns: None, - correct_repair_tries: None, - correct_repair_ns: None, + min_repair_size: None, + min_repairs_samples: failures_at.len() as u64, + success: false, + time_ns, }; Ok((stats, make_result(None, window))) }