Merged PR 1265: hide Transition, but keep the same contract.

There is no reason to expose Transition objects and force users to "return" a Transition.  As is evidenced by the dangling Transition PR, it didn't actually improve things and the solution to dangling Transitions shows that exposing Transition is not required to ensure the same contract (namely, that only one is created per action) as shown by the internal PendingTransition member variable.

We also decided to rename some methods to make them all have a similar and therefore consistent name:

```
RaiseEvent is unchanged
Rename “GotoState” to “RaiseGotoStateEvent”
Rename “PushState” to “RaisePushStateEvent”
Rename “PopState” to “RaisePopStateEvent”
Rename “Halt” to “RaiseHaltEvent”
```

The idea being that the "Raise...Event" language more clearly communicates to the user that these operations are queuing something up to happen after the action completes and they are not processed immediately.  This also makes it easier for the user to remember the idea that currently you can only do one Raise operation per action.

Source/Core/Actors/Actor.cs

@@ -375,9 +375,9 @@ namespace Microsoft.Coyote.Actors
             this.Runtime.Assert(predicate, s, args);
 
         /// <summary>
-        /// Halts the actor at the end of the current action.
+        /// Raises a <see cref='HaltEvent'/> to halt the actor at the end of the current action.
         /// </summary>
-        protected void Halt()
+        protected virtual void RaiseHaltEvent()
         {
             this.Assert(this.CurrentStatus is Status.Active, "{0} invoked Halt while halting.", this.Id);
             this.CurrentStatus = Status.Halting;

Source/Core/Actors/StateMachine.cs

@@ -141,93 +141,167 @@ namespace Microsoft.Coyote.Actors
         }
 
         /// <summary>
-        /// Creates a transition that raises the specified <see cref="Event"/>
-        /// at the end of the current action.
+        /// 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.
+        /// Only one of the following can be called per action:
+        /// <see cref="StateMachine.RaiseEvent"/>, <see cref="StateMachine.RaiseGotoStateEvent{T}"/>,  <see cref="StateMachine.RaisePushStateEvent{T}"/> or
+        /// <see cref="StateMachine.RaisePopStateEvent"/> and <see cref="StateMachine.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>
-        /// <returns>The raise event transition.</returns>
-        protected Transition RaiseEvent(Event e)
+        protected void RaiseEvent(Event e)
         {
             this.Assert(this.CurrentStatus is Status.Active, "{0} invoked RaiseEvent while halting.", this.Id);
             this.Assert(e != null, "{0} is raising a null event.", this.Id);
             this.CheckDanglingTransition();
-            return this.PendingTransition = new Transition(Transition.Type.RaiseEvent, default, e);
+            this.PendingTransition = new Transition(Transition.Type.RaiseEvent, default, e);
         }
 
         /// <summary>
-        /// Creates a <see cref="StateMachine.Transition"/> that pops the current <see cref="State"/>
-        /// and pushes the specified <see cref="State"/> to the state stack
-        /// at the end of the current action.
+        /// Raise a special event that performs a goto state operation at the end of the current action.
         /// </summary>
+        /// <remarks>
+        /// Goto state pops the current <see cref="State"/> and pushes the specified <see cref="State"/> on the active state stack.
+        /// This is shorthand for the following code:
+        /// <code>
+        /// class Event E { }
+        /// [OnEventGotoState(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.
+        /// Only one of the following can be called per action:
+        /// <see cref="StateMachine.RaiseEvent"/>, <see cref="StateMachine.RaiseGotoStateEvent{T}"/>,  <see cref="StateMachine.RaisePushStateEvent{T}"/> or
+        /// <see cref="StateMachine.RaisePopStateEvent"/> and <see cref="StateMachine.RaiseHaltEvent"/>.
+        /// An Assert is raised if you accidentally try and do two of these operations in a single action.
+        /// </remarks>
         /// <typeparam name="S">Type of the state.</typeparam>
-        /// <returns>The goto state transition.</returns>
-        protected Transition GotoState<S>()
+        protected void RaiseGotoStateEvent<S>()
             where S : State =>
-            this.GotoState(typeof(S));
+            this.RaiseGotoStateEvent(typeof(S));
 
         /// <summary>
-        /// Creates a transition that pops the current <see cref="State"/>
-        /// and pushes the specified <see cref="State"/> to the state stack
-        /// at the end of the current action.
+        /// Raise a special event that performs a goto state operation at the end of the current action.
         /// </summary>
+        /// <remarks>
+        /// Goto state pops the current <see cref="State"/> and pushes the specified <see cref="State"/> on the active state stack.
+        /// This is shorthand for the following code:
+        /// <code>
+        /// class Event E { }
+        /// [OnEventGotoState(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.
+        /// Only one of the following can be called per action:
+        /// <see cref="StateMachine.RaiseEvent"/>, <see cref="StateMachine.RaiseGotoStateEvent{T}"/>,  <see cref="StateMachine.RaisePushStateEvent{T}"/> or
+        /// <see cref="StateMachine.RaisePopStateEvent"/> and <see cref="StateMachine.RaiseHaltEvent"/>.
+        /// An Assert is raised if you accidentally try and do two of these operations in a single action.
+        /// </remarks>
         /// <param name="state">Type of the state.</param>
-        /// <returns>The goto state transition.</returns>
-        protected Transition GotoState(Type state)
+        protected void RaiseGotoStateEvent(Type state)
         {
             this.Assert(this.CurrentStatus is Status.Active, "{0} invoked GotoState while halting.", this.Id);
             this.Assert(StateTypeCache[this.GetType()].Any(val => val.DeclaringType.Equals(state.DeclaringType) && val.Name.Equals(state.Name)),
                 "{0} is trying to transition to non-existing state '{1}'.", this.Id, state.Name);
             this.CheckDanglingTransition();
-            return this.PendingTransition = new Transition(Transition.Type.GotoState, state, default);
+            this.PendingTransition = new Transition(Transition.Type.GotoState, state, default);
         }
 
         /// <summary>
-        /// Creates a transition that pushes the specified <see cref="State"/> to
-        /// the state stack at the end of the current action.
+        /// Raise a special event that performs a push state operation at the end of the current action.
         /// </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.
+        /// 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.
+        /// Only one of the following can be called per action:
+        /// <see cref="StateMachine.RaiseEvent"/>, <see cref="StateMachine.RaiseGotoStateEvent{T}"/>,  <see cref="StateMachine.RaisePushStateEvent{T}"/> or
+        /// <see cref="StateMachine.RaisePopStateEvent"/> and <see cref="StateMachine.RaiseHaltEvent"/>.
+        /// An Assert is raised if you accidentally try and do two of these operations in a single action.
+        /// </remarks>
         /// <typeparam name="S">Type of the state.</typeparam>
-        /// <returns>The push state transition.</returns>
-        protected Transition PushState<S>()
+        protected void RaisePushStateEvent<S>()
             where S : State =>
-            this.PushState(typeof(S));
+            this.RasiePushStateEvent(typeof(S));
 
         /// <summary>
-        /// Creates a transition that pushes the specified <see cref="State"/> to
-        /// the state stack at the end of the current action.
+        /// Raise a special event that performs a push state operation at the end of the current action.
         /// </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.
+        /// 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.
+        /// Only one of the following can be called per action:
+        /// <see cref="StateMachine.RaiseEvent"/>, <see cref="StateMachine.RaiseGotoStateEvent{T}"/>,  <see cref="StateMachine.RaisePushStateEvent{T}"/> or
+        /// <see cref="StateMachine.RaisePopStateEvent"/> and <see cref="StateMachine.RaiseHaltEvent"/>.
+        /// An Assert is raised if you accidentally try and do two of these operations in a single action.
+        /// </remarks>
         /// <param name="state">Type of the state.</param>
-        /// <returns>The push state transition.</returns>
-        protected Transition PushState(Type state)
+        protected void RasiePushStateEvent(Type state)
         {
             this.Assert(this.CurrentStatus is Status.Active, "{0} invoked PushState while halting.", this.Id);
             this.Assert(StateTypeCache[this.GetType()].Any(val => val.DeclaringType.Equals(state.DeclaringType) && val.Name.Equals(state.Name)),
                 "{0} is trying to transition to non-existing state '{1}'.", this.Id, state.Name);
             this.CheckDanglingTransition();
-            return this.PendingTransition = new Transition(Transition.Type.PushState, state, default);
+            this.PendingTransition = new Transition(Transition.Type.PushState, state, default);
         }
 
         /// <summary>
-        /// Creates a transition that pops the current <see cref="State"/>
-        /// from the state stack at the end of the current action.
+        /// Raise a special event that performs a pop state operation at the end of the current action.
         /// </summary>
-        /// <returns>The pop state transition.</returns>
-        protected Transition PopState()
+        /// <remarks>
+        /// 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.
+        ///
+        /// Only one of the following can be called per action:
+        /// <see cref="StateMachine.RaiseEvent"/>, <see cref="StateMachine.RaiseGotoStateEvent{T}"/>,  <see cref="StateMachine.RaisePushStateEvent{T}"/> or
+        /// <see cref="StateMachine.RaisePopStateEvent"/> and <see cref="StateMachine.RaiseHaltEvent"/>.
+        /// An Assert is raised if you accidentally try and do two of these operations in a single action.
+        /// </remarks>
+        protected void RaisePopStateEvent()
         {
             this.Assert(this.CurrentStatus is Status.Active, "{0} invoked PopState while halting.", this.Id);
             this.CheckDanglingTransition();
-            return this.PendingTransition = new Transition(Transition.Type.PopState, null, default);
+            this.PendingTransition = new Transition(Transition.Type.PopState, null, default);
         }
 
         /// <summary>
-        /// Creates a transition that halts the state machine
-        /// at the end of the current action.
+        /// Raises a <see cref='HaltEvent'/> to halt the actor at the end of the current action.
         /// </summary>
-        /// <returns>The halt transition.</returns>
-        protected new Transition Halt()
+        /// <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:
+        /// <see cref="StateMachine.RaiseEvent"/>, <see cref="StateMachine.RaiseGotoStateEvent{T}"/>,  <see cref="StateMachine.RaisePushStateEvent{T}"/> or
+        /// <see cref="StateMachine.RaisePopStateEvent"/> and <see cref="StateMachine.RaiseHaltEvent"/>.
+        /// An Assert is raised if you accidentally try and do two of these operations in a single action.
+        /// </remarks>
+        protected override void RaiseHaltEvent()
         {
-            this.Assert(this.CurrentStatus is Status.Active, "{0} invoked Halt while halting.", this.Id);
+            base.RaiseHaltEvent();
             this.CheckDanglingTransition();
-            return this.PendingTransition = new Transition(Transition.Type.Halt, null, default);
+            this.PendingTransition = new Transition(Transition.Type.Halt, null, default);
         }
 
         /// <summary>
@@ -306,8 +380,8 @@ namespace Microsoft.Coyote.Actors
                 {
                     CachedDelegate cachedAction = this.ActionMap[actionEventHandler.Name];
                     this.Runtime.NotifyInvokedAction(this, cachedAction.MethodInfo, e);
-                    Transition transition = await this.InvokeActionAsync(cachedAction, e);
-                    await this.ApplyEventHandlerTransitionAsync(transition, e);
+                    await this.InvokeActionAsync(cachedAction, e);
+                    await this.ApplyEventHandlerTransitionAsync(this.PendingTransition, e);
                 }
                 else
                 {
@@ -328,22 +402,14 @@ namespace Microsoft.Coyote.Actors
         /// <summary>
         /// Invokes the specified action delegate.
         /// </summary>
-        private async Task<Transition> InvokeActionAsync(CachedDelegate cachedAction, Event e)
+        private async Task InvokeActionAsync(CachedDelegate cachedAction, Event e)
         {
             try
             {
                 if (cachedAction.IsAsync)
                 {
                     Task task = null;
-                    if (cachedAction.Handler is Func<Event, Task<Transition>> taskFuncWithEventAndResult)
-                    {
-                        task = taskFuncWithEventAndResult(e);
-                    }
-                    else if (cachedAction.Handler is Func<Task<Transition>> taskFuncWithResult)
-                    {
-                        task = taskFuncWithResult();
-                    }
-                    else if (cachedAction.Handler is Func<Event, Task> taskFuncWithEvent)
+                    if (cachedAction.Handler is Func<Event, Task> taskFuncWithEvent)
                     {
                         task = taskFuncWithEvent(e);
                     }
@@ -353,26 +419,10 @@ namespace Microsoft.Coyote.Actors
                     }
 
                     this.Runtime.NotifyWaitTask(this, task);
+                    await task;
+                }
 
-                    // We have no reliable stack for awaited operations.
-                    if (task is Task<Transition> taskWithResult)
-                    {
-                        return await taskWithResult;
-                    }
-                    else
-                    {
-                        await task;
-                    }
-                }
-                else if (cachedAction.Handler is Func<Event, Transition> funcWithEventAndResult)
-                {
-                    return funcWithEventAndResult(e);
-                }
-                else if (cachedAction.Handler is Func<Transition> funcWithResult)
-                {
-                    return funcWithResult();
-                }
-                else if (cachedAction.Handler is Action<Event> actionWithEvent)
+                if (cachedAction.Handler is Action<Event> actionWithEvent)
                 {
                     actionWithEvent(e);
                 }
@@ -396,8 +446,6 @@ namespace Microsoft.Coyote.Actors
             {
                 await this.TryHandleActionInvocationExceptionAsync(ex, cachedAction.MethodInfo.Name);
             }
-
-            return Transition.None;
         }
 
         /// <summary>
