fixed actor halting when calling raise event (#483)

Source/Actors/Runtime/StateMachine.cs

@@ -122,20 +122,29 @@ internal override async Task InitializeAsync(Event initialEvent)
         /// Raises the specified <see cref="Event"/> at the end of the current action.
         /// </summary>
         /// <remarks>
-        /// This event is not handled until the action that calls this method returns control back
-        /// to the Coyote runtime.  It is handled before any other events are dequeued from the inbox.
+        /// This event is not handled until the action that calls this method returns control back to the
+        /// Coyote runtime, unless it is a <see cref='HaltEvent'/>, which is handled immediately. It is
+        /// handled before any other events are dequeued from the inbox.
         /// Only one of the following can be called per action:
-        /// <see cref="RaiseEvent"/>, <see cref="RaiseGotoStateEvent{T}"/>,  <see cref="RaisePushStateEvent{T}"/> or
+        /// <see cref="RaiseEvent"/>, <see cref="RaiseGotoStateEvent{T}"/>, <see cref="RaisePushStateEvent{T}"/> or
         /// <see cref="RaisePopStateEvent"/> and <see cref="RaiseHaltEvent"/>.
         /// An Assert is raised if you accidentally try and do two of these operations in a single action.
         /// </remarks>
         /// <param name="e">The event to raise.</param>
         protected void RaiseEvent(Event e)
         {
-            this.Assert(this.CurrentStatus is ActorExecutionStatus.Active, "{0} invoked RaiseEvent while halting.", this.Id);
-            this.Assert(e != null, "{0} is raising a null event.", this.Id);
-            this.CheckDanglingTransition();
-            this.PendingTransition = new Transition(Transition.Type.RaiseEvent, default, e);
+            if (e is HaltEvent)
+            {
+                // Special case for the halt event, which is handled immediately.
+                this.RaiseHaltEvent();
+            }
+            else
+            {
+                this.Assert(this.CurrentStatus is ActorExecutionStatus.Active, "{0} invoked RaiseEvent while halting.", this.Id);
+                this.Assert(e != null, "{0} is raising a null event.", this.Id);
+                this.CheckDanglingTransition();
+                this.PendingTransition = new Transition(Transition.Type.RaiseEvent, default, e);
+            }
         }
 
         /// <summary>
@@ -150,9 +159,9 @@ protected void RaiseEvent(Event e)
         /// this.RaiseEvent(new E());
         /// </code>
         /// This event is not handled until the action that calls this method returns control back
-        /// to the Coyote runtime.  It is handled before any other events are dequeued from the inbox.
+        /// to the Coyote runtime. It is handled before any other events are dequeued from the inbox.
         /// Only one of the following can be called per action:
-        /// <see cref="RaiseEvent"/>, <see cref="RaiseGotoStateEvent{T}"/>,  <see cref="RaisePushStateEvent{T}"/> or
+        /// <see cref="RaiseEvent"/>, <see cref="RaiseGotoStateEvent{T}"/>, <see cref="RaisePushStateEvent{T}"/> or
         /// <see cref="RaisePopStateEvent"/> and <see cref="RaiseHaltEvent"/>.
         /// An Assert is raised if you accidentally try and do two of these operations in a single action.
         /// </remarks>
@@ -173,9 +182,9 @@ protected void RaiseGotoStateEvent<TState>()
         /// this.RaiseEvent(new E());
         /// </code>
         /// This event is not handled until the action that calls this method returns control back
-        /// to the Coyote runtime.  It is handled before any other events are dequeued from the inbox.
+        /// to the Coyote runtime. It is handled before any other events are dequeued from the inbox.
         /// Only one of the following can be called per action:
-        /// <see cref="RaiseEvent"/>, <see cref="RaiseGotoStateEvent{T}"/>,  <see cref="RaisePushStateEvent{T}"/> or
+        /// <see cref="RaiseEvent"/>, <see cref="RaiseGotoStateEvent{T}"/>, <see cref="RaisePushStateEvent{T}"/> or
         /// <see cref="RaisePopStateEvent"/> and <see cref="RaiseHaltEvent"/>.
         /// An Assert is raised if you accidentally try and do two of these operations in a single action.
         /// </remarks>
@@ -194,17 +203,17 @@ protected void RaiseGotoStateEvent(Type state)
         /// </summary>
         /// <remarks>
         /// Pushing a state does not pop the current <see cref="State"/>, instead it pushes the specified <see cref="State"/> on the active state stack
-        /// so that you can have multiple active states.  In this case events can be handled by all active states on the stack.
+        /// so that you can have multiple active states. In this case events can be handled by all active states on the stack.
         /// This is shorthand for the following code:
         /// <code>
         /// class Event E { }
         /// [OnEventPushState(typeof(E), typeof(S))]
         /// this.RaiseEvent(new E());
         /// </code>
         /// This event is not handled until the action that calls this method returns control back
-        /// to the Coyote runtime.  It is handled before any other events are dequeued from the inbox.
+        /// to the Coyote runtime. It is handled before any other events are dequeued from the inbox.
         /// Only one of the following can be called per action:
-        /// <see cref="RaiseEvent"/>, <see cref="RaiseGotoStateEvent{T}"/>,  <see cref="RaisePushStateEvent{T}"/> or
+        /// <see cref="RaiseEvent"/>, <see cref="RaiseGotoStateEvent{T}"/>, <see cref="RaisePushStateEvent{T}"/> or
         /// <see cref="RaisePopStateEvent"/> and <see cref="RaiseHaltEvent"/>.
         /// An Assert is raised if you accidentally try and do two of these operations in a single action.
         /// </remarks>
@@ -218,17 +227,17 @@ protected void RaisePushStateEvent<TState>()
         /// </summary>
         /// <remarks>
         /// Pushing a state does not pop the current <see cref="State"/>, instead it pushes the specified <see cref="State"/> on the active state stack
-        /// so that you can have multiple active states.  In this case events can be handled by all active states on the stack.
+        /// so that you can have multiple active states. In this case events can be handled by all active states on the stack.
         /// This is shorthand for the following code:
         /// <code>
         /// class Event E { }
         /// [OnEventPushState(typeof(E), typeof(S))]
         /// this.RaiseEvent(new E());
         /// </code>
         /// This event is not handled until the action that calls this method returns control back
-        /// to the Coyote runtime.  It is handled before any other events are dequeued from the inbox.
+        /// to the Coyote runtime. It is handled before any other events are dequeued from the inbox.
         /// Only one of the following can be called per action:
-        /// <see cref="RaiseEvent"/>, <see cref="RaiseGotoStateEvent{T}"/>,  <see cref="RaisePushStateEvent{T}"/> or
+        /// <see cref="RaiseEvent"/>, <see cref="RaiseGotoStateEvent{T}"/>, <see cref="RaisePushStateEvent{T}"/> or
         /// <see cref="RaisePopStateEvent"/> and <see cref="RaiseHaltEvent"/>.
         /// An Assert is raised if you accidentally try and do two of these operations in a single action.
         /// </remarks>
@@ -249,10 +258,10 @@ protected void RaisePushStateEvent(Type state)
         /// Popping a state pops the current <see cref="State"/> that was pushed using <see cref='RaisePushStateEvent'/> or an OnEventPushStateAttribute.
         /// An assert is raised if there are no states left to pop.
         /// This event is not handled until the action that calls this method returns control back
-        /// to the Coyote runtime.  It is handled before any other events are dequeued from the inbox.
+        /// to the Coyote runtime. It is handled before any other events are dequeued from the inbox.
         ///
         /// Only one of the following can be called per action:
-        /// <see cref="RaiseEvent"/>, <see cref="RaiseGotoStateEvent{T}"/>,  <see cref="RaisePushStateEvent{T}"/> or
+        /// <see cref="RaiseEvent"/>, <see cref="RaiseGotoStateEvent{T}"/>, <see cref="RaisePushStateEvent{T}"/> or
         /// <see cref="RaisePopStateEvent"/> and <see cref="RaiseHaltEvent"/>.
         /// An Assert is raised if you accidentally try and do two of these operations in a single action.
         /// </remarks>
@@ -268,10 +277,10 @@ protected void RaisePopStateEvent()
         /// </summary>
         /// <remarks>
         /// This event is not handled until the action that calls this method returns control back
-        /// to the Coyote runtime.  It is handled before any other events are dequeued from the inbox.
+        /// to the Coyote runtime. It is handled before any other events are dequeued from the inbox.
         ///
         /// Only one of the following can be called per action:
-        /// <see cref="RaiseEvent"/>, <see cref="RaiseGotoStateEvent{T}"/>,  <see cref="RaisePushStateEvent{T}"/> or
+        /// <see cref="RaiseEvent"/>, <see cref="RaiseGotoStateEvent{T}"/>, <see cref="RaisePushStateEvent{T}"/> or
         /// <see cref="RaisePopStateEvent"/> and <see cref="RaiseHaltEvent"/>.
         /// An Assert is raised if you accidentally try and do two of these operations in a single action.
         /// </remarks>
@@ -640,7 +649,8 @@ private bool TryGetInheritedHandler(Type eventType, out HandlerInfo result)
         /// </summary>
         private void DoStatePush(State state)
         {
-            this.EventHandlerMap = state.EventHandlers;  // non-inheritable handlers.
+            // Non-inheritable handlers.
+            this.EventHandlerMap = state.EventHandlers;
 
             this.StateStack.Push(state);
             this.CurrentState = state.GetType();
@@ -822,7 +832,7 @@ internal override void SetupEventHandlers()
             Type stateMachineType = this.GetType();
 
             // If this type has not already been setup in the ActionCache, then we need to try and grab the ActionCacheLock
-            // for this type.  First make sure we have one and only one lockable object for this type.
+            // for this type. First make sure we have one and only one lockable object for this type.
             object syncObject = ActionCacheLocks.GetOrAdd(stateMachineType, _ => new object());
 
             // Locking this syncObject ensures only one thread enters the initialization code to update
@@ -1062,7 +1072,7 @@ private void AssertStateValidity()
         }
 
         /// <summary>
-        /// Returns the formatted strint to be used with a fair nondeterministic boolean choice.
+        /// Returns the formatted string to be used with a fair nondeterministic boolean choice.
         /// </summary>
         private protected override string FormatFairRandom(string callerMemberName, string callerFilePath, int callerLineNumber) =>
             string.Format(CultureInfo.InvariantCulture, "{0}_{1}_{2}_{3}_{4}",
@@ -1080,7 +1090,7 @@ private protected override void ReportUnhandledException(Exception ex, string ac
 
         /// <summary>
         /// Defines the <see cref="StateMachine"/> transition that is the
-        /// result of executing an event handler.  Transitions are created by using
+        /// result of executing an event handler. Transitions are created by using
         /// <see cref="RaiseGotoStateEvent{T}"/>, <see cref="RaiseEvent"/>, <see cref="RaisePushStateEvent{T}"/> or
         /// <see cref="RaisePopStateEvent"/> and <see cref="RaiseHaltEvent"/>.
         /// The Transition is processed by the Coyote runtime when
@@ -1181,8 +1191,8 @@ private struct HandlerInfo
             public State State;
 
             /// <summary>
-            /// Records where this State is in the StateStack.  This information is needed to implement WildCardEvent
-            /// semantics.  A specific Handler closest to the top of the stack (higher StackDepth) wins over a
+            /// Records where this State is in the StateStack. This information is needed to implement WildCardEvent
+            /// semantics. A specific Handler closest to the top of the stack (higher StackDepth) wins over a
             /// WildCardEvent further down the stack (lower StackDepth).
             /// </summary>
             public int StackDepth;

Tests/Tests.Actors.BugFinding/Callbacks/OnHaltTests.cs

@@ -253,5 +253,37 @@ public void TestOnHaltAsyncWithAPIsInStateMachine()
                 r.CreateActor(typeof(M4Sender), new E(m));
             });
         }
