From f67b723c31d7f93c94f38c1386c361ac7d947f27 Mon Sep 17 00:00:00 2001 From: Christine Zhou Date: Wed, 7 Aug 2024 11:37:44 -0700 Subject: [PATCH] remove commented code --- Src/PChecker/CheckerCore/Actors/Actor.cs | 993 ------------------ .../CheckerCore/Actors/ActorFactory.cs | 12 +- .../CheckerCore/Actors/ActorRuntime.cs | 99 +- .../Actors/EventQueues/EventQueue.cs | 40 +- .../ActionExceptionFilterException.cs | 2 +- .../Actors/Exceptions/OnExceptionOutcome.cs | 2 +- .../Exceptions/UnhandledEventException.cs | 2 +- .../Logging/ActorRuntimeLogTextFormatter.cs | 2 +- .../CheckerCore/Actors/Logging/JsonWriter.cs | 2 +- .../Actors/Managers/ActorManager.cs | 151 --- ...ctorManager.cs => IStateMachineManager.cs} | 24 +- .../Actors/Managers/StateMachineManager.cs | 6 +- .../CheckerCore/Actors/StateMachine.cs | 750 ++++++++++++- .../CheckerCore/PRuntime/PLogFormatter.cs | 5 + .../SystematicTesting/ControlledRuntime.cs | 204 ++-- .../Operations/ActorOperation.cs | 4 +- 16 files changed, 887 insertions(+), 1411 deletions(-) delete mode 100644 Src/PChecker/CheckerCore/Actors/Actor.cs delete mode 100644 Src/PChecker/CheckerCore/Actors/Managers/ActorManager.cs rename Src/PChecker/CheckerCore/Actors/Managers/{IActorManager.cs => IStateMachineManager.cs} (74%) diff --git a/Src/PChecker/CheckerCore/Actors/Actor.cs b/Src/PChecker/CheckerCore/Actors/Actor.cs deleted file mode 100644 index bc2d908bea..0000000000 --- a/Src/PChecker/CheckerCore/Actors/Actor.cs +++ /dev/null @@ -1,993 +0,0 @@ -// Copyright (c) Microsoft Corporation. -// Licensed under the MIT License. - -using System; -using System.Collections.Concurrent; -using System.Collections.Generic; -using System.Globalization; -using System.IO; -using System.Linq; -using System.Reflection; -using System.Runtime.CompilerServices; -using System.Threading.Tasks; -using PChecker.Actors.EventQueues; -using PChecker.Actors.Events; -using PChecker.Actors.Exceptions; -using PChecker.Actors.Handlers; -using PChecker.Actors.Logging; -using PChecker.Actors.Managers; -using PChecker.Exceptions; -using PChecker.IO.Debugging; -using EventInfo = PChecker.Actors.Events.EventInfo; - -namespace PChecker.Actors -{ - /// - /// Type that implements an actor. Inherit from this class to declare a custom actor. - /// - public abstract class Actor - { - /// - /// Cache of actor types to a map of event types to action declarations. - /// - private static readonly ConcurrentDictionary> ActionCache = - new ConcurrentDictionary>(); - - /// - /// A set of lockable objects used to protect static initialization of the ActionCache while - /// also enabling multithreaded initialization of different Actor types. - /// - private static readonly ConcurrentDictionary ActionCacheLocks = - new ConcurrentDictionary(); - - /// - /// A cached array that contains a single event type. - /// - private static readonly Type[] SingleEventTypeArray = new Type[] { typeof(Event) }; - - /// - /// The runtime that executes this actor. - /// - internal ActorRuntime Runtime { get; private set; } - - /// - /// Unique id that identifies this actor. - /// - protected internal ActorId Id { get; private set; } - - /// - /// Manages the actor. - /// - internal IActorManager Manager { get; private set; } - - /// - /// The inbox of the actor. Incoming events are enqueued here. - /// Events are dequeued to be processed. - /// - private protected IEventQueue Inbox; - - /// - /// Map from event types to cached action delegates. - /// - private protected readonly Dictionary ActionMap; - - /// - /// The current status of the actor. It is marked volatile as - /// the runtime can read it concurrently. - /// - private protected volatile Status CurrentStatus; - - /// - /// Gets the name of the current state, if there is one. - /// - internal string CurrentStateName { get; private protected set; } - - /// - /// Checks if the actor is halted. - /// - internal bool IsHalted => CurrentStatus is Status.Halted; - - /// - /// Checks if a default handler is available. - /// - internal bool IsDefaultHandlerAvailable { get; private set; } - - /// - /// Id used to identify subsequent operations performed by this actor. 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 - /// value can also be manually set using the property. - /// - protected internal virtual Guid OperationGroupId - { - get => Manager.OperationGroupId; - - set - { - Manager.OperationGroupId = value; - } - } - - /// - /// The installed runtime logger. - /// - protected TextWriter Logger => Runtime.Logger; - - /// - /// The installed runtime json logger. - /// - protected JsonWriter JsonLogger => Runtime.JsonLogger; - - /// - /// Initializes a new instance of the class. - /// - protected Actor() - { - ActionMap = new Dictionary(); - CurrentStatus = Status.Active; - CurrentStateName = default; - IsDefaultHandlerAvailable = false; - } - - /// - /// Configures the actor. - /// - internal void Configure(ActorRuntime runtime, ActorId id, IActorManager manager, IEventQueue inbox) - { - Runtime = runtime; - Id = id; - Manager = manager; - Inbox = inbox; - } - - /// - /// Initializes the actor with the specified optional event. - /// - /// Optional event used for initialization. - internal virtual async Task InitializeAsync(Event initialEvent) - { - // Invoke the custom initializer, if there is one. - await InvokeUserCallbackAsync(UserCallbackType.OnInitialize, initialEvent); - if (CurrentStatus is Status.Halting) - { - await HaltAsync(initialEvent); - } - } - - /// - /// Creates a new actor of the specified type and with the specified optional - /// . This can only be used to access - /// its payload, and cannot be handled. - /// - /// Type of the actor. - /// Optional initialization event. - /// Optional id that can be used to identify this operation. - /// The unique actor id. - protected ActorId CreateActor(Type type, Event initialEvent = null, Guid opGroupId = default) => - Runtime.CreateActor(null, type, null, initialEvent, this, opGroupId); - - /// - /// Creates a new actor 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. - /// Optional name used for logging. - /// Optional initialization event. - /// Optional id that can be used to identify this operation. - /// The unique actor id. - protected ActorId CreateActor(Type type, string name, Event initialEvent = null, Guid opGroupId = default) => - Runtime.CreateActor(null, type, name, initialEvent, this, opGroupId); - - /// - /// Creates a new actor of the specified and name, using the specified - /// unbound actor id, and passes the specified optional . This event - /// can only be used to access its payload, and cannot be handled. - /// - /// Unbound actor id. - /// Type of the actor. - /// Optional name used for logging. - /// Optional initialization event. - /// Optional id that can be used to identify this operation. - protected void CreateActor(ActorId id, Type type, string name, Event initialEvent = null, Guid opGroupId = default) => - Runtime.CreateActor(id, type, name, initialEvent, this, opGroupId); - - /// - /// Sends an asynchronous to a target. - /// - /// The id of the target. - /// The event to send. - /// Optional id that can be used to identify this operation. - protected void SendEvent(ActorId id, Event e, Guid opGroupId = default) => - Runtime.SendEvent(id, e, this, opGroupId); - - /// - /// Waits to receive an of the specified type - /// that satisfies an optional predicate. - /// - /// The event type. - /// The optional predicate. - /// The received event. - protected internal Task ReceiveEventAsync(Type eventType, Func predicate = null) - { - Assert(CurrentStatus is Status.Active, "{0} invoked ReceiveEventAsync while halting.", Id); - Runtime.NotifyReceiveCalled(this); - return Inbox.ReceiveEventAsync(eventType, predicate); - } - - /// - /// Waits to receive an of the specified types. - /// - /// The event types to wait for. - /// The received event. - protected internal Task ReceiveEventAsync(params Type[] eventTypes) - { - Assert(CurrentStatus is Status.Active, "{0} invoked ReceiveEventAsync while halting.", Id); - Runtime.NotifyReceiveCalled(this); - return Inbox.ReceiveEventAsync(eventTypes); - } - - /// - /// Waits to receive an of the specified types - /// that satisfy the specified predicates. - /// - /// Event types and predicates. - /// The received event. - protected internal Task ReceiveEventAsync(params Tuple>[] events) - { - Assert(CurrentStatus is Status.Active, "{0} invoked ReceiveEventAsync while halting.", Id); - Runtime.NotifyReceiveCalled(this); - return Inbox.ReceiveEventAsync(events); - } - - /// - /// Returns a nondeterministic boolean choice, that can be - /// controlled during analysis or testing. - /// - /// The controlled nondeterministic choice. - protected bool RandomBoolean() => Runtime.GetNondeterministicBooleanChoice(2, Id.Name, Id.Type); - - /// - /// Returns a nondeterministic boolean choice, that can be - /// controlled during analysis or testing. The value is used - /// to generate a number in the range [0..maxValue), where 0 - /// triggers true. - /// - /// The max value. - /// The controlled nondeterministic choice. - protected bool RandomBoolean(int maxValue) => - Runtime.GetNondeterministicBooleanChoice(maxValue, Id.Name, Id.Type); - - /// - /// Returns a nondeterministic integer, that can be controlled during - /// analysis or testing. The value is used to generate an integer in - /// the range [0..maxValue). - /// - /// The max value. - /// The controlled nondeterministic integer. - protected int RandomInteger(int maxValue) => - Runtime.GetNondeterministicIntegerChoice(maxValue, Id.Name, Id.Type); - - /// - /// Invokes the specified monitor with the specified . - /// - /// Type of the monitor. - /// Event to send to the monitor. - protected void Monitor(Event e) => Monitor(typeof(T), e); - - /// - /// Invokes the specified monitor with the specified event. - /// - /// Type of the monitor. - /// The event to send. - protected void Monitor(Type type, Event e) - { - Assert(e != null, "{0} is sending a null event.", Id); - Runtime.Monitor(type, e, Id.Name, Id.Type, CurrentStateName); - } - - /// - /// Checks if the assertion holds, and if not, throws an exception. - /// - protected void Assert(bool predicate) => Runtime.Assert(predicate); - - /// - /// Checks if the assertion holds, and if not, throws an exception. - /// - protected void Assert(bool predicate, string s, object arg0) => - Runtime.Assert(predicate, s, arg0); - - /// - /// Checks if the assertion holds, and if not, throws an exception. - /// - protected void Assert(bool predicate, string s, object arg0, object arg1) => - Runtime.Assert(predicate, s, arg0, arg1); - - /// - /// Checks if the assertion holds, and if not, throws an exception. - /// - protected void Assert(bool predicate, string s, object arg0, object arg1, object arg2) => - Runtime.Assert(predicate, s, arg0, arg1, arg2); - - /// - /// Checks if the assertion holds, and if not, throws an exception. - /// - protected void Assert(bool predicate, string s, params object[] args) => - Runtime.Assert(predicate, s, args); - - /// - /// Raises a to halt the actor at the end of the current action. - /// - protected virtual void RaiseHaltEvent() - { - Assert(CurrentStatus is Status.Active, "{0} invoked Halt while halting.", Id); - CurrentStatus = Status.Halting; - } - - /// - /// Asynchronous callback that is invoked when the actor 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 - /// an event from its inbox. This method is not called when the dequeue happens - /// via a receive statement. - /// - /// The event that was dequeued. - 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 - /// 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 - /// it is not prepared to handle. The callback is invoked first, after which the - /// actor will necessarily throw an - /// - /// The event that was unhandled. - /// The state when the event was dequeued. - protected virtual Task OnEventUnhandledAsync(Event e, string state) => Task.CompletedTask; - - /// - /// Asynchronous callback that is invoked when the actor handles an exception. - /// - /// The exception thrown by the actor. - /// The event being handled when the exception was thrown. - /// The action that the runtime should take. - protected virtual Task OnExceptionHandledAsync(Exception ex, Event e) => Task.CompletedTask; - - /// - /// Asynchronous callback that is invoked when the actor halts. - /// - /// The event being handled when the actor halted. - /// Task that represents the asynchronous operation. - protected virtual Task OnHaltAsync(Event e) => Task.CompletedTask; - - /// - /// Enqueues the specified event and its metadata. - /// - internal EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info) - { - if (CurrentStatus is Status.Halted) - { - return EnqueueStatus.Dropped; - } - - return Inbox.Enqueue(e, opGroupId, info); - } - - /// - /// Runs the event handler. The handler terminates if there is no next - /// event to process or if the actor has halted. - /// - internal async Task RunEventHandlerAsync() - { - Event lastDequeuedEvent = null; - while (CurrentStatus != Status.Halted && Runtime.IsRunning) - { - (var status, var e, var opGroupId, var info) = Inbox.Dequeue(); - if (opGroupId != Guid.Empty) - { - // Inherit the operation group id of the dequeued operation, if it is non-empty. - Manager.OperationGroupId = opGroupId; - } - - if (status is DequeueStatus.Success) - { - // 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. - Runtime.NotifyDequeuedEvent(this, e, info); - await InvokeUserCallbackAsync(UserCallbackType.OnEventDequeued, e); - lastDequeuedEvent = e; - } - else if (status is DequeueStatus.Raised) - { - // Only supported by types (e.g. StateMachine) that allow - // the user to explicitly raise events. - Runtime.NotifyHandleRaisedEvent(this, e); - } - else if (status is DequeueStatus.Default) - { - Runtime.LogWriter.LogDefaultEventHandler(Id, CurrentStateName); - - // If the default event was dequeued, then notify the runtime. - // This is only used during bug-finding, because the runtime must - // instrument a scheduling point between default event handlers. - Runtime.NotifyDefaultEventDequeued(this); - } - else if (status is DequeueStatus.NotAvailable) - { - // Terminate the handler as there is no event available. - break; - } - - if (CurrentStatus is Status.Active) - { - // Handles the next event, if the actor is not halted. - await HandleEventAsync(e); - } - - if (!Inbox.IsEventRaised && lastDequeuedEvent != null && CurrentStatus != Status.Halted) - { - // Inform the user that the actor 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. - await HaltAsync(e); - } - } - } - - /// - /// Handles the specified . - /// - private protected virtual async Task HandleEventAsync(Event e) - { - if (ActionMap.TryGetValue(e.GetType(), out var cachedAction) || - ActionMap.TryGetValue(typeof(WildCardEvent), out cachedAction)) - { - Runtime.NotifyInvokedAction(this, cachedAction.MethodInfo, null, null, e); - await InvokeActionAsync(cachedAction, e); - } - else if (e is HaltEvent) - { - // If it is the halt event, then change the actor status to halting. - CurrentStatus = Status.Halting; - } - else - { - await InvokeUserCallbackAsync(UserCallbackType.OnEventUnhandled, e); - if (CurrentStatus is Status.Active) - { - // If the event cannot be handled then report an error, else halt gracefully. - var ex = new UnhandledEventException(e, default, "Unhandled Event"); - var isHalting = OnUnhandledEventExceptionHandler(ex, e); - Assert(isHalting, "{0} received event '{1}' that cannot be handled.", - Id, e.GetType().FullName); - } - } - } - - /// - /// Invokes the specified action delegate. - /// - private protected async Task InvokeActionAsync(CachedDelegate cachedAction, Event e) - { - try - { - if (cachedAction.IsAsync) - { - Task task = null; - if (cachedAction.Handler is Func taskFuncWithEvent) - { - task = taskFuncWithEvent(e); - } - else if (cachedAction.Handler is Func taskFunc) - { - task = taskFunc(); - } - - Runtime.NotifyWaitTask(this, task); - - // We have no reliable stack for awaited operations. - await task; - } - else if (cachedAction.Handler is Action actionWithEvent) - { - actionWithEvent(e); - } - else if (cachedAction.Handler is Action action) - { - action(); - } - } - catch (Exception ex) when (OnExceptionHandler(ex, cachedAction.MethodInfo.Name, e)) - { - // User handled the exception. - await OnExceptionHandledAsync(ex, e); - } - catch (Exception ex) when (!cachedAction.IsAsync && InvokeOnFailureExceptionFilter(cachedAction, ex)) - { - // Use an exception filter to call OnFailure before the stack - // has been unwound. If the exception filter does not fail-fast, - // it returns false to process the exception normally. - } - catch (Exception ex) - { - await TryHandleActionInvocationExceptionAsync(ex, cachedAction.MethodInfo.Name); - } - } - - /// - /// Invokes the specified event handler user callback. - /// - private protected async Task InvokeUserCallbackAsync(string callbackType, Event e, string currentState = default) - { - try - { - Task task = null; - if (callbackType is UserCallbackType.OnInitialize) - { - task = OnInitializeAsync(e); - } - else if (callbackType is UserCallbackType.OnEventDequeued) - { - task = OnEventDequeuedAsync(e); - } - else if (callbackType is UserCallbackType.OnEventHandled) - { - task = OnEventHandledAsync(e); - } - else if (callbackType is UserCallbackType.OnEventUnhandled) - { - task = OnEventUnhandledAsync(e, currentState); - } - - Runtime.NotifyWaitTask(this, task); - await task; - } - catch (Exception ex) when (OnExceptionHandler(ex, callbackType, e)) - { - // User handled the exception. - await OnExceptionHandledAsync(ex, e); - } - catch (Exception ex) - { - // Reports the unhandled exception. - await TryHandleActionInvocationExceptionAsync(ex, callbackType); - } - } - - /// - /// An exception filter that calls, - /// which can choose to fast-fail the app to get a full dump. - /// - /// The action being executed when the failure occurred. - /// The exception being tested. - private protected bool InvokeOnFailureExceptionFilter(CachedDelegate action, Exception ex) - { - // This is called within the exception filter so the stack has not yet been unwound. - // If the call does not fail-fast, return false to process the exception normally. - Runtime.RaiseOnFailureEvent(new ActionExceptionFilterException(action.MethodInfo.Name, ex)); - return false; - } - - /// - /// Tries to handle an exception thrown during an action invocation. - /// - private protected Task TryHandleActionInvocationExceptionAsync(Exception ex, string actionName) - { - var innerException = ex; - while (innerException is TargetInvocationException) - { - innerException = innerException.InnerException; - } - - if (innerException is AggregateException) - { - innerException = innerException.InnerException; - } - - if (innerException is ExecutionCanceledException || innerException is TaskSchedulerException) - { - CurrentStatus = Status.Halted; - Debug.WriteLine($" {innerException.GetType().Name} was thrown from {Id}."); - } - else - { - // Reports the unhandled exception. - ReportUnhandledException(innerException, actionName); - } - - return Task.CompletedTask; - } - - /// - /// Checks if the specified event is ignored. - /// - internal bool IsEventIgnored(Event e) - { - return false; - } - - /// - /// Returns the hashed state of this actor. - /// - internal virtual int GetHashedState() - { - unchecked - { - var hash = 19; - hash = (hash * 31) + GetType().GetHashCode(); - hash = (hash * 31) + Id.Value.GetHashCode(); - hash = (hash * 31) + IsHalted.GetHashCode(); - - hash = (hash * 31) + Manager.GetCachedState(); - hash = (hash * 31) + Inbox.GetCachedState(); - - return hash; - } - } - - /// - /// Extracts user declarations and sets up the event handlers. - /// - internal virtual void SetupEventHandlers() - { - if (!ActionCache.ContainsKey(GetType())) - { - var actorTypes = new Stack(); - for (var actorType = GetType(); typeof(Actor).IsAssignableFrom(actorType); actorType = actorType.BaseType) - { - actorTypes.Push(actorType); - } - - // process base types in reverse order, so mosts derrived type is cached first. - while (actorTypes.Count > 0) - { - SetupEventHandlers(actorTypes.Pop()); - } - } - - // Now we have all derrived types cached, we can build the combined action map for this type. - for (var actorType = GetType(); typeof(Actor).IsAssignableFrom(actorType); actorType = actorType.BaseType) - { - // Populates the map of event handlers for this actor instance. - foreach (var kvp in ActionCache[actorType]) - { - // use the most derrived action handler for a given event (ignoring any base handlers defined for the same event). - if (!ActionMap.ContainsKey(kvp.Key)) - { - // MethodInfo.Invoke catches the exception to wrap it in a TargetInvocationException. - // This unwinds the stack before the ExecuteAction exception filter is invoked, so - // call through a delegate instead (which is also much faster than Invoke). - ActionMap.Add(kvp.Key, new CachedDelegate(kvp.Value, this)); - } - } - } - } - - private void SetupEventHandlers(Type actorType) - { - // If this type has not already been setup in the ActionCache, then we need to try and grab the ActionCacheLock - // for this type. First make sure we have one and only one lockable object for this type. - var syncObject = ActionCacheLocks.GetOrAdd(actorType, _ => new object()); - - // Locking this syncObject ensures only one thread enters the initialization code to update - // the ActionCache for this specific Actor type. - lock (syncObject) - { - if (ActionCache.ContainsKey(actorType)) - { - // Note: even if we won the GetOrAdd, there is a tiny window of opportunity for another thread - // to slip in and lock the syncObject before us, so we have to check the ActionCache again - // here just in case. - } - else - { - // Events with already declared handlers. - var handledEvents = new HashSet(); - - // Map containing all action bindings. - var actionBindings = new Dictionary(); - var doAttributes = actorType.GetCustomAttributes(typeof(OnEventDoActionAttribute), false) - as OnEventDoActionAttribute[]; - - foreach (var attr in doAttributes) - { - Assert(!handledEvents.Contains(attr.Event), - "{0} declared multiple handlers for event '{1}'.", - actorType.FullName, attr.Event); - actionBindings.Add(attr.Event, new ActionEventHandlerDeclaration(attr.Action)); - handledEvents.Add(attr.Event); - } - - var map = new Dictionary(); - foreach (var action in actionBindings) - { - if (!map.ContainsKey(action.Key)) - { - map.Add(action.Key, GetActionWithName(action.Value.Name)); - } - } - - // Caches the action declarations for this actor type. - ActionCache.TryAdd(actorType, map); - } - } - } - - /// - /// Returns the set of all registered events (for code coverage). - /// It does not include events that are deferred or ignored. - /// - internal HashSet GetAllRegisteredEvents() - { - return new HashSet(from key in ActionMap.Keys select key.FullName); - } - - /// - /// Returns the action with the specified name. - /// - private protected MethodInfo GetActionWithName(string actionName) - { - MethodInfo action; - var actorType = GetType(); - - do - { - var bindingFlags = BindingFlags.Public | BindingFlags.NonPublic | - BindingFlags.Instance | BindingFlags.FlattenHierarchy; - action = actorType.GetMethod(actionName, bindingFlags, Type.DefaultBinder, SingleEventTypeArray, null); - if (action is null) - { - action = actorType.GetMethod(actionName, bindingFlags, Type.DefaultBinder, Array.Empty(), null); - } - - actorType = actorType.BaseType; - } - while (action is null && actorType != typeof(StateMachine) && actorType != typeof(Actor)); - - Assert(action != null, "Cannot detect action declaration '{0}' in '{1}'.", actionName, GetType().FullName); - AssertActionValidity(action); - return action; - } - - /// - /// Checks the validity of the specified action. - /// - private void AssertActionValidity(MethodInfo action) - { - var actionType = action.DeclaringType; - var parameters = action.GetParameters(); - Assert(parameters.Length is 0 || - (parameters.Length is 1 && parameters[0].ParameterType == typeof(Event)), - "Action '{0}' in '{1}' must either accept no parameters or a single parameter of type 'Event'.", - action.Name, actionType.Name); - - // Check if the action is an 'async' method. - if (action.GetCustomAttribute(typeof(AsyncStateMachineAttribute)) != null) - { - Assert(action.ReturnType == typeof(Task), - "Async action '{0}' in '{1}' must have 'Task' return type.", - action.Name, actionType.Name); - } - else - { - Assert(action.ReturnType == typeof(void), - "Action '{0}' in '{1}' must have 'void' return type.", - action.Name, actionType.Name); - } - } - - /// - /// Returns the formatted string to be used with a fair nondeterministic boolean choice. - /// - private protected virtual string FormatFairRandom(string callerMemberName, string callerFilePath, int callerLineNumber) => - string.Format(CultureInfo.InvariantCulture, "{0}_{1}_{2}_{3}", - Id.Name, callerMemberName, callerFilePath, callerLineNumber.ToString()); - - /// - /// Wraps the unhandled exception inside an - /// exception, and throws it to the user. - /// - private protected virtual void ReportUnhandledException(Exception ex, string actionName) - { - Runtime.WrapAndThrowException(ex, $"{0} (action '{1}')", Id, actionName); - } - - /// - /// Invokes user callback when the actor throws an exception. - /// - /// The exception thrown by the actor. - /// 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. - private protected bool OnExceptionHandler(Exception ex, string methodName, Event e) - { - if (ex is ExecutionCanceledException) - { - // Internal exception used during testing. - return false; - } - - Runtime.LogWriter.LogExceptionThrown(Id, CurrentStateName, methodName, ex); - - var outcome = OnException(ex, methodName, e); - if (outcome is OnExceptionOutcome.ThrowException) - { - return false; - } - else if (outcome is OnExceptionOutcome.Halt) - { - CurrentStatus = Status.Halting; - } - - Runtime.LogWriter.LogExceptionHandled(Id, CurrentStateName, methodName, ex); - return true; - } - - /// - /// Invokes user callback when the actor receives an event that it cannot handle. - /// - /// The exception thrown by the actor. - /// The unhandled event. - /// True if the the actor should gracefully halt, else false if the exception - /// should continue to get thrown. - private protected bool OnUnhandledEventExceptionHandler(UnhandledEventException ex, Event e) - { - Runtime.LogWriter.LogExceptionThrown(Id, ex.CurrentStateName, string.Empty, ex); - - var outcome = OnException(ex, string.Empty, e); - if (outcome is OnExceptionOutcome.ThrowException) - { - return false; - } - - CurrentStatus = Status.Halting; - Runtime.LogWriter.LogExceptionHandled(Id, ex.CurrentStateName, string.Empty, ex); - return true; - } - - /// - /// User callback when the actor throws an exception. By default, - /// the actor throws the exception causing the runtime to fail. - /// - /// The exception thrown by the actor. - /// The handler (outermost) that threw the exception. - /// The event being handled when the exception was thrown. - /// The action that the runtime should take. - protected virtual OnExceptionOutcome OnException(Exception ex, string methodName, Event e) - { - return OnExceptionOutcome.ThrowException; - } - - /// - /// Halts the actor. - /// - /// The event being handled when the actor halts. - private protected Task HaltAsync(Event e) - { - CurrentStatus = Status.Halted; - - // Close the inbox, which will stop any subsequent enqueues. - Inbox.Close(); - - Runtime.LogWriter.LogHalt(Id, Inbox.Size); - - // Dispose any held resources. - Inbox.Dispose(); - - // Invoke user callback. - return OnHaltAsync(e); - } - - /// - /// Determines whether the specified object is equal to the current object. - /// - public override bool Equals(object obj) - { - if (obj is Actor m && - GetType() == m.GetType()) - { - return Id.Value == m.Id.Value; - } - - return false; - } - - /// - /// Returns the hash code for this instance. - /// - public override int GetHashCode() - { - return Id.Value.GetHashCode(); - } - - /// - /// Returns a string that represents the current actor. - /// - public override string ToString() - { - return Id.Name; - } - - /// - /// The status of the actor. - /// - private protected enum Status - { - /// - /// The actor is active. - /// - Active = 0, - - /// - /// The actor is halting. - /// - Halting, - - /// - /// The actor is halted. - /// - Halted - } - - /// - /// The type of a user callback. - /// - private protected static class UserCallbackType - { - internal const string OnInitialize = nameof(OnInitializeAsync); - internal const string OnEventDequeued = nameof(OnEventDequeuedAsync); - internal const string OnEventHandled = nameof(OnEventHandledAsync); - internal const string OnEventUnhandled = nameof(OnEventUnhandledAsync); - internal const string OnExceptionHandled = nameof(OnExceptionHandledAsync); - internal const string OnHalt = nameof(OnHaltAsync); - } - - /// - /// Attribute for declaring which action should be invoked - /// to handle a dequeued event of the specified type. - /// - [AttributeUsage(AttributeTargets.Class, AllowMultiple = true)] - protected sealed class OnEventDoActionAttribute : Attribute - { - /// - /// The type of the dequeued event. - /// - internal Type Event; - - /// - /// The name of the action to invoke. - /// - internal string Action; - - /// - /// Initializes a new instance of the class. - /// - /// The type of the dequeued event. - /// The name of the action to invoke. - public OnEventDoActionAttribute(Type eventType, string actionName) - { - Event = eventType; - Action = actionName; - } - } - } -} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/ActorFactory.cs b/Src/PChecker/CheckerCore/Actors/ActorFactory.cs index 7f6929b45f..ecea1cda1a 100644 --- a/Src/PChecker/CheckerCore/Actors/ActorFactory.cs +++ b/Src/PChecker/CheckerCore/Actors/ActorFactory.cs @@ -15,17 +15,17 @@ internal static class ActorFactory /// /// Cache storing actors constructors. /// - private static readonly Dictionary> ActorConstructorCache = - new Dictionary>(); + private static readonly Dictionary> ActorConstructorCache = + new Dictionary>(); /// - /// Creates a new instance of the specified type. + /// Creates a new instance of the specified type. /// /// The type of the actors. /// The created actor instance. - public static Actor Create(Type type) + public static StateMachine Create(Type type) { - Func constructor = null; + Func constructor = null; lock (ActorConstructorCache) { if (!ActorConstructorCache.TryGetValue(type, out constructor)) @@ -36,7 +36,7 @@ public static Actor Create(Type type) throw new Exception("Could not find empty constructor for type " + type.FullName); } - constructor = Expression.Lambda>( + constructor = Expression.Lambda>( Expression.New(constructorInfo)).Compile(); ActorConstructorCache.Add(type, constructor); } diff --git a/Src/PChecker/CheckerCore/Actors/ActorRuntime.cs b/Src/PChecker/CheckerCore/Actors/ActorRuntime.cs index 6398055d29..4743209b19 100644 --- a/Src/PChecker/CheckerCore/Actors/ActorRuntime.cs +++ b/Src/PChecker/CheckerCore/Actors/ActorRuntime.cs @@ -13,7 +13,6 @@ using PChecker.Actors.Events; using PChecker.Actors.Exceptions; using PChecker.Actors.Logging; -using PChecker.Actors.Managers; using PChecker.Random; using PChecker.Runtime; using PChecker.Specifications.Monitors; @@ -29,7 +28,7 @@ internal class ActorRuntime : CoyoteRuntime, IActorRuntime /// /// Map from unique actor ids to actors. /// - private readonly ConcurrentDictionary ActorMap; + private readonly ConcurrentDictionary ActorMap; /// /// Responsible for writing to all registered objects. @@ -58,7 +57,7 @@ internal class ActorRuntime : CoyoteRuntime, IActorRuntime internal ActorRuntime(CheckerConfiguration checkerConfiguration, IRandomValueGenerator valueGenerator) : base(checkerConfiguration, valueGenerator) { - ActorMap = new ConcurrentDictionary(); + ActorMap = new ConcurrentDictionary(); LogWriter = new LogWriter(checkerConfiguration); } @@ -68,7 +67,7 @@ internal ActorRuntime(CheckerConfiguration checkerConfiguration, IRandomValueGen public ActorId CreateActorId(Type type, string name = null) => new ActorId(type, name, this); /// - /// Creates a actor id that is uniquely tied to the specified unique name. The + /// Creates an actor id that is uniquely tied to the specified unique name. The /// returned actor id can either be a fresh id (not yet bound to any actor), or /// it can be bound to a previously created actor. In the second case, this actor /// id can be directly used to communicate with the corresponding actor. @@ -150,56 +149,40 @@ public virtual Task SendEventAndExecuteAsync(ActorId targetId, Event initi /// public virtual Guid GetCurrentOperationGroupId(ActorId currentActorId) { - var actor = GetActorWithId(currentActorId); + var actor = GetActorWithId(currentActorId); return actor is null ? Guid.Empty : actor.OperationGroupId; } /// - /// Creates a new of the specified . + /// Creates a new of the specified . /// internal virtual ActorId CreateActor(ActorId id, Type type, string name, Event initialEvent, - Actor creator, Guid opGroupId) + StateMachine creator, Guid opGroupId) { var actor = CreateActor(id, type, name, creator, opGroupId); - if (actor is StateMachine) - { - LogWriter.LogCreateStateMachine(actor.Id, creator?.Id.Name, creator?.Id.Type); - } - else - { - LogWriter.LogCreateActor(actor.Id, creator?.Id.Name, creator?.Id.Type); - } - + LogWriter.LogCreateStateMachine(actor.Id, creator?.Id.Name, creator?.Id.Type); RunActorEventHandler(actor, initialEvent, true); return actor.Id; } /// - /// Creates a new of the specified . The method + /// Creates a new of the specified . The method /// returns only when the actor is initialized and the (if any) /// is handled. /// internal virtual async Task CreateActorAndExecuteAsync(ActorId id, Type type, string name, - Event initialEvent, Actor creator, Guid opGroupId) + Event initialEvent, StateMachine creator, Guid opGroupId) { var actor = CreateActor(id, type, name, creator, opGroupId); - if (actor is StateMachine) - { - LogWriter.LogCreateStateMachine(actor.Id, creator?.Id.Name, creator?.Id.Type); - } - else - { - LogWriter.LogCreateActor(actor.Id, creator?.Id.Name, creator?.Id.Type); - } - + LogWriter.LogCreateStateMachine(actor.Id, creator?.Id.Name, creator?.Id.Type); await RunActorEventHandlerAsync(actor, initialEvent, true); return actor.Id; } /// - /// Creates a new of the specified . + /// Creates a new of the specified . /// - private Actor CreateActor(ActorId id, Type type, string name, Actor creator, Guid opGroupId) + private StateMachine CreateActor(ActorId id, Type type, string name, StateMachine creator, Guid opGroupId) { throw new NotImplementedException(); } @@ -207,7 +190,7 @@ private Actor CreateActor(ActorId id, Type type, string name, Actor creator, Gui /// /// Sends an asynchronous to an actor. /// - internal virtual void SendEvent(ActorId targetId, Event e, Actor sender, Guid opGroupId) + internal virtual void SendEvent(ActorId targetId, Event e, StateMachine sender, Guid opGroupId) { var enqueueStatus = EnqueueEvent(targetId, e, sender, opGroupId, out var target); if (enqueueStatus is EnqueueStatus.EventHandlerNotRunning) @@ -220,7 +203,7 @@ internal virtual void SendEvent(ActorId targetId, Event e, Actor sender, Guid op /// Sends an asynchronous to an actor. Returns immediately if the target was /// already running. Otherwise blocks until the target handles the event and reaches quiescense. /// - internal virtual async Task SendEventAndExecuteAsync(ActorId targetId, Event e, Actor sender, + internal virtual async Task SendEventAndExecuteAsync(ActorId targetId, Event e, StateMachine sender, Guid opGroupId) { var enqueueStatus = EnqueueEvent(targetId, e, sender, opGroupId, out var target); @@ -236,7 +219,7 @@ internal virtual async Task SendEventAndExecuteAsync(ActorId targetId, Eve /// /// Enqueues an event to the actor with the specified id. /// - private EnqueueStatus EnqueueEvent(ActorId targetId, Event e, Actor sender, Guid opGroupId, out Actor target) + private EnqueueStatus EnqueueEvent(ActorId targetId, Event e, StateMachine sender, Guid opGroupId, out StateMachine target) { if (e is null) { @@ -263,17 +246,17 @@ private EnqueueStatus EnqueueEvent(ActorId targetId, Event e, Actor sender, Guid opGroupId = sender.OperationGroupId; } - target = GetActorWithId(targetId); + target = GetActorWithId(targetId); if (target is null || target.IsHalted) { LogWriter.LogSendEvent(targetId, sender?.Id.Name, sender?.Id.Type, - (sender as StateMachine)?.CurrentStateName ?? string.Empty, e, opGroupId, isTargetHalted: true); + sender?.CurrentStateName ?? string.Empty, e, opGroupId, isTargetHalted: true); TryHandleDroppedEvent(e, targetId); return EnqueueStatus.Dropped; } LogWriter.LogSendEvent(targetId, sender?.Id.Name, sender?.Id.Type, - (sender as StateMachine)?.CurrentStateName ?? string.Empty, e, opGroupId, isTargetHalted: false); + sender?.CurrentStateName ?? string.Empty, e, opGroupId, isTargetHalted: false); var enqueueStatus = target.Enqueue(e, opGroupId, null); if (enqueueStatus == EnqueueStatus.Dropped) @@ -288,7 +271,7 @@ private EnqueueStatus EnqueueEvent(ActorId targetId, Event e, Actor sender, Guid /// Runs a new asynchronous actor event handler. /// This is a fire and forget invocation. /// - private void RunActorEventHandler(Actor actor, Event initialEvent, bool isFresh) + private void RunActorEventHandler(StateMachine actor, Event initialEvent, bool isFresh) { Task.Run(async () => { @@ -319,7 +302,7 @@ private void RunActorEventHandler(Actor actor, Event initialEvent, bool isFresh) /// /// Runs a new asynchronous actor event handler. /// - private async Task RunActorEventHandlerAsync(Actor actor, Event initialEvent, bool isFresh) + private async Task RunActorEventHandlerAsync(StateMachine actor, Event initialEvent, bool isFresh) { try { @@ -369,11 +352,7 @@ internal override void TryCreateMonitor(Type type) /// internal override bool GetNondeterministicBooleanChoice(int maxValue, string callerName, string callerType) { - var result = false; - if (ValueGenerator.Next(maxValue) == 0) - { - result = true; - } + var result = (ValueGenerator.Next(maxValue) == 0); LogWriter.LogRandom(result, callerName, callerType); return result; @@ -392,14 +371,14 @@ internal override int GetNondeterministicIntegerChoice(int maxValue, string call /// or null if no such actor exists. /// private TActor GetActorWithId(ActorId id) - where TActor : Actor => + where TActor : StateMachine => id != null && ActorMap.TryGetValue(id, out var value) && value is TActor actor ? actor : null; /// /// Notifies that an actor invoked an action. /// - internal virtual void NotifyInvokedAction(Actor actor, MethodInfo action, string handlingStateName, + internal virtual void NotifyInvokedAction(StateMachine actor, MethodInfo action, string handlingStateName, string currentStateName, Event receivedEvent) { if (CheckerConfiguration.IsVerbose) @@ -411,11 +390,11 @@ internal virtual void NotifyInvokedAction(Actor actor, MethodInfo action, string /// /// Notifies that an actor dequeued an . /// - internal virtual void NotifyDequeuedEvent(Actor actor, Event e, EventInfo eventInfo) + internal virtual void NotifyDequeuedEvent(StateMachine actor, Event e, EventInfo eventInfo) { if (CheckerConfiguration.IsVerbose) { - var stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : string.Empty; + var stateName = actor.CurrentStateName; LogWriter.LogDequeueEvent(actor.Id, stateName, e); } } @@ -424,7 +403,7 @@ internal virtual void NotifyDequeuedEvent(Actor actor, Event e, EventInfo eventI /// Notifies that an actor dequeued the default . /// [MethodImpl(MethodImplOptions.AggressiveInlining)] - internal virtual void NotifyDefaultEventDequeued(Actor actor) + internal virtual void NotifyDefaultEventDequeued(StateMachine actor) { } @@ -433,18 +412,18 @@ internal virtual void NotifyDefaultEventDequeued(Actor actor) /// checked to see if the default event handler should fire. /// [MethodImpl(MethodImplOptions.AggressiveInlining)] - internal virtual void NotifyDefaultEventHandlerCheck(Actor actor) + internal virtual void NotifyDefaultEventHandlerCheck(StateMachine actor) { } /// /// Notifies that an actor raised an . /// - internal virtual void NotifyRaisedEvent(Actor actor, Event e, EventInfo eventInfo) + internal virtual void NotifyRaisedEvent(StateMachine actor, Event e, EventInfo eventInfo) { if (CheckerConfiguration.IsVerbose) { - var stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : string.Empty; + var stateName = actor.CurrentStateName; LogWriter.LogRaiseEvent(actor.Id, stateName, e); } } @@ -453,27 +432,27 @@ internal virtual void NotifyRaisedEvent(Actor actor, Event e, EventInfo eventInf /// Notifies that an actor is handling a raised . /// [MethodImpl(MethodImplOptions.AggressiveInlining)] - internal virtual void NotifyHandleRaisedEvent(Actor actor, Event e) + internal virtual void NotifyHandleRaisedEvent(StateMachine actor, Event e) { } /// - /// Notifies that an actor called + /// Notifies that an actor called /// or one of its overloaded methods. /// [MethodImpl(MethodImplOptions.AggressiveInlining)] - internal virtual void NotifyReceiveCalled(Actor actor) + internal virtual void NotifyReceiveCalled(StateMachine actor) { } /// /// Notifies that an actor enqueued an event that it was waiting to receive. /// - internal virtual void NotifyReceivedEvent(Actor actor, Event e, EventInfo eventInfo) + internal virtual void NotifyReceivedEvent(StateMachine actor, Event e, EventInfo eventInfo) { if (CheckerConfiguration.IsVerbose) { - var stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : string.Empty; + var stateName = actor.CurrentStateName; LogWriter.LogReceiveEvent(actor.Id, stateName, e, wasBlocked: true); } } @@ -482,11 +461,11 @@ internal virtual void NotifyReceivedEvent(Actor actor, Event e, EventInfo eventI /// Notifies that an actor received an event without waiting because the event /// was already in the inbox when the actor invoked the receive statement. /// - internal virtual void NotifyReceivedEventWithoutWaiting(Actor actor, Event e, EventInfo eventInfo) + internal virtual void NotifyReceivedEventWithoutWaiting(StateMachine actor, Event e, EventInfo eventInfo) { if (CheckerConfiguration.IsVerbose) { - var stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : string.Empty; + var stateName = actor.CurrentStateName; LogWriter.LogReceiveEvent(actor.Id, stateName, e, wasBlocked: false); } } @@ -495,18 +474,18 @@ internal virtual void NotifyReceivedEventWithoutWaiting(Actor actor, Event e, Ev /// Notifies that an actor is waiting for the specified task to complete. /// [MethodImpl(MethodImplOptions.AggressiveInlining)] - internal virtual void NotifyWaitTask(Actor actor, Task task) + internal virtual void NotifyWaitTask(StateMachine actor, Task task) { } /// /// Notifies that an actor is waiting to receive an event of one of the specified types. /// - internal virtual void NotifyWaitEvent(Actor actor, IEnumerable eventTypes) + internal virtual void NotifyWaitEvent(StateMachine actor, IEnumerable eventTypes) { if (CheckerConfiguration.IsVerbose) { - var stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : string.Empty; + var stateName = actor.CurrentStateName; var eventWaitTypesArray = eventTypes.ToArray(); if (eventWaitTypesArray.Length == 1) { diff --git a/Src/PChecker/CheckerCore/Actors/EventQueues/EventQueue.cs b/Src/PChecker/CheckerCore/Actors/EventQueues/EventQueue.cs index 410d50c3fd..a02fe0085b 100644 --- a/Src/PChecker/CheckerCore/Actors/EventQueues/EventQueue.cs +++ b/Src/PChecker/CheckerCore/Actors/EventQueues/EventQueue.cs @@ -18,12 +18,12 @@ internal sealed class EventQueue : IEventQueue /// /// Manages the actor that owns this queue. /// - private readonly IActorManager ActorManager; + private readonly IStateMachineManager StateMachineManager; /// /// The actor that owns this queue. /// - private readonly Actor Actor; + private readonly StateMachine Actor; /// /// The internal queue that contains events with their metadata. @@ -66,9 +66,9 @@ internal sealed class EventQueue : IEventQueue /// /// Initializes a new instance of the class. /// - internal EventQueue(IActorManager actorManager, Actor actor) + internal EventQueue(IStateMachineManager stateMachineManager, StateMachine actor) { - ActorManager = actorManager; + StateMachineManager = stateMachineManager; Actor = actor; Queue = new LinkedList<(Event, Guid, EventInfo)>(); EventWaitTypes = new Dictionary>(); @@ -87,15 +87,15 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info) (predicate is null || predicate(e))) { EventWaitTypes.Clear(); - ActorManager.OnReceiveEvent(e, opGroupId, info); + StateMachineManager.OnReceiveEvent(e, opGroupId, info); ReceiveCompletionSource.SetResult(e); return EnqueueStatus.EventHandlerRunning; } - ActorManager.OnEnqueueEvent(e, opGroupId, info); + StateMachineManager.OnEnqueueEvent(e, opGroupId, info); Queue.AddLast((e, opGroupId, info)); - if (!ActorManager.IsEventHandlerRunning) + if (!StateMachineManager.IsEventHandlerRunning) { if (TryDequeueEvent(true).e is null) { @@ -103,7 +103,7 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info) } else { - ActorManager.IsEventHandlerRunning = true; + StateMachineManager.IsEventHandlerRunning = true; return EnqueueStatus.EventHandlerNotRunning; } } @@ -118,7 +118,7 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info) // have priority over the events in the inbox. if (RaisedEvent != default) { - if (ActorManager.IsEventIgnored(RaisedEvent.e, RaisedEvent.opGroupId, RaisedEvent.info)) + if (StateMachineManager.IsEventIgnored(RaisedEvent.e, RaisedEvent.opGroupId, RaisedEvent.info)) { // TODO: should the user be able to raise an ignored event? // The raised event is ignored in the current state. @@ -132,7 +132,7 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info) } } - var hasDefaultHandler = ActorManager.IsDefaultHandlerAvailable(); + var hasDefaultHandler = StateMachineManager.IsDefaultHandlerAvailable(); if (hasDefaultHandler) { Actor.Runtime.NotifyDefaultEventHandlerCheck(Actor); @@ -150,14 +150,13 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info) if (!hasDefaultHandler) { // There is no default event handler installed, so do not return an event. - ActorManager.IsEventHandlerRunning = false; + StateMachineManager.IsEventHandlerRunning = false; return (DequeueStatus.NotAvailable, null, Guid.Empty, null); } // TODO: check op-id of default event. // A default event handler exists. - var stateName = Actor is StateMachine stateMachine ? - NameResolver.GetStateNameForLogging(stateMachine.CurrentState.GetType()) : string.Empty; + var stateName = NameResolver.GetStateNameForLogging(Actor.CurrentState.GetType()); var eventOrigin = new EventOriginInfo(Actor.Id, Actor.GetType().FullName, stateName); return (DequeueStatus.Default, DefaultEvent.Instance, Guid.Empty, new EventInfo(DefaultEvent.Instance, eventOrigin)); } @@ -176,7 +175,7 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info) var nextNode = node.Next; var currentEvent = node.Value; - if (ActorManager.IsEventIgnored(currentEvent.e, currentEvent.opGroupId, currentEvent.info)) + if (StateMachineManager.IsEventIgnored(currentEvent.e, currentEvent.opGroupId, currentEvent.info)) { if (!checkOnly) { @@ -189,7 +188,7 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info) } // Skips a deferred event. - if (!ActorManager.IsEventDeferred(currentEvent.e, currentEvent.opGroupId, currentEvent.info)) + if (!StateMachineManager.IsEventDeferred(currentEvent.e, currentEvent.opGroupId, currentEvent.info)) { nextAvailableEvent = currentEvent; if (!checkOnly) @@ -209,12 +208,11 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info) /// public void RaiseEvent(Event e, Guid opGroupId) { - var stateName = Actor is StateMachine stateMachine ? - NameResolver.GetStateNameForLogging(stateMachine.CurrentState.GetType()) : string.Empty; + var stateName = NameResolver.GetStateNameForLogging(Actor.CurrentState.GetType()); var eventOrigin = new EventOriginInfo(Actor.Id, Actor.GetType().FullName, stateName); var info = new EventInfo(e, eventOrigin); RaisedEvent = (e, opGroupId, info); - ActorManager.OnRaiseEvent(e, opGroupId, info); + StateMachineManager.OnRaiseEvent(e, opGroupId, info); } /// @@ -279,11 +277,11 @@ private Task ReceiveEventAsync(Dictionary> eventW { ReceiveCompletionSource = new TaskCompletionSource(); EventWaitTypes = eventWaitTypes; - ActorManager.OnWaitEvent(EventWaitTypes.Keys); + StateMachineManager.OnWaitEvent(EventWaitTypes.Keys); return ReceiveCompletionSource.Task; } - ActorManager.OnReceiveEventWithoutWaiting(receivedEvent.e, receivedEvent.opGroupId, receivedEvent.info); + StateMachineManager.OnReceiveEventWithoutWaiting(receivedEvent.e, receivedEvent.opGroupId, receivedEvent.info); return Task.FromResult(receivedEvent.e); } @@ -320,7 +318,7 @@ private void Dispose(bool disposing) foreach (var (e, opGroupId, info) in Queue) { - ActorManager.OnDropEvent(e, opGroupId, info); + StateMachineManager.OnDropEvent(e, opGroupId, info); } Queue.Clear(); diff --git a/Src/PChecker/CheckerCore/Actors/Exceptions/ActionExceptionFilterException.cs b/Src/PChecker/CheckerCore/Actors/Exceptions/ActionExceptionFilterException.cs index dcb74df948..afb53fae99 100644 --- a/Src/PChecker/CheckerCore/Actors/Exceptions/ActionExceptionFilterException.cs +++ b/Src/PChecker/CheckerCore/Actors/Exceptions/ActionExceptionFilterException.cs @@ -7,7 +7,7 @@ namespace PChecker.Actors.Exceptions { /// - /// Exception that is thrown by the runtime upon an action failure. + /// Exception that is thrown by the runtime upon an action failure. /// internal sealed class ActionExceptionFilterException : RuntimeException { diff --git a/Src/PChecker/CheckerCore/Actors/Exceptions/OnExceptionOutcome.cs b/Src/PChecker/CheckerCore/Actors/Exceptions/OnExceptionOutcome.cs index dfa5bea2e3..1a09282f54 100644 --- a/Src/PChecker/CheckerCore/Actors/Exceptions/OnExceptionOutcome.cs +++ b/Src/PChecker/CheckerCore/Actors/Exceptions/OnExceptionOutcome.cs @@ -4,7 +4,7 @@ namespace PChecker.Actors.Exceptions { /// - /// The outcome when an throws an exception. + /// The outcome when an throws an exception. /// public enum OnExceptionOutcome { diff --git a/Src/PChecker/CheckerCore/Actors/Exceptions/UnhandledEventException.cs b/Src/PChecker/CheckerCore/Actors/Exceptions/UnhandledEventException.cs index 97a1891bab..d9a23b7801 100644 --- a/Src/PChecker/CheckerCore/Actors/Exceptions/UnhandledEventException.cs +++ b/Src/PChecker/CheckerCore/Actors/Exceptions/UnhandledEventException.cs @@ -7,7 +7,7 @@ namespace PChecker.Actors.Exceptions { /// - /// Signals that an received an unhandled event. + /// Signals that an received an unhandled event. /// public sealed class UnhandledEventException : RuntimeException { diff --git a/Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogTextFormatter.cs b/Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogTextFormatter.cs index 1fd02e2ac3..86859be235 100644 --- a/Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogTextFormatter.cs +++ b/Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogTextFormatter.cs @@ -225,7 +225,7 @@ public virtual void OnPopState(ActorId id, string currentStateName, string resto /// public virtual void OnPopStateUnhandledEvent(ActorId id, string stateName, Event e) { - var eventName = e.GetType().FullName; + var eventName = e.GetType().Name; var text = $" {id} popped state {stateName} due to unhandled event '{eventName}'."; Logger.WriteLine(text); } diff --git a/Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs b/Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs index 2802f9e715..44a72365db 100644 --- a/Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs +++ b/Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs @@ -15,7 +15,7 @@ internal class VectorClockGenerator { /// /// Nested class for handling FIFO send receive requests. - /// NOTE: In the case of sending to a the same machine with the same event and same payload. + /// NOTE: In the case of sending to the same machine with the same event and same payload. /// private class FifoSendReceiveMapping { diff --git a/Src/PChecker/CheckerCore/Actors/Managers/ActorManager.cs b/Src/PChecker/CheckerCore/Actors/Managers/ActorManager.cs deleted file mode 100644 index 57af77ff75..0000000000 --- a/Src/PChecker/CheckerCore/Actors/Managers/ActorManager.cs +++ /dev/null @@ -1,151 +0,0 @@ -// Copyright (c) Microsoft Corporation. -// Licensed under the MIT License. - -using System; -using System.Collections.Generic; -using System.Runtime.CompilerServices; -using PChecker.Actors.Events; -using PChecker.SystematicTesting; - -namespace PChecker.Actors.Managers.Mocks -{ - /// - /// Implements an actor manager that is used during testing. - /// - internal sealed class ActorManager : IActorManager - { - /// - /// The runtime that executes the actor being managed. - /// - private readonly ControlledRuntime Runtime; - - /// - /// The actor being managed. - /// - private readonly Actor Instance; - - /// - public bool IsEventHandlerRunning { get; set; } - - /// - public Guid OperationGroupId { get; set; } - - /// - /// Program counter used for state-caching. Distinguishes - /// scheduling from non-deterministic choices. - /// - internal int ProgramCounter; - - /// - /// True if a transition statement was called in the current action, else false. - /// - internal bool IsTransitionStatementCalledInCurrentAction; - - /// - /// True if the actor is executing an on exit action, else false. - /// - internal bool IsInsideOnExit; - - /// - /// Initializes a new instance of the class. - /// - internal ActorManager(ControlledRuntime runtime, Actor instance, Guid operationGroupId) - { - Runtime = runtime; - Instance = instance; - IsEventHandlerRunning = true; - OperationGroupId = operationGroupId; - ProgramCounter = 0; - IsTransitionStatementCalledInCurrentAction = false; - IsInsideOnExit = false; - } - - /// - public int GetCachedState() - { - unchecked - { - var hash = 19; - hash = (hash * 31) + IsEventHandlerRunning.GetHashCode(); - hash = (hash * 31) + ProgramCounter; - return hash; - } - } - - /// - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public bool IsEventIgnored(Event e, Guid opGroupId, EventInfo eventInfo) => Instance.IsEventIgnored(e); - - /// - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public bool IsEventDeferred(Event e, Guid opGroupId, EventInfo eventInfo) => false; - - /// - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public bool IsDefaultHandlerAvailable() => Instance.IsDefaultHandlerAvailable; - - /// - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public void OnEnqueueEvent(Event e, Guid opGroupId, EventInfo eventInfo) => - Runtime.LogWriter.LogEnqueueEvent(Instance.Id, e); - - /// - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public void OnRaiseEvent(Event e, Guid opGroupId, EventInfo eventInfo) => - Runtime.LogWriter.LogRaiseEvent(Instance.Id, default, e); - - /// - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public void OnWaitEvent(IEnumerable eventTypes) => - Runtime.NotifyWaitEvent(Instance, eventTypes); - - /// - public void OnReceiveEvent(Event e, Guid opGroupId, EventInfo eventInfo) - { - if (opGroupId != Guid.Empty) - { - // Inherit the operation group id of the receive operation, if it is non-empty. - OperationGroupId = opGroupId; - } - - Runtime.NotifyReceivedEvent(Instance, e, eventInfo); - } - - /// - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public void OnReceiveEventWithoutWaiting(Event e, Guid opGroupId, EventInfo eventInfo) - { - if (opGroupId != Guid.Empty) - { - // Inherit the operation group id of the receive operation, if it is non-empty. - OperationGroupId = opGroupId; - } - - Runtime.NotifyReceivedEventWithoutWaiting(Instance, e, eventInfo); - } - - /// - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public void OnDropEvent(Event e, Guid opGroupId, EventInfo eventInfo) - { - Runtime.TryHandleDroppedEvent(e, Instance.Id); - } - - /// - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public void Assert(bool predicate, string s, object arg0) => Runtime.Assert(predicate, s, arg0); - - /// - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public void Assert(bool predicate, string s, object arg0, object arg1) => Runtime.Assert(predicate, s, arg0, arg1); - - /// - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public void Assert(bool predicate, string s, object arg0, object arg1, object arg2) => - Runtime.Assert(predicate, s, arg0, arg1, arg2); - - /// - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public void Assert(bool predicate, string s, params object[] args) => Runtime.Assert(predicate, s, args); - } -} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Managers/IActorManager.cs b/Src/PChecker/CheckerCore/Actors/Managers/IStateMachineManager.cs similarity index 74% rename from Src/PChecker/CheckerCore/Actors/Managers/IActorManager.cs rename to Src/PChecker/CheckerCore/Actors/Managers/IStateMachineManager.cs index bc2ec7ab8e..35045bda4a 100644 --- a/Src/PChecker/CheckerCore/Actors/Managers/IActorManager.cs +++ b/Src/PChecker/CheckerCore/Actors/Managers/IStateMachineManager.cs @@ -8,22 +8,22 @@ namespace PChecker.Actors.Managers { /// - /// Interface for managing an actor. + /// Interface for managing a state machine. /// - internal interface IActorManager + internal interface IStateMachineManager { /// - /// True if the event handler of the actor is running, else false. + /// True if the event handler of the state machine is running, else false. /// bool IsEventHandlerRunning { get; set; } /// - /// Id used to identify subsequent operations performed by the actor. + /// Id used to identify subsequent operations performed by the state machine. /// Guid OperationGroupId { get; set; } /// - /// Returns the cached state of the actor. + /// Returns the cached state of the state machine. /// int GetCachedState(); @@ -43,33 +43,33 @@ internal interface IActorManager bool IsDefaultHandlerAvailable(); /// - /// Notifies the actor that an event has been enqueued. + /// Notifies the state machine that an event has been enqueued. /// void OnEnqueueEvent(Event e, Guid opGroupId, EventInfo eventInfo); /// - /// Notifies the actor that an event has been raised. + /// Notifies the state machine that an event has been raised. /// void OnRaiseEvent(Event e, Guid opGroupId, EventInfo eventInfo); /// - /// Notifies the actor that it is waiting to receive an event of one of the specified types. + /// Notifies the state machine that it is waiting to receive an event of one of the specified types. /// void OnWaitEvent(IEnumerable eventTypes); /// - /// Notifies the actor that an event it was waiting to receive has been enqueued. + /// Notifies the state machine that an event it was waiting to receive has been enqueued. /// void OnReceiveEvent(Event e, Guid opGroupId, EventInfo eventInfo); /// - /// Notifies the actor that an event it was waiting to receive was already in the - /// event queue when the actor invoked the receive statement. + /// Notifies the state machine that an event it was waiting to receive was already in the + /// event queue when the state machine invoked the receiving statement. /// void OnReceiveEventWithoutWaiting(Event e, Guid opGroupId, EventInfo eventInfo); /// - /// Notifies the actor that an event has been dropped. + /// Notifies the state machine that an event has been dropped. /// void OnDropEvent(Event e, Guid opGroupId, EventInfo eventInfo); diff --git a/Src/PChecker/CheckerCore/Actors/Managers/StateMachineManager.cs b/Src/PChecker/CheckerCore/Actors/Managers/StateMachineManager.cs index 85340b8849..c1a9b1f129 100644 --- a/Src/PChecker/CheckerCore/Actors/Managers/StateMachineManager.cs +++ b/Src/PChecker/CheckerCore/Actors/Managers/StateMachineManager.cs @@ -12,7 +12,7 @@ namespace PChecker.Actors.Managers.Mocks /// /// Implements a state machine manager that is used during testing. /// - internal sealed class StateMachineManager : IActorManager + internal sealed class StateMachineManager : IStateMachineManager { /// /// The runtime that executes the state machine being managed. @@ -94,7 +94,7 @@ public void OnReceiveEvent(Event e, Guid opGroupId, EventInfo eventInfo) { if (opGroupId != Guid.Empty) { - // Inherit the operation group id of the receive operation, if it is non-empty. + // Inherit the operation group id of the receiving operation, if it is non-empty. OperationGroupId = opGroupId; } @@ -107,7 +107,7 @@ public void OnReceiveEventWithoutWaiting(Event e, Guid opGroupId, EventInfo even { if (opGroupId != Guid.Empty) { - // Inherit the operation group id of the receive operation, if it is non-empty. + // Inherit the operation group id of the receiving operation, if it is non-empty. OperationGroupId = opGroupId; } diff --git a/Src/PChecker/CheckerCore/Actors/StateMachine.cs b/Src/PChecker/CheckerCore/Actors/StateMachine.cs index 9ce847400b..6958dfdce6 100644 --- a/Src/PChecker/CheckerCore/Actors/StateMachine.cs +++ b/Src/PChecker/CheckerCore/Actors/StateMachine.cs @@ -5,15 +5,23 @@ using System.Collections.Concurrent; using System.Collections.Generic; using System.Globalization; +using System.IO; using System.Linq; using System.Linq.Expressions; using System.Reflection; +using System.Runtime.CompilerServices; using System.Threading.Tasks; +using PChecker.Actors.EventQueues; using PChecker.Actors.Events; using PChecker.Actors.Exceptions; using PChecker.Actors.Handlers; +using PChecker.Actors.Logging; +using PChecker.Actors.Managers; using PChecker.Actors.StateTransitions; using PChecker.Exceptions; +using PChecker.IO.Debugging; +using EventInfo = PChecker.Actors.Events.EventInfo; + namespace PChecker.Actors { @@ -21,8 +29,30 @@ 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. /// - public abstract class StateMachine : Actor + public abstract class StateMachine { + + /// + /// The runtime that executes this actor. + /// + internal ActorRuntime Runtime { get; private set; } + + /// + /// Unique id that identifies this actor. + /// + protected internal ActorId Id { get; private set; } + + /// + /// Manages the actor. + /// + internal IStateMachineManager Manager { get; private set; } + + /// + /// The inbox of the actor. Incoming events are enqueued here. + /// Events are dequeued to be processed. + /// + private protected IEventQueue Inbox; + /// /// Cache of state machine types to a map of action names to action declarations. /// @@ -35,7 +65,7 @@ public abstract class StateMachine : Actor /// private static readonly ConcurrentDictionary ActionCacheLocks = new ConcurrentDictionary(); - + /// /// Cache of state machine types to a set of all possible states types. /// @@ -47,7 +77,6 @@ public abstract class StateMachine : Actor /// private static readonly ConcurrentDictionary> StateInstanceCache = new ConcurrentDictionary>(); - /// /// A map from event type to EventHandlerDeclaration for those EventHandlerDeclarations that @@ -64,6 +93,32 @@ public abstract class StateMachine : Actor /// Map from action names to cached action delegates for all states in this state machine. /// private readonly Dictionary StateMachineActionMap; + + /// + /// A cached array that contains a single event type. + /// + private static readonly Type[] SingleEventTypeArray = new Type[] { typeof(Event) }; + + /// + /// The current status of the actor. It is marked volatile as + /// the runtime can read it concurrently. + /// + private protected volatile Status CurrentStatus; + + /// + /// Gets the name of the current state, if there is one. + /// + internal string CurrentStateName { get; private protected set; } + + /// + /// Checks if the actor is halted. + /// + internal bool IsHalted => CurrentStatus is Status.Halted; + + /// + /// Checks if a default handler is available. + /// + internal bool IsDefaultHandlerAvailable { get; private set; } /// /// Newly created Transition that hasn't been returned from InvokeActionAsync yet. @@ -74,6 +129,16 @@ public abstract class StateMachine : Actor /// Gets the of the current state. /// protected internal State CurrentState { get; private set; } + + /// + /// The installed runtime logger. + /// + protected TextWriter Logger => Runtime.Logger; + + /// + /// The installed runtime json logger. + /// + protected JsonWriter JsonLogger => Runtime.JsonLogger; /// /// Initializes a new instance of the class. @@ -81,15 +146,172 @@ public abstract class StateMachine : Actor protected StateMachine() : base() { + CurrentStatus = Status.Active; + CurrentStateName = default; + IsDefaultHandlerAvailable = false; EventHandlerMap = EmptyEventHandlerMap; StateMachineActionMap = new Dictionary(); } + + /// + /// Configures the actor. + /// + internal void Configure(ActorRuntime runtime, ActorId id, IStateMachineManager manager, IEventQueue inbox) + { + Runtime = runtime; + Id = id; + Manager = manager; + Inbox = inbox; + } + + /// + /// Returns a nondeterministic boolean choice, that can be + /// controlled during analysis or testing. + /// + /// The controlled nondeterministic choice. + protected bool RandomBoolean() => Runtime.GetNondeterministicBooleanChoice(2, Id.Name, Id.Type); + + /// + /// Returns a nondeterministic boolean choice, that can be + /// controlled during analysis or testing. The value is used + /// to generate a number in the range [0..maxValue), where 0 + /// triggers true. + /// + /// The max value. + /// The controlled nondeterministic choice. + protected bool RandomBoolean(int maxValue) => + Runtime.GetNondeterministicBooleanChoice(maxValue, Id.Name, Id.Type); + + /// + /// Returns a nondeterministic integer, that can be controlled during + /// analysis or testing. The value is used to generate an integer in + /// the range [0..maxValue). + /// + /// The max value. + /// The controlled nondeterministic integer. + protected int RandomInteger(int maxValue) => + Runtime.GetNondeterministicIntegerChoice(maxValue, Id.Name, Id.Type); + + /// + /// Invokes the specified monitor with the specified . + /// + /// Type of the monitor. + /// Event to send to the monitor. + protected void Monitor(Event e) => Monitor(typeof(T), e); + + /// + /// Invokes the specified monitor with the specified event. + /// + /// Type of the monitor. + /// The event to send. + protected void Monitor(Type type, Event e) + { + Assert(e != null, "{0} is sending a null event.", Id); + Runtime.Monitor(type, e, Id.Name, Id.Type, CurrentStateName); + } + + /// + /// Checks if the assertion holds, and if not, throws an exception. + /// + protected void Assert(bool predicate) => Runtime.Assert(predicate); + + /// + /// Checks if the assertion holds, and if not, throws an exception. + /// + protected void Assert(bool predicate, string s, object arg0) => + Runtime.Assert(predicate, s, arg0); + + /// + /// Checks if the assertion holds, and if not, throws an exception. + /// + protected void Assert(bool predicate, string s, object arg0, object arg1) => + Runtime.Assert(predicate, s, arg0, arg1); + + /// + /// Checks if the assertion holds, and if not, throws an exception. + /// + protected void Assert(bool predicate, string s, object arg0, object arg1, object arg2) => + Runtime.Assert(predicate, s, arg0, arg1, arg2); + + /// + /// Checks if the assertion holds, and if not, throws an exception. + /// + 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. + /// + /// 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 + /// an event from its inbox. This method is not called when the dequeue happens + /// via a receive statement. + /// + /// The event that was dequeued. + 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 + /// 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 + /// it is not prepared to handle. The callback is invoked first, after which the + /// actor 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. + /// + /// The exception thrown by the actor. + /// 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. + /// + /// The event being handled when the actor halted. + /// Task that represents the asynchronous operation. + protected Task OnHaltAsync(Event e) => Task.CompletedTask; + + /// + /// Halts the actor. + /// + /// The event being handled when the actor halts. + private protected Task HaltAsync(Event e) + { + CurrentStatus = Status.Halted; + + // Close the inbox, which will stop any subsequent enqueues. + Inbox.Close(); + + Runtime.LogWriter.LogHalt(Id, Inbox.Size); + + // Dispose any held resources. + Inbox.Dispose(); + + // Invoke user callback. + return OnHaltAsync(e); + } + /// /// Initializes the actor with the specified optional event. /// /// Optional event used for initialization. - internal override async Task InitializeAsync(Event initialEvent) + internal async Task InitializeAsync(Event initialEvent) { // Invoke the custom initializer, if there is one. await InvokeUserCallbackAsync(UserCallbackType.OnInitialize, initialEvent); @@ -101,6 +323,484 @@ internal override async Task InitializeAsync(Event initialEvent) await HaltAsync(initialEvent); } } + + /// + /// An exception filter that calls, + /// which can choose to fast-fail the app to get a full dump. + /// + /// The action being executed when the failure occurred. + /// The exception being tested. + private protected bool InvokeOnFailureExceptionFilter(CachedDelegate action, Exception ex) + { + // This is called within the exception filter so the stack has not yet been unwound. + // If the call does not fail-fast, return false to process the exception normally. + Runtime.RaiseOnFailureEvent(new ActionExceptionFilterException(action.MethodInfo.Name, ex)); + return false; + } + + /// + /// Tries to handle an exception thrown during an action invocation. + /// + private protected Task TryHandleActionInvocationExceptionAsync(Exception ex, string actionName) + { + var innerException = ex; + while (innerException is TargetInvocationException) + { + innerException = innerException.InnerException; + } + + if (innerException is AggregateException) + { + innerException = innerException.InnerException; + } + + if (innerException is ExecutionCanceledException || innerException is TaskSchedulerException) + { + CurrentStatus = Status.Halted; + Debug.WriteLine($" {innerException.GetType().Name} was thrown from {Id}."); + } + else + { + // Reports the unhandled exception. + ReportUnhandledException(innerException, actionName); + } + + return Task.CompletedTask; + } + + /// + /// ID used to identify subsequent operations performed by this actor. 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 + /// value can also be manually set using the property. + /// + protected internal Guid OperationGroupId + { + get => Manager.OperationGroupId; + + set + { + Manager.OperationGroupId = value; + } + } + + + /// + /// Creates a new actor 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. + /// Optional name used for logging. + /// Optional initialization event. + /// Optional id that can be used to identify this operation. + /// The unique actor id. + protected ActorId CreateActor(Type type, string name, Event initialEvent = null, Guid opGroupId = default) => + Runtime.CreateActor(null, type, name, initialEvent, this, opGroupId); + + + /// + /// Sends an asynchronous to a target. + /// + /// The id of the target. + /// The event to send. + /// Optional id that can be used to identify this operation. + protected void SendEvent(ActorId id, Event e, Guid opGroupId = default) => + Runtime.SendEvent(id, e, this, opGroupId); + + /// + /// Waits to receive an of the specified type + /// that satisfies an optional predicate. + /// + /// The event type. + /// The optional predicate. + /// The received event. + protected internal Task ReceiveEventAsync(Type eventType, Func predicate = null) + { + Assert(CurrentStatus is Status.Active, "{0} invoked ReceiveEventAsync while halting.", Id); + Runtime.NotifyReceiveCalled(this); + return Inbox.ReceiveEventAsync(eventType, predicate); + } + + /// + /// Waits to receive an of the specified types. + /// + /// The event types to wait for. + /// The received event. + protected internal Task ReceiveEventAsync(params Type[] eventTypes) + { + Assert(CurrentStatus is Status.Active, "{0} invoked ReceiveEventAsync while halting.", Id); + Runtime.NotifyReceiveCalled(this); + return Inbox.ReceiveEventAsync(eventTypes); + } + + /// + /// Waits to receive an of the specified types + /// that satisfy the specified predicates. + /// + /// Event types and predicates. + /// The received event. + protected internal Task ReceiveEventAsync(params Tuple>[] events) + { + Assert(CurrentStatus is Status.Active, "{0} invoked ReceiveEventAsync while halting.", Id); + Runtime.NotifyReceiveCalled(this); + return Inbox.ReceiveEventAsync(events); + } + + /// + /// Runs the event handler. The handler terminates if there is no next + /// event to process or if the actor has halted. + /// + internal async Task RunEventHandlerAsync() + { + Event lastDequeuedEvent = null; + while (CurrentStatus != Status.Halted && Runtime.IsRunning) + { + (var status, var e, var opGroupId, var info) = Inbox.Dequeue(); + if (opGroupId != Guid.Empty) + { + // Inherit the operation group id of the dequeued operation, if it is non-empty. + Manager.OperationGroupId = opGroupId; + } + + if (status is DequeueStatus.Success) + { + // 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. + Runtime.NotifyDequeuedEvent(this, e, info); + await InvokeUserCallbackAsync(UserCallbackType.OnEventDequeued, e); + lastDequeuedEvent = e; + } + else if (status is DequeueStatus.Raised) + { + // Only supported by types (e.g. StateMachine) that allow + // the user to explicitly raise events. + Runtime.NotifyHandleRaisedEvent(this, e); + } + else if (status is DequeueStatus.Default) + { + Runtime.LogWriter.LogDefaultEventHandler(Id, CurrentStateName); + + // If the default event was dequeued, then notify the runtime. + // This is only used during bug-finding, because the runtime must + // instrument a scheduling point between default event handlers. + Runtime.NotifyDefaultEventDequeued(this); + } + else if (status is DequeueStatus.NotAvailable) + { + // Terminate the handler as there is no event available. + break; + } + + if (CurrentStatus is Status.Active) + { + // Handles the next event, if the actor is not halted. + await HandleEventAsync(e); + } + + if (!Inbox.IsEventRaised && lastDequeuedEvent != null && CurrentStatus != Status.Halted) + { + // Inform the user that the actor 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. + await HaltAsync(e); + } + } + } + + /// + /// Invokes the specified event handler user callback. + /// + private protected async Task InvokeUserCallbackAsync(string callbackType, Event e, string currentState = default) + { + try + { + Task task = null; + if (callbackType is UserCallbackType.OnInitialize) + { + task = OnInitializeAsync(e); + } + else if (callbackType is UserCallbackType.OnEventDequeued) + { + task = OnEventDequeuedAsync(e); + } + else if (callbackType is UserCallbackType.OnEventHandled) + { + task = OnEventHandledAsync(e); + } + else if (callbackType is UserCallbackType.OnEventUnhandled) + { + task = OnEventUnhandledAsync(e, currentState); + } + + Runtime.NotifyWaitTask(this, task); + await task; + } + catch (Exception ex) when (OnExceptionHandler(ex, callbackType, e)) + { + // User handled the exception. + await OnExceptionHandledAsync(ex, e); + } + catch (Exception ex) + { + // Reports the unhandled exception. + await TryHandleActionInvocationExceptionAsync(ex, callbackType); + } + } + + /// + /// Invokes the specified action delegate. + /// + private protected async Task InvokeActionAsync(CachedDelegate cachedAction, Event e) + { + try + { + if (cachedAction.IsAsync) + { + Task task = null; + if (cachedAction.Handler is Func taskFuncWithEvent) + { + task = taskFuncWithEvent(e); + } + else if (cachedAction.Handler is Func taskFunc) + { + task = taskFunc(); + } + + Runtime.NotifyWaitTask(this, task); + + // We have no reliable stack for awaited operations. + await task; + } + else if (cachedAction.Handler is Action actionWithEvent) + { + actionWithEvent(e); + } + else if (cachedAction.Handler is Action action) + { + action(); + } + } + catch (Exception ex) when (OnExceptionHandler(ex, cachedAction.MethodInfo.Name, e)) + { + // User handled the exception. + await OnExceptionHandledAsync(ex, e); + } + catch (Exception ex) when (!cachedAction.IsAsync && InvokeOnFailureExceptionFilter(cachedAction, ex)) + { + // Use an exception filter to call OnFailure before the stack + // has been unwound. If the exception filter does not fail-fast, + // it returns false to process the exception normally. + } + catch (Exception ex) + { + await TryHandleActionInvocationExceptionAsync(ex, cachedAction.MethodInfo.Name); + } + } + + /// + /// Returns the action with the specified name. + /// + private protected MethodInfo GetActionWithName(string actionName) + { + MethodInfo action; + var actorType = GetType(); + + do + { + var bindingFlags = BindingFlags.Public | BindingFlags.NonPublic | + BindingFlags.Instance | BindingFlags.FlattenHierarchy; + action = actorType.GetMethod(actionName, bindingFlags, Type.DefaultBinder, SingleEventTypeArray, null); + if (action is null) + { + action = actorType.GetMethod(actionName, bindingFlags, Type.DefaultBinder, Array.Empty(), null); + } + + actorType = actorType.BaseType; + } + while (action is null && actorType != typeof(StateMachine)); + + Assert(action != null, "Cannot detect action declaration '{0}' in '{1}'.", actionName, GetType().FullName); + AssertActionValidity(action); + return action; + } + + /// + /// Checks the validity of the specified action. + /// + private void AssertActionValidity(MethodInfo action) + { + var actionType = action.DeclaringType; + var parameters = action.GetParameters(); + Assert(parameters.Length is 0 || + (parameters.Length is 1 && parameters[0].ParameterType == typeof(Event)), + "Action '{0}' in '{1}' must either accept no parameters or a single parameter of type 'Event'.", + action.Name, actionType.Name); + + // Check if the action is an 'async' method. + if (action.GetCustomAttribute(typeof(AsyncStateMachineAttribute)) != null) + { + Assert(action.ReturnType == typeof(Task), + "Async action '{0}' in '{1}' must have 'Task' return type.", + action.Name, actionType.Name); + } + else + { + Assert(action.ReturnType == typeof(void), + "Action '{0}' in '{1}' must have 'void' return type.", + action.Name, actionType.Name); + } + } + + /// + /// Invokes user callback when the actor throws an exception. + /// + /// The exception thrown by the actor. + /// 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. + private bool OnExceptionHandler(Exception ex, string methodName, Event e) + { + if (ex is ExecutionCanceledException) + { + // Internal exception used during testing. + return false; + } + + Runtime.LogWriter.LogExceptionThrown(Id, CurrentStateName, methodName, ex); + + var outcome = OnException(ex, methodName, e); + if (outcome is OnExceptionOutcome.ThrowException) + { + return false; + } + else if (outcome is OnExceptionOutcome.Halt) + { + CurrentStatus = Status.Halting; + } + + Runtime.LogWriter.LogExceptionHandled(Id, CurrentStateName, methodName, ex); + return true; + } + + /// + /// Invokes user callback when the actor receives an event that it cannot handle. + /// + /// The exception thrown by the actor. + /// The unhandled event. + /// True if the actor should gracefully halt, else false if the exception + /// should continue to get thrown. + private bool OnUnhandledEventExceptionHandler(UnhandledEventException ex, Event e) + { + Runtime.LogWriter.LogExceptionThrown(Id, ex.CurrentStateName, string.Empty, ex); + + var outcome = OnException(ex, string.Empty, e); + if (outcome is OnExceptionOutcome.ThrowException) + { + return false; + } + + CurrentStatus = Status.Halting; + Runtime.LogWriter.LogExceptionHandled(Id, ex.CurrentStateName, string.Empty, ex); + return true; + } + + /// + /// User callback when the actor throws an exception. By default, + /// the actor throws the exception causing the runtime to fail. + /// + /// The exception thrown by the actor. + /// The handler (outermost) that threw the exception. + /// The event being handled when the exception was thrown. + /// The action that the runtime should take. + protected virtual OnExceptionOutcome OnException(Exception ex, string methodName, Event e) + { + return OnExceptionOutcome.ThrowException; + } + + /// + /// Determines whether the specified object is equal to the current object. + /// + public override bool Equals(object obj) + { + if (obj is StateMachine m && + GetType() == m.GetType()) + { + return Id.Value == m.Id.Value; + } + + return false; + } + + /// + /// Returns the hash code for this instance. + /// + public override int GetHashCode() + { + return Id.Value.GetHashCode(); + } + + /// + /// Enqueues the specified event and its metadata. + /// + internal EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info) + { + if (CurrentStatus is Status.Halted) + { + return EnqueueStatus.Dropped; + } + + return Inbox.Enqueue(e, opGroupId, info); + } + + /// + /// Returns a string that represents the current actor. + /// + public override string ToString() + { + return Id.Name; + } + + /// + /// The status of the actor. + /// + private protected enum Status + { + /// + /// The actor is active. + /// + Active = 0, + + /// + /// The actor is halting. + /// + Halting, + + /// + /// The actor is halted. + /// + Halted + } + + /// + /// The type of user callback. + /// + private protected static class UserCallbackType + { + internal const string OnInitialize = nameof(OnInitializeAsync); + internal const string OnEventDequeued = nameof(OnEventDequeuedAsync); + internal const string OnEventHandled = nameof(OnEventHandledAsync); + internal const string OnEventUnhandled = nameof(OnEventUnhandledAsync); + internal const string OnExceptionHandled = nameof(OnExceptionHandledAsync); + internal const string OnHalt = nameof(OnHaltAsync); + } /// /// Raises the specified at the end of the current action. @@ -183,26 +883,19 @@ protected void RaiseGotoStateEvent(Type state) /// , and . /// An Assert is raised if you accidentally try and do two of these operations in a single action. /// - protected override void RaiseHaltEvent() + protected void RaiseHaltEvent() { - base.RaiseHaltEvent(); + Assert(CurrentStatus is Status.Active, "{0} invoked Halt while halting.", Id); + CurrentStatus = Status.Halting; CheckDanglingTransition(); PendingTransition = new Transition(Transition.Type.Halt, null, default); } - - /// - /// Asynchronous callback that is invoked when the actor finishes handling a dequeued - /// event, unless the handler of the dequeued event raised an event or caused the actor - /// to halt (either normally or due to an exception). Unless this callback raises an - /// event, the actor will either become idle or dequeue the next event from its inbox. - /// - /// The event that was handled. - protected override Task OnEventHandledAsync(Event e) => Task.CompletedTask; + /// /// Handles the specified . /// - private protected override async Task HandleEventAsync(Event e) + private protected async Task HandleEventAsync(Event e) { var currentState = CurrentState; @@ -247,7 +940,7 @@ private protected override async Task HandleEventAsync(Event e) // Then specific event is more recent than any wild card events. await HandleEventAsync(e, currentState, ehandler); } - else if (ActionMap.TryGetValue(e.GetType(), out var handler)) + else if (StateMachineActionMap.TryGetValue(e.GetType().Name, out var handler)) { // Allow StateMachine to have class level OnEventDoActions the same way Actor allows. Runtime.NotifyInvokedAction(this, handler.MethodInfo, CurrentStateName, CurrentStateName, e); @@ -260,6 +953,9 @@ private protected override async Task HandleEventAsync(Event e) if (CurrentStatus is Status.Active) { Runtime.LogWriter.LogPopStateUnhandledEvent(Id, CurrentStateName, e); + EventHandlerMap = EmptyEventHandlerMap; + CurrentState = null; + CurrentStateName = string.Empty; continue; } } @@ -523,7 +1219,7 @@ internal bool IsDefaultHandlerInstalledInCurrentState() => /// /// Returns the hashed state of this state machine. /// - internal override int GetHashedState() + internal int GetHashedState() { unchecked { @@ -543,9 +1239,8 @@ internal override int GetHashedState() /// /// Extracts user declarations and setups the event handlers and state transitions. /// - internal override void SetupEventHandlers() + internal void SetupEventHandlers() { - base.SetupEventHandlers(); var stateMachineType = GetType(); // If this type has not already been setup in the ActionCache, then we need to try and grab the ActionCacheLock @@ -701,6 +1396,12 @@ private void ExtractStateTypes(Type type) { StateTypeCache[GetType()].Add(nextType); } + + /* TODO: figure whether this part is needed */ + if (nextType.BaseType != null) + { + stack.Push(nextType.BaseType); + } } } @@ -761,18 +1462,11 @@ private void AssertStateValidity() Assert(CurrentState != null, "{0} must not have a null current state.", Id); } - /// - /// Returns the formatted strint to be used with a fair nondeterministic boolean choice. - /// - private protected override string FormatFairRandom(string callerMemberName, string callerFilePath, int callerLineNumber) => - string.Format(CultureInfo.InvariantCulture, "{0}_{1}_{2}_{3}_{4}", - Id.Name, CurrentStateName, callerMemberName, callerFilePath, callerLineNumber.ToString()); - /// /// Wraps the unhandled exception inside an /// exception, and throws it to the user. /// - private protected override void ReportUnhandledException(Exception ex, string actionName) + private protected void ReportUnhandledException(Exception ex, string actionName) { var state = CurrentState is null ? "" : CurrentStateName; Runtime.WrapAndThrowException(ex, "{0} (state '{1}', action '{2}')", Id, state, actionName); diff --git a/Src/PChecker/CheckerCore/PRuntime/PLogFormatter.cs b/Src/PChecker/CheckerCore/PRuntime/PLogFormatter.cs index 5e70ab79c7..51d4ceb61e 100644 --- a/Src/PChecker/CheckerCore/PRuntime/PLogFormatter.cs +++ b/Src/PChecker/CheckerCore/PRuntime/PLogFormatter.cs @@ -43,6 +43,11 @@ public override void OnStateTransition(ActorId id, string stateName, bool isEntr base.OnStateTransition(id, GetShortName(stateName), isEntry); } + public override void OnPopStateUnhandledEvent(ActorId id, string stateName, Event e) + { + base.OnPopStateUnhandledEvent(id, GetShortName(stateName), e); + } + public override void OnDefaultEventHandler(ActorId id, string stateName) { base.OnDefaultEventHandler(id, GetShortName(stateName)); diff --git a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs index ba5b6a81c6..e44f0a4342 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs @@ -289,7 +289,7 @@ internal ActorId CreateActor(ActorId id, Type type, string name, Event initialEv } /// - internal override ActorId CreateActor(ActorId id, Type type, string name, Event initialEvent, Actor creator, + internal override ActorId CreateActor(ActorId id, Type type, string name, Event initialEvent, StateMachine creator, Guid opGroupId) { AssertExpectedCallerActor(creator, "CreateActor"); @@ -314,7 +314,7 @@ internal Task CreateActorAndExecuteAsync(ActorId id, Type type, string /// internal override async Task CreateActorAndExecuteAsync(ActorId id, Type type, string name, - Event initialEvent, Actor creator, Guid opGroupId) + Event initialEvent, StateMachine creator, Guid opGroupId) { AssertExpectedCallerActor(creator, "CreateActorAndExecuteAsync"); Assert(creator != null, "Only an actor can call 'CreateActorAndExecuteAsync': avoid calling " + @@ -331,9 +331,9 @@ internal override async Task CreateActorAndExecuteAsync(ActorId id, Typ /// /// Creates a new actor of the specified . /// - private Actor CreateActor(ActorId id, Type type, string name, Actor creator, Guid opGroupId) + private StateMachine CreateActor(ActorId id, Type type, string name, StateMachine creator, Guid opGroupId) { - Assert(type.IsSubclassOf(typeof(Actor)), "Type '{0}' is not an actor.", type.FullName); + Assert(type.IsSubclassOf(typeof(StateMachine)), "Type '{0}' is not an actor.", type.FullName); // Using ulong.MaxValue because a Create operation cannot specify // the id of its target, because the id does not exist yet. @@ -362,18 +362,10 @@ private Actor CreateActor(ActorId id, Type type, string name, Actor creator, Gui } var actor = ActorFactory.Create(type); - IActorManager actorManager; - if (actor is StateMachine stateMachine) - { - actorManager = new StateMachineManager(this, stateMachine, opGroupId); - } - else - { - actorManager = new ActorManager(this, actor, opGroupId); - } + IStateMachineManager stateMachineManager = new StateMachineManager(this, actor, opGroupId); - IEventQueue eventQueue = new EventQueue(actorManager, actor); - actor.Configure(this, id, actorManager, eventQueue); + IEventQueue eventQueue = new EventQueue(stateMachineManager, actor); + actor.Configure(this, id, stateMachineManager, eventQueue); actor.SetupEventHandlers(); if (CheckerConfiguration.ReportActivityCoverage) @@ -383,25 +375,18 @@ private Actor CreateActor(ActorId id, Type type, string name, Actor creator, Gui var result = Scheduler.RegisterOperation(new ActorOperation(actor)); Assert(result, "Actor id '{0}' is used by an existing or previously halted actor.", id.Value); - if (actor is StateMachine) - { - LogWriter.LogCreateStateMachine(id, creator?.Id.Name, creator?.Id.Type); - } - else - { - LogWriter.LogCreateActor(id, creator?.Id.Name, creator?.Id.Type); - } + LogWriter.LogCreateStateMachine(id, creator?.Id.Name, creator?.Id.Type); return actor; } /// - internal override void SendEvent(ActorId targetId, Event e, Actor sender, Guid opGroupId) + internal override void SendEvent(ActorId targetId, Event e, StateMachine sender, Guid opGroupId) { if (e is null) { var message = sender != null ? - string.Format("{0} is sending a null event.", sender.Id.ToString()) : + string.Format("{0} is sending a null event.", sender.Id) : "Cannot send a null event."; Assert(false, message); } @@ -425,11 +410,9 @@ internal override void SendEvent(ActorId targetId, Event e, Actor sender, Guid o } /// - internal override async Task SendEventAndExecuteAsync(ActorId targetId, Event e, Actor sender, + internal override async Task SendEventAndExecuteAsync(ActorId targetId, Event e, StateMachine sender, Guid opGroupId) { - Assert(sender is StateMachine, "Only an actor can call 'SendEventAndExecuteAsync': avoid " + - "calling it directly from the test method; instead call it through a test driver actor."); Assert(e != null, "{0} is sending a null event.", sender.Id); Assert(targetId != null, "{0} is sending event {1} to a null actor.", sender.Id, e); AssertExpectedCallerActor(sender, "SendEventAndExecuteAsync"); @@ -437,10 +420,10 @@ internal override async Task SendEventAndExecuteAsync(ActorId targetId, Ev var enqueueStatus = EnqueueEvent(targetId, e, sender, opGroupId, out var target); if (enqueueStatus is EnqueueStatus.EventHandlerNotRunning) { - RunActorEventHandler(target, null, false, sender as StateMachine); + RunActorEventHandler(target, null, false, sender); // Wait until the actor reaches quiescence. - await (sender as StateMachine).ReceiveEventAsync(typeof(QuiescentEvent), rev => (rev as QuiescentEvent).ActorId == targetId); + await sender.ReceiveEventAsync(typeof(QuiescentEvent), rev => (rev as QuiescentEvent).ActorId == targetId); return true; } @@ -453,7 +436,7 @@ internal override async Task SendEventAndExecuteAsync(ActorId targetId, Ev /// /// Enqueues an event to the actor with the specified id. /// - private EnqueueStatus EnqueueEvent(ActorId targetId, Event e, Actor sender, Guid opGroupId, out Actor target) + private EnqueueStatus EnqueueEvent(ActorId targetId, Event e, StateMachine sender, Guid opGroupId, out StateMachine target) { target = Scheduler.GetOperationWithId(targetId.Value)?.Actor; Assert(target != null, @@ -461,7 +444,7 @@ private EnqueueStatus EnqueueEvent(ActorId targetId, Event e, Actor sender, Guid e.GetType().FullName, targetId.Value); Scheduler.ScheduleNextEnabledOperation(AsyncOperationType.Send); - ResetProgramCounter(sender as StateMachine); + ResetProgramCounter(sender); // The operation group id of this operation is set using the following precedence: // (1) To the specified send operation group id, if it is non-empty. @@ -475,7 +458,7 @@ private EnqueueStatus EnqueueEvent(ActorId targetId, Event e, Actor sender, Guid if (target.IsHalted) { LogWriter.LogSendEvent(targetId, sender?.Id.Name, sender?.Id.Type, - (sender as StateMachine)?.CurrentStateName ?? string.Empty, e, opGroupId, isTargetHalted: true); + (sender)?.CurrentStateName ?? string.Empty, e, opGroupId, isTargetHalted: true); TryHandleDroppedEvent(e, targetId); return EnqueueStatus.Dropped; } @@ -490,47 +473,33 @@ private EnqueueStatus EnqueueEvent(ActorId targetId, Event e, Actor sender, Guid } /// - /// Enqueues an event to the actor with the specified id. + /// Enqueues an event to the state machine with the specified id. /// - private EnqueueStatus EnqueueEvent(Actor actor, Event e, Actor sender, Guid opGroupId) + private EnqueueStatus EnqueueEvent(StateMachine stateMachine, Event e, StateMachine sender, Guid opGroupId) { - EventOriginInfo originInfo; - - string stateName = null; - if (sender is StateMachine senderStateMachine) - { - originInfo = new EventOriginInfo(sender.Id, senderStateMachine.GetType().FullName, - NameResolver.GetStateNameForLogging(senderStateMachine.CurrentState.GetType())); - stateName = senderStateMachine.CurrentStateName; - } - else if (sender is Actor senderActor) - { - originInfo = new EventOriginInfo(sender.Id, senderActor.GetType().FullName, string.Empty); - } - else - { - // Message comes from the environment. - originInfo = new EventOriginInfo(null, "Env", "Env"); - } + // Directly use sender as a StateMachine + var originInfo = new EventOriginInfo(sender.Id, sender.GetType().FullName, + NameResolver.GetStateNameForLogging(sender.CurrentState.GetType())); var eventInfo = new EventInfo(e, originInfo); - LogWriter.LogSendEvent(actor.Id, sender?.Id.Name, sender?.Id.Type, stateName, + LogWriter.LogSendEvent(stateMachine.Id, sender.Id.Name, sender.Id.Type, sender.CurrentStateName, e, opGroupId, isTargetHalted: false); - return actor.Enqueue(e, opGroupId, eventInfo); + + return stateMachine.Enqueue(e, opGroupId, eventInfo); } /// - /// Runs a new asynchronous event handler for the specified actor. - /// This is a fire and forget invocation. + /// Runs a new asynchronous event handler for the specified state machine. + /// This is a fire-and-forget invocation. /// - /// The actor that executes this event handler. - /// Optional event for initializing the actor. - /// If true, then this is a new actor. - /// Caller actor that is blocked for quiscence. - private void RunActorEventHandler(Actor actor, Event initialEvent, bool isFresh, Actor syncCaller) + /// The state machine that executes this event handler. + /// Optional event for initializing the state machine. + /// If true, then this is a new state machine. + /// Caller state machine that is blocked for quiescence. + private void RunActorEventHandler(StateMachine stateMachine, Event initialEvent, bool isFresh, StateMachine syncCaller) { - var op = Scheduler.GetOperationWithId(actor.Id.Value); + var op = Scheduler.GetOperationWithId(stateMachine.Id.Value); op.OnEnabled(); var task = new Task(async () => @@ -545,21 +514,21 @@ private void RunActorEventHandler(Actor actor, Event initialEvent, bool isFresh, if (isFresh) { - await actor.InitializeAsync(initialEvent); + await stateMachine.InitializeAsync(initialEvent); } - await actor.RunEventHandlerAsync(); + await stateMachine.RunEventHandlerAsync(); if (syncCaller != null) { - EnqueueEvent(syncCaller, new QuiescentEvent(actor.Id), actor, actor.OperationGroupId); + EnqueueEvent(syncCaller, new QuiescentEvent(stateMachine.Id), stateMachine, stateMachine.OperationGroupId); } - if (!actor.IsHalted) + if (!stateMachine.IsHalted) { - ResetProgramCounter(actor); + ResetProgramCounter(stateMachine); } - Debug.WriteLine(" Completed operation {0} on task '{1}'.", actor.Id, Task.CurrentId); + Debug.WriteLine(" Completed operation {0} on task '{1}'.", stateMachine.Id, Task.CurrentId); op.OnCompleted(); // The actor is inactive or halted, schedule the next enabled operation. @@ -725,7 +694,7 @@ public override void Assert(bool predicate, string s, params object[] args) #if !DEBUG [DebuggerHidden] #endif - private void AssertExpectedCallerActor(Actor caller, string calledAPI) + private void AssertExpectedCallerActor(StateMachine caller, string calledAPI) { if (caller is null) { @@ -773,13 +742,9 @@ internal void CheckNoMonitorInHotStateAtTermination() internal override bool GetNondeterministicBooleanChoice(int maxValue, string callerName, string callerType) { var caller = Scheduler.GetExecutingOperation()?.Actor; - if (caller is StateMachine callerStateMachine) + if (caller != null) { - (callerStateMachine.Manager as StateMachineManager).ProgramCounter++; - } - else if (caller is Actor callerActor) - { - (callerActor.Manager as ActorManager).ProgramCounter++; + (caller.Manager as StateMachineManager).ProgramCounter++; } var choice = Scheduler.GetNextNondeterministicBooleanChoice(maxValue); @@ -791,13 +756,9 @@ internal override bool GetNondeterministicBooleanChoice(int maxValue, string cal internal override int GetNondeterministicIntegerChoice(int maxValue, string callerName, string callerType) { var caller = Scheduler.GetExecutingOperation()?.Actor; - if (caller is StateMachine callerStateMachine) - { - (callerStateMachine.Manager as StateMachineManager).ProgramCounter++; - } - else if (caller is Actor callerActor) + if (caller != null) { - (callerActor.Manager as ActorManager).ProgramCounter++; + (caller.Manager as StateMachineManager).ProgramCounter++; } var choice = Scheduler.GetNextNondeterministicIntegerChoice(maxValue); @@ -838,14 +799,14 @@ internal void ScheduleNextOperation(AsyncOperationType type) } /// - internal override void NotifyInvokedAction(Actor actor, MethodInfo action, string handlingStateName, + internal override void NotifyInvokedAction(StateMachine actor, MethodInfo action, string handlingStateName, string currentStateName, Event receivedEvent) { LogWriter.LogExecuteAction(actor.Id, handlingStateName, currentStateName, action.Name); } /// - internal override void NotifyDequeuedEvent(Actor actor, Event e, EventInfo eventInfo) + internal override void NotifyDequeuedEvent(StateMachine actor, Event e, EventInfo eventInfo) { var op = Scheduler.GetOperationWithId(actor.Id.Value); @@ -861,63 +822,63 @@ internal override void NotifyDequeuedEvent(Actor actor, Event e, EventInfo event ResetProgramCounter(actor); } - var stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : null; + var stateName = actor.CurrentStateName; LogWriter.LogDequeueEvent(actor.Id, stateName, e); } /// - internal override void NotifyDefaultEventDequeued(Actor actor) + internal override void NotifyDefaultEventDequeued(StateMachine actor) { Scheduler.ScheduleNextEnabledOperation(AsyncOperationType.Receive); ResetProgramCounter(actor); } /// - internal override void NotifyDefaultEventHandlerCheck(Actor actor) + internal override void NotifyDefaultEventHandlerCheck(StateMachine actor) { Scheduler.ScheduleNextEnabledOperation(AsyncOperationType.Default); } /// - internal override void NotifyRaisedEvent(Actor actor, Event e, EventInfo eventInfo) + internal override void NotifyRaisedEvent(StateMachine actor, Event e, EventInfo eventInfo) { - var stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : null; + var stateName = actor.CurrentStateName; LogWriter.LogRaiseEvent(actor.Id, stateName, e); } /// - internal override void NotifyHandleRaisedEvent(Actor actor, Event e) + internal override void NotifyHandleRaisedEvent(StateMachine actor, Event e) { - var stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : null; + var stateName = actor.CurrentStateName; LogWriter.LogHandleRaisedEvent(actor.Id, stateName, e); } /// - internal override void NotifyReceiveCalled(Actor actor) + internal override void NotifyReceiveCalled(StateMachine actor) { AssertExpectedCallerActor(actor, "ReceiveEventAsync"); } /// - internal override void NotifyReceivedEvent(Actor actor, Event e, EventInfo eventInfo) + internal override void NotifyReceivedEvent(StateMachine actor, Event e, EventInfo eventInfo) { - var stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : null; + var stateName = actor.CurrentStateName; LogWriter.LogReceiveEvent(actor.Id, stateName, e, wasBlocked: true); var op = Scheduler.GetOperationWithId(actor.Id.Value); op.OnReceivedEvent(); } /// - internal override void NotifyReceivedEventWithoutWaiting(Actor actor, Event e, EventInfo eventInfo) + internal override void NotifyReceivedEventWithoutWaiting(StateMachine actor, Event e, EventInfo eventInfo) { - var stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : null; + var stateName = actor.CurrentStateName; LogWriter.LogReceiveEvent(actor.Id, stateName, e, wasBlocked: false); Scheduler.ScheduleNextEnabledOperation(AsyncOperationType.Receive); ResetProgramCounter(actor); } /// - internal override void NotifyWaitTask(Actor actor, Task task) + internal override void NotifyWaitTask(StateMachine actor, Task task) { Assert(task != null, "{0} is waiting for a null task to complete.", actor.Id); @@ -934,9 +895,9 @@ internal override void NotifyWaitTask(Actor actor, Task task) } /// - internal override void NotifyWaitEvent(Actor actor, IEnumerable eventTypes) + internal override void NotifyWaitEvent(StateMachine actor, IEnumerable eventTypes) { - var stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : null; + var stateName = actor.CurrentStateName; var op = Scheduler.GetOperationWithId(actor.Id.Value); op.OnWaitEvent(eventTypes); @@ -1037,39 +998,26 @@ public CoverageInfo GetCoverageInfo() /// /// Reports actors that are to be covered in coverage report. /// - private void ReportActivityCoverageOfActor(Actor actor) + private void ReportActivityCoverageOfActor(StateMachine actor) { var name = actor.GetType().FullName; if (CoverageInfo.IsMachineDeclared(name)) { return; } - - if (actor is StateMachine stateMachine) + + // Fetch states. + var states = actor.GetAllStates(); + foreach (var state in states) { - // Fetch states. - var states = stateMachine.GetAllStates(); - foreach (var state in states) - { - CoverageInfo.DeclareMachineState(name, state); - } - - // Fetch registered events. - var pairs = stateMachine.GetAllStateEventPairs(); - foreach (var tup in pairs) - { - CoverageInfo.DeclareStateEvent(name, tup.Item1, tup.Item2); - } + CoverageInfo.DeclareMachineState(name, state); } - else - { - var fakeStateName = actor.GetType().Name; - CoverageInfo.DeclareMachineState(name, fakeStateName); - foreach (var eventId in actor.GetAllRegisteredEvents()) - { - CoverageInfo.DeclareStateEvent(name, fakeStateName, eventId); - } + // Fetch registered events. + var pairs = actor.GetAllStateEventPairs(); + foreach (var tup in pairs) + { + CoverageInfo.DeclareStateEvent(name, tup.Item1, tup.Item2); } } @@ -1104,15 +1052,11 @@ private void ReportActivityCoverageOfMonitor(Monitor monitor) /// /// Resets the program counter of the specified actor. /// - private static void ResetProgramCounter(Actor actor) + private static void ResetProgramCounter(StateMachine actor) { - if (actor is StateMachine stateMachine) - { - (stateMachine.Manager as StateMachineManager).ProgramCounter = 0; - } - else if (actor != null) + if (actor != null) { - (actor.Manager as ActorManager).ProgramCounter = 0; + (actor.Manager as StateMachineManager).ProgramCounter = 0; } } diff --git a/Src/PChecker/CheckerCore/SystematicTesting/Operations/ActorOperation.cs b/Src/PChecker/CheckerCore/SystematicTesting/Operations/ActorOperation.cs index a6a43aeb26..af9d103e33 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/Operations/ActorOperation.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/Operations/ActorOperation.cs @@ -18,7 +18,7 @@ internal sealed class ActorOperation : AsyncOperation /// /// The actor that executes this operation. /// - internal readonly Actor Actor; + internal readonly StateMachine Actor; /// /// Unique id of the operation. @@ -46,7 +46,7 @@ internal sealed class ActorOperation : AsyncOperation /// /// Initializes a new instance of the class. /// - internal ActorOperation(Actor actor) + internal ActorOperation(StateMachine actor) : base() { Actor = actor;