@@ -417,8 +465,8 @@ namespace Microsoft.Coyote.Actors
             if (entryAction != null)
             {
                 this.Runtime.NotifyInvokedOnEntryAction(this, entryAction.MethodInfo, e);
-                Transition transition = await this.InvokeActionAsync(entryAction, e);
-                await this.ApplyEventHandlerTransitionAsync(transition, e);
+                await this.InvokeActionAsync(entryAction, e);
+                await this.ApplyEventHandlerTransitionAsync(this.PendingTransition, e);
             }
         }
 
@@ -440,7 +488,8 @@ namespace Microsoft.Coyote.Actors
             if (exitAction != null)
             {
                 this.Runtime.NotifyInvokedOnExitAction(this, exitAction.MethodInfo, e);
-                Transition transition = await this.InvokeActionAsync(exitAction, e);
+                await this.InvokeActionAsync(exitAction, e);
+                Transition transition = this.PendingTransition;
                 this.Assert(transition.TypeValue is Transition.Type.None ||
                     transition.TypeValue is Transition.Type.Halt,
                     "{0} has performed a '{1}' transition from an OnExit action.",
@@ -454,7 +503,8 @@ namespace Microsoft.Coyote.Actors
             {
                 CachedDelegate eventHandlerExitAction = this.ActionMap[eventHandlerExitActionName];
                 this.Runtime.NotifyInvokedOnExitAction(this, eventHandlerExitAction.MethodInfo, e);
-                Transition transition = await this.InvokeActionAsync(eventHandlerExitAction, e);
+                await this.InvokeActionAsync(eventHandlerExitAction, e);
+                Transition transition = this.PendingTransition;
                 this.Assert(transition.TypeValue is Transition.Type.None ||
                     transition.TypeValue is Transition.Type.Halt,
                     "{0} has performed a '{1}' transition from an OnExit action.",
@@ -1093,8 +1143,8 @@ namespace Microsoft.Coyote.Actors
         /// <summary>
         /// Defines the <see cref="StateMachine"/> transition that is the
         /// result of executing an event handler.  Transitions are created by using
-        /// <see cref="StateMachine.GotoState{T}"/>, <see cref="StateMachine.RaiseEvent"/>, <see cref="StateMachine.PushState{T}"/> or
-        /// <see cref="StateMachine.PopState"/> and <see cref="StateMachine.Halt"/>.
+        /// <see cref="StateMachine.RaiseGotoStateEvent{T}"/>, <see cref="StateMachine.RaiseEvent"/>, <see cref="StateMachine.RaisePushStateEvent{T}"/> or
+        /// <see cref="StateMachine.RaisePopStateEvent"/> and <see cref="StateMachine.RaiseHaltEvent"/>.
         /// The Transition is processed by the Coyote runtime when
         /// an event handling method of a StateMachine returns a Transition object.
         /// This means such a method can only do one such Transition per method call.
@@ -1104,7 +1154,7 @@ namespace Microsoft.Coyote.Actors
         /// <remarks>
         /// See <see href="/coyote/learn/programming-models/actors/state-machines">State machines</see> for more information.
         /// </remarks>
-        public readonly struct Transition
+        internal readonly struct Transition
         {
             /// <summary>
             /// The type of the transition.
@@ -1157,26 +1207,26 @@ namespace Microsoft.Coyote.Actors
                 RaiseEvent,
 
                 /// <summary>
-                /// A transition created by <see cref="StateMachine.GotoState{S}"/> that pops the current <see cref="StateMachine.State"/>
+                /// A transition created by <see cref="StateMachine.RaiseGotoStateEvent{S}"/> that pops the current <see cref="StateMachine.State"/>
                 /// and pushes the specified <see cref="StateMachine.State"/> on the
                 /// stack of <see cref="StateMachine"/> states.
                 /// </summary>
                 GotoState,
 
                 /// <summary>
-                /// A transition created by <see cref="StateMachine.PushState{S}"/> that pushes the specified <see cref="StateMachine.State"/>
+                /// A transition created by <see cref="StateMachine.RaisePushStateEvent{S}"/> that pushes the specified <see cref="StateMachine.State"/>
                 /// on the stack of <see cref="StateMachine"/> states.
                 /// </summary>
                 PushState,
 
                 /// <summary>
-                /// A transition created by <see cref="StateMachine.PopState"/> that pops the current <see cref="StateMachine.State"/>
+                /// A transition created by <see cref="StateMachine.RaisePopStateEvent"/> that pops the current <see cref="StateMachine.State"/>
                 /// from the stack of <see cref="StateMachine"/> states.
                 /// </summary>
                 PopState,
 
                 /// <summary>
-                /// A transition created by <see cref="StateMachine.Halt"/> that halts the <see cref="StateMachine"/>.
+                /// A transition created by <see cref="StateMachine.RaiseHaltEvent"/> that halts the <see cref="StateMachine"/>.
                 /// </summary>
                 Halt
             }

Source/Core/Specifications/Monitors/Monitor.cs

@@ -174,40 +174,72 @@ namespace Microsoft.Coyote.Specifications
         }
 
         /// <summary>
-        /// Raises an <see cref="Event"/> at the end of the current action.
+        /// 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.
+        /// Only one of the following can be called per action:
+        /// <see cref="Monitor.RaiseEvent"/>, <see cref="Monitor.RaiseGotoStateEvent{T}"/>.
+        /// 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>
-        /// <returns>The raise event transition.</returns>
-        protected Transition RaiseEvent(Event e)
+        protected void RaiseEvent(Event e)
         {
             this.Assert(e != null, "{0} is raising a null event.", this.GetType().Name);
             this.CheckDanglingTransition();
-            return this.PendingTransition = new Transition(Transition.Type.Raise, default, e);
+            this.PendingTransition = new Transition(Transition.Type.Raise, default, e);
         }
 
         /// <summary>
-        /// Transitions the monitor to the specified <see cref="State"/>
-        /// at the end of the current action.
+        /// Raise a special event that performs a goto state operation at the end of the current action.
         /// </summary>
+        /// <remarks>
+        /// Goto state pops the current <see cref="State"/> and pushes the specified <see cref="State"/> on the active state stack.
+        ///
+        /// This is shorthand for the following code:
+        /// <code>
+        /// class Event E { }
+        /// [OnEventGotoState(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.
+        /// Only one of the following can be called per action:
+        /// <see cref="Monitor.RaiseEvent"/>, <see cref="Monitor.RaiseGotoStateEvent{T}"/>.
+        /// An Assert is raised if you accidentally try and do two of these operations in a single action.
+        /// </remarks>
         /// <typeparam name="S">Type of the state.</typeparam>
-        /// <returns>The goto state transition.</returns>
-        protected Transition GotoState<S>()
+        protected void RaiseGotoStateEvent<S>()
             where S : State =>
-            this.GotoState(typeof(S));
+            this.RaiseGotoStateEvent(typeof(S));
 
         /// <summary>
-        /// Transitions the monitor to the specified <see cref="State"/>
-        /// at the end of the current action.
+        /// Raise a special event that performs a goto state operation at the end of the current action.
         /// </summary>
+        /// <remarks>
+        /// Goto state pops the current <see cref="State"/> and pushes the specified <see cref="State"/> on the active state stack.
+        ///
+        /// This is shorthand for the following code:
+        /// <code>
+        /// class Event E { }
+        /// [OnEventGotoState(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.
+        /// Only one of the following can be called per action:
+        /// <see cref="Monitor.RaiseEvent"/>, <see cref="Monitor.RaiseGotoStateEvent{T}"/>.
+        /// An Assert is raised if you accidentally try and do two of these operations in a single action.
+        /// </remarks>
         /// <param name="state">Type of the state.</param>
-        /// <returns>The goto state transition.</returns>
-        protected Transition GotoState(Type state)
+        protected void RaiseGotoStateEvent(Type state)
         {
             // If the state is not a state of the monitor, then report an error and exit.
             this.Assert(StateTypeMap[this.GetType()].Any(val => val.DeclaringType.Equals(state.DeclaringType) && val.Name.Equals(state.Name)),
                 "{0} is trying to transition to non-existing state '{1}'.", this.GetType().Name, state.Name);
             this.CheckDanglingTransition();
-            return this.PendingTransition = new Transition(Transition.Type.Goto, state, default);
+            this.PendingTransition = new Transition(Transition.Type.Goto, state, default);
         }
 
         /// <summary>
@@ -329,8 +361,8 @@ namespace Microsoft.Coyote.Specifications
         {
             CachedDelegate cachedAction = this.ActionMap[actionName];
             this.Runtime.NotifyInvokedAction(this, cachedAction.MethodInfo, e);
-            Transition transition = this.ExecuteAction(cachedAction, e);
-            this.ApplyEventHandlerTransition(transition);
+            this.ExecuteAction(cachedAction, e);
+            this.ApplyEventHandlerTransition(this.PendingTransition);
         }
 
         /// <summary>
@@ -351,8 +383,8 @@ namespace Microsoft.Coyote.Specifications
             // if there is one available.
             if (entryAction != null)
             {
-                Transition transition = this.ExecuteAction(entryAction, e);
-                this.ApplyEventHandlerTransition(transition);
+                this.ExecuteAction(entryAction, e);
+                this.ApplyEventHandlerTransition(this.PendingTransition);
             }
         }
 
@@ -374,7 +406,8 @@ namespace Microsoft.Coyote.Specifications
             // if there is one available.
             if (exitAction != null)
             {
-                Transition transition = this.ExecuteAction(exitAction, e);
+                this.ExecuteAction(exitAction, e);
+                Transition transition = this.PendingTransition;
                 this.Assert(transition.TypeValue is Transition.Type.None,
                     "{0} has performed a '{1}' transition from an OnExit action.",
                     this.Id, transition.TypeValue);
@@ -386,7 +419,8 @@ namespace Microsoft.Coyote.Specifications
             if (eventHandlerExitActionName != null)
             {
                 CachedDelegate eventHandlerExitAction = this.ActionMap[eventHandlerExitActionName];
-                Transition transition = this.ExecuteAction(eventHandlerExitAction, e);
+                this.ExecuteAction(eventHandlerExitAction, e);
+                Transition transition = this.PendingTransition;
                 this.Assert(transition.TypeValue is Transition.Type.None,
                     "{0} has performed a '{1}' transition from an OnExit action.",
                     this.Id, transition.TypeValue);
@@ -398,19 +432,11 @@ namespace Microsoft.Coyote.Specifications
         /// Executes the specified action.
         /// </summary>
         [System.Diagnostics.DebuggerStepThrough]
-        private Transition ExecuteAction(CachedDelegate cachedAction, Event e)
+        private void ExecuteAction(CachedDelegate cachedAction, Event e)
         {
             try
             {
-                if (cachedAction.Handler is Func<Event, Transition> funcWithEventAndResult)
-                {
-                    return funcWithEventAndResult(e);
-                }
-                else if (cachedAction.Handler is Func<Transition> funcWithResult)
-                {
-                    return funcWithResult();
-                }
-                else if (cachedAction.Handler is Action<Event> actionWithEvent)
+                if (cachedAction.Handler is Action<Event> actionWithEvent)
                 {
                     actionWithEvent(e);
                 }
@@ -443,8 +469,6 @@ namespace Microsoft.Coyote.Specifications
                     this.ReportUnhandledException(innerException, cachedAction.MethodInfo.Name);
                 }
             }
-
-            return Transition.None;
         }
 
         /// <summary>
@@ -936,14 +960,14 @@ namespace Microsoft.Coyote.Specifications
         /// <summary>
         /// Defines the <see cref="Monitor"/> transition that is the
         /// result of executing an event handler.  Transitions are created by using
-        /// <see cref="Monitor.GotoState{T}"/>, or <see cref="Monitor.RaiseEvent"/>.
+        /// <see cref="Monitor.RaiseGotoStateEvent{T}"/>, or <see cref="Monitor.RaiseEvent"/>.
         /// The Transition is processed by the Coyote runtime when
         /// an event handling method returns a Transition object.
         /// This means such a method can only do one such Transition per method call.
         /// If the method wants to do a conditional transition it can return
         /// Transition.None to indicate no transition is to be performed.
         /// </summary>
-        public readonly struct Transition
+        internal readonly struct Transition
         {
             /// <summary>
             /// The type of the transition.
@@ -996,7 +1020,7 @@ namespace Microsoft.Coyote.Specifications
                 Raise,
 
                 /// <summary>
-                /// A transition created by <see cref="Monitor.GotoState{S}"/> from the current <see cref="Monitor.State"/>
+                /// A transition created by <see cref="Monitor.RaiseGotoStateEvent{S}"/> from the current <see cref="Monitor.State"/>
                 /// to the specified <see cref="Monitor.State"/>.
                 /// </summary>
                 Goto

Source/TestingServices/Actors/Timers/MockStateMachineTimer.cs

@@ -66,7 +66,7 @@ namespace Microsoft.Coyote.TestingServices.Timers
         /// <summary>
         /// Handles the timeout.
         /// </summary>
-        private Transition HandleTimeout()
+        private void HandleTimeout()
         {
             // Try to send the next timeout event.
             bool isTimeoutSent = false;
@@ -84,10 +84,8 @@ namespace Microsoft.Coyote.TestingServices.Timers
             // inactive until disposal. Else retry.
             if (isTimeoutSent && this.TimerInfo.Period.TotalMilliseconds < 0)
             {
-                return this.GotoState<Inactive>();
+                this.RaiseGotoStateEvent<Inactive>();
             }
-
-            return default;
         }
 
         private class Inactive : State

Tests/Core.Tests/Actors/StateMachines/GotoStateTransitionTests.cs

@@ -28,7 +28,7 @@ namespace Microsoft.Coyote.Core.Tests.Actors.StateMachines
             {
             }
 
-            private Transition InitOnEntry() => this.GotoState<Final>();
+            private void InitOnEntry() => this.RaiseGotoStateEvent<Final>();
 
             private class Final : State
             {
@@ -57,7 +57,7 @@ namespace Microsoft.Coyote.Core.Tests.Actors.StateMachines
             {
             }
 
-            private Transition InitOnEntry() => this.RaiseEvent(new Message());
+            private void InitOnEntry() => this.RaiseEvent(new Message());
 
             private class Final : State
             {

Tests/Core.Tests/Actors/StateMachines/MemoryLeak/NoMemoryLeakAfterHaltTests.cs

@@ -86,11 +86,11 @@ namespace Microsoft.Coyote.Core.Tests.Actors.StateMachines
                 this.LargeArray[this.LargeArray.Length - 1] = 1;
             }
 
-            private Transition Act(Event e)
+            private void Act(Event e)
             {
                 var sender = (e as E).Id;
                 this.SendEvent(sender, new E(this.Id));
-                return this.Halt();
+                this.RaiseHaltEvent();
             }
         }
 

Tests/Core.Tests/Actors/StateMachines/OnEventDroppedTests.cs

@@ -151,10 +151,10 @@ namespace Microsoft.Coyote.Core.Tests.Actors.StateMachines
             {
             }
 
-            private Transition InitOnEntry(Event e)
+            private void InitOnEntry(Event e)
             {
                 this.Tcs = (e as E).Tcs;
-                return this.GotoState<S1>();
+                this.RaiseGotoStateEvent<S1>();
             }
 
             [OnEventGotoState(typeof(EventProcessed), typeof(S2))]

Tests/Core.Tests/Actors/StateMachines/OnHaltTests.cs

@@ -43,7 +43,7 @@ namespace Microsoft.Coyote.Core.Tests.Actors.StateMachines
             {
             }
 
-            private Transition InitOnEntry() => this.Halt();
+            private void InitOnEntry() => this.RaiseHaltEvent();
 
             protected override Task OnHaltAsync(Event e)
             {
@@ -80,7 +80,7 @@ namespace Microsoft.Coyote.Core.Tests.Actors.StateMachines
             {
             }
 
-            private Transition InitOnEntry() => this.Halt();
+            private void InitOnEntry() => this.RaiseHaltEvent();
 
             protected override async Task OnHaltAsync(Event e)
             {
@@ -116,7 +116,7 @@ namespace Microsoft.Coyote.Core.Tests.Actors.StateMachines
             {
             }
 
-            private Transition InitOnEntry() => this.Halt();
+            private void InitOnEntry() => this.RaiseHaltEvent();
         }
 
         private class M3 : StateMachine
@@ -129,10 +129,10 @@ namespace Microsoft.Coyote.Core.Tests.Actors.StateMachines
             {
             }
 
-            private Transition InitOnEntry(Event e)
+            private void InitOnEntry(Event e)
             {
                 this.tcs = (e as E).Tcs;
-                return this.Halt();
+                this.RaiseHaltEvent();
             }
 
             protected override Task OnHaltAsync(Event e)

Tests/Core.Tests/Actors/Timers/TimerStressTests.cs

@@ -46,10 +46,10 @@ namespace Microsoft.Coyote.Core.Tests.Actors
                 this.StartTimer(TimeSpan.FromTicks(1));
             }
 
-            private Transition HandleTimeout()
+            private void HandleTimeout()
             {
                 this.Tcs.SetResult(true);
-                return this.Halt();
+                this.RaiseHaltEvent();
             }
         }
 
@@ -93,16 +93,14 @@ namespace Microsoft.Coyote.Core.Tests.Actors
                 this.StartPeriodicTimer(TimeSpan.FromTicks(1), TimeSpan.FromTicks(1));
             }
 
-            private Transition HandleTimeout()
+            private void HandleTimeout()
             {
                 this.Counter++;
                 if (this.Counter == 10)
                 {
                     this.Tcs.SetResult(true);
-                    return this.Halt();
+                    this.RaiseHaltEvent();
                 }
-
-                return default;
             }
         }
 

Tests/Core.Tests/Actors/Timers/TimerTests.cs

@@ -62,7 +62,7 @@ namespace Microsoft.Coyote.Core.Tests.Actors
                 this.StartTimer(TimeSpan.FromMilliseconds(10));
             }
 
