From 6ab6f927997c7ca656a08f394789ecadaaee2849 Mon Sep 17 00:00:00 2001 From: Christine Zhou Date: Mon, 19 Aug 2024 16:34:44 -0700 Subject: [PATCH] Changing all references of actor to state machine --- .../Exceptions/OnEventDroppedHandler.cs | 12 - .../CheckerCore/Actors/IActorRuntime.cs | 158 ------- .../CheckerCore/CheckerConfiguration.cs | 2 +- .../Coverage/ActivityCoverageReporter.cs | 2 +- ...=> StateMachineRuntimeLogEventCoverage.cs} | 99 ++--- ... => StateMachineRuntimeLogGraphBuilder.cs} | 106 ++--- .../CheckerCore/PRuntime/GodMachine.cs | 6 +- Src/PChecker/CheckerCore/PRuntime/PEvent.cs | 2 +- .../CheckerCore/PRuntime/PJsonFormatter.cs | 70 ++-- .../CheckerCore/PRuntime/PLogFormatter.cs | 50 +-- Src/PChecker/CheckerCore/PRuntime/PMachine.cs | 10 +- Src/PChecker/CheckerCore/PRuntime/PModule.cs | 4 +- Src/PChecker/CheckerCore/PRuntime/PMonitor.cs | 4 +- .../PRuntime/Values/PMachineValue.cs | 8 +- .../CheckerCore/Runtime/CoyoteRuntime.cs | 6 +- .../CheckerCore/Runtime/ICoyoteRuntime.cs | 4 +- .../CheckerCore/Runtime/RuntimeFactory.cs | 2 +- .../Specifications/CachedDelegate.cs | 2 +- .../CheckerCore/Specifications/Monitor.cs | 14 +- .../EventQueues/DequeueStatus.cs | 2 +- .../EventQueues/EnqueueStatus.cs | 2 +- .../EventQueues/EventQueue.cs | 28 +- .../EventQueues/IEventQueue.cs | 4 +- .../Events/DefaultEvent.cs | 2 +- .../{Actors => StateMachines}/Events/Event.cs | 2 +- .../Events/EventInfo.cs | 2 +- .../Events/EventOriginInfo.cs | 16 +- .../Events/GotoStateEvent.cs | 2 +- .../Events/HaltEvent.cs | 2 +- .../Events/QuiescentEvent.cs | 14 +- .../Events/WildcardEvent.cs | 2 +- .../ActionExceptionFilterException.cs | 2 +- .../Exceptions/OnEventDroppedHandler.cs | 12 + .../Exceptions/OnExceptionOutcome.cs | 8 +- .../Exceptions/UnhandledEventException.cs | 8 +- .../Handlers/ActionEventHandlerDeclaration.cs | 2 +- .../Handlers/CachedDelegate.cs | 6 +- .../Handlers/DeferEventHandlerDeclaration.cs | 2 +- .../Handlers/EventHandlerDeclaration.cs | 2 +- .../Handlers/IgnoreEventHandlerDeclaration.cs | 2 +- .../StateMachines/IStateMachineRuntime.cs | 158 +++++++ .../Logging/IStateMachineRuntimeLog.cs} | 128 +++--- .../Logging/JsonWriter.cs | 37 +- .../Logging/LogWriter.cs | 155 ++++--- .../Logging/PCheckerLogJsonFormatter.cs | 53 ++- .../Logging/PCheckerLogTextFormatter.cs | 60 ++- .../Logging/PCheckerLogXmlFormatter.cs | 74 ++-- .../Managers/IStateMachineManager.cs | 4 +- .../Managers/StateMachineManager.cs | 4 +- .../{Actors => StateMachines}/NameResolver.cs | 2 +- .../{Actors => StateMachines}/StateMachine.cs | 38 +- .../StateMachineFactory.cs | 2 +- .../StateMachineId.cs} | 45 +- .../StateTransitions/GotoStateTransition.cs | 4 +- .../StateTransitions/PushStateTransition.cs | 4 +- .../SystematicTesting/ControlledRuntime.cs | 384 +++++++++--------- .../SystematicTesting/OperationScheduler.cs | 2 +- ...rOperation.cs => StateMachineOperation.cs} | 20 +- .../SystematicTesting/TestMethodInfo.cs | 18 +- .../SystematicTesting/TestingEngine.cs | 20 +- .../SystematicTesting/Traces/ScheduleStep.cs | 4 +- .../SystematicTesting/Traces/ScheduleTrace.cs | 4 +- .../Backend/CSharp/CSharpCodeGenerator.cs | 12 +- .../CompilerCore/Backend/CSharp/Constants.cs | 4 +- .../CompilerCore/Backend/Java/TypeManager.cs | 2 +- 65 files changed, 894 insertions(+), 1027 deletions(-) delete mode 100644 Src/PChecker/CheckerCore/Actors/Exceptions/OnEventDroppedHandler.cs delete mode 100644 Src/PChecker/CheckerCore/Actors/IActorRuntime.cs rename Src/PChecker/CheckerCore/Coverage/{ActorRuntimeLogEventCoverage.cs => StateMachineRuntimeLogEventCoverage.cs} (66%) rename Src/PChecker/CheckerCore/Coverage/{ActorRuntimeLogGraphBuilder.cs => StateMachineRuntimeLogGraphBuilder.cs} (90%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/EventQueues/DequeueStatus.cs (93%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/EventQueues/EnqueueStatus.cs (94%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/EventQueues/EventQueue.cs (93%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/EventQueues/IEventQueue.cs (95%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Events/DefaultEvent.cs (94%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Events/Event.cs (86%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Events/EventInfo.cs (96%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Events/EventOriginInfo.cs (61%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Events/GotoStateEvent.cs (94%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Events/HaltEvent.cs (93%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Events/QuiescentEvent.cs (52%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Events/WildcardEvent.cs (92%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Exceptions/ActionExceptionFilterException.cs (96%) create mode 100644 Src/PChecker/CheckerCore/StateMachines/Exceptions/OnEventDroppedHandler.cs rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Exceptions/OnExceptionOutcome.cs (63%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Exceptions/UnhandledEventException.cs (84%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Handlers/ActionEventHandlerDeclaration.cs (94%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Handlers/CachedDelegate.cs (90%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Handlers/DeferEventHandlerDeclaration.cs (88%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Handlers/EventHandlerDeclaration.cs (87%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Handlers/IgnoreEventHandlerDeclaration.cs (88%) create mode 100644 Src/PChecker/CheckerCore/StateMachines/IStateMachineRuntime.cs rename Src/PChecker/CheckerCore/{Actors/Logging/IActorRuntimeLog.cs => StateMachines/Logging/IStateMachineRuntimeLog.cs} (62%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Logging/JsonWriter.cs (96%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Logging/LogWriter.cs (75%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Logging/PCheckerLogJsonFormatter.cs (58%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Logging/PCheckerLogTextFormatter.cs (82%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Logging/PCheckerLogXmlFormatter.cs (84%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Managers/IStateMachineManager.cs (97%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/Managers/StateMachineManager.cs (98%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/NameResolver.cs (98%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/StateMachine.cs (98%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/StateMachineFactory.cs (98%) rename Src/PChecker/CheckerCore/{Actors/ActorId.cs => StateMachines/StateMachineId.cs} (69%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/StateTransitions/GotoStateTransition.cs (94%) rename Src/PChecker/CheckerCore/{Actors => StateMachines}/StateTransitions/PushStateTransition.cs (89%) rename Src/PChecker/CheckerCore/SystematicTesting/Operations/{ActorOperation.cs => StateMachineOperation.cs} (78%) diff --git a/Src/PChecker/CheckerCore/Actors/Exceptions/OnEventDroppedHandler.cs b/Src/PChecker/CheckerCore/Actors/Exceptions/OnEventDroppedHandler.cs deleted file mode 100644 index a96ad02dc..000000000 --- a/Src/PChecker/CheckerCore/Actors/Exceptions/OnEventDroppedHandler.cs +++ /dev/null @@ -1,12 +0,0 @@ -// Copyright (c) Microsoft Corporation. -// Licensed under the MIT License. - -using PChecker.Actors.Events; - -namespace PChecker.Actors.Exceptions -{ - /// - /// Handles the event. - /// - public delegate void OnEventDroppedHandler(Event e, ActorId target); -} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/IActorRuntime.cs b/Src/PChecker/CheckerCore/Actors/IActorRuntime.cs deleted file mode 100644 index c93bb2909..000000000 --- a/Src/PChecker/CheckerCore/Actors/IActorRuntime.cs +++ /dev/null @@ -1,158 +0,0 @@ -// Copyright (c) Microsoft Corporation. -// Licensed under the MIT License. - -using System; -using System.Threading.Tasks; -using PChecker.Actors.Events; -using PChecker.Actors.Exceptions; -using PChecker.Actors.Logging; -using PChecker.Runtime; - -namespace PChecker.Actors -{ - /// - /// Interface that exposes runtime methods for creating and executing actors. - /// - public interface IActorRuntime : ICoyoteRuntime - { - /// - /// Callback that is fired when an event is dropped. - /// - event OnEventDroppedHandler OnEventDropped; - - /// - /// Creates a fresh actor id that has not yet been bound to any actor. - /// - /// Type of the actor. - /// Optional name used for logging. - /// The result is the actor id. - ActorId CreateActorId(Type type, string name = null); - - /// - /// Creates a 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. - /// - /// Type of the actor. - /// Unique name used to create or get the actor id. - /// The result is the actor id. - ActorId CreateActorIdFromName(Type type, string name); - - /// - /// Creates a new actor of the specified and with the specified - /// optional . This event can only be used to access its payload, - /// and cannot be handled. - /// - /// Type of the actor. - /// Optional event used during initialization. - /// Optional id that can be used to identify this operation. - /// The result is the actor id. - ActorId CreateActor(Type type, Event initialEvent = null, Guid opGroupId = default); - - /// - /// Creates a new actor of the specified and name, and with the - /// specified optional . This event can only be used to access - /// its payload, and cannot be handled. - /// - /// Type of the actor. - /// Optional name used for logging. - /// Optional event used during initialization. - /// Optional id that can be used to identify this operation. - /// The result is the actor id. - ActorId CreateActor(Type type, string name, Event initialEvent = null, Guid opGroupId = default); - - /// - /// Creates a new actor of the specified type, using the specified . - /// This method optionally passes an to the new actor, which can only - /// be used to access its payload, and cannot be handled. - /// - /// Unbound actor id. - /// Type of the actor. - /// Optional event used during initialization. - /// Optional id that can be used to identify this operation. - /// The result is the actor id. - ActorId CreateActor(ActorId id, Type type, Event initialEvent = null, Guid opGroupId = default); - - /// - /// Creates a new actor of the specified and with the specified - /// optional . This event can only be used to access its payload, - /// and cannot be handled. The method returns only when the actor is initialized and - /// the (if any) is handled. - /// - /// Type of the actor. - /// Optional event used during initialization. - /// Optional id that can be used to identify this operation. - /// Task that represents the asynchronous operation. The task result is the actor id. - Task CreateActorAndExecuteAsync(Type type, Event initialEvent = null, Guid opGroupId = default); - - /// - /// Creates a new actor of the specified and name, and with the - /// specified optional . This event can only be used to access - /// its payload, and cannot be handled. The method returns only when the actor is - /// initialized and the (if any) is handled. - /// - /// Type of the actor. - /// Optional name used for logging. - /// Optional event used during initialization. - /// Optional id that can be used to identify this operation. - /// Task that represents the asynchronous operation. The task result is the actor id. - Task CreateActorAndExecuteAsync(Type type, string name, Event initialEvent = null, - Guid opGroupId = default); - - /// - /// Creates a new actor of the specified , 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. The method returns only when - /// the actor is initialized and the (if any) - /// is handled. - /// - /// Unbound actor id. - /// Type of the actor. - /// Optional event used during initialization. - /// Optional id that can be used to identify this operation. - /// Task that represents the asynchronous operation. The task result is the actor id. - Task CreateActorAndExecuteAsync(ActorId id, Type type, Event initialEvent = null, - Guid opGroupId = default); - - /// - /// Sends an asynchronous to an actor. - /// - /// The id of the target. - /// The event to send. - /// Optional id that can be used to identify this operation. - void SendEvent(ActorId targetId, Event e, Guid opGroupId = default); - - /// - /// Sends an to an actor. Returns immediately if the target was already - /// running. Otherwise blocks until the target handles the event and reaches quiescense. - /// - /// The id of the target. - /// The event to send. - /// Optional id that can be used to identify this operation. - /// Task that represents the asynchronous operation. The task result is true if - /// the event was handled, false if the event was only enqueued. - Task SendEventAndExecuteAsync(ActorId targetId, Event e, Guid opGroupId = default); - - /// - /// Returns the operation group id of the actor with the specified id. Returns - /// if the id is not set, or if the is not associated with this runtime. During - /// testing, the runtime asserts that the specified actor is currently executing. - /// - /// The id of the currently executing actor. - /// The unique identifier. - Guid GetCurrentOperationGroupId(ActorId currentActorId); - - /// - /// Use this method to register an . - /// - /// The log writer to register. - void RegisterLog(IActorRuntimeLog log); - - /// - /// Use this method to unregister a previously registered . - /// - /// The previously registered log writer to unregister. - void RemoveLog(IActorRuntimeLog log); - } -} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/CheckerConfiguration.cs b/Src/PChecker/CheckerCore/CheckerConfiguration.cs index 04ddade0c..e7bf83b15 100644 --- a/Src/PChecker/CheckerCore/CheckerConfiguration.cs +++ b/Src/PChecker/CheckerCore/CheckerConfiguration.cs @@ -236,7 +236,7 @@ public int MaxSchedulingSteps /// This is the AssemblyQualifiedName of the type to load. /// [DataMember] - public string CustomActorRuntimeLogType; + public string CustomStateMachineRuntimeLogType; /// /// Enables debugging. diff --git a/Src/PChecker/CheckerCore/Coverage/ActivityCoverageReporter.cs b/Src/PChecker/CheckerCore/Coverage/ActivityCoverageReporter.cs index e0b29a15c..9a3b2f1d4 100644 --- a/Src/PChecker/CheckerCore/Coverage/ActivityCoverageReporter.cs +++ b/Src/PChecker/CheckerCore/Coverage/ActivityCoverageReporter.cs @@ -5,7 +5,7 @@ using System.Collections.Generic; using System.IO; using System.Linq; -using PChecker.Actors.Events; +using PChecker.StateMachines.Events; namespace PChecker.Coverage { diff --git a/Src/PChecker/CheckerCore/Coverage/ActorRuntimeLogEventCoverage.cs b/Src/PChecker/CheckerCore/Coverage/StateMachineRuntimeLogEventCoverage.cs similarity index 66% rename from Src/PChecker/CheckerCore/Coverage/ActorRuntimeLogEventCoverage.cs rename to Src/PChecker/CheckerCore/Coverage/StateMachineRuntimeLogEventCoverage.cs index 8d1385701..f9185b17c 100644 --- a/Src/PChecker/CheckerCore/Coverage/ActorRuntimeLogEventCoverage.cs +++ b/Src/PChecker/CheckerCore/Coverage/StateMachineRuntimeLogEventCoverage.cs @@ -4,28 +4,28 @@ using System; using System.Collections.Generic; using System.Runtime.Serialization; -using PChecker.Actors; -using PChecker.Actors.Events; -using PChecker.Actors.Logging; +using PChecker.StateMachines; +using PChecker.StateMachines.Events; +using PChecker.StateMachines.Logging; namespace PChecker.Coverage { /// - /// This class maintains information about events received and sent from each state of each actor. + /// This class maintains information about events received and sent from each state of each state machine. /// [DataContract] public class EventCoverage { /// - /// Map from states to the list of events received by that state. The state id is fully qualified by - /// the actor id it belongs to. + /// Map from states to the list of events received by that state. The state id is fully qualified by + /// the state machine id it belongs to. /// [DataMember] private readonly Dictionary> EventsReceived = new Dictionary>(); /// /// Map from states to the list of events sent by that state. The state id is fully qualified by - /// the actor id it belongs to. + /// the state machine id it belongs to. /// [DataMember] private readonly Dictionary> EventsSent = new Dictionary>(); @@ -44,7 +44,7 @@ internal void AddEventReceived(string stateId, string eventId) /// /// Get list of events received by the given fully qualified state. /// - /// The actor qualified state name + /// The state machine qualified state name public IEnumerable GetEventsReceived(string stateId) { if (EventsReceived.TryGetValue(stateId, out var set)) @@ -69,7 +69,7 @@ internal void AddEventSent(string stateId, string eventId) /// /// Get list of events sent by the given state. /// - /// The actor qualified state name + /// The state machine qualified state name public IEnumerable GetEventsSent(string stateId) { if (EventsSent.TryGetValue(stateId, out var set)) @@ -102,12 +102,12 @@ private static void MergeHashSets(Dictionary> ours, Dict } } - internal class ActorRuntimeLogEventCoverage : IActorRuntimeLog + internal class StateMachineRuntimeLogEventCoverage : IStateMachineRuntimeLog { private readonly EventCoverage InternalEventCoverage = new EventCoverage(); private Event Dequeued; - public ActorRuntimeLogEventCoverage() + public StateMachineRuntimeLogEventCoverage() { } @@ -121,11 +121,7 @@ public void OnCompleted() { } - public void OnCreateActor(ActorId id, string creatorName, string creatorType) - { - } - - public void OnCreateStateMachine(ActorId id, string creatorName, string creatorType) + public void OnCreateStateMachine(StateMachineId id, string creatorName, string creatorType) { } @@ -133,34 +129,34 @@ public void OnCreateMonitor(string monitorType) { } - public void OnDefaultEventHandler(ActorId id, string stateName) + public void OnDefaultEventHandler(StateMachineId id, string stateName) { Dequeued = DefaultEvent.Instance; } - public void OnDequeueEvent(ActorId id, string stateName, Event e) + public void OnDequeueEvent(StateMachineId id, string stateName, Event e) { Dequeued = e; } - public void OnEnqueueEvent(ActorId id, Event e) + public void OnEnqueueEvent(StateMachineId id, Event e) { } - public void OnExceptionHandled(ActorId id, string stateName, string actionName, Exception ex) + public void OnExceptionHandled(StateMachineId id, string stateName, string actionName, Exception ex) { } - public void OnExceptionThrown(ActorId id, string stateName, string actionName, Exception ex) + public void OnExceptionThrown(StateMachineId id, string stateName, string actionName, Exception ex) { } - public void OnExecuteAction(ActorId id, string handlingStateName, string currentStateName, string actionName) + public void OnExecuteAction(StateMachineId id, string handlingStateName, string currentStateName, string actionName) { OnEventHandled(id, handlingStateName); } - private void OnEventHandled(ActorId id, string stateName) + private void OnEventHandled(StateMachineId id, string stateName) { if (Dequeued != null) { @@ -169,16 +165,16 @@ private void OnEventHandled(ActorId id, string stateName) } } - public void OnGotoState(ActorId id, string currentStateName, string newStateName) + public void OnGotoState(StateMachineId id, string currentStateName, string newStateName) { OnEventHandled(id, currentStateName); } - public void OnHalt(ActorId id, int inboxSize) + public void OnHalt(StateMachineId id, int inboxSize) { } - public void OnHandleRaisedEvent(ActorId id, string stateName, Event e) + public void OnHandleRaisedEvent(StateMachineId id, string stateName, Event e) { Dequeued = e; } @@ -211,39 +207,39 @@ public void OnRandom(object result, string callerName, string callerType) { } - public void OnPopState(ActorId id, string currentStateName, string restoredStateName) + public void OnPopState(StateMachineId id, string currentStateName, string restoredStateName) { } - public void OnPopStateUnhandledEvent(ActorId id, string stateName, Event e) + public void OnPopStateUnhandledEvent(StateMachineId id, string stateName, Event e) { } - public void OnPushState(ActorId id, string currentStateName, string newStateName) + public void OnPushState(StateMachineId id, string currentStateName, string newStateName) { OnEventHandled(id, currentStateName); } - public void OnRaiseEvent(ActorId id, string stateName, Event e) + public void OnRaiseEvent(StateMachineId id, string stateName, Event e) { var eventName = e.GetType().FullName; EventCoverage.AddEventSent(GetStateId(id.Type, stateName), eventName); } - public void OnReceiveEvent(ActorId id, string stateName, Event e, bool wasBlocked) + public void OnReceiveEvent(StateMachineId id, string stateName, Event e, bool wasBlocked) { var eventName = e.GetType().FullName; EventCoverage.AddEventReceived(GetStateId(id.Type, stateName), eventName); } - public void OnSendEvent(ActorId targetActorId, string senderName, string senderType, string senderStateName, + public void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName, Event e, Guid opGroupId, bool isTargetHalted) { var eventName = e.GetType().FullName; EventCoverage.AddEventSent(GetStateId(senderType, senderStateName), eventName); } - public void OnStateTransition(ActorId id, string stateName, bool isEntry) + public void OnStateTransition(StateMachineId id, string stateName, bool isEntry) { } @@ -251,20 +247,20 @@ public void OnStrategyDescription(string strategyName, string description) { } - public void OnWaitEvent(ActorId id, string stateName, Type eventType) + public void OnWaitEvent(StateMachineId id, string stateName, Type eventType) { } - public void OnWaitEvent(ActorId id, string stateName, params Type[] eventTypes) + public void OnWaitEvent(StateMachineId id, string stateName, params Type[] eventTypes) { } - private static string GetStateId(string actorType, string stateName) + private static string GetStateId(string stateMachineType, string stateName) { - var id = ResolveActorTypeName(actorType); + var id = ResolvestateMachineTypeName(stateMachineType); if (string.IsNullOrEmpty(stateName)) { - if (actorType == null) + if (stateMachineType == null) { stateName = "ExternalState"; } @@ -277,35 +273,22 @@ private static string GetStateId(string actorType, string stateName) return id += "." + stateName; } - private static string ResolveActorTypeName(string actorType) + private static string ResolvestateMachineTypeName(string stateMachineType) { - if (actorType == null) + if (stateMachineType == null) { - // The sender id can be null if an event is fired from non-actor code. + // The sender id can be null if an event is fired from non-stateMachine code. return "ExternalCode"; } - return actorType; + return stateMachineType; } - private static string GetLabel(string actorId, string fullyQualifiedName) + private static string GetLabel(string stateMachineId, string fullyQualifiedName) { - if (fullyQualifiedName == null) - { - // then this is probably an Actor, not a StateMachine. For Actors we can invent a state - // name equal to the short name of the class, this then looks like a Constructor which is fine. - var pos = actorId.LastIndexOf("."); - if (pos > 0) - { - return actorId.Substring(pos + 1); - } - - return actorId; - } - - if (fullyQualifiedName.StartsWith(actorId)) + if (fullyQualifiedName.StartsWith(stateMachineId)) { - fullyQualifiedName = fullyQualifiedName.Substring(actorId.Length + 1).Trim('+'); + fullyQualifiedName = fullyQualifiedName.Substring(stateMachineId.Length + 1).Trim('+'); } return fullyQualifiedName; diff --git a/Src/PChecker/CheckerCore/Coverage/ActorRuntimeLogGraphBuilder.cs b/Src/PChecker/CheckerCore/Coverage/StateMachineRuntimeLogGraphBuilder.cs similarity index 90% rename from Src/PChecker/CheckerCore/Coverage/ActorRuntimeLogGraphBuilder.cs rename to Src/PChecker/CheckerCore/Coverage/StateMachineRuntimeLogGraphBuilder.cs index 752570a51..610998bee 100644 --- a/Src/PChecker/CheckerCore/Coverage/ActorRuntimeLogGraphBuilder.cs +++ b/Src/PChecker/CheckerCore/Coverage/StateMachineRuntimeLogGraphBuilder.cs @@ -7,26 +7,25 @@ using System.Runtime.Serialization; using System.Text; using System.Xml.Linq; -using PChecker.Actors; -using PChecker.Actors.Events; -using PChecker.Actors.Logging; +using PChecker.StateMachines; +using PChecker.StateMachines.Events; +using PChecker.StateMachines.Logging; namespace PChecker.Coverage { /// - /// Implements the and builds a directed graph + /// Implements the and builds a directed graph /// from the recorded events and state transitions. /// - public class ActorRuntimeLogGraphBuilder : IActorRuntimeLog + public class StateMachineRuntimeLogGraphBuilder : IStateMachineRuntimeLog { private Graph CurrentGraph; - private readonly Dictionary Dequeued = new Dictionary(); // current dequeued event. - private readonly Dictionary HaltedStates = new Dictionary(); // halted state for given actor. + private readonly Dictionary Dequeued = new Dictionary(); // current dequeued event. + private readonly Dictionary HaltedStates = new Dictionary(); // halted state for given state machine. private readonly bool MergeEventLinks; // merge events from node A to node B instead of making them separate links. private const string ExternalCodeName = "ExternalCode"; private const string ExternalStateName = "ExternalState"; private const string StateMachineCategory = "StateMachine"; - private const string ActorCategory = "Actor"; private const string MonitorCategory = "Monitor"; private class EventInfo @@ -51,7 +50,7 @@ private class PopStateEvent : Event { } - static ActorRuntimeLogGraphBuilder() + static StateMachineRuntimeLogGraphBuilder() { EventAliases[typeof(GotoStateEvent).FullName] = "goto"; EventAliases[typeof(HaltEvent).FullName] = "halt"; @@ -63,9 +62,9 @@ static ActorRuntimeLogGraphBuilder() } /// - /// Initializes a new instance of the class. + /// Initializes a new instance of the class. /// - public ActorRuntimeLogGraphBuilder(bool mergeEventLinks) + public StateMachineRuntimeLogGraphBuilder(bool mergeEventLinks) { MergeEventLinks = mergeEventLinks; CurrentGraph = new Graph(); @@ -102,37 +101,26 @@ public Graph Graph } /// - public void OnCreateActor(ActorId id, string creatorName, string creatorType) + public void OnCreateStateMachine(StateMachineId id, string creatorName, string creatorType) { lock (Inbox) { - var resolvedId = GetResolveActorId(id?.Name, id?.Type); - var node = Graph.GetOrCreateNode(resolvedId); - node.Category = ActorCategory; - } - } - - /// - public void OnCreateStateMachine(ActorId id, string creatorName, string creatorType) - { - lock (Inbox) - { - var resolvedId = GetResolveActorId(id?.Name, id?.Type); + var resolvedId = GetResolveStateMachineId(id?.Name, id?.Type); var node = Graph.GetOrCreateNode(resolvedId); node.Category = StateMachineCategory; } } /// - public void OnSendEvent(ActorId targetActorId, string senderName, string senderType, string senderStateName, + public void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName, Event e, Guid opGroupId, bool isTargetHalted) { var eventName = e.GetType().FullName; - AddEvent(targetActorId.Name, targetActorId.Type, senderName, senderType, senderStateName, eventName); + AddEvent(targetStateMachineId.Name, targetStateMachineId.Type, senderName, senderType, senderStateName, eventName); } /// - public void OnRaiseEvent(ActorId id, string stateName, Event e) + public void OnRaiseEvent(StateMachineId id, string stateName, Event e) { var eventName = e.GetType().FullName; // Raising event to self. @@ -140,16 +128,16 @@ public void OnRaiseEvent(ActorId id, string stateName, Event e) } /// - public void OnEnqueueEvent(ActorId id, Event e) + public void OnEnqueueEvent(StateMachineId id, Event e) { } /// - public void OnDequeueEvent(ActorId id, string stateName, Event e) + public void OnDequeueEvent(StateMachineId id, string stateName, Event e) { lock (Inbox) { - var resolvedId = GetResolveActorId(id?.Name, id?.Type); + var resolvedId = GetResolveStateMachineId(id?.Name, id?.Type); var eventName = e.GetType().FullName; var info = PopEvent(resolvedId, eventName); if (info != null) @@ -181,9 +169,9 @@ private EventInfo PopEvent(string resolvedId, string eventName) } /// - public void OnReceiveEvent(ActorId id, string stateName, Event e, bool wasBlocked) + public void OnReceiveEvent(StateMachineId id, string stateName, Event e, bool wasBlocked) { - var resolvedId = GetResolveActorId(id?.Name, id?.Type); + var resolvedId = GetResolveStateMachineId(id?.Name, id?.Type); lock (Inbox) { if (Inbox.TryGetValue(resolvedId, out var inbox)) @@ -195,7 +183,7 @@ public void OnReceiveEvent(ActorId id, string stateName, Event e, bool wasBlocke if (info.Event == eventName) { // Yay, found it so we can draw the complete link connecting the Sender state to this state! - var category = string.IsNullOrEmpty(stateName) ? ActorCategory : StateMachineCategory; + var category = StateMachineCategory; var source = GetOrCreateChild(info.Name, info.Type, info.State); var target = GetOrCreateChild(id?.Name, id?.Type, category, stateName); GetOrCreateEventLink(source, target, info); @@ -208,17 +196,17 @@ public void OnReceiveEvent(ActorId id, string stateName, Event e, bool wasBlocke } /// - public void OnWaitEvent(ActorId id, string stateName, Type eventType) + public void OnWaitEvent(StateMachineId id, string stateName, Type eventType) { } /// - public void OnWaitEvent(ActorId id, string stateName, params Type[] eventTypes) + public void OnWaitEvent(StateMachineId id, string stateName, params Type[] eventTypes) { } /// - public void OnStateTransition(ActorId id, string stateName, bool isEntry) + public void OnStateTransition(StateMachineId id, string stateName, bool isEntry) { if (isEntry) { @@ -228,19 +216,19 @@ public void OnStateTransition(ActorId id, string stateName, bool isEntry) } /// - public void OnExecuteAction(ActorId id, string handlingStateName, string currentStateName, string actionName) + public void OnExecuteAction(StateMachineId id, string handlingStateName, string currentStateName, string actionName) { LinkTransition(typeof(DoActionEvent), id, handlingStateName, currentStateName, null); } /// - public void OnGotoState(ActorId id, string currentStateName, string newStateName) + public void OnGotoState(StateMachineId id, string currentStateName, string newStateName) { LinkTransition(typeof(GotoStateEvent), id, currentStateName, currentStateName, newStateName); } /// - public void OnHalt(ActorId id, int inboxSize) + public void OnHalt(StateMachineId id, int inboxSize) { lock (Inbox) { @@ -268,11 +256,11 @@ public void OnHalt(ActorId id, int inboxSize) } /// - public void OnDefaultEventHandler(ActorId id, string stateName) + public void OnDefaultEventHandler(StateMachineId id, string stateName) { lock (Inbox) { - var resolvedId = GetResolveActorId(id?.Name, id?.Type); + var resolvedId = GetResolveStateMachineId(id?.Name, id?.Type); var eventName = typeof(DefaultEvent).FullName; AddEvent(id.Name, id.Type, id.Name, id.Type, stateName, eventName); Dequeued[id] = PopEvent(resolvedId, eventName); @@ -280,13 +268,13 @@ public void OnDefaultEventHandler(ActorId id, string stateName) } /// - public void OnHandleRaisedEvent(ActorId id, string stateName, Event e) + public void OnHandleRaisedEvent(StateMachineId id, string stateName, Event e) { lock (Inbox) { // We used the inbox to store raised event, but it should be the first one handled since // raised events are highest priority. - var resolvedId = GetResolveActorId(id?.Name, id?.Type); + var resolvedId = GetResolveStateMachineId(id?.Name, id?.Type); lock (Inbox) { if (Inbox.TryGetValue(resolvedId, out var inbox)) @@ -307,21 +295,21 @@ public void OnHandleRaisedEvent(ActorId id, string stateName, Event e) } /// - public void OnPopStateUnhandledEvent(ActorId actorId, string currentStateName, Event e) + public void OnPopStateUnhandledEvent(StateMachineId stateMachineId, string currentStateName, Event e) { if (e is HaltEvent) { - HaltedStates[actorId] = currentStateName; + HaltedStates[stateMachineId] = currentStateName; } } /// - public void OnExceptionThrown(ActorId id, string stateName, string actionName, Exception ex) + public void OnExceptionThrown(StateMachineId id, string stateName, string actionName, Exception ex) { } /// - public void OnExceptionHandled(ActorId id, string stateName, string actionName, Exception ex) + public void OnExceptionHandled(StateMachineId id, string stateName, string actionName, Exception ex) { } @@ -460,11 +448,11 @@ public Graph SnapshotGraph(bool reset) return result; } - private string GetResolveActorId(string name, string type) + private string GetResolveStateMachineId(string name, string type) { if (type == null) { - // The sender id can be null if an event is fired from non-actor code. + // The sender id can be null if an event is fired from non-stateMachine code. return ExternalCodeName; } @@ -479,7 +467,7 @@ private string GetResolveActorId(string name, string type) private EventInfo AddEvent(string targetName, string targetType, string senderName, string senderType, string senderStateName, string eventName) { - var targetId = GetResolveActorId(targetName, targetType); + var targetId = GetResolveStateMachineId(targetName, targetType); EventInfo info = null; lock (Inbox) { @@ -503,7 +491,7 @@ private EventInfo AddEvent(string targetName, string targetType, string senderNa return info; } - private void LinkTransition(Type transitionType, ActorId id, string handlingStateName, + private void LinkTransition(Type transitionType, StateMachineId id, string handlingStateName, string currentStateName, string newStateName) { var name = id.Name; @@ -548,10 +536,10 @@ private GraphNode GetOrCreateChild(string name, string type, string stateName, s var initalStateName = stateName; - // make label relative to fully qualified actor id (it's usually a nested class). + // make label relative to fully qualified state machine id (it's usually a nested class). stateName = GetLabel(name, type, stateName); - var id = GetResolveActorId(name, type); + var id = GetResolveStateMachineId(name, type); var parent = Graph.GetOrCreateNode(id); parent.AddAttribute("Group", "Expanded"); @@ -626,13 +614,7 @@ private string GetLabel(string name, string type, string fullyQualifiedName) } AddNamespace(type); - if (string.IsNullOrEmpty(fullyQualifiedName)) - { - // then this is probably an Actor, not a StateMachine. For Actors we can invent a state - // name equal to the short name of the class, this then looks like a Constructor which is fine. - fullyQualifiedName = CollapseMachineInstances ? type : name; - } - + var len = fullyQualifiedName.Length; var index = fullyQualifiedName.LastIndexOfAny(TypeSeparators); if (index > 0) @@ -908,8 +890,8 @@ public void WriteDgml(TextWriter writer, bool includeDefaultStyles) -