Added VectorTime and BehavioralObserver class for feedback strategy (#…

…799)

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

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

@@ -649,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/Strategies/Feedback/Coverage/BehavioralObserver.cs

@@ -0,0 +1,166 @@
+using System;
+using System.Collections.Generic;
+using System.IO;
+using PChecker.IO.Logging;
+using PChecker.Runtime.Events;
+
+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[]>();
+    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);  
+
+
+    public enum EventType
+    {
+        SEND, DEQUEUE
+    }
+
+    public BehavioralObserver()
+    {
+        CurrTimeline = new HashSet<(VectorTime, Event, EventType)>();
+    }
+
+    public static void AddToCurrentTimeline(Event e, EventType t, VectorTime vectorTime)
+    {
+        CurrTimeline.Add((new VectorTime(vectorTime), e, t));
+    }
+
+    public static int CalculateDiff(int[] currentSignature, int[] otherSignature)
+    {
+        double similarity = minHash.ComputeSimilarity(currentSignature, otherSignature);
+        double differenceScore = 1 - similarity;
+        return (int)(differenceScore * 100);  // Scale the difference score (e.g., multiply by 100)
+    }
+
+    public static int GetUniqueScore(int[] currentSignature)
+    {
+        int scoreSum = 0;
+        foreach (var otherSignature in AllTimeline)
+        {
+            int score = CalculateDiff(currentSignature, otherSignature);
+            if (score == 0)
+            {
+                return 0;
+            }
+            scoreSum += score;
+        }
+        return scoreSum/AllTimeline.Count;
+    }
+
+    public static void PrintTimeline(List<(VectorTime, Event, EventType)> timeline)
+    {
+        Logger.WriteLine("Global state of all machines:");
+        foreach (var entry in timeline)
+        {
+            Logger.WriteLine($"Machine {entry}");
+        }
+    }
+
+    public static List<(VectorTime, Event, EventType)> SortByVectorClock()
+    {
+        List<(VectorTime, Event, EventType)> sortedTimeline = new List<(VectorTime, Event, EventType)>(CurrTimeline);
+
+        // 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));
+
+        return sortedTimeline;
+    }
+
+    public static void NextIter()
+    {
+        if (CurrTimeline.Count == 0)
+        {
+            return;
+        }
+        List<(VectorTime, Event, EventType)> SortedCurrTimeline = SortByVectorClock();
+        int[] currSignature = minHash.ComputeMinHashSignature(SortedCurrTimeline);
+        if (AllTimeline.Count == 0)
+        {
+            AllTimeline.Add(currSignature);
+            return;
+        }
+        int uniqueScore = GetUniqueScore(currSignature);
+        Logger.WriteLine($"----**** UniquenessScore: {uniqueScore}");
+        if (uniqueScore != 0)
+        {
+            AllTimeline.Add(currSignature);
+        }
+        CurrTimeline = new HashSet<(VectorTime, Event, EventType)>();
+    }
+}
+
+public class MinHash
+{
+    private int numHashFunctions;  // Number of hash functions to use
+    private List<Func<int, int>> hashFunctions;  // List of hash functions
+
+    public MinHash(int numHashFunctions)
+    {
+        this.numHashFunctions = numHashFunctions;
+        this.hashFunctions = new List<Func<int, int>>();
+
+        System.Random rand = new System.Random();
+        for (int i = 0; i < numHashFunctions; i++)
+        {
+            int a = rand.Next();
+            int b = rand.Next();
+            hashFunctions.Add(x => a * x + b); 
+        }
+    }
+
+    // Create a MinHash signature for a given set
+    public int[] ComputeMinHashSignature(List<(VectorTime, Event, BehavioralObserver.EventType)> set)
+    {
+        int[] signature = new int[numHashFunctions];
+
+        for (int i = 0; i < numHashFunctions; i++)
+        {
+            signature[i] = int.MaxValue;
+        }
+        foreach (var element in set)
+        {
+            int elementHash = ComputeElementHash(element);
+
+            for (int i = 0; i < numHashFunctions; i++)
+            {
+                int hashedValue = hashFunctions[i](elementHash);
+                if (hashedValue < signature[i])
+                {
+                    signature[i] = hashedValue;
+                }
+            }
+        }
+        return signature;
+    }
+
+    // Compute a composite hash for the (VectorTime, Event, EventType) tuple
+    private int ComputeElementHash((VectorTime, Event, BehavioralObserver.EventType) element)
+    {
+        int hash1 = element.Item1.GetHashCode();
+        int hash2 = element.Item2.GetHashCode();
+        int hash3 = element.Item3.GetHashCode();
+        return hash1 ^ hash2 ^ hash3;
+    }
+
+    // Compute Jaccard similarity based on MinHash signatures
+    public double ComputeSimilarity(int[] signature1, int[] signature2)
+    {
+        int identicalMinHashes = 0;
+
+        for (int i = 0; i < numHashFunctions; i++)
+        {
+            if (signature1[i] == signature2[i])
+            {
+                identicalMinHashes++;
+            }
+        }
+        return (double)identicalMinHashes / numHashFunctions;
+    }
+}
+

Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs

@@ -542,6 +542,7 @@ private void RegisterObservers(ControlledRuntime runtime)
         /// </summary>
         private void RunNextIteration(int schedule)
         {
+            BehavioralObserver.NextIter();
             if (!IsReplayModeEnabled && ShouldPrintIteration(schedule + 1))
             {
                 Logger.WriteLine($"..... Schedule #{schedule + 1}");