-            private Transition HandleTimeout()
+            private void HandleTimeout()
             {
                 this.Count++;
                 if (this.Count == 1)
@@ -74,7 +74,7 @@ namespace Microsoft.Coyote.Core.Tests.Actors
                     this.Tcs.SetResult(false);
                 }
 
-                return this.Halt();
+                this.RaiseHaltEvent();
             }
         }
 
@@ -114,17 +114,15 @@ namespace Microsoft.Coyote.Core.Tests.Actors
                 this.Timer = this.StartPeriodicTimer(TimeSpan.FromMilliseconds(10), TimeSpan.FromMilliseconds(10));
             }
 
-            private Transition HandleTimeout()
+            private void HandleTimeout()
             {
                 this.Count++;
                 if (this.Count == 10)
                 {
                     this.StopTimer(this.Timer);
                     this.Tcs.SetResult(true);
-                    return this.Halt();
+                    this.RaiseHaltEvent();
                 }
-
-                return Transition.None;
             }
         }
 
@@ -169,13 +167,13 @@ namespace Microsoft.Coyote.Core.Tests.Actors
             {
             }
 
-            private async Task<Transition> DoPing(Event e)
+            private async Task DoPing(Event e)
             {
                 this.Tcs = (e as SetupEvent).Tcs;
                 this.PingTimer = this.StartPeriodicTimer(TimeSpan.FromMilliseconds(5), TimeSpan.FromMilliseconds(5));
                 await Task.Delay(100);
                 this.StopTimer(this.PingTimer);
-                return this.GotoState<Pong>();
+                this.RaiseGotoStateEvent<Pong>();
             }
 
             private void DoPong()
@@ -183,7 +181,7 @@ namespace Microsoft.Coyote.Core.Tests.Actors
                 this.PongTimer = this.StartPeriodicTimer(TimeSpan.FromMilliseconds(50), TimeSpan.FromMilliseconds(50));
             }
 
-            private Transition HandleTimeout(Event e)
+            private void HandleTimeout(Event e)
             {
                 var timeout = e as TimerElapsedEvent;
                 if (timeout.Info == this.PongTimer)
@@ -195,7 +193,7 @@ namespace Microsoft.Coyote.Core.Tests.Actors
                     this.Tcs.SetResult(false);
                 }
 
-                return this.Halt();
+                this.RaiseHaltEvent();
             }
         }
 
@@ -220,10 +218,9 @@ namespace Microsoft.Coyote.Core.Tests.Actors
             {
             }
 
-            private Transition Initialize(Event e)
+            private void Initialize(Event e)
             {
                 var tcs = (e as SetupEvent).Tcs;
-
                 try
                 {
                     this.StartTimer(TimeSpan.FromSeconds(-1));
@@ -232,11 +229,12 @@ namespace Microsoft.Coyote.Core.Tests.Actors
                 {
                     this.Logger.WriteLine(ex.Message);
                     tcs.SetResult(true);
-                    return this.Halt();
+                    this.RaiseHaltEvent();
+                    return;
                 }
 
                 tcs.SetResult(false);
-                return this.Halt();
+                this.RaiseHaltEvent();
             }
         }
 
@@ -261,10 +259,9 @@ namespace Microsoft.Coyote.Core.Tests.Actors
             {
             }
 
-            private Transition Initialize(Event e)
+            private void Initialize(Event e)
             {
                 var tcs = (e as SetupEvent).Tcs;
-
                 try
                 {
                     this.StartPeriodicTimer(TimeSpan.FromSeconds(1), TimeSpan.FromSeconds(-1));
@@ -273,11 +270,12 @@ namespace Microsoft.Coyote.Core.Tests.Actors
                 {
                     this.Logger.WriteLine(ex.Message);
                     tcs.SetResult(true);
-                    return this.Halt();
+                    this.RaiseHaltEvent();
+                    return;
                 }
 
                 tcs.SetResult(false);
-                return this.Halt();
+                this.RaiseHaltEvent();
             }
         }
 
@@ -322,7 +320,7 @@ namespace Microsoft.Coyote.Core.Tests.Actors
             {
             }
 
-            private Transition Initialize(Event e)
+            private void Initialize(Event e)
             {
                 var ce = e as ConfigEvent;
                 this.Config = ce;
@@ -345,13 +343,11 @@ namespace Microsoft.Coyote.Core.Tests.Actors
                 {
                     this.Logger.WriteLine(ex.Message);
                     ce.Tcs.SetResult(expectError == true);
-                    return this.Halt();
+                    this.RaiseHaltEvent();
                 }
-
-                return default;
             }
 
-            private Transition OnMyTimeout(Event e)
+            private void OnMyTimeout(Event e)
             {
                 if (e is MyTimeoutEvent)
                 {
@@ -363,7 +359,7 @@ namespace Microsoft.Coyote.Core.Tests.Actors
                     this.Config.Tcs.SetResult(false);
                 }
 
-                return this.Halt();
+                this.RaiseHaltEvent();
             }
         }
 

Tests/Core.Tests/Runtime/CustomActorRuntimeLogTests.cs

@@ -81,7 +81,7 @@ namespace Microsoft.Coyote.Core.Tests.Runtime
             {
             }
 
-            private Transition OnE() => this.GotoState<Done>();
+            private void OnE() => this.RaiseGotoStateEvent<Done>();
         }
 
         internal class N : StateMachine

Tests/Core.Tests/Runtime/SendAndExecuteTests.cs

@@ -222,7 +222,7 @@ namespace Microsoft.Coyote.Core.Tests.Runtime
             {
             }
 
-            private Transition HandleE() => this.Halt();
+            private void HandleE() => this.RaiseHaltEvent();
 
             protected override Task OnHaltAsync(Event e)
             {
@@ -255,11 +255,11 @@ namespace Microsoft.Coyote.Core.Tests.Runtime
                 this.MHalted = true;
             }
 
-            private Transition OnSEReturns()
+            private void OnSEReturns()
             {
                 this.Assert(this.MHalted);
                 this.SEReturned = true;
-                return this.GotoState<Done>();
+                this.RaiseGotoStateEvent<Done>();
             }
         }
 

