Added callback on machine halt (#252)

Source/Core/Library/Machine.cs

@@ -374,6 +374,7 @@ protected void Goto<S>() where S: MachineState
         [Obsolete("Goto(typeof(T)) is deprecated; use Goto<T>() instead.")]
         protected void Goto(Type s)
         {
+            this.Assert(!this.Info.IsHalted, $"Machine '{base.Id}' invoked Goto while halted.");
             // If the state is not a state of the machine, then report an error and exit.
             this.Assert(StateTypeMap[this.GetType()].Any(val
                 => val.DeclaringType.Equals(s.DeclaringType) &&
@@ -388,6 +389,7 @@ protected void Goto(Type s)
         /// <param name="e">Event</param>
         protected void Raise(Event e)
         {
+            this.Assert(!this.Info.IsHalted, $"Machine '{base.Id}' invoked Raise while halted.");
             // If the event is null, then report an error and exit.
             this.Assert(e != null, $"Machine '{base.Id}' is raising a null event.");
             this.RaisedEvent = new EventInfo(e, new EventOriginInfo(
@@ -402,6 +404,7 @@ protected void Raise(Event e)
         /// <returns>Event received</returns>
         protected internal Task<Event> Receive(params Type[] eventTypes)
         {
+            this.Assert(!this.Info.IsHalted, $"Machine '{base.Id}' invoked Receive while halted.");
             base.Runtime.NotifyReceiveCalled(this);
 
             lock (this.Inbox)
@@ -425,6 +428,7 @@ protected internal Task<Event> Receive(params Type[] eventTypes)
         /// <returns>Event received</returns>
         protected internal Task<Event> Receive(Type eventType, Func<Event, bool> predicate)
         {
+            this.Assert(!this.Info.IsHalted, $"Machine '{base.Id}' invoked Receive while halted.");
             base.Runtime.NotifyReceiveCalled(this);
 
             lock (this.Inbox)
@@ -444,6 +448,7 @@ protected internal Task<Event> Receive(Type eventType, Func<Event, bool> predica
         /// <returns>Event received</returns>
         protected internal Task<Event> Receive(params Tuple<Type, Func<Event, bool>>[] events)
         {
+            this.Assert(!this.Info.IsHalted, $"Machine '{base.Id}' invoked Receive while halted.");
             base.Runtime.NotifyReceiveCalled(this);
 
             lock (this.Inbox)
@@ -817,6 +822,9 @@ private async Task HandleEvent(Event e)
                             this.CleanUpResources();
                         }
 
+                        // Invoke user callback outside the lock.
+                        this.OnHalt();
+
                         return;
                     }
 
@@ -1728,6 +1736,11 @@ private void CleanUpResources()
             this.ReceivedEvent = null;
         }
 
+        /// <summary>
+        /// User callback when a machine halts.
+        /// </summary>
+        protected virtual void OnHalt() { }
+
         #endregion
     }
 }

Tests/Core.Tests.Unit/Features/OnHaltTest.cs

@@ -0,0 +1,210 @@
+//-----------------------------------------------------------------------
+// <copyright file="OnHaltTest.cs">
+//      Copyright (c) Microsoft Corporation. All rights reserved.
+// 
+//      THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+//      EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+//      MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+//      IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+//      CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+//      TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+//      SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+// </copyright>
+//-----------------------------------------------------------------------
+
+using System;
+using System.Threading.Tasks;
+using Xunit;
+
+namespace Microsoft.PSharp.Core.Tests.Unit
+{
+    public class OnHaltTest
+    {
+        class E : Event
+        {
+            public MachineId Id;
+            public TaskCompletionSource<bool> tcs;
+
+            public E() { }
+
+            public E(MachineId id)
+            {
+                Id = id;
+            }
+            public E(TaskCompletionSource<bool> tcs)
+            {
+                this.tcs = tcs;
+            }
+        }
+
+        class M1 : Machine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            class Init : MachineState { }
+
+            void InitOnEntry()
+            {
+                this.Raise(new Halt());
+            }
+
+            protected override void OnHalt()
+            {
+                this.Assert(false);
+            }
+        }
+
+        class M2a : Machine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            class Init : MachineState { }
+
+            void InitOnEntry()
+            {
+                this.Raise(new Halt());
+            }
+
+            protected override void OnHalt()
+            {
+                this.Receive(typeof(Event)).Wait();
+            }
+        }
+
+        class M2b : Machine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            class Init : MachineState { }
+
+            void InitOnEntry()
+            {
+                this.Raise(new Halt());
+            }
+
+            protected override void OnHalt()
+            {
+                this.Raise(new E());
+            }
+        }
+
+        class M2c : Machine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            class Init : MachineState { }
+
+            void InitOnEntry()
+            {
+                this.Raise(new Halt());
+            }
+
+            protected override void OnHalt()
+            {
+                this.Goto<Init>();
+            }
+        }
+
+        class Dummy : Machine
+        {
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            class Init : MachineState { }
+
+            void InitOnEntry()
+            {
+                this.Raise(new Halt());
+            }
+        }
+
+        class M3 : Machine
+        {
+            TaskCompletionSource<bool> tcs;
+
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            class Init : MachineState { }
+
+            void InitOnEntry()
+            {
+                tcs = (this.ReceivedEvent as E).tcs;
+                this.Raise(new Halt());
+            }
+
+            protected override void OnHalt()
+            {
+                // no-ops but no failure
+                this.Send(this.Id, new E());
+                this.Random();
+                this.Assert(true);
+                this.CreateMachine(typeof(Dummy));
+
+                tcs.SetResult(true);
+            }
+        }
+
+        public void AssertSucceeded(Type machine)
+        {
+            var runtime = PSharpRuntime.Create();
+            var failed = false;
+            var tcs = new TaskCompletionSource<bool>();
+            runtime.OnFailure += delegate
+            {
+                failed = true;
+                tcs.SetResult(true);
+            };
+
+            runtime.CreateMachine(machine, new E(tcs));
+
+            tcs.Task.Wait(100);
+            Assert.False(failed);
+        }
+
+        public void AssertFailed(Type machine)
+        {
+            var runtime = PSharpRuntime.Create();
+            var failed = false;
+            var tcs = new TaskCompletionSource<bool>();
+            runtime.OnFailure += delegate
+            {
+                failed = true;
+                tcs.SetResult(true);
+            };
+
+            runtime.CreateMachine(machine);
+
+            tcs.Task.Wait(100);
+            Assert.True(failed);
+        }
+
+        [Fact]
+        public void TestHaltCalled()
+        {
+            AssertFailed(typeof(M1));
+        }
+
+        [Fact]
+        public void TestReceiveOnHalt()
+        {
+            AssertFailed(typeof(M2a));
+        }
+
+        [Fact]
+        public void TestRaiseOnHalt()
+        {
+            AssertFailed(typeof(M2b));
+        }
+
+        [Fact]
+        public void TestGotoOnHalt()
+        {
+            AssertFailed(typeof(M2c));
+        }
+
+        [Fact]
+        public void TestAPIsOnHalt()
+        {
+            AssertSucceeded(typeof(M3));
+        }
+    }
+}