diff --git a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventBag.cs b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventBag.cs
new file mode 100644
index 0000000000..957a205e70
--- /dev/null
+++ b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventBag.cs
@@ -0,0 +1,320 @@
+using System;
+using System.Collections.Generic;
+using System.Threading.Tasks;
+using PChecker.Runtime.Events;
+using PChecker.Runtime.StateMachines.Managers;
+
+
+namespace PChecker.Runtime.StateMachines.EventQueues;
+
+/// <summary>
+/// Implements a bag of events that is used during testing.
+/// </summary>
+internal sealed class EventBag : IEventQueue
+{
+    /// <summary>
+    /// Manages the state machine that owns this queue.
+    /// </summary>
+    private readonly IStateMachineManager StateMachineManager;
+
+    /// <summary>
+    /// The state machine that owns this queue.
+    /// </summary>
+    private readonly StateMachine StateMachine;
+
+    /// <summary>
+    /// The internal queue that contains events with their metadata.
+    /// </summary>
+    private readonly List<(Event e, EventInfo info)> Bag;
+
+    /// <summary>
+    /// The raised event and its metadata, or null if no event has been raised.
+    /// </summary>
+    private (Event e, EventInfo info) RaisedEvent;
+
+    /// <summary>
+    /// Map from the types of events that the owner of the queue is waiting to receive
+    /// to an optional predicate. If an event of one of these types is enqueued, then
+    /// if there is no predicate, or if there is a predicate and evaluates to true, then
+    /// the event is received, else the event is deferred.
+    /// </summary>
+    private Dictionary<Type, Func<Event, bool>> EventWaitTypes;
+
+    /// <summary>
+    /// Task completion source that contains the event obtained using an explicit receive.
+    /// </summary>
+    private TaskCompletionSource<Event> ReceiveCompletionSource;
+
+    /// <summary>
+    /// Checks if the queue is accepting new events.
+    /// </summary>
+    private bool IsClosed;
+
+    /// <summary>
+    /// The size of the queue.
+    /// </summary>
+    public int Size => Bag.Count;
+
+    /// <summary>
+    /// Checks if an event has been raised.
+    /// </summary>
+    public bool IsEventRaised => RaisedEvent != default;
+    
+    /// <summary>
+    /// Initializes a new instance of the <see cref="EventBag"/> class.
+    /// </summary>
+    internal EventBag(IStateMachineManager stateMachineManager, StateMachine stateMachine)
+    {
+        StateMachineManager = stateMachineManager;
+        StateMachine = stateMachine;
+        Bag = new List<(Event, EventInfo)>();
+        EventWaitTypes = new Dictionary<Type, Func<Event, bool>>();
+        IsClosed = false;
+    }
+    
+    /// <inheritdoc/>
+    public EnqueueStatus Enqueue(Event e, EventInfo info)
+    {
+        if (IsClosed)
+        {
+            return EnqueueStatus.Dropped;
+        }
+
+        if (EventWaitTypes.TryGetValue(e.GetType(), out var predicate) &&
+            (predicate is null || predicate(e)))
+        {
+            EventWaitTypes.Clear();
+            StateMachineManager.OnReceiveEvent(e, info);
+            ReceiveCompletionSource.SetResult(e);
+            return EnqueueStatus.EventHandlerRunning;
+        }
+
+        StateMachineManager.OnEnqueueEvent(e, info);
+        Bag.Add((e, info));
+
+        if (!StateMachineManager.IsEventHandlerRunning)
+        {
+            if (TryDequeueEvent(true).e is null)
+            {
+                return EnqueueStatus.NextEventUnavailable;
+            }
+            else
+            {
+                StateMachineManager.IsEventHandlerRunning = true;
+                return EnqueueStatus.EventHandlerNotRunning;
+            }
+        }
+
+        return EnqueueStatus.EventHandlerRunning;
+    }
+    
+    /// <inheritdoc/>
+        public (DequeueStatus status, Event e, EventInfo info) Dequeue()
+        {
+            // Try to get the raised event, if there is one. Raised events
+            // have priority over the events in the inbox.
+            if (RaisedEvent != default)
+            {
+                if (StateMachineManager.IsEventIgnored(RaisedEvent.e, RaisedEvent.info))
+                {
+                    // TODO: should the user be able to raise an ignored event?
+                    // The raised event is ignored in the current state.
+                    RaisedEvent = default;
+                }
+                else
+                {
+                    var raisedEvent = RaisedEvent;
+                    RaisedEvent = default;
+                    return (DequeueStatus.Raised, raisedEvent.e, raisedEvent.info);
+                }
+            }
+
+            var hasDefaultHandler = StateMachineManager.IsDefaultHandlerAvailable();
+            if (hasDefaultHandler)
+            {
+                StateMachine.Runtime.NotifyDefaultEventHandlerCheck(StateMachine);
+            }
+
+            // Try to dequeue the next event, if there is one.
+            var (e, info) = TryDequeueEvent();
+            if (e != null)
+            {
+                // Found next event that can be dequeued.
+                return (DequeueStatus.Success, e, info);
+            }
+
+            // No event can be dequeued, so check if there is a default event handler.
+            if (!hasDefaultHandler)
+            {
+                // There is no default event handler installed, so do not return an event.
+                StateMachineManager.IsEventHandlerRunning = false;
+                return (DequeueStatus.NotAvailable, null, null);
+            }
+
+            // TODO: check op-id of default event.
+            // 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, StateMachine.VectorTime));
+        }
+        
+    /// <summary>
+    /// Dequeues the next event and its metadata, if there is one available, else returns null.
+    /// </summary>
+    private (Event e, EventInfo info) TryDequeueEvent(bool checkOnly = false)
+    {
+        (Event e, EventInfo info) availableEvent = default;
+        List<(Event, EventInfo)> deferredEvents = new List<(Event, EventInfo)>();
+
+        // Iterates through the events and metadata in the inbox.
+        while (availableEvent == default)
+        {
+            if (Bag.Count == 0)
+            {
+                break;
+            }
+            var index = StateMachine.RandomInteger(Bag.Count);
+            availableEvent = Bag[index];
+
+            if (StateMachineManager.IsEventIgnored(availableEvent.e, availableEvent.info))
+            {
+                if (!checkOnly)
+                {
+                    // Removes an ignored event.
+                    Bag.Remove(availableEvent);
+                    availableEvent = default;
+                }
+
+                continue;
+            }
+
+            // Skips a deferred event.
+            if (StateMachineManager.IsEventDeferred(availableEvent.Item1, availableEvent.Item2))
+            {
+                Bag.Remove(availableEvent);
+                deferredEvents.Add(availableEvent);
+                availableEvent = default;
+            }
+        }
+        
+        Bag.AddRange(deferredEvents);
+        if (!checkOnly)
+        {
+            Bag.Remove(availableEvent);
+        }
+
+        return availableEvent;
+    }
+    
+    /// <inheritdoc/>
+    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, StateMachine.VectorTime);
+        RaisedEvent = (e, info);
+        StateMachineManager.OnRaiseEvent(e, info);
+    }
+
+    /// <inheritdoc/>
+    public Task<Event> ReceiveEventAsync(Type eventType, Func<Event, bool> predicate = null)
+    {
+        var eventWaitTypes = new Dictionary<Type, Func<Event, bool>>
+        {
+            { eventType, predicate }
+        };
+
+        return ReceiveEventAsync(eventWaitTypes);
+    }
+
+    /// <inheritdoc/>
+    public Task<Event> ReceiveEventAsync(params Type[] eventTypes)
+    {
+        var eventWaitTypes = new Dictionary<Type, Func<Event, bool>>();
+        foreach (var type in eventTypes)
+        {
+            eventWaitTypes.Add(type, null);
+        }
+
+        return ReceiveEventAsync(eventWaitTypes);
+    }
+    
+    /// <inheritdoc/>
+    public Task<Event> ReceiveEventAsync(params Tuple<Type, Func<Event, bool>>[] events)
+    {
+        var eventWaitTypes = new Dictionary<Type, Func<Event, bool>>();
+        foreach (var e in events)
+        {
+            eventWaitTypes.Add(e.Item1, e.Item2);
+        }
+
+        return ReceiveEventAsync(eventWaitTypes);
+    }
+    
+    /// <summary>
+    /// Waits for an event to be enqueued.
+    /// </summary>
+    private Task<Event> ReceiveEventAsync(Dictionary<Type, Func<Event, bool>> eventWaitTypes)
+    {
+        StateMachine.Runtime.NotifyReceiveCalled(StateMachine);
+
+        (Event e, EventInfo info) receivedEvent = default;
+        int index = 0;
+        while (index < Bag.Count)
+        {
+            receivedEvent = Bag[index];
+            // Dequeue the first event that the caller waits to receive, if there is one in the queue.
+            if (eventWaitTypes.TryGetValue(receivedEvent.e.GetType(), out var predicate) &&
+                (predicate is null || predicate(receivedEvent.e)))
+            {
+                Bag.Remove(receivedEvent);
+                break;
+            }
+
+            index++;
+        }
+
+        if (receivedEvent == default)
+        {
+            ReceiveCompletionSource = new TaskCompletionSource<Event>();
+            EventWaitTypes = eventWaitTypes;
+            StateMachineManager.OnWaitEvent(EventWaitTypes.Keys);
+            return ReceiveCompletionSource.Task;
+        }
+
+        StateMachineManager.OnReceiveEventWithoutWaiting(receivedEvent.e, receivedEvent.info);
+        return Task.FromResult(receivedEvent.e);
+    }
+    
+    /// <inheritdoc/>
+    public void Close()
+    {
+        IsClosed = true;
+    }
+    
+    /// <summary>
+    /// Disposes the queue resources.
+    /// </summary>
+    private void Dispose(bool disposing)
+    {
+        if (!disposing)
+        {
+            return;
+        }
+
+        foreach (var (e, info) in Bag)
+        {
+            StateMachineManager.OnDropEvent(e, info);
+        }
+
+        Bag.Clear();
+    }
+
+    /// <inheritdoc/>
+    public void Dispose()
+    {
+        Dispose(true);
+        GC.SuppressFinalize(this);
+    }
+    
+}
\ No newline at end of file
diff --git a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventChannel.cs b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventChannel.cs
new file mode 100644
index 0000000000..9b9b1560ef
--- /dev/null
+++ b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventChannel.cs
@@ -0,0 +1,332 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System;
+using System.Collections.Generic;
+using System.Threading.Tasks;
+using PChecker.Runtime.Events;
+using PChecker.Runtime.StateMachines.Managers;
+
+namespace PChecker.Runtime.StateMachines.EventQueues
+{
+    /// <summary>
+    /// Implements a queue of events that is used during testing.
+    /// </summary>
+    internal sealed class EventChannel : IEventQueue
+    {
+        /// <summary>
+        /// Manages the state machine that owns this queue.
+        /// </summary>
+        private readonly IStateMachineManager StateMachineManager;
+
+        /// <summary>
+        /// The state machine that owns this queue.
+        /// </summary>
+        private readonly StateMachine StateMachine;
+
+        /// <summary>
+        /// The internal queue that contains events with their metadata.
+        /// </summary>
+        private readonly Dictionary<string, LinkedList<(Event e, EventInfo info)>> Map;
+        
+        
+        /// <summary>
+        /// The list of event sender state machines.
+        /// </summary>
+        private List<string> SenderMachineNames;
+        
+        /// <summary>
+        /// The raised event and its metadata, or null if no event has been raised.
+        /// </summary>
+        private (Event e, EventInfo info) RaisedEvent;
+
+        /// <summary>
+        /// Map from the types of events that the owner of the queue is waiting to receive
+        /// to an optional predicate. If an event of one of these types is enqueued, then
+        /// if there is no predicate, or if there is a predicate and evaluates to true, then
+        /// the event is received, else the event is deferred.
+        /// </summary>
+        private Dictionary<Type, Func<Event, bool>> EventWaitTypes;
+
+        /// <summary>
+        /// Checks if the queue is accepting new events.
+        /// </summary>
+        private bool IsClosed;
+
+        /// <summary>
+        /// The size of the queue.
+        /// </summary>
+        public int Size => Map.Count;
+
+        /// <summary>
+        /// Checks if an event has been raised.
+        /// </summary>
+        public bool IsEventRaised => RaisedEvent != default;
+
+        /// <summary>
+        /// Initializes a new instance of the <see cref="EventQueue"/> class.
+        /// </summary>
+        internal EventChannel(IStateMachineManager stateMachineManager, StateMachine stateMachine)
+        {
+            StateMachineManager = stateMachineManager;
+            StateMachine = stateMachine;
+            Map = new Dictionary<string, LinkedList<(Event e, EventInfo info)>>();
+            SenderMachineNames = new List<string>();
+            EventWaitTypes = new Dictionary<Type, Func<Event, bool>>();
+            IsClosed = false;
+        }
+
+        /// <inheritdoc/>
+        public EnqueueStatus Enqueue(Event e, EventInfo info)
+        {
+            if (IsClosed)
+            {
+                return EnqueueStatus.Dropped;
+            }
+
+            if (EventWaitTypes.TryGetValue(e.GetType(), out var predicate) &&
+                (predicate is null || predicate(e)))
+            {
+                EventWaitTypes.Clear();
+                StateMachineManager.OnReceiveEvent(e, info);
+                return EnqueueStatus.EventHandlerRunning;
+            }
+
+            StateMachineManager.OnEnqueueEvent(e, info);
+            string senderStateMachineName = info.OriginInfo.SenderStateMachineId.ToString();
+            if (!Map.ContainsKey(senderStateMachineName))
+            {
+                Map[senderStateMachineName] = new LinkedList<(Event e, EventInfo info)>();
+                SenderMachineNames.Add(senderStateMachineName);
+            }
+            Map[senderStateMachineName].AddLast((e, info));
+            
+            if (!StateMachineManager.IsEventHandlerRunning)
+            {
+                if (TryDequeueEvent(true).e is null)
+                {
+                    return EnqueueStatus.NextEventUnavailable;
+                }
+                else
+                {
+                    StateMachineManager.IsEventHandlerRunning = true;
+                    return EnqueueStatus.EventHandlerNotRunning;
+                }
+            }
+
+            return EnqueueStatus.EventHandlerRunning;
+        }
+
+        /// <inheritdoc/>
+        public (DequeueStatus status, Event e, EventInfo info) Dequeue()
+        {
+            // Try to get the raised event, if there is one. Raised events
+            // have priority over the events in the inbox.
+            if (RaisedEvent != default)
+            {
+                if (StateMachineManager.IsEventIgnored(RaisedEvent.e, RaisedEvent.info))
+                {
+                    // TODO: should the user be able to raise an ignored event?
+                    // The raised event is ignored in the current state.
+                    RaisedEvent = default;
+                }
+                else
+                {
+                    var raisedEvent = RaisedEvent;
+                    RaisedEvent = default;
+                    return (DequeueStatus.Raised, raisedEvent.e, raisedEvent.info);
+                }
+            }
+
+            var hasDefaultHandler = StateMachineManager.IsDefaultHandlerAvailable();
+            if (hasDefaultHandler)
+            {
+                StateMachine.Runtime.NotifyDefaultEventHandlerCheck(StateMachine);
+            }
+
+            // Try to dequeue the next event, if there is one.
+            var (e, info) = TryDequeueEvent();
+            if (e != null)
+            {
+                // Found next event that can be dequeued.
+                return (DequeueStatus.Success, e, info);
+            }
+
+            // No event can be dequeued, so check if there is a default event handler.
+            if (!hasDefaultHandler)
+            {
+                // There is no default event handler installed, so do not return an event.
+                StateMachineManager.IsEventHandlerRunning = false;
+                return (DequeueStatus.NotAvailable, null, null);
+            }
+
+            // TODO: check op-id of default event.
+            // 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, StateMachine.VectorTime));
+        }
+
+        /// <summary>
+        /// Dequeues the next event and its metadata, if there is one available, else returns null.
+        /// </summary>
+        private (Event e, EventInfo info) TryDequeueEvent(bool checkOnly = false)
+        {
+            List<string> temp = [];
+            (Event, EventInfo) nextAvailableEvent = default;
+            while (SenderMachineNames.Count > 0)
+            {
+                var randomIndex = StateMachine.RandomInteger(SenderMachineNames.Count);
+                string stateMachine = SenderMachineNames[randomIndex];
+                SenderMachineNames.RemoveAt(randomIndex);
+                temp.Add(stateMachine);
+                if (Map.TryGetValue(stateMachine, out var eventList) && eventList.Count > 0)
+                {
+                    nextAvailableEvent = TryDequeueEvent(stateMachine, checkOnly);
+                }
+
+                if (nextAvailableEvent != default)
+                {
+                    SenderMachineNames.AddRange(temp);
+                    break;
+                }
+            }
+            SenderMachineNames.AddRange(temp);
+            return nextAvailableEvent;
+        }
+
+        /// <summary>
+        /// Dequeues the next event and its metadata, if there is one available, else returns null.
+        /// </summary>
+        private (Event e, EventInfo info) TryDequeueEvent(string stateMachineName, bool checkOnly = false)
+        {
+            (Event, EventInfo) nextAvailableEvent = default;
+
+            // Iterates through the events and metadata in the inbox.
+            var node = Map[stateMachineName].First;
+            while (node != null)
+            {
+                var nextNode = node.Next;
+                var currentEvent = node.Value;
+
+                if (StateMachineManager.IsEventIgnored(currentEvent.e, currentEvent.info))
+                {
+                    if (!checkOnly)
+                    {
+                        // Removes an ignored event.
+                        Map[stateMachineName].Remove(node);
+                    }
+
+                    node = nextNode;
+                    continue;
+                }
+
+                // Skips a deferred event.
+                if (!StateMachineManager.IsEventDeferred(currentEvent.e, currentEvent.info))
+                {
+                    nextAvailableEvent = currentEvent;
+                    if (!checkOnly)
+                    {
+                        Map[stateMachineName].Remove(node);
+                    }
+
+                    break;
+                }
+
+                node = nextNode;
+            }
+
+            return nextAvailableEvent;
+        }
+
+        /// <inheritdoc/>
+        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, StateMachine.VectorTime);
+            RaisedEvent = (e, info);
+            StateMachineManager.OnRaiseEvent(e, info);
+        }
+
+        /// <inheritdoc/>
+        public Task<Event> ReceiveEventAsync(Type eventType, Func<Event, bool> predicate = null)
+        {
+            var eventWaitTypes = new Dictionary<Type, Func<Event, bool>>
+            {
+                { eventType, predicate }
+            };
+
+            return ReceiveEventAsync(eventWaitTypes);
+        }
+
+        /// <inheritdoc/>
+        public Task<Event> ReceiveEventAsync(params Type[] eventTypes)
+        {
+            var eventWaitTypes = new Dictionary<Type, Func<Event, bool>>();
+            foreach (var type in eventTypes)
+            {
+                eventWaitTypes.Add(type, null);
+            }
+
+            return ReceiveEventAsync(eventWaitTypes);
+        }
+
+        /// <inheritdoc/>
+        public Task<Event> ReceiveEventAsync(params Tuple<Type, Func<Event, bool>>[] events)
+        {
+            var eventWaitTypes = new Dictionary<Type, Func<Event, bool>>();
+            foreach (var e in events)
+            {
+                eventWaitTypes.Add(e.Item1, e.Item2);
+            }
+
+            return ReceiveEventAsync(eventWaitTypes);
+        }
+
+        /// <summary>
+        /// Waits for an event to be enqueued.
+        /// </summary>
+        private Task<Event> ReceiveEventAsync(Dictionary<Type, Func<Event, bool>> eventWaitTypes)
+        {
+            StateMachine.Runtime.NotifyReceiveCalled(StateMachine);
+
+            (Event e, EventInfo info) receivedEvent = default;
+            return Task.FromResult(receivedEvent.e);
+        }
+
+        /// <inheritdoc/>
+        public void Close()
+        {
+            IsClosed = true;
+        }
+
+        /// <summary>
+        /// Disposes the queue resources.
+        /// </summary>
+        private void Dispose(bool disposing)
+        {
+            if (!disposing)
+            {
+                return;
+            }
+
+            foreach (var (_, linkedList) in Map)
+            {
+                foreach (var (e, info) in linkedList)
+                {
+                    StateMachineManager.OnDropEvent(e, info);
+                }
+            }
+
+            Map.Clear();
+        }
+
+        /// <inheritdoc/>
+        public void Dispose()
+        {
+            Dispose(true);
+            GC.SuppressFinalize(this);
+        }
+    }
+}
\ 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 569c082438..2d2dfada83 100644
--- a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventQueue.cs
+++ b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventQueue.cs
@@ -284,21 +284,6 @@ private Task<Event> ReceiveEventAsync(Dictionary<Type, Func<Event, bool>> eventW
             return Task.FromResult(receivedEvent.e);
         }
 
