Improving the code with some cleanup. (#719)

* Disable trace logging to save disk space.

* Update feedback algorithm.

* fix feedback strategy.

* refactor.

* Remove experiment features.

---------

Co-authored-by: Ao Li <[email protected]>

Src/PChecker/CheckerCore/Actors/ActorRuntime.cs

@@ -264,6 +264,8 @@ private Actor CreateActor(ActorId id, Type type, string name, Actor creator, Gui
         /// </summary>
         internal virtual void SendEvent(ActorId targetId, Event e, Actor sender, Guid opGroupId)
         {
+            e.Sender = sender.ToString();
+            e.Receiver = targetId.ToString();
             var enqueueStatus = EnqueueEvent(targetId, e, sender, opGroupId, out var target);
             if (enqueueStatus is EnqueueStatus.EventHandlerNotRunning)
             {

Src/PChecker/CheckerCore/Actors/Events/Event.cs

@@ -12,5 +12,9 @@ namespace PChecker.Actors.Events
     public abstract class Event
     {
         public int Loc { get; set; }
+        public string? Sender;
+        public string? Receiver;
+        public string? State;
+        public int Index;
     }
 }

Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogBase.cs

@@ -0,0 +1,124 @@
+using System;
+using PChecker.Actors.Events;
+
+namespace PChecker.Actors.Logging;
+
+internal abstract class ActorRuntimeLogBase : IActorRuntimeLog
+{
+    public virtual void OnCreateActor(ActorId id, string creatorName, string creatorType)
+    {
+    }
+
+    public virtual void OnCreateStateMachine(ActorId id, string creatorName, string creatorType)
+    {
+    }
+
+    public virtual void OnExecuteAction(ActorId id, string handlingStateName, string currentStateName,
+        string actionName)
+    {
+    }
+
+    public virtual void OnSendEvent(ActorId targetActorId, string senderName, string senderType, string senderStateName,
+        Event e,
+        Guid opGroupId, bool isTargetHalted)
+    {
+    }
+
+    public virtual void OnRaiseEvent(ActorId id, string stateName, Event e)
+    {
+    }
+
+    public virtual void OnEnqueueEvent(ActorId id, Event e)
+    {
+    }
+
+    public virtual void OnDequeueEvent(ActorId id, string stateName, Event e)
+    {
+    }
+
+    public virtual void OnReceiveEvent(ActorId id, string stateName, Event e, bool wasBlocked)
+    {
+    }
+
+    public virtual void OnWaitEvent(ActorId id, string stateName, Type eventType)
+    {
+    }
+
+    public virtual void OnWaitEvent(ActorId id, string stateName, params Type[] eventTypes)
+    {
+    }
+
+    public virtual void OnStateTransition(ActorId id, string stateName, bool isEntry)
+    {
+    }
+
+    public virtual void OnGotoState(ActorId id, string currentStateName, string newStateName)
+    {
+    }
+
+    public virtual void OnDefaultEventHandler(ActorId id, string stateName)
+    {
+    }
+
+    public virtual void OnHalt(ActorId id, int inboxSize)
+    {
+    }
+
+    public virtual void OnHandleRaisedEvent(ActorId id, string stateName, Event e)
+    {
+    }
+
+    public virtual void OnPopStateUnhandledEvent(ActorId id, string stateName, Event e)
+    {
+    }
+
+    public virtual void OnExceptionThrown(ActorId id, string stateName, string actionName, Exception ex)
+    {
+    }
+
+    public virtual void OnExceptionHandled(ActorId id, string stateName, string actionName, Exception ex)
+    {
+    }
+
+    public virtual void OnCreateMonitor(string monitorType)
+    {
+    }
+
+    public virtual void OnMonitorExecuteAction(string monitorType, string stateName, string actionName)
+    {
+    }
+
+    public virtual void OnMonitorProcessEvent(string monitorType, string stateName, string senderName,
+        string senderType,
+        string senderStateName, Event e)
+    {
+    }
+
+    public virtual void OnMonitorRaiseEvent(string monitorType, string stateName, Event e)
+    {
+    }
+
+    public virtual void OnMonitorStateTransition(string monitorType, string stateName, bool isEntry, bool? isInHotState)
+    {
+    }
+
+    public virtual void OnMonitorError(string monitorType, string stateName, bool? isInHotState)
+    {
+    }
+
+    public virtual void OnRandom(object result, string callerName, string callerType)
+    {
+    }
+
+    public virtual void OnAssertionFailure(string error)
+    {
+    }
+
+    public virtual void OnStrategyDescription(string strategyName, string description)
+    {
+    }
+
+    public virtual void OnCompleted()
+    {
+    }
+}

Src/PChecker/CheckerCore/CheckerConfiguration.cs

@@ -292,36 +292,18 @@ public int MaxSchedulingSteps
         [DataMember]
         public string JvmArgs;
 
-        /// <summary>
-        /// For feedback strategy, save input if the pattern are partially matched.
-        /// </summary>
-        [DataMember]
-        public bool SavePartialMatch;
-
         /// <summary>
         /// For feedback strategy, discard saved generators if the size of the buffer is greater than N.
         /// </summary>
         [DataMember]
         public int DiscardAfter;
 
         /// <summary>
-        /// For feedback strategy, schedule generator mutations based on diversity.
+        /// For QL strategy, schedule generator mutations based on diversity.
         /// </summary>
         [DataMember]
         public bool DiversityBasedPriority;
 
-        /// <summary>
-        /// For feedback strategy, ignore the pattern feedback.
-        /// </summary>
-        [DataMember]
-        public bool IgnorePatternFeedback;
-
-        /// <summary>
-        /// For feedback strategy, use priority based sampling.
-        /// </summary>
-        [DataMember]
-        public bool PriorityBasedSampling;
-
         /// <summary>
         /// Enable conflict analysis for scheduling optimization.
         /// </summary>
@@ -373,11 +355,8 @@ protected CheckerConfiguration()
 
             EnableColoredConsoleOutput = false;
             DisableEnvironmentExit = true;
-            SavePartialMatch = true;
             DiscardAfter = 100;
             DiversityBasedPriority = true;
-            IgnorePatternFeedback = false;
-            PriorityBasedSampling = true;
             EnableConflictAnalysis = false;
 
             PSymArgs = "";