Improve /timing

viperproject · Jan 13, 2025 · f5700f3 · f5700f3
1 parent 9506ffc
commit f5700f3
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 11 deletions.
diff --git a/source/Loader.cs b/source/Loader.cs
@@ -171,12 +171,14 @@ void taskLoadZ3LogFile(string logFile)
                         }
                     }
                     });
-                    while (!stop) {
-                        stop = true;
-                        if (task.Wait(TimeSpan.FromMilliseconds(1000))) {
-                            stop = false;
-                            break;
-                        }
+                    if (!task.Wait(TimeSpan.FromMilliseconds(300))) {
+                        do {
+                            stop = true;
+                            if (task.Wait(TimeSpan.FromMilliseconds(1000))) {
+                                stop = false;
+                                break;
+                            }
+                        } while (!stop);
                     }
                     if (stop)
                         isCancelled = true;
@@ -201,8 +203,9 @@ void taskLoadZ3LogFile(string logFile)
             }
             statusUpdate(1000);
             if (!config.timing) return;
-            if (isCancelled) Console.WriteLine("[Parse] Err " + oldperc + "‰");
-            else Console.WriteLine("[Parse] " + parseMs + "ms");
+            Console.Write("[Parse] ");
+            if (isCancelled) Console.Write("Err " + oldperc + "‰ ");
+            Console.WriteLine(parseMs + "ms");
             Console.WriteLine("[Graph] " + analysisMs + "ms");
         }
 

diff --git a/source/ScriptingSupport.cs b/source/ScriptingSupport.cs
@@ -33,9 +33,9 @@ public static bool RunScriptingTasks(Model model, ScriptingTasks tasks, bool tim
             var trueLoops = new List<List<Quantifier>>();
             var falseLoops = new List<List<Quantifier>>();
             var error = "";
+            var watch = new System.Diagnostics.Stopwatch();
             try
             {
-                var watch = System.Diagnostics.Stopwatch.StartNew();
                 // Output basic information
                 var basicFileExists = false;
                 if (tasks.ShowNumChecks)
@@ -58,6 +58,7 @@ public static bool RunScriptingTasks(Model model, ScriptingTasks tasks, bool tim
                         }
                     }
                 }
+                watch.Start();
 
                 // Check logest paths for potential loops
                 var pathsToCheck = model.instances.Where(inst => inst.Depth == 1)
@@ -66,17 +67,21 @@ public static bool RunScriptingTasks(Model model, ScriptingTasks tasks, bool tim
                     .Select(inst => deepestPathStartingFrom(inst)).ToList();
                 if (pathsToCheck.Any())
                 {
+                    watch.Stop();
                     using (var writer = new StreamWriter(basePath + ".loops", false))
                     {
                         writer.WriteLine("# repetitions,repeating pattern");
+                        watch.Start();
                         foreach (var path in pathsToCheck)
                         {
                             var cycleDetection = new CycleDetection.CycleDetection(path.getInstantiations(), 3);
                             var gen = cycleDetection.getGeneralization();
                             if (gen != null)
                             {
                                 var quantifiers = cycleDetection.getCycleQuantifiers();
+                                watch.Stop();
                                 writer.WriteLine(cycleDetection.GetNumRepetitions() + "," + string.Join(" -> ", quantifiers.Select(quant => quant.PrintName)) + "," + gen.TrueLoop);
+                                watch.Start();
                                 if (gen.TrueLoop) {
                                     if (!trueLoops.Contains(quantifiers))
                                         trueLoops.Add(quantifiers);
@@ -91,13 +96,16 @@ public static bool RunScriptingTasks(Model model, ScriptingTasks tasks, bool tim
                                 break;
                             }
                         }
+                        watch.Stop();
                     }
+                    watch.Start();
                 }
 
                 // High branching analysis
                 var highBranchingInsts = model.instances.Where(inst => inst.DependantInstantiations.Count() >= tasks.FindHighBranchingThreshold).ToList();
                 if (highBranchingInsts.Any())
                 {
+                    watch.Stop();
                     using (var writer = new StreamWriter(basePath + ".branching"))
                     {
                         writer.WriteLine($"Quantifier,# instances with ≥ {tasks.FindHighBranchingThreshold} direct children");
@@ -106,12 +114,14 @@ public static bool RunScriptingTasks(Model model, ScriptingTasks tasks, bool tim
                             writer.WriteLine(quant.Key.PrintName + "," + quant.Count());
                         }
                     }
+                    watch.Start();
                 }
                 watch.Stop();
                 tasksMs = watch.ElapsedMilliseconds;
             }
             catch (Exception e)
             {
+                watch.Stop();
                 error = e.Message;
                 const int ERROR_HANDLE_DISK_FULL = 0x27;
                 const int ERROR_DISK_FULL = 0x70;
@@ -125,10 +135,11 @@ public static bool RunScriptingTasks(Model model, ScriptingTasks tasks, bool tim
                 }
             }
             if (timing) {
+                Console.Write("[Analysis] ");
                 if (tasksMs == long.MaxValue)
-                    Console.WriteLine("[Analysis] Err " + error);
+                    Console.WriteLine("Err " + watch.ElapsedMilliseconds + "ms " + error);
                 else
-                    Console.WriteLine("[Analysis] " + tasksMs + "ms");
+                    Console.WriteLine(tasksMs + "ms");
                 Console.WriteLine("[Loops] " + trueLoops.Count + " true, " + falseLoops.Count + " false");
             }