-        /// <inheritdoc/>
-        public int GetCachedState()
-        {
-            unchecked
-            {
-                var hash = 19;
-                foreach (var (_, info) in Queue)
-                {
-                    hash = (hash * 31) + info.EventName.GetHashCode();
-                }
-
-                return hash;
-            }
-        }
-
         /// <inheritdoc/>
         public void Close()
         {
diff --git a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/IEventQueue.cs b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/IEventQueue.cs
index a74b05edf1..948876eaea 100644
--- a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/IEventQueue.cs
+++ b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/IEventQueue.cs
@@ -52,11 +52,6 @@ internal interface IEventQueue : IDisposable
         /// </summary>
         Task<Event> ReceiveEventAsync(params Tuple<Type, Func<Event, bool>>[] events);
 
-        /// <summary>
-        /// Returns the cached state of the queue.
-        /// </summary>
-        int GetCachedState();
-
         /// <summary>
         /// Closes the queue, which stops any further event enqueues.
         /// </summary>
diff --git a/Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs b/Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs
index 6f6019b443..1d5a38e443 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
         /// </summary>
         private protected IEventQueue Inbox;
         
+        /// <summary>
+        /// Event inbox type.
+        /// </summary>
+        public string InboxType;
+        
         /// <summary>
         /// Keeps track of state machine's current vector time.
         /// </summary>
@@ -1381,8 +1386,6 @@ internal int GetHashedState()
 
                 hash = (hash * 31) + Manager.GetCachedState();
                 
-                hash = (hash * 31) + Inbox.GetCachedState();
-
                 return hash;
             }
         }