Tests/TestingServices.Tests/Actors/Callbacks/OnEventHandledTests.cs

@@ -74,7 +74,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition Process(Event e)
+            private void Process(Event e)
             {
                 if (this.Counter == 0 && e is Begin beginE1 && beginE1.Event is UnitEvent)
                 {
@@ -99,10 +99,8 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
 
                 if (this.Counter == 4)
                 {
-                    return this.GotoState<S2>();
+                    this.RaiseGotoStateEvent<S2>();
                 }
-
-                return default;
             }
         }
 
@@ -116,9 +114,9 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition Process()
+            private void Process()
             {
-                return this.RaiseEvent(new E2());
+                this.RaiseEvent(new E2());
             }
 
             private void ProcessE3()
@@ -172,7 +170,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition Process(Event e)
+            private void Process(Event e)
             {
                 if (this.Counter == 0 && e is Begin beginE1 && beginE1.Event is UnitEvent)
                 {
@@ -189,17 +187,15 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
 
                 if (this.Counter == 2)
                 {
-                    return this.GotoState<S2>();
+                    this.RaiseGotoStateEvent<S2>();
                 }
-
-                return default;
             }
         }
 
         [OnEventDoAction(typeof(UnitEvent), nameof(Process))]
         private class A2 : Actor
         {
-            private void Process() => this.Halt();
+            private void Process() => this.RaiseHaltEvent();
 
             protected override Task OnEventDequeuedAsync(Event e)
             {
@@ -233,9 +229,9 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition Process()
+            private void Process()
             {
-                return this.RaiseEvent(HaltEvent.Instance);
+                this.RaiseEvent(HaltEvent.Instance);
             }
 
             protected override Task OnEventDequeuedAsync(Event e)

Tests/TestingServices.Tests/Actors/Callbacks/OnExceptionTests.cs

@@ -142,9 +142,9 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
-                return this.RaiseEvent(new E(this.Id));
+                this.RaiseEvent(new E(this.Id));
             }
 
             private void Act()
@@ -216,9 +216,9 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
-                return this.RaiseEvent(new E(this.Id));
+                this.RaiseEvent(new E(this.Id));
             }
 
             private async Task Act()
@@ -257,9 +257,9 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
-                return this.RaiseEvent(new E(this.Id));
+                this.RaiseEvent(new E(this.Id));
             }
 
             private void InitOnExit()

Tests/TestingServices.Tests/Actors/Callbacks/OnHaltTests.cs

@@ -94,7 +94,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry() => this.Halt();
+            private void InitOnEntry() => this.RaiseHaltEvent();
 
             protected override Task OnHaltAsync(Event e)
             {
@@ -147,7 +147,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry() => this.Halt();
+            private void InitOnEntry() => this.RaiseHaltEvent();
 
             protected override async Task OnHaltAsync(Event e)
             {
@@ -174,7 +174,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry() => this.Halt();
+            private void InitOnEntry() => this.RaiseHaltEvent();
         }
 
         private class M4Receiver : StateMachine
@@ -228,10 +228,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry(Event e)
+            private void InitOnEntry(Event e)
             {
                 this.Receiver = (e as E).Id;
-                return this.Halt();
+                this.RaiseHaltEvent();
             }
 
             protected override Task OnHaltAsync(Event e)

Tests/TestingServices.Tests/Actors/Creation/CreateActorWithIdTests.cs

@@ -130,10 +130,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 }
             }
 
-            private Transition Terminate(Event e)
+            private void Terminate(Event e)
             {
                 this.SendEvent((e as TerminateReq).Sender, new TerminateResp());
-                return this.Halt();
+                this.RaiseHaltEvent();
             }
         }
 

Tests/TestingServices.Tests/Actors/Declarations/GenericStateMachineTests.cs

@@ -24,10 +24,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
                 this.Item = default;
-                return this.GotoState<Active>();
+                this.RaiseGotoStateEvent<Active>();
             }
 
             [OnEntry(nameof(ActiveInit))]

Tests/TestingServices.Tests/Actors/Declarations/NameofTests.cs

@@ -41,10 +41,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            protected Transition Coyote_Init_on_entry_action()
+            protected void Coyote_Init_on_entry_action()
             {
                 WithNameofValue += 1;
-                return this.RaiseEvent(new E1());
+                this.RaiseEvent(new E1());
             }
 
             protected void Coyote_Init_on_exit_action()
@@ -52,10 +52,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 WithNameofValue += 10;
             }
 
-            protected Transition Coyote_Next_on_entry_action()
+            protected void Coyote_Next_on_entry_action()
             {
                 WithNameofValue += 1000;
-                return this.RaiseEvent(new E2());
+                this.RaiseEvent(new E2());
             }
 
             protected void Coyote_Init_E1_action()
@@ -85,10 +85,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            protected Transition Coyote_Init_on_entry_action()
+            protected void Coyote_Init_on_entry_action()
             {
                 WithoutNameofValue += 1;
-                return this.RaiseEvent(new E1());
+                this.RaiseEvent(new E1());
             }
 
             protected void Coyote_Init_on_exit_action()
@@ -96,10 +96,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 WithoutNameofValue += 10;
             }
 
-            protected Transition Coyote_Next_on_entry_action()
+            protected void Coyote_Next_on_entry_action()
             {
                 WithoutNameofValue += 1000;
-                return this.RaiseEvent(new E2());
+                this.RaiseEvent(new E2());
             }
 
             protected void Coyote_Init_E1_action()

Tests/TestingServices.Tests/Actors/EventHandling/EventHandlerTests.cs

@@ -146,10 +146,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
                 this.SendEvent(this.Id, new E1());
-                return this.RaiseEvent(UnitEvent.Instance);
+                this.RaiseEvent(UnitEvent.Instance);
             }
 
             private void HandleUnitEvent()
@@ -485,11 +485,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition ActiveOnEntry()
+            private void ActiveOnEntry()
             {
                 this.Test = true;
                 this.SendEvent(this.Id, new E2());
-                return this.PopState();
+                this.RaisePopStateEvent();
             }
 
             private void HandleE2()
@@ -704,10 +704,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition ActiveOnEntry()
+            private void ActiveOnEntry()
             {
                 this.Test = true;
-                return this.PopState();
+                this.RaisePopStateEvent();
             }
 
             private void ActiveOnExit()
@@ -759,7 +759,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition ActiveOnEntry() => this.RaiseEvent(UnitEvent.Instance);
+            private void ActiveOnEntry() => this.RaiseEvent(UnitEvent.Instance);
 
             private void HandleE2()
             {
@@ -786,7 +786,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry() => this.RaiseEvent(UnitEvent.Instance);
+            private void InitOnEntry() => this.RaiseEvent(UnitEvent.Instance);
 
             [OnEntry(nameof(ActiveOnEntry))]
             [OnExit(nameof(ActiveOnExit))]
@@ -794,7 +794,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition ActiveOnEntry() => this.PopState();
+            private void ActiveOnEntry() => this.RaisePopStateEvent();
 
             private void ActiveOnExit()
             {
@@ -825,10 +825,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
                 this.SendEvent(this.Id, UnitEvent.Instance);
-                return this.RaiseEvent(HaltEvent.Instance);
+                this.RaiseEvent(HaltEvent.Instance);
             }
 
             [OnEntry(nameof(ActiveOnEntry))]
@@ -871,7 +871,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry() => this.RaiseEvent(new E1());
+            private void InitOnEntry() => this.RaiseEvent(new E1());
 
             private void HandleUnitEvent()
             {
@@ -949,10 +949,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
                 this.Value = 0;
-                return this.RaiseEvent(UnitEvent.Instance);
+                this.RaiseEvent(UnitEvent.Instance);
             }
 
             private void DefaultAction()
@@ -966,18 +966,16 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition ActiveOnEntry()
+            private void ActiveOnEntry()
             {
                 if (this.Value == 0)
                 {
-                    return this.RaiseEvent(UnitEvent.Instance);
+                    this.RaiseEvent(UnitEvent.Instance);
                 }
                 else
                 {
                     this.Value++;
                 }
-
-                return default;
             }
         }
 
@@ -1052,10 +1050,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition EntryS1()
+            private void EntryS1()
             {
                 this.Assert(this.Test == true); // Holds.
-                return this.RaiseEvent(UnitEvent.Instance);
+                this.RaiseEvent(UnitEvent.Instance);
             }
 
             [OnEntry(nameof(EntryS2))]
@@ -1134,11 +1132,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
                 this.GhostMachine = this.CreateActor(typeof(M22b));
                 this.SendEvent(this.GhostMachine, new SetupEvent(this.Id));
-                return this.RaiseEvent(UnitEvent.Instance);
+                this.RaiseEvent(UnitEvent.Instance);
             }
 
             [OnEntry(nameof(EntryS1))]
@@ -1239,11 +1237,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
                 this.GhostMachine = this.CreateActor(typeof(M23b));
                 this.SendEvent(this.GhostMachine, new SetupEvent(this.Id));
-                return this.RaiseEvent(UnitEvent.Instance);
+                this.RaiseEvent(UnitEvent.Instance);
             }
 
             [OnEntry(nameof(EntryS1))]

Tests/TestingServices.Tests/Actors/EventHandling/IgnoreEventTests.cs

@@ -67,7 +67,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition Foo() => this.RaiseEvent(UnitEvent.Instance);
+            private void Foo() => this.RaiseEvent(UnitEvent.Instance);
 
             private void Bar(Event e)
             {

Tests/TestingServices.Tests/Actors/EventHandling/MaxEventInstancesTests.cs

@@ -61,11 +61,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
                 this.N = this.CreateActor(typeof(N));
                 this.SendEvent(this.N, new SetupEvent(this.Id));
-                return this.RaiseEvent(UnitEvent.Instance);
+                this.RaiseEvent(UnitEvent.Instance);
             }
 
             [OnEntry(nameof(EntryS1))]
@@ -85,7 +85,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition EntryS2() => this.RaiseEvent(UnitEvent.Instance);
+            private void EntryS2() => this.RaiseEvent(UnitEvent.Instance);
 
             [OnEventGotoState(typeof(E4), typeof(S3))]
             private class S3 : State
@@ -111,10 +111,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition SetupEvent(Event e)
+            private void SetupEvent(Event e)
             {
                 this.M = (e as SetupEvent).Id;
-                return this.RaiseEvent(UnitEvent.Instance);
+                this.RaiseEvent(UnitEvent.Instance);
             }
 
             [OnEventGotoState(typeof(E1), typeof(S1))]

Tests/TestingServices.Tests/Actors/EventHandling/MustHandleEventTests.cs

@@ -75,7 +75,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry() => this.Halt();
+            private void InitOnEntry() => this.RaiseHaltEvent();
         }
 
         [Fact(Timeout = 5000)]

Tests/TestingServices.Tests/Actors/EventHandling/ReceiveEventTests.cs

@@ -98,7 +98,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                     this.SendPong();
                 }
 
-                this.Halt();
+                this.RaiseHaltEvent();
             }
 
             private void SendPong()
@@ -215,11 +215,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition SetupEvent(Event e)
+            private void SetupEvent(Event e)
             {
                 this.Server = (e as SetupEvent).Id;
                 this.Counter = 0;
-                return this.RaiseEvent(UnitEvent.Instance);
+                this.RaiseEvent(UnitEvent.Instance);
             }
 
             [OnEntry(nameof(ActiveOnEntry))]
@@ -227,7 +227,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private async Task<Transition> ActiveOnEntry()
+            private async Task ActiveOnEntry()
             {
                 while (this.Counter < 5)
                 {
@@ -235,7 +235,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                     this.SendPong();
                 }
 
-                return this.Halt();
+                this.RaiseHaltEvent();
             }
 
             private void SendPong()
@@ -256,11 +256,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
                 this.Client = this.CreateActor(typeof(ClientStateMachine));
                 this.SendEvent(this.Client, new SetupEvent(this.Id));
-                return this.RaiseEvent(UnitEvent.Instance);
+                this.RaiseEvent(UnitEvent.Instance);
             }
 
             [OnEntry(nameof(ActiveOnEntry))]
@@ -301,11 +301,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
                 this.Client = this.CreateActor(typeof(ClientStateMachine));
                 this.SendEvent(this.Client, new SetupEvent(this.Id));
-                return this.RaiseEvent(UnitEvent.Instance);
+                this.RaiseEvent(UnitEvent.Instance);
             }
 
             [OnEntry(nameof(ActiveOnEntry))]

