Removed added timeline in summary.txt for pintcdk

p-org · Dec 2, 2024 · 1f0aa16 · 1f0aa16
1 parent cfa62a1
commit 1f0aa16
Show file tree

Hide file tree

Showing 5 changed files with 22 additions and 7 deletions.
diff --git a/Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs b/Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs
@@ -543,7 +543,7 @@ public void SendEvent(PMachineValue target, Event ev)
             AnnounceInternal(ev);
             // Update vector clock
             VectorTime.Increment();
-            BehavioralObserver.AddToCurrentTimeline(ev, BehavioralObserver.EventType.SEND, VectorTime);
+            // BehavioralObserver.AddToCurrentTimeline(ev, BehavioralObserver.EventType.SEND, VectorTime);
             Runtime.SendEvent(target.Id, ev, this);
         }
 
@@ -601,7 +601,7 @@ internal async Task RunEventHandlerAsync()
                 {
                     // Update state machine vector clock
                     VectorTime.Merge(info.VectorTime);
-                    BehavioralObserver.AddToCurrentTimeline(e, BehavioralObserver.EventType.DEQUEUE, VectorTime);
+                    // BehavioralObserver.AddToCurrentTimeline(e, BehavioralObserver.EventType.DEQUEUE, VectorTime);
 
                     // Notify the runtime for a new event to handle. This is only used
                     // during bug-finding and operation bounding, because the runtime

diff --git a/...PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/BehavioralObserver.cs b/...PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/BehavioralObserver.cs
@@ -9,7 +9,8 @@ namespace PChecker.Runtime;
 public class BehavioralObserver
 {
     private static HashSet<(VectorTime, Event, EventType)> CurrTimeline = new HashSet<(VectorTime, Event, EventType)>();
-    private static List<int[]> AllTimeline = new List<int[]>();
+    public static int uniquenessScore;
+    public static List<int[]> AllTimeline = new List<int[]>();
     private static TextWriter Logger = new ConsoleLogger();
     // MinHash object with 100 hash functions, check how many of these 100 values are identical between the two sets
     private static MinHash minHash = new MinHash(100);  
@@ -68,6 +69,7 @@ public static void PrintTimeline(List<(VectorTime, Event, EventType)> timeline)
         // Sort by event name then vector time
         sortedTimeline.Sort((x, y) => x.Item2.ToString().CompareTo(y.Item2.ToString()));
         sortedTimeline.Sort((x, y) => x.Item1.CompareTo(y.Item1));
+        // PrintTimeline(sortedTimeline);
 
         return sortedTimeline;
     }
@@ -85,9 +87,9 @@ public static void NextIter()
             AllTimeline.Add(currSignature);
             return;
         }
-        int uniqueScore = GetUniqueScore(currSignature);
-        Logger.WriteLine($"----**** UniquenessScore: {uniqueScore}");
-        if (uniqueScore != 0)
+        uniquenessScore = GetUniqueScore(currSignature);
+        // Logger.WriteLine($"----**** UniquenessScore: {uniqueScore}");
+        if (uniquenessScore != 0)
         {
             AllTimeline.Add(currSignature);
         }

diff --git a/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/FeedbackGuidedStrategy.cs b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/FeedbackGuidedStrategy.cs
@@ -5,6 +5,7 @@
 using PChecker.Generator;
 using PChecker.Feedback;
 using PChecker.Generator.Object;
+using PChecker.Runtime;
 using PChecker.SystematicTesting.Strategies.Probabilistic;
 using AsyncOperation = PChecker.SystematicTesting.Operations.AsyncOperation;
 using Debug = System.Diagnostics.Debug;
@@ -160,6 +161,7 @@ public virtual void ObserveRunningResults(TimelineObserver timelineObserver)
         var timelineMinhash = timelineObserver.GetTimelineMinhash();
 
         int diversityScore = ComputeDiversity(timelineHash, timelineMinhash);
+        // int diversityScore = BehavioralObserver.uniquenessScore;
 
         if (diversityScore == 0)
         {

diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs
@@ -6,6 +6,7 @@
 using System.Runtime.Serialization;
 using System.Text;
 using PChecker.Coverage;
+using PChecker.Runtime;
 using PChecker.Utilities;
 
 namespace PChecker.SystematicTesting
@@ -208,6 +209,9 @@ public string GetSummaryText(Profiler Profiler) {
             report.AppendLine();
 
             report.AppendFormat($"memory_max_mb:{Profiler.GetMaxMemoryUsage():0.##}");
+            report.AppendLine();
+
+            report.AppendFormat("timelines:{0}", ExploredTimelines.Count);
 
             return report.ToString();
         }
@@ -247,6 +251,11 @@ public string GetText(CheckerConfiguration checkerConfiguration, string prefix =
                 prefix.Equals("...") ? "....." : prefix,
                 ExploredTimelines.Count,
                 ExploredTimelines.Count == 1 ? string.Empty : "s");
+            // report.AppendFormat(
+            //     "{0} Christine's method Explored {1} timeline{2}",
+            //     prefix.Equals("...") ? "....." : prefix,
+            //     BehavioralObserver.AllTimeline.Count,
+            //     ExploredTimelines.Count == 1 ? string.Empty : "s");
 
             if (totalExploredSchedules > 0 &&
                 NumOfFoundBugs > 0)

diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs
@@ -542,7 +542,7 @@ private void RegisterObservers(ControlledRuntime runtime)
         /// </summary>
         private void RunNextIteration(int schedule)
         {
-            BehavioralObserver.NextIter();
+            // BehavioralObserver.NextIter();
             if (!IsReplayModeEnabled && ShouldPrintIteration(schedule + 1))
             {
                 Logger.WriteLine($"..... Schedule #{schedule + 1}");
@@ -700,6 +700,7 @@ public string GetReport()
                     TestReport.NumOfFoundBugs == 1 ? string.Empty : "s");
                 report.AppendLine();
                 report.Append($"... Elapsed {Profiler.GetElapsedTime():0.##} sec and used {Profiler.GetMaxMemoryUsage():0.##} GB.");
+                // report.Append($"... Passed through {BehavioralObserver.AllTimeline.Count} unique timelines");
                 return report.ToString();
             }
 
@@ -969,6 +970,7 @@ private void GatherTestingStatistics(ControlledRuntime runtime, TimelineObserver
             TestReport.Merge(report);
             var timelineHash = timelineObserver.GetTimelineHash();
             TestReport.ExploredTimelines.Add(timelineObserver.GetTimelineHash());
+            Logger.WriteLine("Timeline:" + timelineObserver.GetAbstractTimeline());
             // Also save the graph snapshot of the last iteration, if there is one.
             Graph = coverageInfo.CoverageGraph;
             // Also save the graph snapshot of the last schedule, if there is one.