+
+        public class M5 : StateMachine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            [DeferEvents(typeof(WildCardEvent))]
+            private class Init : State
+            {
+            }
+
+            private void InitOnEntry()
+            {
+                this.RaiseEvent(HaltEvent.Instance);
+            }
+
+            protected override Task OnHaltAsync(Event e)
+            {
+                this.Assert(false, "Reached test assertion.");
+                return Task.CompletedTask;
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestOnHaltAsyncWithWildCardInStateMachine()
+        {
+            this.TestWithError(r =>
+            {
+                r.CreateActor(typeof(M5));
+            },
+            expectedError: "Reached test assertion.",
+            replay: true);
+        }
     }
 }

Tests/Tests.Actors.BugFinding/EventHandling/EventHandlerTests.cs

@@ -845,7 +845,13 @@ private void ActiveOnEntry()
 
             private void HandleUnitEvent()
             {
-                this.Assert(this.Test is false, "Reached test assertion.");
+                this.Assert(this.Test is false, "Reached the Active state.");
+            }
+
+            protected override Task OnHaltAsync(Event e)
+            {
+                this.Assert(false, "Reached test assertion.");
+                return Task.CompletedTask;
             }
         }
 

Tests/compare-rewriting-diff-logs.ps1

@@ -17,7 +17,7 @@ $expected_hashes = [ordered]@{
     "rewriting-helpers" = "556A68FF0849371E8AFD7A5159B6D2C53F566917D5F9741FCD1BA89C5F8B67CC"
     "testing" = "8AE199B7410928ED4378B42C7183A8B6730898C248486D79C430063EB2C101A2"
     "actors" = "65E9E6270A12BF675150B31ABB2D5888DAC5CC71ECB8523DD1B4657EA14928CB"
-    "actors-testing" = "304E594DE7E0D95F73FC4569BCFD6CDC5F38C61AF2CBC7ED8646DC072004FAF3"
+    "actors-testing" = "503A3FDA7E0EB5A5B74E12A0810BC09BB59251FF7CFB5605434C2F0F5E521739"
 }
 
 Write-Comment -prefix "." -text "Comparing the test rewriting diff logs" -color "yellow"

