From 524eab48d125bc7b2015e0fcc2726c518923ab31 Mon Sep 17 00:00:00 2001 From: Christine Zhou Date: Tue, 14 Jan 2025 23:39:42 -0800 Subject: [PATCH 1/5] Added EventBag and EventChannel inbox types for StateMachine --- .../StateMachines/EventQueues/EventBag.cs | 337 +++++++++++++++++ .../StateMachines/EventQueues/EventChannel.cs | 349 ++++++++++++++++++ .../Runtime/StateMachines/StateMachine.cs | 5 + .../SystematicTesting/ControlledRuntime.cs | 9 +- .../Backend/CSharp/CSharpCodeGenerator.cs | 5 + Src/PCompiler/CompilerCore/Parser/PLexer.g4 | 5 + Src/PCompiler/CompilerCore/Parser/PParser.g4 | 6 +- .../TypeChecker/AST/Declarations/Machine.cs | 2 + .../TypeChecker/DeclarationVisitor.cs | 12 + .../Correct/EventChannel/EventChannel.p | 67 ++++ .../DynamicError/EvengBag/EventBag.p | 41 ++ .../DynamicError/EventChannel/EventChannel.p | 67 ++++ .../StaticError/EvengBag/EventBag.p | 41 ++ .../StaticError/EventChannel/EventChannel.p | 67 ++++ 14 files changed, 1010 insertions(+), 3 deletions(-) create mode 100644 Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventBag.cs create mode 100644 Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventChannel.cs create mode 100644 Tst/RegressionTests/Feature1SMLevelDecls/Correct/EventChannel/EventChannel.p create mode 100644 Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EvengBag/EventBag.p create mode 100644 Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventChannel/EventChannel.p create mode 100644 Tst/RegressionTests/Feature1SMLevelDecls/StaticError/EvengBag/EventBag.p create mode 100644 Tst/RegressionTests/Feature1SMLevelDecls/StaticError/EventChannel/EventChannel.p 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..5154daa908 --- /dev/null +++ b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventBag.cs @@ -0,0 +1,337 @@ +using System; +using System.Collections.Generic; +using System.Threading.Tasks; +using PChecker.Runtime.Events; +using PChecker.Runtime.StateMachines.Managers; + + +namespace PChecker.Runtime.StateMachines.EventQueues; + +/// +/// Implements a bag of events that is used during testing. +/// +internal sealed class EventBag : IEventQueue +{ + /// + /// Manages the state machine that owns this queue. + /// + private readonly IStateMachineManager StateMachineManager; + + /// + /// The state machine that owns this queue. + /// + private readonly StateMachine StateMachine; + + /// + /// The internal queue that contains events with their metadata. + /// + private readonly List<(Event e, EventInfo info)> Bag; + + /// + /// The raised event and its metadata, or null if no event has been raised. + /// + private (Event e, EventInfo info) RaisedEvent; + + /// + /// 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. + /// + private Dictionary> EventWaitTypes; + + /// + /// Task completion source that contains the event obtained using an explicit receive. + /// + private TaskCompletionSource ReceiveCompletionSource; + + /// + /// Checks if the queue is accepting new events. + /// + private bool IsClosed; + + /// + /// The size of the queue. + /// + public int Size => Bag.Count; + + /// + /// Checks if an event has been raised. + /// + public bool IsEventRaised => RaisedEvent != default; + + /// + /// Initializes a new instance of the class. + /// + internal EventBag(IStateMachineManager stateMachineManager, StateMachine stateMachine) + { + StateMachineManager = stateMachineManager; + StateMachine = stateMachine; + Bag = new List<(Event, EventInfo)>(); + EventWaitTypes = new Dictionary>(); + IsClosed = false; + } + + /// + 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; + } + + /// + 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)); + } + + /// + /// Dequeues the next event and its metadata, if there is one available, else returns null. + /// + 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; + } + + /// + 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); + } + + /// + public Task ReceiveEventAsync(Type eventType, Func predicate = null) + { + var eventWaitTypes = new Dictionary> + { + { eventType, predicate } + }; + + return ReceiveEventAsync(eventWaitTypes); + } + + /// + public Task ReceiveEventAsync(params Type[] eventTypes) + { + var eventWaitTypes = new Dictionary>(); + foreach (var type in eventTypes) + { + eventWaitTypes.Add(type, null); + } + + return ReceiveEventAsync(eventWaitTypes); + } + + /// + public Task ReceiveEventAsync(params Tuple>[] events) + { + var eventWaitTypes = new Dictionary>(); + foreach (var e in events) + { + eventWaitTypes.Add(e.Item1, e.Item2); + } + + return ReceiveEventAsync(eventWaitTypes); + } + + /// + /// Waits for an event to be enqueued. + /// + private Task ReceiveEventAsync(Dictionary> eventWaitTypes) + { + StateMachine.Runtime.NotifyReceiveCalled(StateMachine); + + (Event e, EventInfo info) receivedEvent = default; + int index = 0; + while (Bag.Count != 0) + { + 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(); + EventWaitTypes = eventWaitTypes; + StateMachineManager.OnWaitEvent(EventWaitTypes.Keys); + return ReceiveCompletionSource.Task; + } + + StateMachineManager.OnReceiveEventWithoutWaiting(receivedEvent.e, receivedEvent.info); + return Task.FromResult(receivedEvent.e); + } + + /// + public int GetCachedState() + { + unchecked + { + var hash = 19; + foreach (var (_, info) in Bag) + { + hash = (hash * 31) + info.EventName.GetHashCode(); + } + + return hash; + } + } + + /// + public void Close() + { + IsClosed = true; + } + + /// + /// Disposes the queue resources. + /// + private void Dispose(bool disposing) + { + if (!disposing) + { + return; + } + + foreach (var (e, info) in Bag) + { + StateMachineManager.OnDropEvent(e, info); + } + + Bag.Clear(); + } + + /// + 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..3505144090 --- /dev/null +++ b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventChannel.cs @@ -0,0 +1,349 @@ +// 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 +{ + /// + /// Implements a queue of events that is used during testing. + /// + internal sealed class EventChannel : IEventQueue + { + /// + /// Manages the state machine that owns this queue. + /// + private readonly IStateMachineManager StateMachineManager; + + /// + /// The state machine that owns this queue. + /// + private readonly StateMachine StateMachine; + + /// + /// The internal queue that contains events with their metadata. + /// + private readonly Dictionary> Map; + + + /// + /// The list of event sender state machines. + /// + private Queue SenderMachineNames; + + /// + /// The raised event and its metadata, or null if no event has been raised. + /// + private (Event e, EventInfo info) RaisedEvent; + + /// + /// 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. + /// + private Dictionary> EventWaitTypes; + + /// + /// Checks if the queue is accepting new events. + /// + private bool IsClosed; + + /// + /// The size of the queue. + /// + public int Size => Map.Count; + + /// + /// Checks if an event has been raised. + /// + public bool IsEventRaised => RaisedEvent != default; + + /// + /// Initializes a new instance of the class. + /// + internal EventChannel(IStateMachineManager stateMachineManager, StateMachine stateMachine) + { + StateMachineManager = stateMachineManager; + StateMachine = stateMachine; + Map = new Dictionary>(); + SenderMachineNames = new Queue(); + EventWaitTypes = new Dictionary>(); + IsClosed = false; + } + + /// + 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.Enqueue(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; + } + + /// + 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)); + } + + /// + /// Dequeues the next event and its metadata, if there is one available, else returns null. + /// + private (Event e, EventInfo info) TryDequeueEvent(bool checkOnly = false) + { + int checkedCount = 0; + int totalMachines = SenderMachineNames.Count; + (Event, EventInfo) nextAvailableEvent = default; + + while (checkedCount < totalMachines) + { + if (SenderMachineNames.TryDequeue(out string stateMachine)) + { + if (Map.TryGetValue(stateMachine, out var eventList) && eventList.Count > 0) + { + nextAvailableEvent = TryDequeueEvent(stateMachine, checkOnly); + SenderMachineNames.Enqueue(stateMachine); + break; + } + SenderMachineNames.Enqueue(stateMachine); + checkedCount++; + } + } + return nextAvailableEvent; + } + + /// + /// Dequeues the next event and its metadata, if there is one available, else returns null. + /// + 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; + } + + /// + 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); + } + + /// + public Task ReceiveEventAsync(Type eventType, Func predicate = null) + { + var eventWaitTypes = new Dictionary> + { + { eventType, predicate } + }; + + return ReceiveEventAsync(eventWaitTypes); + } + + /// + public Task ReceiveEventAsync(params Type[] eventTypes) + { + var eventWaitTypes = new Dictionary>(); + foreach (var type in eventTypes) + { + eventWaitTypes.Add(type, null); + } + + return ReceiveEventAsync(eventWaitTypes); + } + + /// + public Task ReceiveEventAsync(params Tuple>[] events) + { + var eventWaitTypes = new Dictionary>(); + foreach (var e in events) + { + eventWaitTypes.Add(e.Item1, e.Item2); + } + + return ReceiveEventAsync(eventWaitTypes); + } + + /// + /// Waits for an event to be enqueued. + /// + private Task ReceiveEventAsync(Dictionary> eventWaitTypes) + { + StateMachine.Runtime.NotifyReceiveCalled(StateMachine); + + (Event e, EventInfo info) receivedEvent = default; + return Task.FromResult(receivedEvent.e); + } + + /// + public int GetCachedState() + { + unchecked + { + var hash = 19; + + foreach (var (_, linkedList) in Map) + { + foreach (var (_, info) in linkedList) + { + hash = (hash * 31) + (info.EventName?.GetHashCode() ?? 0); + } + } + + return hash; + } + } + + /// + public void Close() + { + IsClosed = true; + } + + /// + /// Disposes the queue resources. + /// + 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(); + } + + /// + public void Dispose() + { + Dispose(true); + GC.SuppressFinalize(this); + } + } +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs b/Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs index 6f6019b443..a1c0a73f26 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; + /// + /// Event inbox type. + /// + public string InboxType; + /// /// Keeps track of state machine's current vector time. /// diff --git a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs index 1c6b814453..295247feea 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); /// - /// 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. @@ -506,7 +506,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/CSharp/CSharpCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs index e13a8fa14f..d51a376fe1 100644 --- a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs +++ b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs @@ -553,6 +553,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/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 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/Tst/RegressionTests/Feature1SMLevelDecls/Correct/EventChannel/EventChannel.p b/Tst/RegressionTests/Feature1SMLevelDecls/Correct/EventChannel/EventChannel.p new file mode 100644 index 0000000000..ae870b0563 --- /dev/null +++ b/Tst/RegressionTests/Feature1SMLevelDecls/Correct/EventChannel/EventChannel.p @@ -0,0 +1,67 @@ +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((sender= this, num= count1)); + m2 = new M2((sender= this, num= count2)); + i = 0; + while (i < 10) + { + print format("Waiting {0}", i); + i = i + 1; + } + } + 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: (sender: Main, num: int)) { + print format("sender: {0}", payload.sender); + i = payload.num; + j = i + 10; + while (i < j) + { + send payload.sender, e, i; + i = i + 1; + } + } + } +} + +machine M2 { + var i: int; + var j: int; + start state Init { + entry (payload: (sender: Main, num: int)) { + print format("sender: {0}", payload.sender); + i = payload.num; + j = i + 10; + while (i < j) + { + send payload.sender, e2, i; + i = i + 1; + } + } + } +} diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EvengBag/EventBag.p b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EvengBag/EventBag.p new file mode 100644 index 0000000000..63e27c792d --- /dev/null +++ b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EvengBag/EventBag.p @@ -0,0 +1,41 @@ +event e: int; + +eventbag machine Main { + var m1: M1; + var i: int; + var prev: int; + start state Init { + + entry { + m1 = new M1((sender= this, num= 0)); + i = 0; + prev = 0; + while (i < 100) + { + print format("Waiting for events to pile up {0}", i); + i = i + 1; + } + } + 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, num: int)) { + print format("sender: {0}", payload.sender); + i = payload.num; + j = i + 10; + while (i < j) + { + send payload.sender, e, i; + i = i + 1; + } + } + } +} \ No newline at end of file diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventChannel/EventChannel.p b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventChannel/EventChannel.p new file mode 100644 index 0000000000..b0411db590 --- /dev/null +++ b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventChannel/EventChannel.p @@ -0,0 +1,67 @@ +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((sender= this, num= count1)); + m2 = new M2((sender= this, num= count2)); + i = 0; + while (i < 10) + { + print format("Waiting {0}", i); + i = i + 1; + } + } + 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: (sender: Main, num: int)) { + print format("sender: {0}", payload.sender); + i = payload.num; + j = i + 10; + while (i < j) + { + send payload.sender, e, i; + i = i + 1; + } + } + } +} + +machine M2 { + var i: int; + var j: int; + start state Init { + entry (payload: (sender: Main, num: int)) { + print format("sender: {0}", payload.sender); + i = payload.num; + j = i + 10; + while (i < j) + { + send payload.sender, e2, i; + i = i + 1; + } + } + } +} diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/EvengBag/EventBag.p b/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/EvengBag/EventBag.p new file mode 100644 index 0000000000..82859cd8ad --- /dev/null +++ b/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/EvengBag/EventBag.p @@ -0,0 +1,41 @@ +event e: int; + +eventBag machine Main { + var m1: M1; + var i: int; + var prev: int; + start state Init { + + entry { + m1 = new M1((sender= this, num= 0)); + i = 0; + prev = 0; + while (i < 100) + { + print format("Waiting for events to pile up {0}", i); + i = i + 1; + } + } + 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, num: int)) { + print format("sender: {0}", payload.sender); + i = payload.num; + j = i + 10; + while (i < j) + { + 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..aaabf0b578 --- /dev/null +++ b/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/EventChannel/EventChannel.p @@ -0,0 +1,67 @@ +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((sender= this, num= count1)); + m2 = new M2((sender= this, num= count2)); + i = 0; + while (i < 10) + { + print format("Waiting {0}", i); + i = i + 1; + } + } + 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: (sender: Main, num: int)) { + print format("sender: {0}", payload.sender); + i = payload.num; + j = i + 10; + while (i < j) + { + send payload.sender, e, i; + i = i + 1; + } + } + } +} + +machine M2 { + var i: int; + var j: int; + start state Init { + entry (payload: (sender: Main, num: int)) { + print format("sender: {0}", payload.sender); + i = payload.num; + j = i + 10; + while (i < j) + { + send payload.sender, e2, i; + i = i + 1; + } + } + } +} From d5125ca4ea361776bd101339765d458829b62841 Mon Sep 17 00:00:00 2001 From: Christine Zhou Date: Wed, 15 Jan 2025 12:22:47 -0800 Subject: [PATCH 2/5] Fix while loop bug, event channel now selects state machines randomly instead of round robin fashion --- .../StateMachines/EventQueues/EventBag.cs | 2 +- .../StateMachines/EventQueues/EventChannel.cs | 30 +++++++++---------- 2 files changed, 15 insertions(+), 17 deletions(-) diff --git a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventBag.cs b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventBag.cs index 5154daa908..fc19d9571d 100644 --- a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventBag.cs +++ b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventBag.cs @@ -262,7 +262,7 @@ private Task ReceiveEventAsync(Dictionary> eventW (Event e, EventInfo info) receivedEvent = default; int index = 0; - while (Bag.Count != 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. diff --git a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventChannel.cs b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventChannel.cs index 3505144090..f570619241 100644 --- a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventChannel.cs +++ b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventChannel.cs @@ -33,7 +33,7 @@ internal sealed class EventChannel : IEventQueue /// /// The list of event sender state machines. /// - private Queue SenderMachineNames; + private List SenderMachineNames; /// /// The raised event and its metadata, or null if no event has been raised. @@ -71,7 +71,7 @@ internal EventChannel(IStateMachineManager stateMachineManager, StateMachine sta StateMachineManager = stateMachineManager; StateMachine = stateMachine; Map = new Dictionary>(); - SenderMachineNames = new Queue(); + SenderMachineNames = new List(); EventWaitTypes = new Dictionary>(); IsClosed = false; } @@ -97,7 +97,7 @@ public EnqueueStatus Enqueue(Event e, EventInfo info) if (!Map.ContainsKey(senderStateMachineName)) { Map[senderStateMachineName] = new LinkedList<(Event e, EventInfo info)>(); - SenderMachineNames.Enqueue(senderStateMachineName); + SenderMachineNames.Add(senderStateMachineName); } Map[senderStateMachineName].AddLast((e, info)); @@ -172,24 +172,22 @@ public EnqueueStatus Enqueue(Event e, EventInfo info) /// private (Event e, EventInfo info) TryDequeueEvent(bool checkOnly = false) { - int checkedCount = 0; - int totalMachines = SenderMachineNames.Count; + List temp = []; (Event, EventInfo) nextAvailableEvent = default; - - while (checkedCount < totalMachines) + while (SenderMachineNames.Count > 0) { - if (SenderMachineNames.TryDequeue(out string stateMachine)) + 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) { - if (Map.TryGetValue(stateMachine, out var eventList) && eventList.Count > 0) - { - nextAvailableEvent = TryDequeueEvent(stateMachine, checkOnly); - SenderMachineNames.Enqueue(stateMachine); - break; - } - SenderMachineNames.Enqueue(stateMachine); - checkedCount++; + nextAvailableEvent = TryDequeueEvent(stateMachine, checkOnly); + SenderMachineNames.AddRange(temp); + break; } } + SenderMachineNames.AddRange(temp); return nextAvailableEvent; } From e5d90dc2d02f7d93f020f15ccd4b5d51e723ffb7 Mon Sep 17 00:00:00 2001 From: Christine Zhou Date: Wed, 15 Jan 2025 14:01:53 -0800 Subject: [PATCH 3/5] Removing GetCachedState function from EventQueue interface and classes --- .../StateMachines/EventQueues/EventBag.cs | 17 +---------------- .../StateMachines/EventQueues/EventChannel.cs | 19 ------------------- .../StateMachines/EventQueues/EventQueue.cs | 15 --------------- .../StateMachines/EventQueues/IEventQueue.cs | 5 ----- .../Runtime/StateMachines/StateMachine.cs | 2 -- 5 files changed, 1 insertion(+), 57 deletions(-) diff --git a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventBag.cs b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventBag.cs index fc19d9571d..d19fd1e38b 100644 --- a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventBag.cs +++ b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventBag.cs @@ -287,22 +287,7 @@ private Task ReceiveEventAsync(Dictionary> eventW StateMachineManager.OnReceiveEventWithoutWaiting(receivedEvent.e, receivedEvent.info); return Task.FromResult(receivedEvent.e); } - - /// - public int GetCachedState() - { - unchecked - { - var hash = 19; - foreach (var (_, info) in Bag) - { - hash = (hash * 31) + info.EventName.GetHashCode(); - } - - return hash; - } - } - + /// public void Close() { diff --git a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventChannel.cs b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventChannel.cs index f570619241..bb452af843 100644 --- a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventChannel.cs +++ b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventChannel.cs @@ -291,25 +291,6 @@ private Task ReceiveEventAsync(Dictionary> eventW return Task.FromResult(receivedEvent.e); } - /// - public int GetCachedState() - { - unchecked - { - var hash = 19; - - foreach (var (_, linkedList) in Map) - { - foreach (var (_, info) in linkedList) - { - hash = (hash * 31) + (info.EventName?.GetHashCode() ?? 0); - } - } - - return hash; - } - } - /// public void Close() { 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 ReceiveEventAsync(Dictionary> eventW return Task.FromResult(receivedEvent.e); } - /// - public int GetCachedState() - { - unchecked - { - var hash = 19; - foreach (var (_, info) in Queue) - { - hash = (hash * 31) + info.EventName.GetHashCode(); - } - - return hash; - } - } - /// 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 /// Task ReceiveEventAsync(params Tuple>[] events); - /// - /// Returns the cached state of the queue. - /// - int GetCachedState(); - /// /// Closes the queue, which stops any further event enqueues. /// diff --git a/Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs b/Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs index a1c0a73f26..1d5a38e443 100644 --- a/Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs +++ b/Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs @@ -1386,8 +1386,6 @@ internal int GetHashedState() hash = (hash * 31) + Manager.GetCachedState(); - hash = (hash * 31) + Inbox.GetCachedState(); - return hash; } } From 632ba13e73d4f3a558004cb6b70a68236ebd9317 Mon Sep 17 00:00:00 2001 From: Christine Zhou Date: Sun, 19 Jan 2025 21:56:20 -0800 Subject: [PATCH 4/5] Fixed a bug causing error: ".dll file not found" --- Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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") From 08003e34fd23ed087df4dec3a3a8f8b1cd3951d9 Mon Sep 17 00:00:00 2001 From: Christine Zhou Date: Mon, 20 Jan 2025 00:16:31 -0800 Subject: [PATCH 5/5] EventBag, EventChannel, EventQueue added more test cases + minor fixes --- .../StateMachines/EventQueues/EventBag.cs | 2 - .../StateMachines/EventQueues/EventChannel.cs | 4 ++ .../Backend/PChecker/PCheckerNameManager.cs | 3 +- .../Correct/EventChannel/EventChannel.p | 29 ++++----- .../Correct/EventQueue/EventQueue.p | 50 ++++++++++++++++ .../DynamicError/EvengBag/EventBag.p | 17 ++---- .../DynamicError/EventBag2/EventBag2.p | 60 +++++++++++++++++++ .../DynamicError/EventChannel/EventChannel.p | 31 ++++------ .../EventChannel2/EventChannel2.p | 60 +++++++++++++++++++ .../StaticError/EvengBag/EventBag.p | 17 ++---- .../StaticError/EvengQueue/EventQueue.p | 31 ++++++++++ .../StaticError/EventChannel/EventChannel.p | 35 ++++------- 12 files changed, 249 insertions(+), 90 deletions(-) create mode 100644 Tst/RegressionTests/Feature1SMLevelDecls/Correct/EventQueue/EventQueue.p create mode 100644 Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventBag2/EventBag2.p create mode 100644 Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventChannel2/EventChannel2.p create mode 100644 Tst/RegressionTests/Feature1SMLevelDecls/StaticError/EvengQueue/EventQueue.p diff --git a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventBag.cs b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventBag.cs index d19fd1e38b..957a205e70 100644 --- a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventBag.cs +++ b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventBag.cs @@ -194,9 +194,7 @@ public EnqueueStatus Enqueue(Event e, EventInfo info) Bag.Remove(availableEvent); deferredEvents.Add(availableEvent); availableEvent = default; - } - } Bag.AddRange(deferredEvents); diff --git a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventChannel.cs b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventChannel.cs index bb452af843..9b9b1560ef 100644 --- a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventChannel.cs +++ b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventChannel.cs @@ -183,6 +183,10 @@ public EnqueueStatus Enqueue(Event e, EventInfo info) if (Map.TryGetValue(stateMachine, out var eventList) && eventList.Count > 0) { nextAvailableEvent = TryDequeueEvent(stateMachine, checkOnly); + } + + if (nextAvailableEvent != default) + { SenderMachineNames.AddRange(temp); break; } 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/Tst/RegressionTests/Feature1SMLevelDecls/Correct/EventChannel/EventChannel.p b/Tst/RegressionTests/Feature1SMLevelDecls/Correct/EventChannel/EventChannel.p index ae870b0563..af43e3c44a 100644 --- a/Tst/RegressionTests/Feature1SMLevelDecls/Correct/EventChannel/EventChannel.p +++ b/Tst/RegressionTests/Feature1SMLevelDecls/Correct/EventChannel/EventChannel.p @@ -12,14 +12,9 @@ eventchannel machine Main { entry { count1 = 0; count2 = 10; - m1 = new M1((sender= this, num= count1)); - m2 = new M2((sender= this, num= count2)); + m1 = new M1(this); + m2 = new M2(this); i = 0; - while (i < 10) - { - print format("Waiting {0}", i); - i = i + 1; - } } on e do (p: int) { assert p == count1; @@ -36,13 +31,11 @@ machine M1 { var i: int; var j: int; start state Init { - entry (payload: (sender: Main, num: int)) { - print format("sender: {0}", payload.sender); - i = payload.num; - j = i + 10; - while (i < j) + entry (payload: Main) { + i = 0; + while (i < 10) { - send payload.sender, e, i; + send payload, e, i; i = i + 1; } } @@ -53,13 +46,11 @@ machine M2 { var i: int; var j: int; start state Init { - entry (payload: (sender: Main, num: int)) { - print format("sender: {0}", payload.sender); - i = payload.num; - j = i + 10; - while (i < j) + entry (payload: Main) { + i = 10; + while (i < 20) { - send payload.sender, e2, i; + 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 index 63e27c792d..4fe23244c3 100644 --- a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EvengBag/EventBag.p +++ b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EvengBag/EventBag.p @@ -7,14 +7,9 @@ eventbag machine Main { start state Init { entry { - m1 = new M1((sender= this, num= 0)); + m1 = new M1(this); i = 0; prev = 0; - while (i < 100) - { - print format("Waiting for events to pile up {0}", i); - i = i + 1; - } } on e do (p: int) { assert p >= prev; @@ -27,13 +22,11 @@ machine M1 { var i: int; var j: int; start state Init { - entry (payload: (sender: Main, num: int)) { - print format("sender: {0}", payload.sender); - i = payload.num; - j = i + 10; - while (i < j) + entry (payload: Main) { + i = 0; + while (i < 10) { - send payload.sender, e, i; + send payload, e, i; i = i + 1; } } 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 index b0411db590..5132f4cbf9 100644 --- a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventChannel/EventChannel.p +++ b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventChannel/EventChannel.p @@ -4,7 +4,6 @@ event e2: int; eventchannel machine Main { var m1: M1; var m2: M2; - var i: int; var count1: int; var count2: int; start state Init { @@ -12,14 +11,8 @@ eventchannel machine Main { entry { count1 = 0; count2 = 10; - m1 = new M1((sender= this, num= count1)); - m2 = new M2((sender= this, num= count2)); - i = 0; - while (i < 10) - { - print format("Waiting {0}", i); - i = i + 1; - } + m1 = new M1(this); + m2 = new M2(this); } on e do (p: int) { assert p != count1; @@ -36,13 +29,11 @@ machine M1 { var i: int; var j: int; start state Init { - entry (payload: (sender: Main, num: int)) { - print format("sender: {0}", payload.sender); - i = payload.num; - j = i + 10; - while (i < j) + entry (payload: Main) { + i = 0; + while (i < 10) { - send payload.sender, e, i; + send payload, e, i; i = i + 1; } } @@ -53,13 +44,11 @@ machine M2 { var i: int; var j: int; start state Init { - entry (payload: (sender: Main, num: int)) { - print format("sender: {0}", payload.sender); - i = payload.num; - j = i + 10; - while (i < j) + entry (payload: Main) { + i = 10; + while (i < 20) { - send payload.sender, e2, i; + 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 index 82859cd8ad..044778a4a5 100644 --- a/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/EvengBag/EventBag.p +++ b/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/EvengBag/EventBag.p @@ -7,14 +7,9 @@ eventBag machine Main { start state Init { entry { - m1 = new M1((sender= this, num= 0)); + m1 = new M1(this); i = 0; prev = 0; - while (i < 100) - { - print format("Waiting for events to pile up {0}", i); - i = i + 1; - } } on e do (p: int) { assert p >= prev; @@ -27,13 +22,11 @@ machine M1 { var i: int; var j: int; start state Init { - entry (payload: (sender: Main, num: int)) { - print format("sender: {0}", payload.sender); - i = payload.num; - j = i + 10; - while (i < j) + entry (payload: Main) { + i = 0; + while (i < 10) { - send payload.sender, e, i; + send payload, e, i; i = i + 1; } } 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 index aaabf0b578..991b63d7a6 100644 --- a/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/EventChannel/EventChannel.p +++ b/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/EventChannel/EventChannel.p @@ -4,7 +4,6 @@ event e2: int; eventChannel machine Main { var m1: M1; var m2: M2; - var i: int; var count1: int; var count2: int; start state Init { @@ -12,21 +11,15 @@ eventChannel machine Main { entry { count1 = 0; count2 = 10; - m1 = new M1((sender= this, num= count1)); - m2 = new M2((sender= this, num= count2)); - i = 0; - while (i < 10) - { - print format("Waiting {0}", i); - i = i + 1; - } + m1 = new M1(this); + m2 = new M2(this); } on e do (p: int) { - assert p == count1; + assert p != count1; count1 = count1 + 1; } on e2 do (p: int) { - assert p == count2; + assert p != count2; count2 = count2 + 1; } } @@ -36,13 +29,11 @@ machine M1 { var i: int; var j: int; start state Init { - entry (payload: (sender: Main, num: int)) { - print format("sender: {0}", payload.sender); - i = payload.num; - j = i + 10; - while (i < j) + entry (payload: Main) { + i = 0; + while (i < 10) { - send payload.sender, e, i; + send payload, e, i; i = i + 1; } } @@ -53,13 +44,11 @@ machine M2 { var i: int; var j: int; start state Init { - entry (payload: (sender: Main, num: int)) { - print format("sender: {0}", payload.sender); - i = payload.num; - j = i + 10; - while (i < j) + entry (payload: Main) { + i = 10 + while (i < 20) { - send payload.sender, e2, i; + send payload, e2, i; i = i + 1; } }