diff --git a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs
index 3b71228be9..cdd72a68b7 100644
--- a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs
+++ b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs
@@ -269,7 +269,7 @@ internal ControlledRuntime(CheckerConfiguration checkerConfiguration,
         public StateMachineId CreateStateMachineId(Type type, string name = null) => new StateMachineId(type, name, this);
 
         /// <summary>
-        /// Creates an state machine id that is uniquely tied to the specified unique name. The
+        /// Creates a state machine id that is uniquely tied to the specified unique name. The
         /// returned state machine id can either be a fresh id (not yet bound to any state machine), or
         /// it can be bound to a previously created state machine. In the second case, this state machine
         /// id can be directly used to communicate with the corresponding state machine.
@@ -505,7 +505,12 @@ private StateMachine CreateStateMachine(StateMachineId id, Type type, string nam
             var stateMachine = Create(type);
             IStateMachineManager stateMachineManager = new StateMachineManager(this, stateMachine);
 
-            IEventQueue eventQueue = new EventQueue(stateMachineManager, stateMachine);
+            IEventQueue eventQueue = stateMachine.InboxType! switch
+            {
+                "eventbag" => new EventBag(stateMachineManager, stateMachine),
+                "eventchannel" => new EventChannel(stateMachineManager, stateMachine),
+                _ => new EventQueue(stateMachineManager, stateMachine)
+            };
             stateMachine.Configure(this, id, stateMachineManager, eventQueue);
             stateMachine.SetupEventHandlers();
             stateMachine.self = new PMachineValue(id, stateMachine.receives.ToList());
diff --git a/Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerCodeGenerator.cs
index 6bfcef6c6b..e131a59c9b 100644
--- a/Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerCodeGenerator.cs
+++ b/Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerCodeGenerator.cs
@@ -556,6 +556,11 @@ private static void WriteMachineConstructor(CompilationContext context, StringWr
                 context.WriteLine(output, $"this.creates.Add(nameof({context.Names.GetNameForDecl(iCreate)}));");
             }
 
+            if (machine.DequeueOption != null)
+            {
+                context.WriteLine(output, $"this.InboxType=\"{machine.DequeueOption}\";");
+            }
+
             context.WriteLine(output, "}");
             context.WriteLine(output);
         }
diff --git a/Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerNameManager.cs b/Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerNameManager.cs
index 13f69fc296..d49be0dc6d 100644
--- a/Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerNameManager.cs
+++ b/Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerNameManager.cs
@@ -17,7 +17,8 @@ internal class PCheckerNameManager : NameManagerBase
             "case", "default", "lock", "try", "throw", "catch", "finally", "goto", "break", "continue", "return", "public", "private", "internal",
             "protected", "static", "readonly", "sealed", "const", "fixed", "stackalloc", "volatile", "new", "override", "abstract", "virtual",
             "event", "extern", "ref", "out", "in", "is", "as", "params", "__arglist", "__makeref", "__reftype", "__refvalue", "this", "base",
-            "namespace", "using", "class", "struct", "interface", "enum", "delegate", "checked", "unchecked", "unsafe", "operator", "implicit", "explicit"
+            "namespace", "using", "class", "struct", "interface", "enum", "delegate", "checked", "unchecked", "unsafe", "operator", "implicit", "explicit",
+            "eventbag", "eventqueue", "eventchannel"
         };
 
         public PCheckerNameManager(string namePrefix) : base(namePrefix)
