fixing

Src/PChecker/CheckerCore/Actors/StateMachine.cs

@@ -26,29 +26,28 @@
 namespace PChecker.Actors
 {
     /// <summary>
-    /// Type that implements a state machine actor. Inherit from this class to declare
-    /// a custom actor with states, state transitions and event handlers.
+    /// Type that implements a state machine with states, state transitions and event handlers.
     /// </summary>
     public abstract class StateMachine
     {
 
         /// <summary>
-        /// The runtime that executes this actor.
+        /// The runtime that executes this state machine.
         /// </summary>
         internal ActorRuntime Runtime { get; private set; }
 
         /// <summary>
-        /// Unique id that identifies this actor.
+        /// Unique id that identifies this state machine.
         /// </summary>
         protected internal ActorId Id { get; private set; }
 
         /// <summary>
-        /// Manages the actor.
+        /// Manages the state machine.
         /// </summary>
         internal IStateMachineManager Manager { get; private set; }
 
         /// <summary>
-        /// The inbox of the actor. Incoming events are enqueued here.
+        /// The inbox of the state machine. Incoming events are enqueued here.
         /// Events are dequeued to be processed.
         /// </summary>
         private protected IEventQueue Inbox;
@@ -100,7 +99,7 @@ public abstract class StateMachine
         private static readonly Type[] SingleEventTypeArray = new Type[] { typeof(Event) };
 
         /// <summary>
-        /// The current status of the actor. It is marked volatile as
+        /// The current status of the state machine. It is marked volatile as
         /// the runtime can read it concurrently.
         /// </summary>
         private protected volatile Status CurrentStatus;
@@ -111,7 +110,7 @@ public abstract class StateMachine
         internal string CurrentStateName { get; private protected set; }
 
         /// <summary>
-        /// Checks if the actor is halted.
+        /// Checks if the state machine is halted.
         /// </summary>
         internal bool IsHalted => CurrentStatus is Status.Halted;
 
@@ -154,7 +153,7 @@ protected StateMachine()
         }
 
         /// <summary>
-        /// Configures the actor.
+        /// Configures the state machine.
         /// </summary>
         internal void Configure(ActorRuntime runtime, ActorId id, IStateMachineManager manager, IEventQueue inbox)
         {
@@ -240,57 +239,57 @@ protected void Assert(bool predicate, string s, params object[] args) =>
             Runtime.Assert(predicate, s, args);
 
         /// <summary>
-        /// Asynchronous callback that is invoked when the actor is initialized with an optional event.
+        /// Asynchronous callback that is invoked when the state machine is initialized with an optional event.
         /// </summary>
         /// <param name="initialEvent">Optional event used for initialization.</param>
         /// <returns>Task that represents the asynchronous operation.</returns>
         protected virtual Task OnInitializeAsync(Event initialEvent) => Task.CompletedTask;
 
         /// <summary>
-        /// Asynchronous callback that is invoked when the actor successfully dequeues
+        /// Asynchronous callback that is invoked when the state machine successfully dequeues
         /// an event from its inbox. This method is not called when the dequeue happens
         /// via a receive statement.
         /// </summary>
         /// <param name="e">The event that was dequeued.</param>
         protected virtual Task OnEventDequeuedAsync(Event e) => Task.CompletedTask;
 
         /// <summary>
-        /// Asynchronous callback that is invoked when the actor finishes handling a dequeued
-        /// event, unless the handler of the dequeued event caused the actor to halt (either
-        /// normally or due to an exception). The actor will either become idle or dequeue
+        /// Asynchronous callback that is invoked when the state machine finishes handling a dequeued
+        /// event, unless the handler of the dequeued event caused the state machine to halt (either
+        /// normally or due to an exception). The state machine will either become idle or dequeue
         /// the next event from its inbox.
         /// </summary>
         /// <param name="e">The event that was handled.</param>
         protected virtual Task OnEventHandledAsync(Event e) => Task.CompletedTask;
 
         /// <summary>
-        /// Asynchronous callback that is invoked when the actor receives an event that
+        /// Asynchronous callback that is invoked when the state machine receives an event that
         /// it is not prepared to handle. The callback is invoked first, after which the
-        /// actor will necessarily throw an <see cref="UnhandledEventException"/>
+        /// state machine will necessarily throw an <see cref="UnhandledEventException"/>
         /// </summary>
         /// <param name="e">The event that was unhandled.</param>
         /// <param name="state">The state when the event was dequeued.</param>
         protected Task OnEventUnhandledAsync(Event e, string state) => Task.CompletedTask;
 
         /// <summary>
-        /// Asynchronous callback that is invoked when the actor handles an exception.
+        /// Asynchronous callback that is invoked when the state machine handles an exception.
         /// </summary>
-        /// <param name="ex">The exception thrown by the actor.</param>
+        /// <param name="ex">The exception thrown by the state machine.</param>
         /// <param name="e">The event being handled when the exception was thrown.</param>
         /// <returns>The action that the runtime should take.</returns>
         protected Task OnExceptionHandledAsync(Exception ex, Event e) => Task.CompletedTask;
 
         /// <summary>
-        /// Asynchronous callback that is invoked when the actor halts.
+        /// Asynchronous callback that is invoked when the state machine halts.
         /// </summary>
-        /// <param name="e">The event being handled when the actor halted.</param>
+        /// <param name="e">The event being handled when the state machine halted.</param>
         /// <returns>Task that represents the asynchronous operation.</returns>
         protected Task OnHaltAsync(Event e) => Task.CompletedTask;
 
         /// <summary>
-        /// Halts the actor.
+        /// Halts the state machine.
         /// </summary>
-        /// <param name="e">The event being handled when the actor halts.</param>
+        /// <param name="e">The event being handled when the state machine halts.</param>
         private protected Task HaltAsync(Event e)
         {
             CurrentStatus = Status.Halted;
@@ -308,7 +307,7 @@ private protected Task HaltAsync(Event e)
         }
 
         /// <summary>
-        /// Initializes the actor with the specified optional event.
+        /// Initializes the state machine with the specified optional event.
         /// </summary>
         /// <param name="initialEvent">Optional event used for initialization.</param>
         internal async Task InitializeAsync(Event initialEvent)
@@ -369,7 +368,7 @@ private protected Task TryHandleActionInvocationExceptionAsync(Exception ex, str
         }
 
         /// <summary>
-        /// ID used to identify subsequent operations performed by this actor. This value
+        /// ID used to identify subsequent operations performed by this state machine. This value
         /// is initially either <see cref="Guid.Empty"/> or the <see cref="Guid"/> specified
         /// upon creation. This value is automatically set to the operation group id of the
         /// last dequeue or receive operation, if it is not <see cref="Guid.Empty"/>. This
@@ -387,15 +386,15 @@ protected internal Guid OperationGroupId
 
 
         /// <summary>
-        /// Creates a new actor of the specified type and name, and with the specified
+        /// Creates a new state machine of the specified type and name, and with the specified
         /// optional <see cref="Event"/>. This <see cref="Event"/> can only be used to
         /// access its payload, and cannot be handled.
         /// </summary>
-        /// <param name="type">Type of the actor.</param>
+        /// <param name="type">Type of the state machine.</param>
         /// <param name="name">Optional name used for logging.</param>
         /// <param name="initialEvent">Optional initialization event.</param>
         /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
-        /// <returns>The unique actor id.</returns>
+        /// <returns>The unique state machine id.</returns>
         protected ActorId CreateActor(Type type, string name, Event initialEvent = null, Guid opGroupId = default) =>
             Runtime.CreateActor(null, type, name, initialEvent, this, opGroupId);
 
@@ -450,7 +449,7 @@ protected internal Task<Event> ReceiveEventAsync(params Tuple<Type, Func<Event,
 
         /// <summary>
         /// Runs the event handler. The handler terminates if there is no next
-        /// event to process or if the actor has halted.
+        /// event to process or if the state machine has halted.
         /// </summary>
         internal async Task RunEventHandlerAsync()
         {
@@ -468,7 +467,7 @@ internal async Task RunEventHandlerAsync()
                 {
                     // Notify the runtime for a new event to handle. This is only used
                     // during bug-finding and operation bounding, because the runtime
-                    // has to schedule an actor when a new operation is dequeued.
+                    // has to schedule an state machine when a new operation is dequeued.
                     Runtime.NotifyDequeuedEvent(this, e, info);
                     await InvokeUserCallbackAsync(UserCallbackType.OnEventDequeued, e);
                     lastDequeuedEvent = e;
@@ -496,20 +495,20 @@ internal async Task RunEventHandlerAsync()
 
                 if (CurrentStatus is Status.Active)
                 {
-                    // Handles the next event, if the actor is not halted.
+                    // Handles the next event, if the state machine is not halted.
                     await HandleEventAsync(e);
                 }
 
                 if (!Inbox.IsEventRaised && lastDequeuedEvent != null && CurrentStatus != Status.Halted)
                 {
-                    // Inform the user that the actor handled the dequeued event.
+                    // Inform the user that the state machine handled the dequeued event.
                     await InvokeUserCallbackAsync(UserCallbackType.OnEventHandled, lastDequeuedEvent);
                     lastDequeuedEvent = null;
                 }
 
                 if (CurrentStatus is Status.Halting)
                 {
-                    // If the current status is halting, then halt the actor.
+                    // If the current status is halting, then halt the state machine.
                     await HaltAsync(e);
                 }
             }
@@ -660,9 +659,9 @@ private void AssertActionValidity(MethodInfo action)
         }
 
         /// <summary>
-        /// Invokes user callback when the actor throws an exception.
+        /// Invokes user callback when the state machine throws an exception.
         /// </summary>
-        /// <param name="ex">The exception thrown by the actor.</param>
+        /// <param name="ex">The exception thrown by the state machine.</param>
         /// <param name="methodName">The handler (outermost) that threw the exception.</param>
         /// <param name="e">The event being handled when the exception was thrown.</param>
         /// <returns>True if the exception was handled, else false if it should continue to get thrown.</returns>
@@ -691,11 +690,11 @@ private bool OnExceptionHandler(Exception ex, string methodName, Event e)
         }
 
         /// <summary>
-        /// Invokes user callback when the actor receives an event that it cannot handle.
+        /// Invokes user callback when the state machine receives an event that it cannot handle.
         /// </summary>
-        /// <param name="ex">The exception thrown by the actor.</param>
+        /// <param name="ex">The exception thrown by the state machine.</param>
         /// <param name="e">The unhandled event.</param>
-        /// <returns>True if the actor should gracefully halt, else false if the exception
+        /// <returns>True if the state machine should gracefully halt, else false if the exception
         /// should continue to get thrown.</returns>
         private bool OnUnhandledEventExceptionHandler(UnhandledEventException ex, Event e)
         {
@@ -713,10 +712,10 @@ private bool OnUnhandledEventExceptionHandler(UnhandledEventException ex, Event
         }
 
         /// <summary>
-        /// User callback when the actor throws an exception. By default,
-        /// the actor throws the exception causing the runtime to fail.
+        /// User callback when the state machine throws an exception. By default,
+        /// the state machine throws the exception causing the runtime to fail.
         /// </summary>
-        /// <param name="ex">The exception thrown by the actor.</param>
+        /// <param name="ex">The exception thrown by the state machine.</param>
         /// <param name="methodName">The handler (outermost) that threw the exception.</param>
         /// <param name="e">The event being handled when the exception was thrown.</param>
         /// <returns>The action that the runtime should take.</returns>
@@ -761,30 +760,30 @@ internal EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info)
         }
 
         /// <summary>
-        /// Returns a string that represents the current actor.
+        /// Returns a string that represents the current state machine.
         /// </summary>
         public override string ToString()
         {
             return Id.Name;
         }
 
         /// <summary>
-        /// The status of the actor.
+        /// The status of the state machine.
         /// </summary>
         private protected enum Status
         {
             /// <summary>
-            /// The actor is active.
+            /// The state machine is active.
             /// </summary>
             Active = 0,
 
             /// <summary>
-            /// The actor is halting.
+            /// The state machine is halting.
             /// </summary>
             Halting,
 
             /// <summary>
-            /// The actor is halted.
+            /// The state machine is halted.
             /// </summary>
             Halted
         }
@@ -873,7 +872,7 @@ protected void RaiseGotoStateEvent(Type state)
         }
 
         /// <summary>