Tests/TestingServices.Tests/Actors/Integration/ChainReplicationTests.cs

@@ -199,7 +199,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry(Event e)
+            private void InitOnEntry(Event e)
             {
                 this.Master = (e as SetupEvent).Master;
                 this.Servers = (e as SetupEvent).Servers;
@@ -207,7 +207,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.CheckNodeIdx = 0;
                 this.Failures = 100;
 
-                return this.RaiseEvent(new Local());
+                this.RaiseEvent(new Local());
             }
 
             [OnEntry(nameof(StartMonitoringOnEntry))]
@@ -217,11 +217,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition StartMonitoringOnEntry()
+            private void StartMonitoringOnEntry()
             {
                 if (this.Failures < 1)
                 {
-                    return this.Halt();
+                    this.RaiseHaltEvent();
                 }
                 else
                 {
@@ -245,8 +245,6 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
 
                     this.Failures--;
                 }
-
-                return default;
             }
 
             private void HandlePong()
@@ -373,7 +371,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry(Event e)
+            private void InitOnEntry(Event e)
             {
                 this.Servers = (e as SetupEvent).Servers;
                 this.Clients = (e as SetupEvent).Clients;
@@ -385,7 +383,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.Head = this.Servers[0];
                 this.Tail = this.Servers[this.Servers.Count - 1];
 
-                return this.RaiseEvent(new Local());
+                this.RaiseEvent(new Local());
             }
 
             [OnEventGotoState(typeof(HeadFailed), typeof(CorrectHeadFailure))]
@@ -396,7 +394,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition CheckWhichNodeFailed(Event e)
+            private void CheckWhichNodeFailed(Event e)
             {
                 this.Assert(this.Servers.Count > 1, "All nodes have failed.");
 
@@ -404,11 +402,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
 
                 if (this.Head.Equals(failedServer))
                 {
-                    return this.RaiseEvent(new HeadFailed());
+                    this.RaiseEvent(new HeadFailed());
                 }
                 else if (this.Tail.Equals(failedServer))
                 {
-                    return this.RaiseEvent(new TailFailed());
+                    this.RaiseEvent(new TailFailed());
                 }
                 else
                 {
@@ -420,7 +418,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                         }
                     }
 
-                    return this.RaiseEvent(new ServerFailed());
+                    this.RaiseEvent(new ServerFailed());
                 }
             }
 
@@ -445,14 +443,14 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.SendEvent(this.Head, new BecomeHead(this.Id));
             }
 
-            private Transition UpdateClients()
+            private void UpdateClients()
             {
                 for (int i = 0; i < this.Clients.Count; i++)
                 {
                     this.SendEvent(this.Clients[i], new Client.UpdateHeadTail(this.Head, this.Tail));
                 }
 
-                return this.RaiseEvent(new Done());
+                this.RaiseEvent(new Done());
             }
 
             private void UpdateFailureDetector()
@@ -491,7 +489,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition CorrectServerFailureOnEntry()
+            private void CorrectServerFailureOnEntry()
             {
                 this.Servers.RemoveAt(this.FaultyNodeIndex);
 
@@ -500,7 +498,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.Monitor<ServerResponseSeqMonitor>(
                     new ServerResponseSeqMonitor.UpdateServers(this.Servers));
 
-                return this.RaiseEvent(new FixSuccessor());
+                this.RaiseEvent(new FixSuccessor());
             }
 
             private void ProcessFixPredecessor()
@@ -509,19 +507,16 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                     this.Id, this.Servers[this.FaultyNodeIndex], this.LastAckSent, this.LastUpdateReceivedSucc));
             }
 
-            private Transition SetLastUpdate(Event e)
+            private void SetLastUpdate(Event e)
             {
                 this.LastUpdateReceivedSucc = (e as
                     ChainReplicationServer.NewSuccInfo).LastUpdateReceivedSucc;
                 this.LastAckSent = (e as
                     ChainReplicationServer.NewSuccInfo).LastAckSent;
-                return this.RaiseEvent(new FixPredecessor());
+                this.RaiseEvent(new FixPredecessor());
             }
 
-            private Transition ProcessSuccess()
-            {
-                return this.RaiseEvent(new Done());
-            }
+            private void ProcessSuccess() => this.RaiseEvent(new Done());
         }
 
         private class ChainReplicationServer : StateMachine
@@ -683,11 +678,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.NextSeqId = 0;
             }
 
-            private Transition SetupPredSucc(Event e)
+            private void SetupPredSucc(Event e)
             {
                 this.Predecessor = (e as PredSucc).Predecessor;
                 this.Successor = (e as PredSucc).Successor;
-                return this.RaiseEvent(new Local());
+                this.RaiseEvent(new Local());
             }
 
             [OnEventGotoState(typeof(Client.Update), typeof(ProcessUpdate), nameof(ProcessUpdateAction))]
@@ -827,7 +822,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition ProcessUpdateOnEntry(Event e)
+            private void ProcessUpdateOnEntry(Event e)
             {
                 var client = (e as Client.Update).Client;
                 var key = (e as Client.Update).Key;
@@ -853,7 +848,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
 
                 this.SendEvent(this.Successor, new ForwardUpdate(this.Id, this.NextSeqId, client, key, value));
 
-                return this.RaiseEvent(new Local());
+                this.RaiseEvent(new Local());
             }
 
             [OnEntry(nameof(ProcessFwdUpdateOnEntry))]
@@ -862,7 +857,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition ProcessFwdUpdateOnEntry(Event e)
+            private void ProcessFwdUpdateOnEntry(Event e)
             {
                 var pred = (e as ForwardUpdate).Predecessor;
                 var nextSeqId = (e as ForwardUpdate).NextSeqId;
@@ -911,7 +906,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                     }
                 }
 
-                return this.RaiseEvent(new Local());
+                this.RaiseEvent(new Local());
             }
 
             [OnEntry(nameof(ProcessBckAckOnEntry))]
@@ -920,7 +915,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition ProcessBckAckOnEntry(Event e)
+            private void ProcessBckAckOnEntry(Event e)
             {
                 var nextSeqId = (e as BackwardAck).NextSeqId;
 
@@ -931,7 +926,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                     this.SendEvent(this.Predecessor, new BackwardAck(nextSeqId));
                 }
 
-                return this.RaiseEvent(new Local());
+                this.RaiseEvent(new Local());
             }
 
             private void RemoveItemFromSent(int seqId)
@@ -1036,7 +1031,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry(Event e)
+            private void InitOnEntry(Event e)
             {
                 this.HeadNode = (e as SetupEvent).HeadNode;
                 this.TailNode = (e as SetupEvent).TailNode;
@@ -1052,7 +1047,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                     { 4 * this.StartIn, 400 }
                 };
 
-                return this.RaiseEvent(new Local());
+                this.RaiseEvent(new Local());
             }
 
             [OnEntry(nameof(PumpUpdateRequestsOnEntry))]
@@ -1063,18 +1058,18 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition PumpUpdateRequestsOnEntry()
+            private void PumpUpdateRequestsOnEntry()
             {
                 this.SendEvent(this.HeadNode, new Update(this.Id, this.Next * this.StartIn,
                     this.KeyValueStore[this.Next * this.StartIn]));
 
                 if (this.Next >= 3)
                 {
-                    return this.RaiseEvent(new Done());
+                    this.RaiseEvent(new Done());
                 }
                 else
                 {
-                    return this.RaiseEvent(new Local());
+                    this.RaiseEvent(new Local());
                 }
             }
 
@@ -1085,17 +1080,17 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition PumpQueryRequestsOnEntry()
+            private void PumpQueryRequestsOnEntry()
             {
                 this.SendEvent(this.TailNode, new Query(this.Id, this.Next * this.StartIn));
 
                 if (this.Next >= 3)
                 {
-                    return this.Halt();
+                    this.RaiseHaltEvent();
                 }
                 else
                 {
-                    return this.RaiseEvent(new Local());
+                    this.RaiseEvent(new Local());
                 }
             }
 
@@ -1180,13 +1175,13 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition Setup(Event e)
+            private void Setup(Event e)
             {
                 this.Servers = (e as SetupEvent).Servers;
                 this.History = new Dictionary<ActorId, List<int>>();
                 this.SentHistory = new Dictionary<ActorId, List<int>>();
                 this.TempSeq = new List<int>();
-                return this.RaiseEvent(new Local());
+                this.RaiseEvent(new Local());
             }
 
             [OnEventDoAction(typeof(HistoryUpdate), nameof(CheckUpdatePropagationInvariant))]
@@ -1466,11 +1461,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition Setup(Event e)
+            private void Setup(Event e)
             {
                 this.Servers = (e as SetupEvent).Servers;
                 this.LastUpdateResponse = new Dictionary<int, int>();
-                return this.RaiseEvent(new Local());
+                this.RaiseEvent(new Local());
             }
 
             [OnEventDoAction(typeof(ResponseToUpdate), nameof(ResponseToUpdateAction))]

Tests/TestingServices.Tests/Actors/Integration/ChordTests.cs

@@ -69,7 +69,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
                 this.NumOfNodes = 3;
                 this.NumOfIds = (int)Math.Pow(2, this.NumOfNodes);
@@ -92,7 +92,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 }
 
                 this.CreateActor(typeof(Client), new Client.SetupEvent(this.Id, new List<int>(this.Keys)));
-                return this.RaiseEvent(new Local());
+                this.RaiseEvent(new Local());
             }
 
             [OnEventDoAction(typeof(ChordNode.FindSuccessor), nameof(ForwardFindSuccessor))]
@@ -399,7 +399,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.FingerTable = new Dictionary<int, Finger>();
             }
 
-            private Transition Setup(Event e)
+            private void Setup(Event e)
             {
                 this.NodeId = (e as SetupEvent).Id;
                 this.Keys = (e as SetupEvent).Keys;
@@ -428,7 +428,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                     }
                 }
 
-                return this.RaiseEvent(new Local());
+                this.RaiseEvent(new Local());
             }
 
             private void JoinCluster(Event e)
@@ -623,7 +623,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 }
             }
 
-            private Transition ProcessTerminate() => this.Halt();
+            private void ProcessTerminate() => this.RaiseHaltEvent();
 
             private static int GetSuccessorNodeId(int start, List<int> nodeIds)
             {
@@ -702,7 +702,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry(Event e)
+            private void InitOnEntry(Event e)
             {
                 this.ClusterManager = (e as SetupEvent).ClusterManager;
                 this.Keys = (e as SetupEvent).Keys;
@@ -713,7 +713,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
 
                 this.QueryCounter = 0;
 
-                return this.RaiseEvent(new Local());
+                this.RaiseEvent(new Local());
             }
 
             [OnEntry(nameof(QueryingOnEntry))]
@@ -722,7 +722,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition QueryingOnEntry()
+            private void QueryingOnEntry()
             {
                 if (this.QueryCounter < 5)
                 {
@@ -745,7 +745,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                     this.QueryCounter++;
                 }
 
-                return this.RaiseEvent(new Local());
+                this.RaiseEvent(new Local());
             }
 
             private int GetNextQueryKey()
@@ -781,7 +781,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.SendEvent(successor, new ChordNode.QueryId(this.Id));
             }
 
-            private Transition ProcessQueryIdResp() => this.RaiseEvent(new Local());
+            private void ProcessQueryIdResp() => this.RaiseEvent(new Local());
         }
 
         private class LivenessMonitor : Monitor
@@ -814,7 +814,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry() => this.GotoState<Responded>();
+            private void InitOnEntry() => this.RaiseGotoStateEvent<Responded>();
 
             [Cold]
             [OnEventGotoState(typeof(NotifyClientRequest), typeof(Requested))]

Tests/TestingServices.Tests/Actors/Integration/RaftTests.cs

@@ -86,7 +86,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition EntryOnInit()
+            private void EntryOnInit()
             {
                 this.NumberOfServers = 5;
                 this.LeaderTerm = 0;
@@ -100,7 +100,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
 
                 this.Client = this.CreateActor(typeof(Client));
 
-                return this.RaiseEvent(new LocalEvent());
+                this.RaiseEvent(new LocalEvent());
             }
 
             [OnEntry(nameof(ConfiguringOnInit))]
@@ -109,7 +109,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition ConfiguringOnInit()
+            private void ConfiguringOnInit()
             {
                 for (int idx = 0; idx < this.NumberOfServers; idx++)
                 {
@@ -118,7 +118,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
 
                 this.SendEvent(this.Client, new Client.ConfigureEvent(this.Id));
 
-                return this.RaiseEvent(new LocalEvent());
+                this.RaiseEvent(new LocalEvent());
             }
 
             private class Availability : StateGroup
@@ -141,10 +141,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 }
             }
 