diff --git a/Src/PCompiler/CompilerCore/Parser/PLexer.g4 b/Src/PCompiler/CompilerCore/Parser/PLexer.g4
index 8f7511ac8d..947dedabb1 100644
--- a/Src/PCompiler/CompilerCore/Parser/PLexer.g4
+++ b/Src/PCompiler/CompilerCore/Parser/PLexer.g4
@@ -84,6 +84,11 @@ MAIN		   : 'main' ;
 RECEIVES  : 'receives' ;
 SENDS     : 'sends' ;
 
+// machine declarations
+EVENTQUEUE: 'eventqueue' ;
+EVENTBAG: 'eventbag' ;
+EVENTCHANNEL: 'eventchannel' ;
+
 // Common keywords
 CREATES : 'creates' ;
 TO      : 'to' ;
diff --git a/Src/PCompiler/CompilerCore/Parser/PParser.g4 b/Src/PCompiler/CompilerCore/Parser/PParser.g4
index dc00fca475..49dac77ede 100644
--- a/Src/PCompiler/CompilerCore/Parser/PParser.g4
+++ b/Src/PCompiler/CompilerCore/Parser/PParser.g4
@@ -86,7 +86,11 @@ eventSetLiteral : events+=nonDefaultEvent (COMMA events+=nonDefaultEvent)* ;
 interfaceDecl : INTERFACE name=iden LPAREN type? RPAREN (RECEIVES nonDefaultEventList?) SEMI ;
 
 // has scope