docs/ref/Microsoft.Coyote.Actors/StateMachine/RaiseEvent.md

@@ -12,7 +12,7 @@ protected void RaiseEvent(Event e)
 
 ## Remarks
 
-This event is not handled until the action that calls this method returns control back to the Coyote runtime. It is handled before any other events are dequeued from the inbox. Only one of the following can be called per action: `RaiseEvent`, [`RaiseGotoStateEvent`](./RaiseGotoStateEvent.md), [`RaisePushStateEvent`](./RaisePushStateEvent.md) or [`RaisePopStateEvent`](./RaisePopStateEvent.md) and [`RaiseHaltEvent`](./RaiseHaltEvent.md). An Assert is raised if you accidentally try and do two of these operations in a single action.
+This event is not handled until the action that calls this method returns control back to the Coyote runtime, unless it is a [`HaltEvent`](../HaltEvent.md), which is handled immediately. It is handled before any other events are dequeued from the inbox. Only one of the following can be called per action: `RaiseEvent`, [`RaiseGotoStateEvent`](./RaiseGotoStateEvent.md), [`RaisePushStateEvent`](./RaisePushStateEvent.md) or [`RaisePopStateEvent`](./RaisePopStateEvent.md) and [`RaiseHaltEvent`](./RaiseHaltEvent.md). An Assert is raised if you accidentally try and do two of these operations in a single action.
 
 ## See Also
 