-        /// Raises a <see cref='HaltEvent'/> to halt the actor at the end of the current action.
+        /// Raises a <see cref='HaltEvent'/> to halt the state machine at the end of the current action.
         /// </summary>
         /// <remarks>
         /// This event is not handled until the action that calls this method returns control back
@@ -906,7 +905,7 @@ private protected async Task HandleEventAsync(Event e)
                     // If the stack of states is empty then halt or fail the state machine.
                     if (e is HaltEvent)
                     {
-                        // If it is the halt event, then change the actor status to halting.
+                        // If it is the halt event, then change the state machine status to halting.
                         CurrentStatus = Status.Halting;
                         break;
                     }
@@ -942,7 +941,7 @@ private protected async Task HandleEventAsync(Event e)
                     }
                     else if (StateMachineActionMap.TryGetValue(e.GetType().Name, out var handler))
                     {
-                        // Allow StateMachine to have class level OnEventDoActions the same way Actor allows.
+                        // Allow StateMachine to have class level OnEventDoActions.
                         Runtime.NotifyInvokedAction(this, handler.MethodInfo, CurrentStateName, CurrentStateName, e);
                         await InvokeActionAsync(handler, e);
                     }
@@ -1089,7 +1088,7 @@ private Task ApplyEventHandlerTransitionAsync(Transition transition, Event e)
             }
             else if (transition.TypeValue is Transition.Type.Halt)
             {
-                // If it is the halt transition, then change the actor status to halting.
+                // If it is the halt transition, then change the state machine status to halting.
                 PendingTransition = default;
                 CurrentStatus = Status.Halting;
             }
