Removing Pattern

Src/PChecker/CheckerCore/CheckerConfiguration.cs

@@ -257,12 +257,6 @@ public int MaxSchedulingSteps
         [DataMember]
         public uint TestingProcessId;
 
-        /// <summary>
-        /// The source of the pattern generator.
-        /// </summary>
-        [DataMember]
-        public string PatternSource;
-
         /// <summary>
         /// Additional assembly specifications to instrument for code coverage, besides those in the
         /// dependency graph between <see cref="AssemblyToBeAnalyzed"/> and the Microsoft.Coyote DLLs.
@@ -347,7 +341,6 @@ protected CheckerConfiguration()
 
             PSymArgs = "";
             JvmArgs = "";
-            PatternSource = "";
         }
 
         /// <summary>

Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/FeedbackGuidedStrategy.cs

@@ -30,7 +30,7 @@
     private int _pendingMutations = 0;
     private bool _shouldExploreNew = false;
     private HashSet<GeneratorRecord> _visitedGenerators = new HashSet<GeneratorRecord>();
     private GeneratorRecord? _currentParent = null;
 
     private System.Random _rnd = new System.Random();
 
@@ -155,7 +155,7 @@
     /// <summary>
     /// This method observes the results of previous run and prepare for the next run.
     /// </summary>
-    public virtual void ObserveRunningResults(EventPatternObserver patternObserver, TimelineObserver timelineObserver)
+    public virtual void ObserveRunningResults(TimelineObserver timelineObserver)
     {
         var timelineHash = timelineObserver.GetTimelineHash();
         var timelineMinhash = timelineObserver.GetTimelineMinhash();
@@ -167,18 +167,8 @@
             return;
         }
 
-        int priority = 0;
-        if (patternObserver == null)
-        {
-            priority = diversityScore;
-        }
-        else
-        {
-            int coverageResult = patternObserver.ShouldSave();
-            double coverageScore = 1.0 / coverageResult;
-            priority = (int)(diversityScore * coverageScore);
-        }
-
+        int priority = diversityScore;
+
         if (priority > 0)
         {
             var record = new GeneratorRecord(priority, Generator, timelineMinhash);

Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/IFeedbackGuidedStrategy.cs

@@ -6,7 +6,7 @@ namespace PChecker.SystematicTesting.Strategies.Feedback;
 
 internal interface IFeedbackGuidedStrategy: ISchedulingStrategy
 {
-    public void ObserveRunningResults(EventPatternObserver patternObserver, TimelineObserver timelineObserver);
+    public void ObserveRunningResults(TimelineObserver timelineObserver);
     public int TotalSavedInputs();
     public void DumpStats(TextWriter writer);
 }

Src/PChecker/CheckerCore/SystematicTesting/Strategies/Probabilistic/QLearningStrategy.cs

@@ -394,7 +394,7 @@ private int ComputeDiversity(int timeline, List<int> hash)
             return (hash.Count - maxSim) * 10 + 20;
         }
 
-        public void ObserveRunningResults(EventPatternObserver patternObserver, TimelineObserver timelineObserver)
+        public void ObserveRunningResults(TimelineObserver timelineObserver)
         {
             var timelineHash = timelineObserver.GetTimelineHash();
             var timelineMinhash = timelineObserver.GetTimelineMinhash();

Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs

@@ -100,20 +100,13 @@ public class TestReport
         /// </summary>
         [DataMember]
         public HashSet<string> InternalErrors { get; internal set; }
-
-
+
         /// <summary>
         /// Set of hashes of timelines discovered by the scheduler.
         /// </summary>
         [DataMember]
         public Dictionary<int, int> ExploredTimelines = new();
 
-        /// <summary>
-        /// Number of schedulings that satisfies the pattern.
-        /// </summary>
-        [DataMember]
-        public Dictionary<int, int> ValidScheduling = new();
-
         /// <summary>
         /// Lock for the test report.
         /// </summary>

Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs

@@ -65,11 +65,6 @@ public class TestingEngine
         /// </summary>
         internal readonly ISchedulingStrategy Strategy;
 
-        /// <summary>
-        /// Pattern coverage observer if pattern is provided
-        /// </summary>
-        private EventPatternObserver? _eventPatternObserver;
-
         /// <summary>
         /// Monitors conflict operations used by the POS Strategy.
         /// </summary>
@@ -217,27 +212,20 @@ public static TestingEngine Create(CheckerConfiguration checkerConfiguration, As
             }
 
             TestMethodInfo testMethodInfo = null;
-            EventPatternObserver eventMatcher = null;
             try
             {
                 testMethodInfo = TestMethodInfo.GetFromAssembly(assembly, checkerConfiguration.TestCaseName);
                 Console.Out.WriteLine($".. Test case :: {testMethodInfo.Name}");
 
                 Type t = assembly.GetType("PImplementation.GlobalFunctions");
-                if (checkerConfiguration.PatternSource.Length > 0)
-                {
-                    var result = t.GetMethod(checkerConfiguration.PatternSource,
-                        BindingFlags.Public | BindingFlags.Static)!;
-                    eventMatcher = new EventPatternObserver(result);
-                }
             }
             catch
             {
                 Error.ReportAndExit(
                     $"Failed to get test method '{checkerConfiguration.TestCaseName}' from assembly '{assembly.FullName}'");
             }
 
-            return new TestingEngine(checkerConfiguration, testMethodInfo, eventMatcher);
+            return new TestingEngine(checkerConfiguration, testMethodInfo);
         }
 
         /// <summary>
