synth: print out final window size

synth/src/basic.rs

@@ -7,14 +7,24 @@ use libpatron::mc::*;
 
 use crate::repair::*;
 use crate::testbench::StepInt;
+use crate::Stats;
 
 pub fn basic_repair<S: Simulator, E: TransitionSystemEncoding>(
     mut rctx: RepairContext<S, E>,
-) -> Result<Option<Vec<RepairAssignment>>> {
+) -> Result<RepairResult> {
     let res = generate_minimal_repair(&mut rctx, 0, None)?;
+    let stats = Stats::default();
     match res {
-        None => Ok(None), // no solution
-        Some((repair, _)) => Ok(Some(vec![repair])),
+        None => Ok(RepairResult {
+            status: RepairStatus::CannotRepair,
+            stats,
+            solutions: vec![],
+        }), // no solution
+        Some((repair, _)) => Ok(RepairResult {
+            status: RepairStatus::Success,
+            stats,
+            solutions: vec![repair],
+        }),
     }
 }
 

synth/src/incremental.rs

@@ -10,6 +10,7 @@ use std::collections::HashMap;
 use std::fmt::Debug;
 
 use crate::repair::*;
+use crate::Stats;
 
 pub struct IncrementalConf {
     pub fail_at: StepInt,
@@ -41,7 +42,7 @@ where
         })
     }
 
-    pub fn run(&mut self) -> Result<Option<Vec<RepairAssignment>>> {
+    pub fn run(&mut self) -> Result<RepairResult> {
         let mut window = RepairWindow::new();
 
         while window.len() <= self.conf.max_repair_window_size {
@@ -95,7 +96,7 @@ where
                             correct_solutions.push(repair.clone());
                             // early exit when we reached the max number of solutions
                             if correct_solutions.len() >= self.conf.max_solutions {
-                                return Ok(Some(correct_solutions));
+                                return Ok(make_result(Some(correct_solutions), &window));
                             }
                         }
                         Some(fail) => {
@@ -129,7 +130,7 @@ where
             self.rctx.smt_ctx.pop_many(1)?;
 
             if !correct_solutions.is_empty() {
-                return Ok(Some(correct_solutions));
+                return Ok(make_result(Some(correct_solutions), &window));
             }
 
             // we did not find a repair and we continue on
@@ -144,7 +145,7 @@ where
                     println!("Could not further increase the repair window.")
                 }
                 // we were not able to properly update the window
-                return Ok(None);
+                return Ok(make_result(None, &window));
             }
         }
 
@@ -155,7 +156,7 @@ where
                 self.conf.max_repair_window_size
             );
         }
-        Ok(None)
+        Ok(make_result(None, &window))
     }
 
     fn verbose(&self) -> bool {
@@ -209,6 +210,22 @@ where
     }
 }
 
