diff --git a/Src/PChecker/CheckerCore/Actors/StateMachine.cs b/Src/PChecker/CheckerCore/Actors/StateMachine.cs index 6958dfdce6..25d79b62bd 100644 --- a/Src/PChecker/CheckerCore/Actors/StateMachine.cs +++ b/Src/PChecker/CheckerCore/Actors/StateMachine.cs @@ -26,29 +26,28 @@ namespace PChecker.Actors { /// - /// 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. /// public abstract class StateMachine { /// - /// The runtime that executes this actor. + /// The runtime that executes this state machine. /// internal ActorRuntime Runtime { get; private set; } /// - /// Unique id that identifies this actor. + /// Unique id that identifies this state machine. /// protected internal ActorId Id { get; private set; } /// - /// Manages the actor. + /// Manages the state machine. /// internal IStateMachineManager Manager { get; private set; } /// - /// 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. /// private protected IEventQueue Inbox; @@ -100,7 +99,7 @@ public abstract class StateMachine private static readonly Type[] SingleEventTypeArray = new Type[] { typeof(Event) }; /// - /// 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. /// private protected volatile Status CurrentStatus; @@ -111,7 +110,7 @@ public abstract class StateMachine internal string CurrentStateName { get; private protected set; } /// - /// Checks if the actor is halted. + /// Checks if the state machine is halted. /// internal bool IsHalted => CurrentStatus is Status.Halted; @@ -154,7 +153,7 @@ protected StateMachine() } /// - /// Configures the actor. + /// Configures the state machine. /// internal void Configure(ActorRuntime runtime, ActorId id, IStateMachineManager manager, IEventQueue inbox) { @@ -240,14 +239,14 @@ protected void Assert(bool predicate, string s, params object[] args) => Runtime.Assert(predicate, s, args); /// - /// 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. /// /// Optional event used for initialization. /// Task that represents the asynchronous operation. protected virtual Task OnInitializeAsync(Event initialEvent) => Task.CompletedTask; /// - /// 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. /// @@ -255,42 +254,42 @@ protected void Assert(bool predicate, string s, params object[] args) => protected virtual Task OnEventDequeuedAsync(Event e) => Task.CompletedTask; /// - /// 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. /// /// The event that was handled. protected virtual Task OnEventHandledAsync(Event e) => Task.CompletedTask; /// - /// 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 + /// state machine will necessarily throw an /// /// The event that was unhandled. /// The state when the event was dequeued. protected Task OnEventUnhandledAsync(Event e, string state) => Task.CompletedTask; /// - /// Asynchronous callback that is invoked when the actor handles an exception. + /// Asynchronous callback that is invoked when the state machine handles an exception. /// - /// The exception thrown by the actor. + /// The exception thrown by the state machine. /// The event being handled when the exception was thrown. /// The action that the runtime should take. protected Task OnExceptionHandledAsync(Exception ex, Event e) => Task.CompletedTask; /// - /// Asynchronous callback that is invoked when the actor halts. + /// Asynchronous callback that is invoked when the state machine halts. /// - /// The event being handled when the actor halted. + /// The event being handled when the state machine halted. /// Task that represents the asynchronous operation. protected Task OnHaltAsync(Event e) => Task.CompletedTask; /// - /// Halts the actor. + /// Halts the state machine. /// - /// The event being handled when the actor halts. + /// The event being handled when the state machine halts. private protected Task HaltAsync(Event e) { CurrentStatus = Status.Halted; @@ -308,7 +307,7 @@ private protected Task HaltAsync(Event e) } /// - /// Initializes the actor with the specified optional event. + /// Initializes the state machine with the specified optional event. /// /// Optional event used for initialization. internal async Task InitializeAsync(Event initialEvent) @@ -369,7 +368,7 @@ private protected Task TryHandleActionInvocationExceptionAsync(Exception ex, str } /// - /// 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 or the specified /// upon creation. This value is automatically set to the operation group id of the /// last dequeue or receive operation, if it is not . This @@ -387,15 +386,15 @@ protected internal Guid OperationGroupId /// - /// 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 . This can only be used to /// access its payload, and cannot be handled. /// - /// Type of the actor. + /// Type of the state machine. /// Optional name used for logging. /// Optional initialization event. /// Optional id that can be used to identify this operation. - /// The unique actor id. + /// The unique state machine id. 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 ReceiveEventAsync(params Tuple /// 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. /// 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) } /// - /// Invokes user callback when the actor throws an exception. + /// Invokes user callback when the state machine throws an exception. /// - /// The exception thrown by the actor. + /// The exception thrown by the state machine. /// The handler (outermost) that threw the exception. /// The event being handled when the exception was thrown. /// True if the exception was handled, else false if it should continue to get thrown. @@ -691,11 +690,11 @@ private bool OnExceptionHandler(Exception ex, string methodName, Event e) } /// - /// 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. /// - /// The exception thrown by the actor. + /// The exception thrown by the state machine. /// The unhandled event. - /// True if the actor should gracefully halt, else false if the exception + /// True if the state machine should gracefully halt, else false if the exception /// should continue to get thrown. private bool OnUnhandledEventExceptionHandler(UnhandledEventException ex, Event e) { @@ -713,10 +712,10 @@ private bool OnUnhandledEventExceptionHandler(UnhandledEventException ex, Event } /// - /// 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. /// - /// The exception thrown by the actor. + /// The exception thrown by the state machine. /// The handler (outermost) that threw the exception. /// The event being handled when the exception was thrown. /// The action that the runtime should take. @@ -761,7 +760,7 @@ internal EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info) } /// - /// Returns a string that represents the current actor. + /// Returns a string that represents the current state machine. /// public override string ToString() { @@ -769,22 +768,22 @@ public override string ToString() } /// - /// The status of the actor. + /// The status of the state machine. /// private protected enum Status { /// - /// The actor is active. + /// The state machine is active. /// Active = 0, /// - /// The actor is halting. + /// The state machine is halting. /// Halting, /// - /// The actor is halted. + /// The state machine is halted. /// Halted } @@ -873,7 +872,7 @@ protected void RaiseGotoStateEvent(Type state) } /// - /// Raises a to halt the actor at the end of the current action. + /// Raises a to halt the state machine at the end of the current action. /// /// /// 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)) diff --git a/Src/PChecker/CheckerCore/Actors/ActorFactory.cs b/Src/PChecker/CheckerCore/Actors/StateMachineFactory.cs similarity index 90% rename from Src/PChecker/CheckerCore/Actors/ActorFactory.cs rename to Src/PChecker/CheckerCore/Actors/StateMachineFactory.cs index ecea1cda1a..6e0af4786b 100644 --- a/Src/PChecker/CheckerCore/Actors/ActorFactory.cs +++ b/Src/PChecker/CheckerCore/Actors/StateMachineFactory.cs @@ -8,9 +8,9 @@ namespace PChecker.Actors { /// - /// Factory for creating actor instances. + /// Factory for creating state machine instances. /// - internal static class ActorFactory + internal static class StateMachineFactory { /// /// Cache storing actors constructors. @@ -22,7 +22,7 @@ internal static class ActorFactory /// Creates a new instance of the specified type. /// /// The type of the actors. - /// The created actor instance. + /// The created state machine instance. public static StateMachine Create(Type type) { Func constructor = null; diff --git a/Src/PChecker/CheckerCore/CheckerConfiguration.cs b/Src/PChecker/CheckerCore/CheckerConfiguration.cs index 43e557cf92..04ddade0c5 100644 --- a/Src/PChecker/CheckerCore/CheckerConfiguration.cs +++ b/Src/PChecker/CheckerCore/CheckerConfiguration.cs @@ -213,7 +213,7 @@ public int MaxSchedulingSteps /// /// 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. /// [DataMember] public bool IsDgmlGraphEnabled { get; set; } diff --git a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs index e44f0a4342..cf181d38c0 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs +++ b/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);