print efficiency

Author: Jérôme FERET

core/KaSa_rep/main/KaSaIncremental.ml

@@ -88,7 +88,7 @@ let main () =
       state
   in
   let module KaSaUtil = KaSaUtil.KaSaUtil (Export_to_KaSa) in
-  let print_result parameters state print_analysis start_time =
+  let print_result parameters state print_analysis =
     let state, _ = Export_to_KaSa.get_reachability_analysis state in
     let state =
       if print_analysis then
@@ -98,12 +98,14 @@ let main () =
     in
     let error = Export_to_KaSa.get_errors state in
     let () = Exception.print parameters error in
-    let () = KaSaUtil.print_efficiency parameters state start_time in
     state
   in
-  let state = print_result parameters state false initial_start_time in
+  let state = print_result parameters state false  in
   let log = Remanent_parameters.get_logger parameters in
-  let rec loop state =
+  let rec loop_time state start_time =
+    Loggers.fprintf log "This computation step took ";
+    KaSaUtil.print_only_timing parameters start_time;
+    Loggers.print_newline log; 
     Loggers.fprintf log "> ";
     Loggers.flush_logger log;
     let state =
@@ -115,7 +117,7 @@ let main () =
       | "quit" | "q" -> ()
       | "help" | "h" ->
         Loggers.fprintf log "%s" help_message;
-        loop state
+        loop state 
       | "print rules" | "p rules" ->
         let state, compilation = Export_to_KaSa.get_compilation state in
         let () =
@@ -131,13 +133,11 @@ let main () =
         let () = Exception.print parameters error in
         loop state
       | "print result" | "p result" | "p" ->
-        let start_time = Sys.time () in
-        let state = print_result parameters state true start_time in
+        let state = print_result parameters state true in
         loop state
       | input
         when String.length input > 12 && String.sub input 0 12 = "update file "
         ->
-        let start_time = Sys.time () in
         let l = String.split_on_char ' ' input in
         let do_not_restart_fixpoint_computation =
           match !Config.do_restart_fixpoint_iterations with
@@ -168,10 +168,9 @@ let main () =
             in
             Export_to_KaSa.set_errors error state
         in
-        let state = print_result parameters state false start_time in
+        let state = print_result parameters state false  in
         loop state
       | input ->
-        let start_time = Sys.time () in
         let success, state =
           match parse_input input with
           | Enable (false, i) ->
@@ -208,7 +207,7 @@ let main () =
         in
         let state =
           if success then
-            print_result parameters state true start_time
+            print_result parameters state true 
           else (
             let error = Export_to_KaSa.get_errors state in
             let () = Exception.print parameters error in
@@ -217,7 +216,7 @@ let main () =
         in
         loop state
     with End_of_file -> ()
-  in
-  loop state
+  and loop state = loop_time state (Sys.time ()) 
+in loop_time state initial_start_time
 
 let () = main ()

core/KaSa_rep/main/KaSaUtil.ml

@@ -1,4 +1,28 @@
 module KaSaUtil (Export_to_KaSa : Export_to_KaSa.Type) = struct
+  let print_only_timing parameters start_time = 
+      if Remanent_parameters.get_print_efficiency parameters then 
+      let end_time = Sys.time () in
+      let cpu_time = end_time -. start_time in
+        let () =
+      if cpu_time <= 1. then
+        Loggers.fprintf
+          (Remanent_parameters.get_logger parameters)
+          "%0.6f s." cpu_time
+      else if cpu_time <= 10. then
+        Loggers.fprintf
+          (Remanent_parameters.get_logger parameters)
+          "%.6f s." cpu_time
+      else if cpu_time <= 1000. then
+        Loggers.fprintf
+          (Remanent_parameters.get_logger parameters)
+          "%3.3f s." cpu_time
+      else
+        Loggers.fprintf
+          (Remanent_parameters.get_logger parameters)
+          "%3.3g s." cpu_time
+    in
+    ()
+
   let print_efficiency parameters state start_time =
     if Remanent_parameters.get_print_efficiency parameters then (
       let end_time = Sys.time () in

core/KaSa_rep/main/KaSaUtil.mli

@@ -6,4 +6,7 @@ module KaSaUtil : functor (E : Export_to_KaSa.Type) -> sig
 
   val print_efficiency :
     Remanent_parameters_sig.parameters -> E.state -> float -> unit
+
+ val print_only_timing : 
+    Remanent_parameters_sig.parameters -> float -> unit
 end

core/KaSa_rep/more_datastructures/int_storage.ml

@@ -155,7 +155,7 @@ module Int_storage_imperatif :
     let error, dimension = dimension parameters error array in
     if dimension < size then (
       let error, array' = create parameters error size in
-      let _ = Array.blit array.array 0 array'.array 0 dimension in
+      let _ = Array.blit array.array 0 array'.array 0 (dimension+1) in
       error, array'
     ) else
       error, { array = Array.sub array.array 0 (size + 1); size }