@@ -1248,7 +1247,7 @@ internal void SetupEventHandlers()
             var syncObject = ActionCacheLocks.GetOrAdd(stateMachineType, _ => new object());
 
             // Locking this syncObject ensures only one thread enters the initialization code to update
-            // the ActionCache for this specific Actor type.
+            // the ActionCache for this specific state machine type.
             lock (syncObject)
             {
                 if (ActionCache.ContainsKey(stateMachineType))

Src/PChecker/CheckerCore/Actors/ActorFactory.cs → Src/PChecker/CheckerCore/Actors/StateMachineFactory.cs

@@ -8,9 +8,9 @@
 namespace PChecker.Actors
 {
     /// <summary>
-    /// Factory for creating actor instances.
+    /// Factory for creating state machine instances.
     /// </summary>
-    internal static class ActorFactory
+    internal static class StateMachineFactory
     {
         /// <summary>
         /// Cache storing actors constructors.
@@ -22,7 +22,7 @@ internal static class ActorFactory
         /// Creates a new <see cref="StateMachine"/> instance of the specified type.
         /// </summary>
         /// <param name="type">The type of the actors.</param>
-        /// <returns>The created actor instance.</returns>
+        /// <returns>The created state machine instance.</returns>
         public static StateMachine Create(Type type)
         {
             Func<StateMachine> constructor = null;

Src/PChecker/CheckerCore/CheckerConfiguration.cs

@@ -213,7 +213,7 @@ public int MaxSchedulingSteps
 
         /// <summary>
         /// If specified, requests a DGML graph of the schedule that contains a bug, if a bug is found.
-        /// This is different from a coverage activity graph, as it will also show actor instances.
+        /// This is different from a coverage activity graph, as it will also show state machine instances.
         /// </summary>
         [DataMember]
         public bool IsDgmlGraphEnabled { get; set; }

Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs

@@ -361,7 +361,7 @@ private StateMachine CreateActor(ActorId id, Type type, string name, StateMachin
                 opGroupId = creator.OperationGroupId;
             }
 
-            var actor = ActorFactory.Create(type);
+            var actor = StateMachineFactory.Create(type);
             IStateMachineManager stateMachineManager = new StateMachineManager(this, actor, opGroupId);
 
             IEventQueue eventQueue = new EventQueue(stateMachineManager, actor);