-implMachineDecl : MACHINE name=iden cardinality? receivesSends* machineBody ;
+dequeueOption : EVENTBAG
+                | EVENTCHANNEL
+                | EVENTQUEUE
+                ;             
+implMachineDecl : dequeueOption? MACHINE name=iden cardinality? receivesSends* machineBody ;
 idenList : names+=iden (COMMA names+=iden)* ;
 
 receivesSends : RECEIVES eventSetLiteral? SEMI # MachineReceive
diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Machine.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Machine.cs
index 3b360419e8..2079c247f8 100644
--- a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Machine.cs
+++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Machine.cs
@@ -1,3 +1,4 @@
+using System;
 using System.Collections.Generic;
 using System.Diagnostics;
 using System.Linq;
@@ -38,6 +39,7 @@ public Machine(string name, ParserRuleContext sourceNode)
         public string Name { get; }
         public IStateContainer ParentStateContainer { get; } = null;
         public IEnumerable<State> States => states.Values;
+        public string DequeueOption { get; set;}
 
         public State GetState(string stateName)
         {
diff --git a/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs
index f29e8eb273..3ead66f46b 100644
--- a/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs
+++ b/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs
@@ -269,6 +269,18 @@ public override object VisitImplMachineDecl(PParser.ImplMachineDeclContext conte
             if (cardinality > uint.MaxValue) throw Handler.ValueOutOfRange(context.cardinality(), "uint32");
             machine.Assume = hasAssume ? (uint?) cardinality : null;
             machine.Assert = hasAssert ? (uint?) cardinality : null;
+            
+            // dequeueOption?
+            if (context.dequeueOption() != null)
+            {
+                var dequeueOption = context.dequeueOption().GetText();
+                if (dequeueOption != "eventqueue" && dequeueOption != "eventbag" && dequeueOption != "eventchannel")
+                {
+                    Debug.Fail($"Invalid dequeue option: {dequeueOption}. Allowed: 'eventqueue', 'eventbag', 'eventchannel'.");
+                }
+                machine.DequeueOption = dequeueOption;
+            }
+
 
             // receivesSends*
             foreach (var receivesSends in context.receivesSends())
diff --git a/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs b/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs
index f93a61c0f6..7ad306e366 100644
--- a/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs
+++ b/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs
@@ -400,7 +400,7 @@ from file in Directory.GetFiles(checkerConfiguration.PCompiledPath, filePattern,
                 {
                     if (checkerConfiguration.Mode == CheckerMode.BugFinding)
                     {
-                        if (!fileName.Contains($"CSharp{pathSep}"))
+                        if (!fileName.Contains($"PChecker{pathSep}"))
                             continue;
                         if (fileName.EndsWith("PCheckerCore.dll")
                             || fileName.EndsWith("PCSharpRuntime.dll")
diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/Correct/EventChannel/EventChannel.p b/Tst/RegressionTests/Feature1SMLevelDecls/Correct/EventChannel/EventChannel.p
new file mode 100644
index 0000000000..af43e3c44a
--- /dev/null
+++ b/Tst/RegressionTests/Feature1SMLevelDecls/Correct/EventChannel/EventChannel.p
@@ -0,0 +1,58 @@
+event e: int;
+event e2: int;
+
+eventchannel machine Main {
+	var m1: M1;
+	var m2: M2;
+	var i: int;
+	var count1: int;
+	var count2: int;
+	start state Init {
+		
+		entry {
+			count1 = 0;
+			count2 = 10;
+			m1 = new M1(this);
+			m2 = new M2(this);
+			i = 0;
+		}
+		on e do (p: int) {
+			assert p == count1;
+			count1 = count1 + 1;
+		}
+		on e2 do (p: int) {
+			assert p == count2;
+			count2 = count2 + 1;
+		}
+	}
+}
+
+machine M1 {
+	var i: int;
+	var j: int;
+	start state Init {
+		entry (payload: Main) {
+			i = 0;
+			while (i < 10)
+			{
+				send payload, e, i;
+				i = i + 1;
+			}
+		}
+	}
+}
+
+machine M2 {
+	var i: int;
+	var j: int;
+	start state Init {
+		entry (payload: Main) {
+			i = 10;
+			while (i < 20)
+			{
+				send payload, e2, i;
+				i = i + 1;
+			}
+		}
+	}
+}
diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/Correct/EventQueue/EventQueue.p b/Tst/RegressionTests/Feature1SMLevelDecls/Correct/EventQueue/EventQueue.p
new file mode 100644
index 0000000000..a1648ba02b
--- /dev/null
+++ b/Tst/RegressionTests/Feature1SMLevelDecls/Correct/EventQueue/EventQueue.p
@@ -0,0 +1,50 @@
+event A: int;
+event B: M1;
+event C: int;
+event unblock;
+
+machine Main {
+	var m1: M1;
+	var m2: M2;
+	start state Init {
+		entry {
+      m1 = new M1();
+      m2 = new M2();
+			send m1, A, 1;
+      send m2, B, m1;
+		}
+	}
+}
+
+eventqueue machine M1 {
+	start state Init {
+    on unblock do {
+      goto dequeueEvents;
+    }
+    defer A;
+    defer C;
+  }
+  state dequeueEvents {
+    on A do {
+			goto receivedA;
+    }
+    on C do {
+      assert false, "Event C was received before A";
+    }
+	}
+  state receivedA {
+    on C do {
+      assert true;
+    }
+  }
+}
+
+machine M2 {
+	start state Init {
+		on B do (payload: M1) {
+      send payload, C, 1;
+      send payload, unblock;
+    }
+	}
+}
+
diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EvengBag/EventBag.p b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EvengBag/EventBag.p
new file mode 100644
index 0000000000..4fe23244c3
--- /dev/null
+++ b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EvengBag/EventBag.p
@@ -0,0 +1,34 @@
+event e: int;
+
+eventbag machine Main {
+	var m1: M1;
+	var i: int;
+	var prev: int;
+	start state Init {
+
+		entry {
+			m1 = new M1(this);
+			i = 0;
+			prev = 0;
+		}
+		on e do (p: int) {
+			assert p >= prev;
+			prev = p;
+		}
+	}
+}
+
+machine M1 {
+	var i: int;
+	var j: int;
+	start state Init {
+		entry (payload: Main) {
+			i = 0;
+			while (i < 10)
+			{
+				send payload, e, i;
+				i = i + 1;
+			}
+		}
+	}
+}
\ No newline at end of file
diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventBag2/EventBag2.p b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventBag2/EventBag2.p
new file mode 100644
index 0000000000..c9984428e4
--- /dev/null
+++ b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventBag2/EventBag2.p
@@ -0,0 +1,60 @@
+event A: Main;
+event B: M1;
+event C: int;
+event unblock;
+event iter;
+
+machine Main {
+	var m1: M1;
+	var m2: M2;
+  var i: int;
+	start state Init {
+		entry {
+      m1 = new M1();
+      m2 = new M2();
+			send m1, A, this;
+      send m2, B, m1;
+      i = 0;
+		}
+    // Repeat until M1 receives event C before A
+    on iter do {
+      send m1, A, this;
+      send m2, B, m1;
+    }
+	}
+}
+
+eventbag machine M1 {
+  var m: Main;
+	start state Init {
+    on unblock do {
+      goto dequeueEvents;
+    }
+    defer A;
+    defer C;
+  }
+  state dequeueEvents {
+    on A do (payload: Main){
+      m = payload;
+			goto receivedA;
+    }
+    on C do {
+      assert false, "Event C was received before A";
+    }
+	}
+  state receivedA {
+    on C do {
+      send m, iter;
+      goto Init;
+    }
+  }
+}
+
+machine M2 {
+	start state Init {
+		on B do (payload: M1) {
+      send payload, C, 1;
+      send payload, unblock;
+    }
+	}
+}
diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventChannel/EventChannel.p b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventChannel/EventChannel.p
new file mode 100644
index 0000000000..5132f4cbf9
--- /dev/null
+++ b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventChannel/EventChannel.p
@@ -0,0 +1,56 @@
+event e: int;
+event e2: int;
+
+eventchannel machine Main {
+	var m1: M1;
+	var m2: M2;
+	var count1: int;
+	var count2: int;
+	start state Init {
+		
+		entry {
+			count1 = 0;
+			count2 = 10;
+			m1 = new M1(this);
+			m2 = new M2(this);
+		}
+		on e do (p: int) {
+			assert p != count1;
+			count1 = count1 + 1;
+		}
+		on e2 do (p: int) {
+			assert p != count2;
+			count2 = count2 + 1;
+		}
+	}
+}
+
+machine M1 {
+	var i: int;
+	var j: int;
+	start state Init {
+		entry (payload: Main) {
+			i = 0;
+			while (i < 10)
+			{
+				send payload, e, i;
+				i = i + 1;
+			}
+		}
+	}
+}
+
+machine M2 {
+	var i: int;
+	var j: int;
+	start state Init {
+		entry (payload: Main) {
+			i = 10;
+			while (i < 20)
+			{
+				send payload, e2, i;
+				i = i + 1;
+			}
+		}
+	}
+}
diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventChannel2/EventChannel2.p b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventChannel2/EventChannel2.p
new file mode 100644
index 0000000000..4e9e09b731
--- /dev/null
+++ b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventChannel2/EventChannel2.p
@@ -0,0 +1,60 @@
+event A: Main;
+event B: M1;
+event C: int;
+event unblock;
+event iter;
+
+machine Main {
+	var m1: M1;
+	var m2: M2;
+  var i: int;
+	start state Init {
+		entry {
+      m1 = new M1();
+      m2 = new M2();
+			send m1, A, this;
+      send m2, B, m1;
+      i = 0;
+		}
+    // Repeat until M1 receives event C before A
+    on iter do {
+      send m1, A, this;
+      send m2, B, m1;
+    }
+	}
+}
+
+eventchannel machine M1 {
+  var m: Main;
+	start state Init {
+    on unblock do {
+      goto dequeueEvents;
+    }
+    defer A;
+    defer C;
+  }
+  state dequeueEvents {
+    on A do (payload: Main){
+      m = payload;
+			goto receivedA;
+    }
+    on C do {
+      assert false, "Event C was received before A";
+    }
+	}
+  state receivedA {
+    on C do {
+      send m, iter;
+      goto Init;
+    }
+  }
+}
+
+machine M2 {
+	start state Init {
+		on B do (payload: M1) {
+      send payload, C, 1;
+      send payload, unblock;
+    }
+	}
+}
diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/EvengBag/EventBag.p b/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/EvengBag/EventBag.p
new file mode 100644
index 0000000000..044778a4a5
--- /dev/null
+++ b/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/EvengBag/EventBag.p
@@ -0,0 +1,34 @@
+event e: int;
+
+eventBag machine Main {
+	var m1: M1;
+	var i: int;
+	var prev: int;
+	start state Init {
+
+		entry {
+			m1 = new M1(this);
+			i = 0;
+			prev = 0;
+		}
+		on e do (p: int) {
+			assert p >= prev;
+			prev = p;
+		}
+	}
+}
+
+machine M1 {
+	var i: int;
+	var j: int;
+	start state Init {
+		entry (payload: Main) {
+			i = 0;
+			while (i < 10)
+			{
+				send payload, e, i;
+				i = i + 1;
+			}
+		}
+	}
+}
\ No newline at end of file
diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/EvengQueue/EventQueue.p b/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/EvengQueue/EventQueue.p
new file mode 100644
index 0000000000..a13014e7c3
--- /dev/null
+++ b/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/EvengQueue/EventQueue.p
@@ -0,0 +1,31 @@
+event e: int;
+
+eventQueue machine Main {
+	var m1: M1;
+	var prev: int;
+	start state Init {
+		entry {
+			m1 = new M1((sender= this));
+			prev = 0;
+		}
+		on e do (p: int) {
+			assert p >= prev;
+			prev = p;
+		}
+	}
+}
+
+machine M1 {
+	var i: int;
+	var j: int;
+	start state Init {
+		entry (payload: (sender: Main)) {
+			i = 0;
+			while (i < 10)
+			{
+				send payload.sender, e, i;
+				i = i + 1;
+			}
+		}
+	}
+}
\ No newline at end of file
diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/EventChannel/EventChannel.p b/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/EventChannel/EventChannel.p
new file mode 100644
index 0000000000..991b63d7a6
--- /dev/null
+++ b/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/EventChannel/EventChannel.p
@@ -0,0 +1,56 @@
+event e: int;
+event e2: int;
+
+eventChannel machine Main {
+	var m1: M1;
+	var m2: M2;
+	var count1: int;
+	var count2: int;
+	start state Init {
+		
+		entry {
+			count1 = 0;
+			count2 = 10;
+			m1 = new M1(this);
+			m2 = new M2(this);
+		}
+		on e do (p: int) {
+			assert p != count1;
+			count1 = count1 + 1;
+		}
+		on e2 do (p: int) {
+			assert p != count2;
+			count2 = count2 + 1;
+		}
+	}
+}
+
+machine M1 {
+	var i: int;
+	var j: int;
+	start state Init {
+		entry (payload: Main) {
+			i = 0;
+			while (i < 10)
+			{
+				send payload, e, i;
+				i = i + 1;
+			}
+		}
+	}
+}
+
+machine M2 {
+	var i: int;
+	var j: int;
+	start state Init {
+		entry (payload: Main) {
+			i = 10
+			while (i < 20)
+			{
+				send payload, e2, i;
+				i = i + 1;
+			}
+		}
+	}
+}