Add feedback-guided scheduling algorithms (#791)

* Add feedback strategy. (#715)

* Add feedback guided scheduling algorithms.

* Fix tests.

* Add location information to events.

* fix change.

* 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]>

* PR cleanup (#723)

* Added support for generating a warning when spec handles an event but does not add it in its observes list (#716)

* Create custom converter for JSON serialization in .NET8 (#717)

* Create custom converter for JSON serialization in .NET8

* Add check for different dictionary type for null replacement

---------

Co-authored-by: Eric Hua <[email protected]>

---------

Co-authored-by: Ankush Desai <[email protected]>
Co-authored-by: Eric Hua <[email protected]>
Co-authored-by: Eric Hua <[email protected]>

* Merge Recent Bug Fixes (#778)

* Added support for generating a warning when spec handles an event but does not add it in its observes list (#716)

* Create custom converter for JSON serialization in .NET8 (#717)

* Create custom converter for JSON serialization in .NET8

* Add check for different dictionary type for null replacement

---------

Co-authored-by: Eric Hua <[email protected]>

* udpate.

* update.

* update.

---------

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

* Fix feedback strategy and remove experiment features.

* Removing Pattern (#786)

Co-authored-by: Christine Zhou <[email protected]>

* Remove conflict analysis

* Removing compiler changes (#789)

Co-authored-by: Christine Zhou <[email protected]>

* Cleanup.

* Revert changes to Event.

* Revert changes.

* Fix merge conflicts.

* Remove temp file.

* Rename LastSentReceiver to MessageReceiver

* Simplify scheduler implementation.

* Revert changes in QLearning strategy.

* Refactor.

* Added VectorTime and BehavioralObserver class for feedback strategy (#799)

Co-authored-by: Christine Zhou <[email protected]>

* Revert changes in PCTStrategy.

* Revert changes in Probabilistic folder.

* revert change.

---------

Co-authored-by: Ankush Desai <[email protected]>
Co-authored-by: ChristineZh0u <[email protected]>
Co-authored-by: Christine Zhou <[email protected]>

Author: 4 people

Src/PChecker/CheckerCore/Coverage/CoverageInfo.cs

@@ -54,6 +54,8 @@ public CoverageInfo()
             Machines = new HashSet<string>();
             MachinesToStates = new Dictionary<string, HashSet<string>>();
             RegisteredEvents = new Dictionary<string, HashSet<string>>();
+            EventInfo = new EventCoverage();
+            CoverageGraph = new Graph();
         }
 
         /// <summary>

Src/PChecker/CheckerCore/Random/IRandomValueGenerator.cs

@@ -1,6 +1,8 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
+using System;
+
 namespace PChecker.Random
 {
     /// <summary>

Src/PChecker/CheckerCore/Runtime/Events/EventInfo.cs

@@ -23,6 +23,8 @@ internal class EventInfo
         [DataMember]
         internal EventOriginInfo OriginInfo { get; private set; }
 
+        internal VectorTime VectorTime;
+
         /// <summary>
         /// Initializes a new instance of the <see cref="EventInfo"/> class.
         /// </summary>
@@ -34,10 +36,11 @@ internal EventInfo(Event e)
         /// <summary>
         /// Initializes a new instance of the <see cref="EventInfo"/> class.
         /// </summary>
-        internal EventInfo(Event e, EventOriginInfo originInfo)
+        internal EventInfo(Event e, EventOriginInfo originInfo, VectorTime v)
             : this(e)
         {
             OriginInfo = originInfo;
+            VectorTime = new VectorTime(v);
         }
     }
 }

Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventQueue.cs

@@ -157,7 +157,7 @@ public EnqueueStatus Enqueue(Event e, EventInfo info)
             // A default event handler exists.
             var stateName = StateMachine.CurrentState.GetType().Name;
             var eventOrigin = new EventOriginInfo(StateMachine.Id, StateMachine.GetType().FullName, stateName);
-            return (DequeueStatus.Default, DefaultEvent.Instance, new EventInfo(DefaultEvent.Instance, eventOrigin));
+            return (DequeueStatus.Default, DefaultEvent.Instance, new EventInfo(DefaultEvent.Instance, eventOrigin, StateMachine.VectorTime));
         }
 
         /// <summary>
@@ -209,7 +209,7 @@ public void RaiseEvent(Event e)
         {
             var stateName = StateMachine.CurrentState.GetType().Name;
             var eventOrigin = new EventOriginInfo(StateMachine.Id, StateMachine.GetType().FullName, stateName);
-            var info = new EventInfo(e, eventOrigin);
+            var info = new EventInfo(e, eventOrigin, StateMachine.VectorTime);
             RaisedEvent = (e, info);
             StateMachineManager.OnRaiseEvent(e, info);
         }

Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs

@@ -54,6 +54,11 @@ public abstract class StateMachine
         /// </summary>
         private protected IEventQueue Inbox;
 
+        /// <summary>
+        /// Keeps track of state machine's current vector time.
+        /// </summary>
+        public VectorTime VectorTime;
+        
         /// <summary>
         /// Cache of state machine types to a map of action names to action declarations.
         /// </summary>
@@ -295,6 +300,7 @@ internal void Configure(ControlledRuntime runtime, StateMachineId id, IStateMach
             Id = id;
             Manager = manager;
             Inbox = inbox;
+            VectorTime = new VectorTime(Id);
         }
 
         /// <summary>
@@ -535,6 +541,9 @@ public void SendEvent(PMachineValue target, Event ev)
             Assert(target.Permissions.Contains(ev.GetType().Name),
                 $"Event {ev.GetType().Name} is not in the permissions set of the target machine");
             AnnounceInternal(ev);
+            // Update vector clock
+            VectorTime.Increment();
+            BehavioralObserver.AddToCurrentTimeline(ev, BehavioralObserver.EventType.SEND, VectorTime);
             Runtime.SendEvent(target.Id, ev, this);
         }
 
@@ -590,6 +599,10 @@ internal async Task RunEventHandlerAsync()
 
                 if (status is DequeueStatus.Success)
                 {
+                    // Update state machine vector clock
+                    VectorTime.Merge(info.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
                     // has to schedule an state machine when a new operation is dequeued.

Src/PChecker/CheckerCore/Runtime/VectorTime.cs

@@ -0,0 +1,124 @@
+using System;
+using System.Collections.Generic;
+using System.IO;
+using System.Linq;
+using PChecker.Runtime.StateMachines;
+using PChecker.IO.Logging;
+
+public class VectorTime
+{
+    // Dictionary that uses StateMachineId as the key and stores the logical clock as the value
+    public Dictionary<StateMachineId, int> Clock { get; private set; }
+
+    // The ID of the current state machine
+    
+    private StateMachineId stateMachineId;
+
+    public VectorTime(StateMachineId stateMachineId)
+    {
+        this.stateMachineId = stateMachineId;
+        Clock = new Dictionary<StateMachineId, int>();
+        Clock[stateMachineId] = 0;  // Initialize the clock for this state machine
+    }
+    
+    // Clone constructor (creates a snapshot of the vector clock)
+    public VectorTime(VectorTime other)
+    {
+        Clock = new Dictionary<StateMachineId, int>(other.Clock);
+    }
+
+    // Increment the logical clock for this state machine
+    public void Increment()
+    {
+        Clock[stateMachineId]++;
+    }
+
+    // Merge another vector clock into this one
+    public void Merge(VectorTime otherTime)
+    {
+        foreach (var entry in otherTime.Clock)
+        {
+            StateMachineId otherMachineId = entry.Key;
+            int otherTimestamp = entry.Value;
+
+            if (Clock.ContainsKey(otherMachineId))
+            {
+                // Take the maximum timestamp for each state machine
+                Clock[otherMachineId] = Math.Max(Clock[otherMachineId], otherTimestamp);
+            }
+            else
+            {
+                // Add the state machine's timestamp if it doesn't exist in this time
+                Clock[otherMachineId] = otherTimestamp;
+            }
+        }
+    }
+    
+    // Compare this vector clock to another for sorting purposes
+    // Rturn value: -1 = This vector clock happens after the other, 1 = This vector clock happens before the other,
+    // 0 = Clocks are equal or concurrent
+    public int CompareTo(VectorTime other)
+    {
+        bool atLeastOneLess = false;
+        bool atLeastOneGreater = false;
+
+        foreach (var machineId in Clock.Keys)
+        {
+            int thisTime = Clock[machineId];
+            int otherTime = other.Clock.ContainsKey(machineId) ? other.Clock[machineId] : 0;
+
+            if (thisTime < otherTime)
+            {
+                atLeastOneLess = true;
+            }
+            else if (thisTime > otherTime)
+            {
+                atLeastOneGreater = true;
+            }
+            if (atLeastOneLess && atLeastOneGreater)
+            {
+                return 0;
+            }
+        }
+        if (atLeastOneLess && !atLeastOneGreater)
+        {
+            return -1;
+        }
+        if (atLeastOneGreater && !atLeastOneLess)
+        {
+            return 1;
+        }
+        return 0;
+    }
+
+    
+    public override string ToString()
+    {
+        var elements = new List<string>();
+        foreach (var entry in Clock)
+        {
+            elements.Add($"StateMachine {entry.Key.Name}: {entry.Value}");
+        }
+        return $"[{string.Join(", ", elements)}]";
+    }
+    
+    public override bool Equals(object obj)
+    {
+        if (obj is VectorTime other)
+        {
+            return Clock.OrderBy(x => x.Key).SequenceEqual(other.Clock.OrderBy(x => x.Key));
+        }
+        return false;
+    }
+
+    public override int GetHashCode()
+    {
+        int hash = 17;
+        foreach (var entry in Clock)
+        {
+            hash = hash * 31 + entry.Key.GetHashCode();
+            hash = hash * 31 + entry.Value.GetHashCode();
+        }
+        return hash;
+    }
+}

Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs

@@ -14,6 +14,7 @@
 using System.Threading.Tasks;
 using PChecker.Coverage;
 using PChecker.Exceptions;
+using PChecker.Feedback;
 using PChecker.Random;
 using PChecker.Runtime.Events;
 using PChecker.Runtime.Logging;
@@ -150,7 +151,6 @@ private static ControlledRuntime CreateWithConfiguration(CheckerConfiguration ch
         /// </summary>
         public JsonWriter JsonLogger => LogWriter.JsonLogger;
 
-
         /// <summary>
         /// Returns the current hashed state of the monitors.
         /// </summary>
@@ -618,6 +618,8 @@ private EnqueueStatus EnqueueEvent(StateMachineId targetId, Event e, StateMachin
                 "Cannot send event '{0}' to state machine id '{1}' that is not bound to an state machine instance.",
                 e.GetType().FullName, targetId.Value);
 
+            Scheduler.ScheduledOperation.MessageReceiver = targetId.ToString();
+
             Scheduler.ScheduleNextEnabledOperation(AsyncOperationType.Send);
             ResetProgramCounter(sender);
 
@@ -647,7 +649,7 @@ private EnqueueStatus EnqueueEvent(StateMachine stateMachine, Event e, StateMach
             var originInfo = new EventOriginInfo(sender.Id, sender.GetType().FullName,
                 sender.CurrentState.GetType().Name);
 
-            var eventInfo = new EventInfo(e, originInfo);
+            var eventInfo = new EventInfo(e, originInfo, sender.VectorTime);
 
             LogWriter.LogSendEvent(stateMachine.Id, sender.Id.Name, sender.Id.Type, sender.CurrentStateName,
                 e, isTargetHalted: false);

Src/PChecker/CheckerCore/SystematicTesting/Operations/AsyncOperation.cs

@@ -49,6 +49,11 @@ internal abstract class AsyncOperation : IAsyncOperation
         /// True if the next awaiter is controlled, else false.
         /// </summary>
         internal bool IsAwaiterControlled;
+        
+        /// <summary>
+        /// The receiver if the operation is Send.
+        /// </summary>
+        public string MessageReceiver = "";
 
         /// <summary>
         /// Initializes a new instance of the <see cref="AsyncOperation"/> class.