-            private Transition BecomeAvailable(Event e)
+            private void BecomeAvailable(Event e)
             {
                 this.UpdateLeader(e as NotifyLeaderUpdate);
-                return this.RaiseEvent(new LocalEvent());
+                this.RaiseEvent(new LocalEvent());
             }
 
             private void SendClientRequestToLeader(Event e)
@@ -162,14 +162,14 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.UpdateLeader(e as NotifyLeaderUpdate);
             }
 
-            private Transition ShuttingDown()
+            private void ShuttingDown()
             {
                 for (int idx = 0; idx < this.NumberOfServers; idx++)
                 {
                     this.SendEvent(this.Servers[idx], new Server.ShutDown());
                 }
 
-                return this.Halt();
+                this.RaiseHaltEvent();
             }
 
             private void UpdateLeader(NotifyLeaderUpdate request)
@@ -413,7 +413,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.MatchIndex = new Dictionary<ActorId, int>();
             }
 
-            private Transition SetupEvent(Event e)
+            private void SetupEvent(Event e)
             {
                 this.ServerId = (e as ConfigureEvent).Id;
                 this.Servers = (e as ConfigureEvent).Servers;
@@ -425,7 +425,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.PeriodicTimer = this.CreateActor(typeof(PeriodicTimer));
                 this.SendEvent(this.PeriodicTimer, new PeriodicTimer.ConfigureEvent(this.Id));
 
-                return this.RaiseEvent(new BecomeFollower());
+                this.RaiseEvent(new BecomeFollower());
             }
 
             [OnEntry(nameof(FollowerOnInit))]
@@ -463,9 +463,9 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 }
             }
 
-            private Transition StartLeaderElection()
+            private void StartLeaderElection()
             {
-                return this.RaiseEvent(new BecomeCandidate());
+                this.RaiseEvent(new BecomeCandidate());
             }
 
             private void VoteAsFollower(Event e)
@@ -559,7 +559,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 }
             }
 
-            private Transition VoteAsCandidate(Event e)
+            private void VoteAsCandidate(Event e)
             {
                 var request = e as VoteRequest;
                 if (request.Term > this.CurrentTerm)
@@ -567,28 +567,26 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                     this.CurrentTerm = request.Term;
                     this.VotedFor = null;
                     this.Vote(e as VoteRequest);
-                    return this.RaiseEvent(new BecomeFollower());
+                    this.RaiseEvent(new BecomeFollower());
                 }
                 else
                 {
                     this.Vote(e as VoteRequest);
                 }
-
-                return default;
             }
 
-            private Transition RespondVoteAsCandidate(Event e)
+            private void RespondVoteAsCandidate(Event e)
             {
                 var request = e as VoteResponse;
                 if (request.Term > this.CurrentTerm)
                 {
                     this.CurrentTerm = request.Term;
                     this.VotedFor = null;
-                    return this.RaiseEvent(new BecomeFollower());
+                    this.RaiseEvent(new BecomeFollower());
                 }
                 else if (request.Term != this.CurrentTerm)
                 {
-                    return default;
+                    return;
                 }
 
                 if (request.VoteGranted)
@@ -597,14 +595,12 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                     if (this.VotesReceived >= (this.Servers.Length / 2) + 1)
                     {
                         this.VotesReceived = 0;
-                        return this.RaiseEvent(new BecomeLeader());
+                        this.RaiseEvent(new BecomeLeader());
                     }
                 }
-
-                return default;
             }
 
-            private Transition AppendEntriesAsCandidate(Event e)
+            private void AppendEntriesAsCandidate(Event e)
             {
                 var request = e as AppendEntriesRequest;
                 if (request.Term > this.CurrentTerm)
@@ -612,27 +608,23 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                     this.CurrentTerm = request.Term;
                     this.VotedFor = null;
                     this.AppendEntries(e as AppendEntriesRequest);
-                    return this.RaiseEvent(new BecomeFollower());
+                    this.RaiseEvent(new BecomeFollower());
                 }
                 else
                 {
                     this.AppendEntries(e as AppendEntriesRequest);
                 }
-
-                return default;
             }
 
-            private Transition RespondAppendEntriesAsCandidate(Event e)
+            private void RespondAppendEntriesAsCandidate(Event e)
             {
                 var request = e as AppendEntriesResponse;
                 if (request.Term > this.CurrentTerm)
                 {
                     this.CurrentTerm = request.Term;
                     this.VotedFor = null;
-                    return this.RaiseEvent(new BecomeFollower());
+                    this.RaiseEvent(new BecomeFollower());
                 }
-
-                return default;
             }
 
             [OnEntry(nameof(LeaderOnInit))]
@@ -719,7 +711,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 }
             }
 
-            private Transition VoteAsLeader(Event e)
+            private void VoteAsLeader(Event e)
             {
                 var request = e as VoteRequest;
 
@@ -731,17 +723,15 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                     this.RedirectLastClientRequestToClusterManager();
                     this.Vote(e as VoteRequest);
 
-                    return this.RaiseEvent(new BecomeFollower());
+                    this.RaiseEvent(new BecomeFollower());
                 }
                 else
                 {
                     this.Vote(e as VoteRequest);
                 }
-
-                return default;
             }
 
-            private Transition RespondVoteAsLeader(Event e)
+            private void RespondVoteAsLeader(Event e)
             {
                 var request = e as VoteResponse;
                 if (request.Term > this.CurrentTerm)
@@ -750,13 +740,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                     this.VotedFor = null;
 
                     this.RedirectLastClientRequestToClusterManager();
-                    return this.RaiseEvent(new BecomeFollower());
+                    this.RaiseEvent(new BecomeFollower());
                 }
-
-                return default;
             }
 
-            private Transition AppendEntriesAsLeader(Event e)
+            private void AppendEntriesAsLeader(Event e)
             {
                 var request = e as AppendEntriesRequest;
                 if (request.Term > this.CurrentTerm)
@@ -767,13 +755,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                     this.RedirectLastClientRequestToClusterManager();
                     this.AppendEntries(e as AppendEntriesRequest);
 
-                    return this.RaiseEvent(new BecomeFollower());
+                    this.RaiseEvent(new BecomeFollower());
                 }
-
-                return default;
             }
 
-            private Transition RespondAppendEntriesAsLeader(Event e)
+            private void RespondAppendEntriesAsLeader(Event e)
             {
                 var request = e as AppendEntriesResponse;
                 if (request.Term > this.CurrentTerm)
@@ -782,11 +768,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                     this.VotedFor = null;
 
                     this.RedirectLastClientRequestToClusterManager();
-                    return this.RaiseEvent(new BecomeFollower());
+                    this.RaiseEvent(new BecomeFollower());
                 }
                 else if (request.Term != this.CurrentTerm)
                 {
-                    return default;
+                    return;
                 }
 
                 if (request.Success)
@@ -826,8 +812,6 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                     this.SendEvent(request.Server, new AppendEntriesRequest(this.CurrentTerm, this.Id, prevLogIndex,
                         prevLogTerm, logs, this.CommitIndex, request.ReceiverEndpoint));
                 }
-
-                return default;
             }
 
             /// <summary>
@@ -940,11 +924,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 return logTerm;
             }
 
-            private Transition ShuttingDown()
+            private void ShuttingDown()
             {
                 this.SendEvent(this.ElectionTimer, HaltEvent.Instance);
                 this.SendEvent(this.PeriodicTimer, HaltEvent.Instance);
-                return this.Halt();
+                this.RaiseHaltEvent();
             }
         }
 
@@ -1007,10 +991,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.Counter = 0;
             }
 
-            private Transition SetupEvent(Event e)
+            private void SetupEvent(Event e)
             {
                 this.Cluster = (e as ConfigureEvent).Cluster;
-                return this.RaiseEvent(new LocalEvent());
+                this.RaiseEvent(new LocalEvent());
             }
 
             [OnEntry(nameof(PumpRequestOnEntry))]
@@ -1027,16 +1011,16 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.SendEvent(this.Cluster, new Request(this.Id, this.LatestCommand));
             }
 
-            private Transition ProcessResponse()
+            private void ProcessResponse()
             {
                 if (this.Counter == 3)
                 {
                     this.SendEvent(this.Cluster, new ClusterManager.ShutDown());
-                    return this.Halt();
+                    this.RaiseHaltEvent();
                 }
                 else
                 {
-                    return this.RaiseEvent(new LocalEvent());
+                    this.RaiseEvent(new LocalEvent());
                 }
             }
         }
@@ -1097,14 +1081,14 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.SendEvent(this.Id, new TickEvent());
             }
 
-            private Transition Tick()
+            private void Tick()
             {
                 if (this.Random())
                 {
                     this.SendEvent(this.Target, new Timeout());
                 }
 
-                return this.RaiseEvent(new CancelTimer());
+                this.RaiseEvent(new CancelTimer());
             }
 
             [OnEventGotoState(typeof(StartTimerEvent), typeof(Active))]
@@ -1170,14 +1154,14 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.SendEvent(this.Id, new TickEvent());
             }
 
-            private Transition Tick()
+            private void Tick()
             {
                 if (this.Random())
                 {
                     this.SendEvent(this.Target, new Timeout());
                 }
 
-                return this.RaiseEvent(new CancelTimer());
+                this.RaiseEvent(new CancelTimer());
             }
 
             [OnEventGotoState(typeof(StartTimerEvent), typeof(Active))]
@@ -1213,10 +1197,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
                 this.TermsWithLeader = new HashSet<int>();
-                return this.RaiseEvent(new LocalEvent());
+                this.RaiseEvent(new LocalEvent());
             }
 
             [OnEventDoAction(typeof(NotifyLeaderElected), nameof(ProcessLeaderElected))]

Tests/TestingServices.Tests/Actors/Integration/ReplicatingStorageTests.cs

@@ -67,7 +67,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition EntryOnInit()
+            private void EntryOnInit()
             {
                 this.NumberOfReplicas = 3;
                 this.NumberOfFaults = 1;
@@ -78,7 +78,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.NodeManager = this.CreateActor(typeof(NodeManager));
                 this.Client = this.CreateActor(typeof(Client));
 
-                return this.RaiseEvent(new LocalEvent());
+                this.RaiseEvent(new LocalEvent());
             }
 
             [OnEntry(nameof(ConfiguringOnInit))]
@@ -88,11 +88,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition ConfiguringOnInit()
+            private void ConfiguringOnInit()
             {
                 this.SendEvent(this.NodeManager, new NodeManager.ConfigureEvent(this.Id, this.NumberOfReplicas));
                 this.SendEvent(this.Client, new Client.ConfigureEvent(this.NodeManager));
-                return this.RaiseEvent(new LocalEvent());
+                this.RaiseEvent(new LocalEvent());
             }
 
             [OnEventDoAction(typeof(NotifyNode), nameof(UpdateAliveNodes))]
@@ -197,7 +197,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.SendEvent(this.RepairTimer, new RepairTimer.ConfigureEvent(this.Id));
             }
 
-            private Transition SetupEvent(Event e)
+            private void SetupEvent(Event e)
             {
                 this.Environment = (e as ConfigureEvent).Environment;
                 this.NumberOfReplicas = (e as ConfigureEvent).NumberOfReplicas;
@@ -207,7 +207,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                     this.CreateNewNode();
                 }
 
-                return this.RaiseEvent(new LocalEvent());
+                this.RaiseEvent(new LocalEvent());
             }
 
             private void CreateNewNode()
@@ -378,7 +378,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.SendEvent(this.SyncTimer, new SyncTimer.ConfigureEvent(this.Id));
             }
 
-            private Transition SetupEvent(Event e)
+            private void SetupEvent(Event e)
             {
                 this.Environment = (e as ConfigureEvent).Environment;
                 this.NodeManager = (e as ConfigureEvent).NodeManager;
@@ -387,7 +387,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.Monitor<LivenessMonitor>(new LivenessMonitor.NotifyNodeCreated(this.NodeId));
                 this.SendEvent(this.Environment, new Environment.NotifyNode(this.Id));
 
-                return this.RaiseEvent(new LocalEvent());
+                this.RaiseEvent(new LocalEvent());
             }
 
             [OnEventDoAction(typeof(StoreRequest), nameof(Store))]
@@ -417,11 +417,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.SendEvent(this.NodeManager, new SyncReport(this.NodeId, this.Data));
             }
 