docs/ref/Microsoft.Coyote.Rewriting/SkipRewritingAttribute.md

@@ -0,0 +1,22 @@
+# SkipRewritingAttribute class
+
+Attribute for declaring source code targets that must not be rewritten.
+
+```csharp
+[AttributeUsage(AttributeTargets.Class | AttributeTargets.Struct)]
+public sealed class SkipRewritingAttribute : Attribute
+```
+
+## Public Members
+
+| name | description |
+| --- | --- |
+| [SkipRewritingAttribute](SkipRewritingAttribute/SkipRewritingAttribute.md)(…) | Initializes a new instance of the [`SkipRewritingAttribute`](./SkipRewritingAttribute.md) class. |
+| readonly [Reason](SkipRewritingAttribute/Reason.md) | The reason for skipping rewriting. |
+
+## See Also
+
+* namespace [Microsoft.Coyote.Rewriting](../Microsoft.Coyote.RewritingNamespace.md)
+* assembly [Microsoft.Coyote.Test](../Microsoft.Coyote.Test.md)
+
+<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/SkipRewritingAttribute/Reason.md

@@ -0,0 +1,15 @@
+# SkipRewritingAttribute.Reason field
+
+The reason for skipping rewriting.
+
+```csharp
+public readonly string Reason;
+```
+
+## See Also
+
+* class [SkipRewritingAttribute](../SkipRewritingAttribute.md)
+* namespace [Microsoft.Coyote.Rewriting](../SkipRewritingAttribute.md)
+* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
+
+<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/SkipRewritingAttribute/SkipRewritingAttribute.md