+fn make_result(solutions: Option<Vec<RepairAssignment>>, window: &RepairWindow) -> RepairResult {
+    RepairResult {
+        status: if solutions.is_none() {
+            RepairStatus::CannotRepair
+        } else {
+            RepairStatus::Success
+        },
+        stats: Stats {
+            final_past_k: window.past_k,
+            final_future_k: window.future_k,
+            solver_time: 0,
+        },
+        solutions: solutions.unwrap_or_default(),
+    }
+}
+
 #[derive(Debug, Copy, Clone, Eq, PartialEq)]
 struct RepairWindow {
     future_k: StepInt,

synth/src/main.rs

@@ -10,7 +10,9 @@ mod testbench;
 use crate::basic::basic_repair;
 use crate::filters::can_be_repaired_from_arbitrary_state;
 use crate::incremental::{IncrementalConf, IncrementalRepair};
-use crate::repair::{add_change_count, create_smt_ctx, RepairContext, RepairVars};
+use crate::repair::{
+    add_change_count, create_smt_ctx, RepairContext, RepairResult, RepairStatus, RepairVars,
+};
 use crate::testbench::*;
 use clap::{arg, Parser, ValueEnum};
 use easy_smt as smt;
@@ -179,7 +181,7 @@ fn main() {
         if args.verbose {
             println!("Design seems to work.");
         }
-        print_no_repair();
+        print_no_repair(&synth_vars, &ctx);
         return;
     }
 
@@ -189,7 +191,7 @@ fn main() {
         if args.verbose {
             println!("No changes possible.");
         }
-        print_cannot_repair();
+        print_cannot_repair(&synth_vars, &ctx);
         return;
     }
 
@@ -231,7 +233,7 @@ fn main() {
         if args.verbose {
             println!("Cannot be repaired, even when we start from an arbitrary state!");
         }
-        print_cannot_repair();
+        print_cannot_repair(&synth_vars, &ctx);
         return;
     }
 
@@ -258,30 +260,7 @@ fn main() {
     }
 
     // print status
-    let solutions = match repair {
-        None => {
-            print_cannot_repair();
-            return;
-        }
-        Some(assignments) => {
-            let mut res = Vec::with_capacity(assignments.len());
-            for aa in assignments.iter() {
-                let assignment_json = synth_vars.to_json(&ctx, aa);
-                res.push(json!({"assignment": assignment_json}));
-            }
-            json!(res)
-        }
-    };
-
-    let res = json!({
-        "status": "success",
-        "solver-time": 0,
-        "past-k": 0,
-        "future-k": 0,
-        "solutions": solutions,
-    });
-
-    print_result(&res);
+    print_result(&repair, &synth_vars, &ctx);
 }
 
 fn start_solver(
@@ -295,32 +274,64 @@ fn start_solver(
     Ok((smt_ctx, enc))
 }
 
-fn print_cannot_repair() {
-    let res = json!({
-        "status": "cannot-repair",
-        "solver-time": 0,
-        "past-k": 0,
-        "future-k": 0,
-        "solutions": [],
-    });
+fn print_result(result: &RepairResult, synth_vars: &RepairVars, ctx: &Context) {
+    let mut solutions = Vec::with_capacity(result.solutions.len());
+    for aa in result.solutions.iter() {
+        let assignment_json = synth_vars.to_json(ctx, aa);
+        solutions.push(json!({"assignment": assignment_json}));
+    }
 
-    print_result(&res);
-}
+    let status_name = match result.status {
+        RepairStatus::CannotRepair => "cannot-repair",
+        RepairStatus::NoRepair => "no-repair",
+        RepairStatus::Success => "success",
+    };
 
-fn print_no_repair() {
+    let solution_jsons = json!(solutions);
     let res = json!({
-        "status": "no-repair",
-        "solver-time": 0,
-        "past-k": 0,
-        "future-k": 0,
-        "solutions": [],
+        "status": status_name,
+        "solver-time": result.stats.solver_time,
+        "past-k": result.stats.final_past_k,
+        "future-k": result.stats.final_future_k,
+        "solutions": solution_jsons,
     });
 
-    print_result(&res);
-}
-
-fn print_result(res: &serde_json::Value) {
     println!("== RESULT =="); // needle to find the JSON output
     let j = serde_json::to_string(&res).unwrap();
     println!("{}", j);
 }
+
+fn print_cannot_repair(synth_vars: &RepairVars, ctx: &Context) {
+    let res = RepairResult {
+        status: RepairStatus::CannotRepair,
+        stats: Default::default(),
+        solutions: vec![],
+    };
+    print_result(&res, synth_vars, ctx);
+}
+
+fn print_no_repair(synth_vars: &RepairVars, ctx: &Context) {
+    let res = RepairResult {
+        status: RepairStatus::NoRepair,
+        stats: Default::default(),
+        solutions: vec![],
+    };
+    print_result(&res, synth_vars, ctx);
+}
+
+#[derive(Debug, Copy, Clone, Eq, PartialEq)]
+pub struct Stats {
+    final_past_k: StepInt,
+    final_future_k: StepInt,
+    solver_time: u64,
+}
+
+impl Default for Stats {
+    fn default() -> Self {
+        Self {
+            final_past_k: 0,
+            final_future_k: 0,
+            solver_time: 0,
+        }
+    }
+}

synth/src/repair.rs

@@ -3,6 +3,7 @@
 // author: Kevin Laeufer <[email protected]>
 
 use crate::testbench::{StepInt, Testbench};
+use crate::Stats;
 use easy_smt as smt;
 use libpatron::ir::*;
 use libpatron::mc::*;
@@ -13,6 +14,18 @@ use std::str::FromStr;
 
 pub type Result<T> = std::io::Result<T>;
 
+pub enum RepairStatus {
+    CannotRepair,
+    NoRepair,
+    Success,
+}
+
+pub struct RepairResult {
+    pub status: RepairStatus,
+    pub stats: Stats,
+    pub solutions: Vec<RepairAssignment>,
+}
+
 pub struct RepairContext<'a, S: Simulator, E: TransitionSystemEncoding> {
     pub ctx: &'a mut Context,
     pub sys: &'a TransitionSystem,