-            private Transition Terminate()
+            private void Terminate()
             {
                 this.Monitor<LivenessMonitor>(new LivenessMonitor.NotifyNodeFail(this.NodeId));
                 this.SendEvent(this.SyncTimer, HaltEvent.Instance);
-                return this.Halt();
+                this.RaiseHaltEvent();
             }
         }
 
@@ -463,10 +463,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition SetupEvent(Event e)
+            private void SetupEvent(Event e)
             {
                 this.Target = (e as ConfigureEvent).Target;
-                return this.RaiseEvent(new StartTimerEvent());
+                this.RaiseEvent(new StartTimerEvent());
             }
 
             [OnEntry(nameof(ActiveOnEntry))]
@@ -537,10 +537,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition SetupEvent(Event e)
+            private void SetupEvent(Event e)
             {
                 this.Target = (e as ConfigureEvent).Target;
-                return this.RaiseEvent(new StartTimerEvent());
+                this.RaiseEvent(new StartTimerEvent());
             }
 
             [OnEntry(nameof(ActiveOnEntry))]
@@ -611,10 +611,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition SetupEvent(Event e)
+            private void SetupEvent(Event e)
             {
                 this.Target = (e as ConfigureEvent).Target;
-                return this.RaiseEvent(new StartTimerEvent());
+                this.RaiseEvent(new StartTimerEvent());
             }
 
             [OnEntry(nameof(ActiveOnEntry))]
@@ -694,10 +694,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.Counter = 0;
             }
 
-            private Transition SetupEvent(Event e)
+            private void SetupEvent(Event e)
             {
                 this.NodeManager = (e as ConfigureEvent).NodeManager;
-                return this.RaiseEvent(new LocalEvent());
+                this.RaiseEvent(new LocalEvent());
             }
 
             [OnEntry(nameof(PumpRequestOnEntry))]
@@ -706,7 +706,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition PumpRequestOnEntry()
+            private void PumpRequestOnEntry()
             {
                 int command = this.RandomInteger(100) + 1;
                 this.Counter++;
@@ -715,11 +715,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
 
                 if (this.Counter == 1)
                 {
-                    return this.Halt();
+                    this.RaiseHaltEvent();
                 }
                 else
                 {
-                    return this.RaiseEvent(new LocalEvent());
+                    this.RaiseEvent(new LocalEvent());
                 }
             }
         }
@@ -792,10 +792,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.DataMap = new Dictionary<int, int>();
             }
 
-            private Transition SetupEvent(Event e)
+            private void SetupEvent(Event e)
             {
                 this.NumberOfReplicas = (e as ConfigureEvent).NumberOfReplicas;
-                return this.RaiseEvent(new LocalEvent());
+                this.RaiseEvent(new LocalEvent());
             }
 
             [Cold]
@@ -813,10 +813,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.DataMap.Add(nodeId, 0);
             }
 
-            private Transition FailAndCheckRepair(Event e)
+            private void FailAndCheckRepair(Event e)
             {
                 this.ProcessNodeFail(e);
-                return this.RaiseEvent(new LocalEvent());
+                this.RaiseEvent(new LocalEvent());
             }
 
             private void ProcessNodeUpdate(Event e)
@@ -841,7 +841,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 this.DataMap.Remove(nodeId);
             }
 
-            private Transition CheckIfRepaired(Event e)
+            private void CheckIfRepaired(Event e)
             {
                 this.ProcessNodeUpdate(e);
                 var consensus = this.DataMap.Select(kvp => kvp.Value).GroupBy(v => v).
@@ -850,10 +850,8 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 var numOfReplicas = consensus.Count();
                 if (numOfReplicas >= this.NumberOfReplicas)
                 {
-                    return this.RaiseEvent(new LocalEvent());
+                    this.RaiseEvent(new LocalEvent());
                 }
-
-                return default;
             }
         }
 

Tests/TestingServices.Tests/Actors/Integration/TwoActorIntegrationTests.cs

@@ -65,10 +65,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
                 this.TargetId = this.CreateActor(typeof(M1b));
-                return this.RaiseEvent(new E1());
+                this.RaiseEvent(new E1());
             }
 
             private void InitOnExit()
@@ -127,10 +127,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
                 this.TargetId = this.CreateActor(typeof(M2b));
-                return this.RaiseEvent(new SuccessE());
+                this.RaiseEvent(new SuccessE());
             }
 
             [OnEntry(nameof(ActiveOnEntry))]
@@ -139,7 +139,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition ActiveOnEntry()
+            private void ActiveOnEntry()
             {
                 this.Count += 1;
                 if (this.Count == 1)
@@ -152,7 +152,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                     this.SendEvent(this.TargetId, new IgnoredE());
                 }
 
-                return this.RaiseEvent(new SuccessE());
+                this.RaiseEvent(new SuccessE());
             }
 
             [OnEventGotoState(typeof(E1), typeof(Active))]
@@ -185,10 +185,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition ActiveOnEntry(Event e)
+            private void ActiveOnEntry(Event e)
             {
                 this.SendEvent((e as E4).Id, new E1(), options: new SendOptions(assert: 1));
-                return this.RaiseEvent(new SuccessE());
+                this.RaiseEvent(new SuccessE());
             }
         }
 
@@ -216,10 +216,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
                 this.TargetId = this.CreateActor(typeof(M3b));
-                return this.RaiseEvent(new SuccessE());
+                this.RaiseEvent(new SuccessE());
             }
 
             [OnEntry(nameof(ActiveOnEntry))]
@@ -228,7 +228,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition ActiveOnEntry()
+            private void ActiveOnEntry()
             {
                 this.Count += 1;
                 if (this.Count == 1)
@@ -242,7 +242,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                     this.SendEvent(this.TargetId, new IgnoredE());
                 }
 
-                return this.RaiseEvent(new SuccessE());
+                this.RaiseEvent(new SuccessE());
             }
 
             [OnEventGotoState(typeof(E1), typeof(Active))]
@@ -270,10 +270,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition ActiveOnEntry(Event e)
+            private void ActiveOnEntry(Event e)
             {
                 this.SendEvent((e as E4).Id, new E1(), options: new SendOptions(assert: 1));
-                return this.RaiseEvent(new SuccessE());
+                this.RaiseEvent(new SuccessE());
             }
 
             [OnEventDoAction(typeof(IgnoredE), nameof(Action1))]
@@ -311,10 +311,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
                 this.TargetId = this.CreateActor(typeof(M4b));
-                return this.RaiseEvent(new SuccessE());
+                this.RaiseEvent(new SuccessE());
             }
 
             [OnEntry(nameof(ActiveOnEntry))]
@@ -323,10 +323,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition ActiveOnEntry()
+            private void ActiveOnEntry()
             {
                 this.SendEvent(this.TargetId, new E4(this.Id), options: new SendOptions(assert: 1));
-                return this.RaiseEvent(new SuccessE());
+                this.RaiseEvent(new SuccessE());
             }
 
             [OnEventGotoState(typeof(E1), typeof(Active))]
@@ -351,7 +351,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition ActiveOnEntry(Event e)
+            private void ActiveOnEntry(Event e)
             {
                 this.Count++;
                 if (this.Count == 1)
@@ -361,10 +361,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 else if (this.Count == 2)
                 {
                     this.SendEvent((e as E4).Id, new E1(), options: new SendOptions(assert: 1));
-                    return this.Halt();
+                    this.RaiseHaltEvent();
+                    return;
                 }
 
-                return this.RaiseEvent(new SuccessE());
+                this.RaiseEvent(new SuccessE());
             }
 
             protected override Task OnHaltAsync(Event e)
@@ -374,7 +375,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             }
         }
 
-        [Fact(Timeout = 5000)]
+        [Fact(Timeout = 50000)]
         public void TestTwoActorIntegration4()
         {
             this.TestWithError(r =>
@@ -398,7 +399,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry() => this.RaiseEvent(new E1());
+            private void InitOnEntry() => this.RaiseEvent(new E1());
 
             private void InitOnExit()
             {

Tests/TestingServices.Tests/Actors/StateMachines/CurrentStateTests.cs

@@ -25,10 +25,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
                 this.Assert(this.CurrentState == typeof(Init));
-                return this.RaiseEvent(UnitEvent.Instance);
+                this.RaiseEvent(UnitEvent.Instance);
             }
 
             [OnEntry(nameof(ActiveOnEntry))]

Tests/TestingServices.Tests/Actors/StateMachines/GotoStateTransitionTests.cs

@@ -22,7 +22,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry() => this.GotoState<Done>();
+            private void InitOnEntry() => this.RaiseGotoStateEvent<Done>();
 
             private class Done : State
             {
@@ -46,7 +46,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry() => this.GotoState<M2b.Done>();
+            private void InitOnEntry() => this.RaiseGotoStateEvent<M2b.Done>();
 
             private class Done : State
             {
@@ -90,7 +90,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry() => this.GotoState<Done>();
+            private void InitOnEntry() => this.RaiseGotoStateEvent<Done>();
 
             private void ExitInit()
             {
@@ -123,9 +123,9 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry() => this.GotoState<Done>();
+            private void InitOnEntry() => this.RaiseGotoStateEvent<Done>();
 
-            private Transition ExitMethod() => this.GotoState<Done>();
+            private void ExitMethod() => this.RaiseGotoStateEvent<Done>();
 
             private class Done : State
             {

Tests/TestingServices.Tests/Actors/StateMachines/PopStateTransitionTests.cs

@@ -22,7 +22,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition Init() => this.PopState();
+            private void Init() => this.RaisePopStateEvent();
         }
 
         [Fact(Timeout = 5000)]
@@ -45,9 +45,9 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry() => this.GotoState<Done>();
+            private void InitOnEntry() => this.RaiseGotoStateEvent<Done>();
 
-            private Transition ExitMethod() => this.PopState();
+            private void ExitMethod() => this.RaisePopStateEvent();
 
             private class Done : State
             {

Tests/TestingServices.Tests/Actors/StateMachines/PushStateTransitionTests.cs

@@ -23,7 +23,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry() => this.PushState<Done>();
+            private void InitOnEntry() => this.RaisePushStateEvent<Done>();
 
             [OnEntry(nameof(EntryDone))]
             private class Done : State
@@ -59,11 +59,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
                 this.Assert(this.cnt == 0); // called once
                 this.cnt++;
-                return this.PushState<Done>();
+                this.RaisePushStateEvent<Done>();
             }
 
             [OnEntry(nameof(EntryDone))]
@@ -71,7 +71,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition EntryDone() => this.PopState();
+            private void EntryDone() => this.RaisePopStateEvent();
         }
 
         [Fact(Timeout = 5000)]
@@ -93,7 +93,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry() => this.PushState<Done>();
+            private void InitOnEntry() => this.RaisePushStateEvent<Done>();
 
             private void ExitInit()
             {
@@ -123,7 +123,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry() => this.PushState<M4b.Done>();
+            private void InitOnEntry() => this.RaisePushStateEvent<M4b.Done>();
 
             private class Done : State
             {
@@ -176,7 +176,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition Bar() => this.PopState();
+            private void Bar() => this.RaisePopStateEvent();
         }
 
         private class E1 : Event
@@ -230,9 +230,9 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry() => this.GotoState<Done>();
+            private void InitOnEntry() => this.RaiseGotoStateEvent<Done>();
 
-            private Transition ExitMethod() => this.PushState<Done>();
+            private void ExitMethod() => this.RaisePushStateEvent<Done>();
 
             private class Done : State
             {

Tests/TestingServices.Tests/Actors/StateMachines/RaiseEventTransitionTests.cs

@@ -28,7 +28,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition HandleUnitEvent() => this.RaiseEvent(new E());
+            private void HandleUnitEvent() => this.RaiseEvent(new E());
 
             private void HandleE()
             {
@@ -58,9 +58,9 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry() => this.GotoState<Done>();
+            private void InitOnEntry() => this.RaiseGotoStateEvent<Done>();
 
-            private Transition ExitMethod() => this.RaiseEvent(UnitEvent.Instance);
+            private void ExitMethod() => this.RaiseEvent(UnitEvent.Instance);
 
             private class Done : State
             {

Tests/TestingServices.Tests/Actors/StateMachines/StateGroupTests.cs

@@ -47,11 +47,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                 }
             }
 
-            private Transition States1S1OnEntry() => this.RaiseEvent(UnitEvent.Instance);
+            private void States1S1OnEntry() => this.RaiseEvent(UnitEvent.Instance);
 
-            private Transition States1S2OnEntry() => this.RaiseEvent(UnitEvent.Instance);
+            private void States1S2OnEntry() => this.RaiseEvent(UnitEvent.Instance);
 
-            private Transition States2S1OnEntry() => this.RaiseEvent(UnitEvent.Instance);
+            private void States2S1OnEntry() => this.RaiseEvent(UnitEvent.Instance);
 
             private void States2S2OnEntry()
             {

Tests/TestingServices.Tests/Actors/Timers/BasicTimerTests.cs

@@ -207,13 +207,13 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition DoPing(Event e)
+            private void DoPing(Event e)
             {
                 this.Config = (TimerCountEvent)e;
                 this.Config.Count = 0;
                 this.PingTimer = this.StartPeriodicTimer(TimeSpan.FromMilliseconds(5), TimeSpan.FromMilliseconds(5));
                 this.StopTimer(this.PingTimer);
-                return this.GotoState<Pong>();
+                this.RaiseGotoStateEvent<Pong>();
             }
 
             private void DoPong()
@@ -354,11 +354,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
                 // Start a regular timer.
                 this.StartTimer(TimeSpan.FromMilliseconds(10));
-                return this.GotoState<Final>();
+                this.RaiseGotoStateEvent<Final>();
             }
 
             [OnEntry(nameof(FinalOnEntry))]
@@ -367,7 +367,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition FinalOnEntry() => this.Halt();
+            private void FinalOnEntry() => this.RaiseHaltEvent();
         }
 
         [Fact(Timeout = 10000)]
@@ -408,7 +408,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
             {
             }
 
-            private Transition Initialize(Event e)
+            private void Initialize(Event e)
             {
                 var ce = e as ConfigEvent;
                 this.Config = ce;
@@ -424,8 +424,6 @@ namespace Microsoft.Coyote.TestingServices.Tests.Actors
                     default:
                         break;
                 }
-
-                return default;
             }
 
             private void OnMyTimeout(Event e)

Tests/TestingServices.Tests/Coverage/ActivityCoverageTests.cs

@@ -35,7 +35,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Coverage
             {
             }
 
-            private Transition InitOnEntry() => this.GotoState<Done>();
+            private void InitOnEntry() => this.RaiseGotoStateEvent<Done>();
 
             private class Done : State
             {
@@ -91,7 +91,7 @@ Event coverage: 100.0%
             {
             }
 
-            private Transition InitOnEntry() => this.RaiseEvent(UnitEvent.Instance);
+            private void InitOnEntry() => this.RaiseEvent(UnitEvent.Instance);
 
             private class Done : State
             {

Tests/TestingServices.Tests/Runtime/SendAndExecuteTests.cs

@@ -328,7 +328,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Runtime
             {
             }
 
-            private Transition HandleE() => this.Halt();
+            private void HandleE() => this.RaiseHaltEvent();
 
             protected override Task OnHaltAsync(Event e)
             {
@@ -369,11 +369,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Runtime
                 this.MHalted = true;
             }
 
-            private Transition OnSEReturns()
+            private void OnSEReturns()
             {
                 this.Assert(this.MHalted);
                 this.SEReturned = true;
-                return this.GotoState<Done>();
+                this.RaiseGotoStateEvent<Done>();
             }
         }
 
@@ -550,7 +550,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Runtime
             {
             }
 
-            private Transition Handle() => this.RaiseEvent(new E3());
+            private void Handle() => this.RaiseEvent(new E3());
         }
 
         [Fact(Timeout = 5000)]

Tests/TestingServices.Tests/Specifications/Monitors/GenericMonitorTests.cs

@@ -25,10 +25,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Specifications
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
                 this.Item = default;
-                return this.GotoState<Active>();
+                this.RaiseGotoStateEvent<Active>();
             }
 
             [OnEntry(nameof(ActiveInit))]
@@ -54,7 +54,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Specifications
             {
             }
 
-            private Transition Init() => this.GotoState<S2>();
+            private void Init() => this.RaiseGotoStateEvent<S2>();
         }
 
         [Fact(Timeout = 5000)]

Tests/TestingServices.Tests/Specifications/Monitors/Liveness/HotStateTests.cs

@@ -61,7 +61,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Specifications
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
                 this.Workers = new List<ActorId>();
 
@@ -73,7 +73,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Specifications
                 }
 
                 this.Monitor<M>(new MConfig(this.Workers));
-                return this.RaiseEvent(UnitEvent.Instance);
+                this.RaiseEvent(UnitEvent.Instance);
             }
 
             [OnEntry(nameof(ActiveOnEntry))]