@@ -0,0 +1,15 @@
+# SkipRewritingAttribute constructor
+
+Initializes a new instance of the [`SkipRewritingAttribute`](../SkipRewritingAttribute.md) class.
+
+```csharp
+public SkipRewritingAttribute(string reason)
+```
+
+## See Also
+
+* class [SkipRewritingAttribute](../SkipRewritingAttribute.md)
+* namespace [Microsoft.Coyote.Rewriting](../SkipRewritingAttribute.md)
+* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
+
+<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.RewritingNamespace.md

@@ -4,5 +4,6 @@
 | --- | --- |
 | class [RewritingEngine](./Microsoft.Coyote.Rewriting/RewritingEngine.md) | Engine that can rewrite a set of assemblies for systematic testing. |
 | class [RewritingSignatureAttribute](./Microsoft.Coyote.Rewriting/RewritingSignatureAttribute.md) | Attribute that contains a signature identifying the parameters used during binary rewriting of an assembly. |
+| class [SkipRewritingAttribute](./Microsoft.Coyote.Rewriting/SkipRewritingAttribute.md) | Attribute for declaring source code targets that must not be rewritten. |
 
 <!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.SystematicTesting.Frameworks.XUnit/TestOutputLogger.md

@@ -0,0 +1,23 @@
+# TestOutputLogger class
+
+Logger that writes to the xUnit test output.
+
+```csharp
+public sealed class TestOutputLogger : ILogger
+```
+
+## Public Members
+
+| name | description |
+| --- | --- |
+| [TestOutputLogger](TestOutputLogger/TestOutputLogger.md)(…) | Initializes a new instance of the [`TestOutputLogger`](./TestOutputLogger.md) class. |
+| [Dispose](TestOutputLogger/Dispose.md)() | Releases any resources held by the logger. |
+| [Write](TestOutputLogger/Write.md)(…) | Writes an informational string to the log. (10 methods) |
+| [WriteLine](TestOutputLogger/WriteLine.md)(…) | Writes an informational string to the log. (10 methods) |
+
+## See Also
+
+* namespace [Microsoft.Coyote.SystematicTesting.Frameworks.XUnit](../Microsoft.Coyote.SystematicTesting.Frameworks.XUnitNamespace.md)
+* assembly [Microsoft.Coyote.Test](../Microsoft.Coyote.Test.md)
+
+<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.SystematicTesting.Frameworks.XUnit/TestOutputLogger/Dispose.md

@@ -0,0 +1,15 @@
+# TestOutputLogger.Dispose method
+
+Releases any resources held by the logger.
+
+```csharp
+public void Dispose()
+```
+
+## See Also
+
+* class [TestOutputLogger](../TestOutputLogger.md)
+* namespace [Microsoft.Coyote.SystematicTesting.Frameworks.XUnit](../TestOutputLogger.md)
+* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
+
+<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.SystematicTesting.Frameworks.XUnit/TestOutputLogger/TestOutputLogger.md

@@ -0,0 +1,19 @@
+# TestOutputLogger constructor
+
+Initializes a new instance of the [`TestOutputLogger`](../TestOutputLogger.md) class.
+
+```csharp
+public TestOutputLogger(ITestOutputHelper output)
+```
+
+| parameter | description |
+| --- | --- |
+| output | The test output helper. |
+
+## See Also
+
+* class [TestOutputLogger](../TestOutputLogger.md)
+* namespace [Microsoft.Coyote.SystematicTesting.Frameworks.XUnit](../TestOutputLogger.md)
+* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
+
+<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->