@@ -284,21 +272,15 @@ internal TestingEngine(CheckerConfiguration checkerConfiguration, Delegate test)
             : this(checkerConfiguration, new TestMethodInfo(test))
         {
         }
-
-        private TestingEngine(CheckerConfiguration checkerConfiguration, TestMethodInfo testMethodInfo)
-            : this(checkerConfiguration, testMethodInfo, null)
-        {
-        }
+
 
         /// <summary>
         /// Initializes a new instance of the <see cref="TestingEngine"/> class.
         /// </summary>
-        private TestingEngine(CheckerConfiguration checkerConfiguration, TestMethodInfo testMethodInfo,
-            EventPatternObserver observer)
+        private TestingEngine(CheckerConfiguration checkerConfiguration, TestMethodInfo testMethodInfo)
         {
             _checkerConfiguration = checkerConfiguration;
             TestMethodInfo = testMethodInfo;
-            _eventPatternObserver = observer;
 
             Logger = new ConsoleLogger();
             ErrorReporter = new ErrorReporter(checkerConfiguration, Logger);
@@ -586,10 +568,6 @@ private void RegisterObservers(ControlledRuntime runtime)
                 // Always output a json log of the error
                 JsonLogger = new JsonWriter();
                 runtime.SetJsonLogger(JsonLogger);
-                if (_eventPatternObserver != null)
-                {
-                    runtime.RegisterLog(_eventPatternObserver);
-                }
 
                 if (_conflictOpObserver != null)
                 {
@@ -666,7 +644,7 @@ private void RunNextIteration(int schedule)
 
                 if (Strategy is IFeedbackGuidedStrategy strategy)
                 {
-                    strategy.ObserveRunningResults(_eventPatternObserver, timelineObserver);
+                    strategy.ObserveRunningResults(timelineObserver);
                 }
 
                 // Checks that no monitor is in a hot state at termination. Only
@@ -735,14 +713,9 @@ private void RunNextIteration(int schedule)
                 }
 
                 // Cleans up the runtime before the next iteration starts.
-                if (_eventPatternObserver != null)
-                {
-                    runtime.RemoveLog(_eventPatternObserver);
-                }
 
                 runtimeLogger?.Dispose();
                 runtime?.Dispose();
-                _eventPatternObserver?.Reset();
                 _conflictOpObserver?.Reset();
             }
         }
@@ -1037,29 +1010,17 @@ private void GatherTestingStatistics(ControlledRuntime runtime, TimelineObserver
             {
                 report.CoverageInfo.CoverageGraph = Graph;
             }
-
-            int shouldSave = 1;
-
-            if (_eventPatternObserver != null)
-            {
-                shouldSave = _eventPatternObserver.ShouldSave();
-                TestReport.ValidScheduling.TryAdd(shouldSave, 0);
-                TestReport.ValidScheduling[shouldSave] += 1;
-            }
-
-            if (shouldSave == 1)
-            {
-                var coverageInfo = runtime.GetCoverageInfo();
-                report.CoverageInfo.Merge(coverageInfo);
-                TestReport.Merge(report);
-                var timelineHash = timelineObserver.GetTimelineHash();
-                TestReport.ExploredTimelines[timelineHash] =
-                    TestReport.ExploredTimelines.GetValueOrDefault(timelineHash, 0) + 1;
-                // 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.
-                Graph = coverageInfo.CoverageGraph;
-            }
+
+            var coverageInfo = runtime.GetCoverageInfo();
+            report.CoverageInfo.Merge(coverageInfo);
+            TestReport.Merge(report);
+            var timelineHash = timelineObserver.GetTimelineHash();
+            TestReport.ExploredTimelines[timelineHash] =
+                TestReport.ExploredTimelines.GetValueOrDefault(timelineHash, 0) + 1;
+            // 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.
+            Graph = coverageInfo.CoverageGraph;
         }
 
         /// <summary>

Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs

@@ -81,7 +81,6 @@ internal PCheckerOptions()
             advancedGroup.AddArgument("xml-trace", null, "Specify a filename for XML runtime log output to be written to", typeof(bool));
             advancedGroup.AddArgument("psym-args", null, "Specify a concatenated list of additional PSym-specific arguments to pass, each starting with a colon").IsHidden = true;
             advancedGroup.AddArgument("jvm-args", null, "Specify a concatenated list of PSym-specific JVM arguments to pass, each starting with a colon").IsHidden = true;
-            advancedGroup.AddArgument("pattern", null, "The name of the pattern matcher generator", typeof(string));
             advancedGroup.AddArgument("conflict-analysis", null, "Enable POS conflict analysis.", typeof(bool));
         }
 
@@ -328,9 +327,6 @@ private static void UpdateConfigurationWithParsedArgument(CheckerConfiguration c
                 case "jvm-args":
                     checkerConfiguration.JvmArgs = ((string)option.Value).Replace(':', ' ');
                     break;
-                case "pattern":
-                    checkerConfiguration.PatternSource = (string) option.Value;
-                    break;
                 case "conflict-analysis":
                     checkerConfiguration.EnableConflictAnalysis = true;
                     break;