@@ -107,10 +107,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Specifications
             {
             }
 
-            private Transition SetupEvent(Event e)
+            private void SetupEvent(Event e)
             {
                 this.Master = (e as SetupEvent).Id;
-                return this.RaiseEvent(UnitEvent.Instance);
+                this.RaiseEvent(UnitEvent.Instance);
             }
 
             [OnEventGotoState(typeof(DoProcessing), typeof(Done))]
@@ -123,14 +123,14 @@ namespace Microsoft.Coyote.TestingServices.Tests.Specifications
             {
             }
 
-            private Transition DoneOnEntry()
+            private void DoneOnEntry()
             {
                 if (this.Random())
                 {
                     this.SendEvent(this.Master, new FinishedProcessing());
                 }
 
-                return this.Halt();
+                this.RaiseHaltEvent();
             }
         }
 
@@ -152,16 +152,14 @@ namespace Microsoft.Coyote.TestingServices.Tests.Specifications
                 this.Workers = (e as MConfig).Ids;
             }
 
-            private Transition ProcessNotification()
+            private void ProcessNotification()
             {
                 this.Workers.RemoveAt(0);
 
                 if (this.Workers.Count == 0)
                 {
-                    return this.RaiseEvent(UnitEvent.Instance);
+                    this.RaiseEvent(UnitEvent.Instance);
                 }
-
-                return Transition.None;
             }
 
             private class Done : State

Tests/TestingServices.Tests/Specifications/Monitors/Liveness/Liveness1Tests.cs

@@ -42,7 +42,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Specifications
             {
             }
 
-            private Transition InitOnEntry() => this.RaiseEvent(UnitEvent.Instance);
+            private void InitOnEntry() => this.RaiseEvent(UnitEvent.Instance);
 
             [OnEntry(nameof(WaitForUserOnEntry))]
             [OnEventGotoState(typeof(UserEvent), typeof(HandleEvent))]

Tests/TestingServices.Tests/Specifications/Monitors/Liveness/Liveness2BugFoundTests.cs

@@ -42,7 +42,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Specifications
             {
             }
 
-            private Transition InitOnEntry() => this.RaiseEvent(UnitEvent.Instance);
+            private void InitOnEntry() => this.RaiseEvent(UnitEvent.Instance);
 
             [OnEntry(nameof(WaitForUserOnEntry))]
             [OnEventGotoState(typeof(UserEvent), typeof(HandleEvent))]

Tests/TestingServices.Tests/Specifications/Monitors/Liveness/Liveness2LoopMachineTests.cs

@@ -41,10 +41,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Specifications
             {
             }
 
-            private Transition InitOnEntry()
+            private void InitOnEntry()
             {
                 this.CreateActor(typeof(Loop));
-                return this.RaiseEvent(UnitEvent.Instance);
+                this.RaiseEvent(UnitEvent.Instance);
             }
 
             [OnEntry(nameof(WaitForUserOnEntry))]

Tests/TestingServices.Tests/Specifications/Monitors/Liveness/UnfairExecutionTests.cs

@@ -38,11 +38,11 @@ namespace Microsoft.Coyote.TestingServices.Tests.Specifications
             {
             }
 
-            private Transition SOnEntry()
+            private void SOnEntry()
             {
                 this.N = this.CreateActor(typeof(N));
                 this.SendEvent(this.N, new E(this.Id));
-                return this.RaiseEvent(UnitEvent.Instance);
+                this.RaiseEvent(UnitEvent.Instance);
             }
 
             [OnEntry(nameof(S2OnEntry))]
@@ -62,10 +62,10 @@ namespace Microsoft.Coyote.TestingServices.Tests.Specifications
             {
             }
 
-            private Transition S3OnEntry()
+            private void S3OnEntry()
             {
                 this.Monitor<LivenessMonitor>(new E(this.Id));
-                return this.Halt();
+                this.RaiseHaltEvent();
             }
         }
 

Tests/TestingServices.Tests/Specifications/Monitors/Liveness/WarmStateTests.cs

@@ -42,7 +42,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Specifications
             {
             }
 
-            private Transition InitOnEntry() => this.RaiseEvent(UnitEvent.Instance);
+            private void InitOnEntry() => this.RaiseEvent(UnitEvent.Instance);
 
             [OnEntry(nameof(WaitForUserOnEntry))]
             [OnEventGotoState(typeof(UserEvent), typeof(HandleEvent))]

Tests/TestingServices.Tests/Specifications/Monitors/OverloadedEventHandlerTests.cs

@@ -24,7 +24,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Specifications
             {
             }
 
-            private Transition InitOnEntry() => this.RaiseEvent(UnitEvent.Instance);
+            private void InitOnEntry() => this.RaiseEvent(UnitEvent.Instance);
 
             private void HandleUnitEvent()
             {

Tests/TestingServices.Tests/Specifications/Monitors/Transitions/GotoStateTransitionTests.cs

@@ -29,7 +29,7 @@ namespace Microsoft.Coyote.TestingServices.Tests.Specifications
             {
             }
 
-            private Transition Init() => this.GotoState<S2>();
+            private void Init() => this.RaiseGotoStateEvent<S2>();
 
             private void IncrementValue()
             {

Tests/TestingServices.Tests/Specifications/Monitors/Transitions/StateGroupTests.cs

@@ -46,9 +46,9 @@ namespace Microsoft.Coyote.TestingServices.Tests.Specifications
                 }
             }
 
-            private Transition States1S2OnEntry() => this.RaiseEvent(UnitEvent.Instance);
+            private void States1S2OnEntry() => this.RaiseEvent(UnitEvent.Instance);
 
-            private Transition States2S1OnEntry() => this.RaiseEvent(UnitEvent.Instance);
+            private void States2S1OnEntry() => this.RaiseEvent(UnitEvent.Instance);
 
             private void States2S2OnEntry()
             {

Tools/BenchmarkRunner/Tests/Actors/StateMachines/Creation/CreationThroughputBenchmark.cs

@@ -39,7 +39,7 @@ namespace Microsoft.Coyote.Benchmarking.Actors.StateMachines
             {
             }
 
-            private Transition InitOnEntry(Event e)
+            private void InitOnEntry(Event e)
             {
                 var tcs = (e as SetupEvent).Tcs;
                 var numMachines = (e as SetupEvent).NumMachines;
@@ -53,10 +53,8 @@ namespace Microsoft.Coyote.Benchmarking.Actors.StateMachines
 
                 if (doHalt)
                 {
-                    return this.Halt();
+                    this.RaiseHaltEvent();
                 }
-
-                return default;
             }
         }
 

Tools/BenchmarkRunner/Tests/Actors/StateMachines/Messaging/DequeueEventThroughputBenchmark.cs

@@ -64,14 +64,14 @@ namespace Microsoft.Coyote.Benchmarking.Actors.StateMachines
             {
             }
 
-            private Transition InitOnEntry(Event e)
+            private void InitOnEntry(Event e)
             {
                 this.TcsSetup = (e as SetupProducerEvent).TcsSetup;
                 this.Consumer = (e as SetupProducerEvent).Consumer;
                 this.NumMessages = (e as SetupProducerEvent).NumMessages;
 
                 this.TcsSetup.SetResult(true);
-                return this.GotoState<Experiment>();
+                this.RaiseGotoStateEvent<Experiment>();
             }
 
             [OnEventDoAction(typeof(StartExperiment), nameof(Run))]

Tools/BenchmarkRunner/Tests/Actors/StateMachines/Messaging/SendEventThroughputBenchmark.cs

@@ -89,16 +89,14 @@ namespace Microsoft.Coyote.Benchmarking.Actors.StateMachines
                 }
             }
 
-            private Transition HandleCreationAck()
+            private void HandleCreationAck()
             {
                 this.Counter++;
                 if (this.Counter == this.NumConsumers)
                 {
                     this.TcsSetup.SetResult(true);
-                    return this.GotoState<Experiment>();
+                    this.RaiseGotoStateEvent<Experiment>();
                 }
-
-                return default;
             }
 
             [OnEventDoAction(typeof(StartExperiment), nameof(Run))]