diff --git a/Src/PChecker/CheckerCore/Runtime/Events/EventInfo.cs b/Src/PChecker/CheckerCore/Runtime/Events/EventInfo.cs
index a4de78098..993ab9dae 100644
--- a/Src/PChecker/CheckerCore/Runtime/Events/EventInfo.cs
+++ b/Src/PChecker/CheckerCore/Runtime/Events/EventInfo.cs
@@ -23,6 +23,8 @@ internal class EventInfo
[DataMember]
internal EventOriginInfo OriginInfo { get; private set; }
+ internal VectorTime VectorTime;
+
///
/// Initializes a new instance of the class.
///
@@ -34,10 +36,11 @@ internal EventInfo(Event e)
///
/// Initializes a new instance of the class.
///
- internal EventInfo(Event e, EventOriginInfo originInfo)
+ internal EventInfo(Event e, EventOriginInfo originInfo, VectorTime v)
: this(e)
{
OriginInfo = originInfo;
+ VectorTime = new VectorTime(v);
}
}
}
\ No newline at end of file
diff --git a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventQueue.cs b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventQueue.cs
index 7db5bb744..569c08243 100644
--- a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventQueue.cs
+++ b/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));
}
///
@@ -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);
}
diff --git a/Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs b/Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs
index 0c2ae5701..6f6019b44 100644
--- a/Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs
+++ b/Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs
@@ -54,6 +54,11 @@ public abstract class StateMachine
///
private protected IEventQueue Inbox;
+ ///
+ /// Keeps track of state machine's current vector time.
+ ///
+ public VectorTime VectorTime;
+
///
/// Cache of state machine types to a map of action names to action declarations.
///
@@ -295,6 +300,7 @@ internal void Configure(ControlledRuntime runtime, StateMachineId id, IStateMach
Id = id;
Manager = manager;
Inbox = inbox;
+ VectorTime = new VectorTime(Id);
}
///
@@ -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.
diff --git a/Src/PChecker/CheckerCore/Runtime/VectorTime.cs b/Src/PChecker/CheckerCore/Runtime/VectorTime.cs
new file mode 100644
index 000000000..02359e892
--- /dev/null
+++ b/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 Clock { get; private set; }
+
+ // The ID of the current state machine
+
+ private StateMachineId stateMachineId;
+
+ public VectorTime(StateMachineId stateMachineId)
+ {
+ this.stateMachineId = stateMachineId;
+ Clock = new Dictionary();
+ 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(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();
+ 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;
+ }
+}
\ No newline at end of file
diff --git a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs
index 23327d0a8..1c6b81445 100644
--- a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs
+++ b/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);
diff --git a/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/BehavioralObserver.cs b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/BehavioralObserver.cs
new file mode 100644
index 000000000..35a3353d0
--- /dev/null
+++ b/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 AllTimeline = new List();
+ 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> hashFunctions; // List of hash functions
+
+ public MinHash(int numHashFunctions)
+ {
+ this.numHashFunctions = numHashFunctions;
+ this.hashFunctions = new List>();
+
+ 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;
+ }
+}
+
diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs
index d0bfe9974..da7952ce7 100644
--- a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs
+++ b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs
@@ -542,6 +542,7 @@ private void RegisterObservers(ControlledRuntime runtime)
///
private void RunNextIteration(int schedule)
{
+ BehavioralObserver.NextIter();
if (!IsReplayModeEnabled && ShouldPrintIteration(schedule + 1))
{
Logger.WriteLine($"..... Schedule #{schedule + 1}");