From 1d95c31d319e7af6ae8af6e8581f0075c8bfd945 Mon Sep 17 00:00:00 2001 From: Ankush Desai Date: Mon, 5 Aug 2024 16:43:24 -0700 Subject: [PATCH] Removed push transitions and cleaned up the state machine code. --- Src/PChecker/CheckerCore/Actors/Actor.cs | 14 +- .../Actors/EventQueues/EventQueue.cs | 4 +- .../CheckerCore/Actors/NameResolver.cs | 5 - .../CheckerCore/Actors/StateMachine.cs | 534 ++---------------- .../SystematicTesting/ControlledRuntime.cs | 2 +- .../CheckerCore/Testing/TestingProcess.cs | 2 +- 6 files changed, 61 insertions(+), 500 deletions(-) diff --git a/Src/PChecker/CheckerCore/Actors/Actor.cs b/Src/PChecker/CheckerCore/Actors/Actor.cs index 1804591e2..bc2d908be 100644 --- a/Src/PChecker/CheckerCore/Actors/Actor.cs +++ b/Src/PChecker/CheckerCore/Actors/Actor.cs @@ -119,12 +119,6 @@ protected internal virtual Guid OperationGroupId /// protected JsonWriter JsonLogger => Runtime.JsonLogger; - /// - /// User-defined hashed state of the actor. Override to improve the - /// accuracy of stateful techniques during testing. - /// - protected virtual int HashedState => 0; - /// /// Initializes a new instance of the class. /// @@ -646,12 +640,6 @@ internal virtual int GetHashedState() hash = (hash * 31) + Manager.GetCachedState(); hash = (hash * 31) + Inbox.GetCachedState(); - if (this.HashedState != 0) - { - // Adds the user-defined hashed state. - hash = (hash * 31) + HashedState; - } - return hash; } } @@ -808,7 +796,7 @@ private void AssertActionValidity(MethodInfo action) } /// - /// Returns the formatted strint to be used with a fair nondeterministic boolean choice. + /// 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}", diff --git a/Src/PChecker/CheckerCore/Actors/EventQueues/EventQueue.cs b/Src/PChecker/CheckerCore/Actors/EventQueues/EventQueue.cs index 29315a9f2..410d50c3f 100644 --- a/Src/PChecker/CheckerCore/Actors/EventQueues/EventQueue.cs +++ b/Src/PChecker/CheckerCore/Actors/EventQueues/EventQueue.cs @@ -157,7 +157,7 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info) // TODO: check op-id of default event. // A default event handler exists. var stateName = Actor is StateMachine stateMachine ? - NameResolver.GetStateNameForLogging(stateMachine.CurrentState) : string.Empty; + NameResolver.GetStateNameForLogging(stateMachine.CurrentState.GetType()) : string.Empty; var eventOrigin = new EventOriginInfo(Actor.Id, Actor.GetType().FullName, stateName); return (DequeueStatus.Default, DefaultEvent.Instance, Guid.Empty, new EventInfo(DefaultEvent.Instance, eventOrigin)); } @@ -210,7 +210,7 @@ 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) : string.Empty; + NameResolver.GetStateNameForLogging(stateMachine.CurrentState.GetType()) : string.Empty; var eventOrigin = new EventOriginInfo(Actor.Id, Actor.GetType().FullName, stateName); var info = new EventInfo(e, eventOrigin); RaisedEvent = (e, opGroupId, info); diff --git a/Src/PChecker/CheckerCore/Actors/NameResolver.cs b/Src/PChecker/CheckerCore/Actors/NameResolver.cs index 501876baf..17cee7344 100644 --- a/Src/PChecker/CheckerCore/Actors/NameResolver.cs +++ b/Src/PChecker/CheckerCore/Actors/NameResolver.cs @@ -36,11 +36,6 @@ internal static string GetQualifiedStateName(Type state) var nextState = state; while (nextState.DeclaringType != null) { - if (!nextState.DeclaringType.IsSubclassOf(typeof(StateMachine.StateGroup))) - { - break; - } - name = string.Format(CultureInfo.InvariantCulture, "{0}.{1}", nextState.DeclaringType.Name, name); nextState = nextState.DeclaringType; } diff --git a/Src/PChecker/CheckerCore/Actors/StateMachine.cs b/Src/PChecker/CheckerCore/Actors/StateMachine.cs index 27e5d910d..9ce847400 100644 --- a/Src/PChecker/CheckerCore/Actors/StateMachine.cs +++ b/Src/PChecker/CheckerCore/Actors/StateMachine.cs @@ -47,19 +47,7 @@ public abstract class StateMachine : Actor /// private static readonly ConcurrentDictionary> StateInstanceCache = new ConcurrentDictionary>(); - - /// - /// A stack of states. The state on the top of the stack represents the current state. - /// - private readonly Stack StateStack; - - /// - /// A map from event type to a Stack of HandlerInfo where the stack contains the inheritable - /// event handlers defined by each state that has been pushed onto the StateStack (if any). - /// The HandlerInfo also remembers which state the handler was defined on so that when the - /// handler is invoked the IActorRuntimeLog can be given that information. - /// - private readonly Dictionary> InheritableEventHandlerMap; + /// /// A map from event type to EventHandlerDeclaration for those EventHandlerDeclarations that @@ -85,7 +73,7 @@ public abstract class StateMachine : Actor /// /// Gets the of the current state. /// - protected internal Type CurrentState { get; private set; } + protected internal State CurrentState { get; private set; } /// /// Initializes a new instance of the class. @@ -93,8 +81,6 @@ public abstract class StateMachine : Actor protected StateMachine() : base() { - StateStack = new Stack(); - InheritableEventHandlerMap = new Dictionary>(); EventHandlerMap = EmptyEventHandlerMap; StateMachineActionMap = new Dictionary(); } @@ -232,7 +218,7 @@ private protected override async Task HandleEventAsync(Event e) break; } - var currentStateName = NameResolver.GetQualifiedStateName(currentState); + var currentStateName = NameResolver.GetQualifiedStateName(currentState.GetType()); await InvokeUserCallbackAsync(UserCallbackType.OnEventUnhandled, e, currentStateName); if (CurrentStatus is Status.Active) { @@ -252,32 +238,14 @@ private protected override async Task HandleEventAsync(Event e) } else if (EventHandlerMap.ContainsKey(e.GetType())) { - await HandleEventAsync(e, StateStack.Peek(), EventHandlerMap[e.GetType()]); + await HandleEventAsync(e, currentState, EventHandlerMap[e.GetType()]); } else { - var hasWildCard = TryGetInheritedHandler(typeof(WildCardEvent), out var wildInfo); - if (EventHandlerMap.ContainsKey(typeof(WildCardEvent))) - { - // A non-inherited wildcard handler cannot beat a "specific" event handler if that - // "specific" event handler is also at the top of the stack. - wildInfo = new HandlerInfo(StateStack.Peek(), StateStack.Count, - EventHandlerMap[typeof(WildCardEvent)]); - hasWildCard = true; - } - - var hasSpecific = TryGetInheritedHandler(e.GetType(), out var info); - - if ((hasWildCard && hasSpecific && wildInfo.StackDepth > info.StackDepth) || - (!hasSpecific && hasWildCard)) - { - // Then wild card takes precedence over earlier specific event handlers. - await HandleEventAsync(e, wildInfo.State, wildInfo.Handler); - } - else if (hasSpecific) + if (TryGetHandler(e.GetType(), out EventHandlerDeclaration ehandler)) { // Then specific event is more recent than any wild card events. - await HandleEventAsync(e, info.State, info.Handler); + await HandleEventAsync(e, currentState, ehandler); } else if (ActionMap.TryGetValue(e.GetType(), out var handler)) { @@ -292,7 +260,6 @@ private protected override async Task HandleEventAsync(Event e) if (CurrentStatus is Status.Active) { Runtime.LogWriter.LogPopStateUnhandledEvent(Id, CurrentStateName, e); - DoStatePop(); continue; } } @@ -302,6 +269,24 @@ private protected override async Task HandleEventAsync(Event e) } } + private bool TryGetHandler(Type e, out EventHandlerDeclaration o) + { + if (EventHandlerMap.ContainsKey(e)) + { + o = EventHandlerMap[e]; + return true; + } + + if (EventHandlerMap.ContainsKey(typeof(WildCardEvent))) + { + o = EventHandlerMap[typeof(WildCardEvent)]; + return true; + } + + o = null; + return false; + } + private async Task HandleEventAsync(Event e, State declaringState, EventHandlerDeclaration eventHandler) { var handlingStateName = NameResolver.GetQualifiedStateName(declaringState.GetType()); @@ -330,9 +315,9 @@ private async Task ExecuteCurrentStateOnEntryAsync(Event e) Runtime.NotifyEnteredState(this); CachedDelegate entryAction = null; - if (StateStack.Peek().EntryAction != null) + if (CurrentState.EntryAction != null) { - entryAction = StateMachineActionMap[StateStack.Peek().EntryAction]; + entryAction = StateMachineActionMap[CurrentState.EntryAction]; } // Invokes the entry action of the new state, if there is one available. @@ -352,9 +337,9 @@ private async Task ExecuteCurrentStateOnExitAsync(string eventHandlerExitActionN Runtime.NotifyExitedState(this); CachedDelegate exitAction = null; - if (StateStack.Peek().ExitAction != null) + if (CurrentState.ExitAction != null) { - exitAction = StateMachineActionMap[StateStack.Peek().ExitAction]; + exitAction = StateMachineActionMap[CurrentState.ExitAction]; } // Invokes the exit action of the current state, @@ -463,11 +448,9 @@ private async Task GotoStateAsync(Type s, string onExitActionName, Event e) await ExecuteCurrentStateOnExitAsync(onExitActionName, e); if (CurrentStatus is Status.Active) { - DoStatePop(); - // The state machine transitions to the new state. var nextState = StateInstanceCache[GetType()].First(val => val.GetType().Equals(s)); - DoStatePush(nextState); + DoStateTransition(nextState); // The state machine performs the on entry action of the new state. await ExecuteCurrentStateOnEntryAsync(e); @@ -481,126 +464,23 @@ private async Task PushStateAsync(Type s, Event e) { var nextState = StateInstanceCache[GetType()].First(val => val.GetType().Equals(s)); - DoStatePush(nextState); + DoStateTransition(nextState); // The state machine performs the on entry statements of the new state. await ExecuteCurrentStateOnEntryAsync(e); } - private void PushHandler(State state, Type eventType, EventHandlerDeclaration handler) - { - if (handler.Inheritable) - { - if (!InheritableEventHandlerMap.TryGetValue(eventType, out var stack)) - { - stack = new Stack(); - InheritableEventHandlerMap[eventType] = stack; - } - - stack.Push(new HandlerInfo(state, StateStack.Count, handler)); - } - } - - private bool TryGetInheritedHandler(Type eventType, out HandlerInfo result) - { - if (InheritableEventHandlerMap.TryGetValue(eventType, out var stack) && stack.Count > 0) - { - result = stack.Peek(); - return true; - } - - result = default; - return false; - } - /// /// Configures the state transitions of the state machine when a state is pushed into the stack. /// - private void DoStatePush(State state) + private void DoStateTransition(State state) { EventHandlerMap = state.EventHandlers; // non-inheritable handlers. - - StateStack.Push(state); - CurrentState = state.GetType(); - CurrentStateName = NameResolver.GetQualifiedStateName(CurrentState); - - // Push the inheritable event handlers. - foreach (var eventHandler in state.InheritableEventHandlers) - { - PushHandler(state, eventHandler.Key, eventHandler.Value); - } + CurrentState = state; + CurrentStateName = NameResolver.GetQualifiedStateName(CurrentState.GetType()); } - /// - /// Configures the state transitions of the state machine - /// when a state is popped. - /// - private void DoStatePop() - { - var state = StateStack.Pop(); - foreach (var item in InheritableEventHandlerMap) - { - var stack = item.Value; - if (stack != null && stack.Count > 0 && stack.Peek().State == state) - { - stack.Pop(); - } - } - - if (StateStack.Count > 0) - { - // re-instate the non-inheritable handlers from previous state. - state = StateStack.Peek(); - CurrentState = state.GetType(); - CurrentStateName = NameResolver.GetQualifiedStateName(CurrentState); - EventHandlerMap = StateStack.Peek().EventHandlers; - } - else - { - EventHandlerMap = EmptyEventHandlerMap; - CurrentState = null; - CurrentStateName = string.Empty; - } - } - - /// - /// Get the appropriate inherited event handler for the given event. - /// - /// The event we want to handle - /// The HandlerInfo in the state stack - /// True if a handler is found, otherwise false - private bool GetInheritedEventHandler(Event e, ref HandlerInfo info) - { - var eventType = e.GetType(); - // Wild card only takes precidence if it is higher on the state stack. - var hasWildCard = TryGetInheritedHandler(typeof(WildCardEvent), out var wildInfo); - if (EventHandlerMap.ContainsKey(typeof(WildCardEvent))) - { - // a non-inherited wildcard handler cannot beat a "specific" IgnoreEvent instruction if that - // "specific" instruction is also at the top of the stack. - wildInfo.StackDepth = StateStack.Count; - wildInfo.State = StateStack.Peek(); - wildInfo.Handler = EventHandlerMap[typeof(WildCardEvent)]; - hasWildCard = true; - } - - var hasSpecific = TryGetInheritedHandler(eventType, out info); - - if ((hasSpecific && hasWildCard && wildInfo.StackDepth > info.StackDepth) || - (!hasSpecific && hasWildCard)) - { - info = wildInfo; - return true; - } - - if (hasSpecific) - { - return true; - } - - info = new HandlerInfo(null, 0, null); - return false; - } + /// /// Checks if the specified event is ignored in the current state. @@ -613,13 +493,7 @@ internal bool IsEventIgnoredInCurrentState(Event e) // because the non-inheritable operation takes precedent. if (EventHandlerMap.ContainsKey(eventType)) { - return false; - } - - var info = new HandlerInfo(null, 0, null); - if (GetInheritedEventHandler(e, ref info)) - { - return info.Handler is IgnoreEventHandlerDeclaration; + return EventHandlerMap[eventType] is IgnoreEventHandlerDeclaration; } return false; @@ -635,15 +509,8 @@ internal bool IsEventDeferredInCurrentState(Event e) // If a non-inheritable transition is defined, then the event is not deferred. if (EventHandlerMap.ContainsKey(eventType)) { - return false; + return EventHandlerMap[eventType] is DeferEventHandlerDeclaration; } - - var info = new HandlerInfo(null, 0, null); - if (GetInheritedEventHandler(e, ref info)) - { - return info.Handler is DeferEventHandlerDeclaration; - } - return false; } @@ -651,8 +518,7 @@ internal bool IsEventDeferredInCurrentState(Event e) /// Checks if a default handler is installed in current state. /// internal bool IsDefaultHandlerInstalledInCurrentState() => - EventHandlerMap.ContainsKey(typeof(DefaultEvent)) || - TryGetInheritedHandler(typeof(DefaultEvent), out _); + EventHandlerMap.ContainsKey(typeof(DefaultEvent)); /// /// Returns the hashed state of this state machine. @@ -667,20 +533,9 @@ internal override int GetHashedState() hash = (hash * 31) + IsHalted.GetHashCode(); hash = (hash * 31) + Manager.GetCachedState(); - - foreach (var state in StateStack) - { - hash = (hash * 31) + state.GetType().GetHashCode(); - } - + hash = (hash * 31) + Inbox.GetCachedState(); - if (HashedState != 0) - { - // Adds the user-defined hashed state. - hash = (hash * 31) + HashedState; - } - return hash; } } @@ -791,17 +646,6 @@ internal override void SetupEventHandlers() map.Add(state.ExitAction, GetActionWithName(state.ExitAction)); } - foreach (var handler in state.InheritableEventHandlers.Values) - { - if (handler is ActionEventHandlerDeclaration action) - { - if (!map.ContainsKey(action.Name)) - { - map.Add(action.Name, GetActionWithName(action.Name)); - } - } - } - foreach (var handler in state.EventHandlers.Values) { if (handler is GotoStateTransition transition) @@ -812,6 +656,14 @@ internal override void SetupEventHandlers() map.Add(transition.Lambda, GetActionWithName(transition.Lambda)); } } + + if (handler is ActionEventHandlerDeclaration action) + { + if (!map.ContainsKey(action.Name)) + { + map.Add(action.Name, GetActionWithName(action.Name)); + } + } } } @@ -829,19 +681,10 @@ internal override void SetupEventHandlers() Assert(initialStates.Count != 0, "{0} must declare a start state.", Id); Assert(initialStates.Count is 1, "{0} can not declare more than one start states.", Id); - DoStatePush(initialStates[0]); + DoStateTransition(initialStates[0]); AssertStateValidity(); } - /// - /// Returns the type of the state at the specified state - /// stack index, if there is one. - /// - internal Type GetStateTypeAtStackIndex(int index) - { - return StateStack.ElementAtOrDefault(index)?.GetType(); - } - /// /// Processes a type, looking for states. /// @@ -858,18 +701,6 @@ private void ExtractStateTypes(Type type) { StateTypeCache[GetType()].Add(nextType); } - else if (nextType.IsClass && nextType.IsSubclassOf(typeof(StateGroup))) - { - // Adds the contents of the group of states to the stack. - foreach (var t in nextType.GetNestedTypes(BindingFlags.Instance | - BindingFlags.NonPublic | BindingFlags.Public | - BindingFlags.DeclaredOnly)) - { - Assert(t.IsSubclassOf(typeof(StateGroup)) || t.IsSubclassOf(typeof(State)), - "'{0}' is neither a group of states nor a state.", t.Name); - stack.Push(t); - } - } } } @@ -910,7 +741,7 @@ internal HashSet> GetAllStateEventPairs() var pairs = new HashSet>(); foreach (var state in StateInstanceCache[GetType()]) { - foreach (var binding in from b in state.InheritableEventHandlers.Concat(state.EventHandlers) + foreach (var binding in from b in state.EventHandlers where IncludeInCoverage(b.Value) select b) { @@ -927,7 +758,7 @@ where IncludeInCoverage(b.Value) private void AssertStateValidity() { Assert(StateTypeCache[GetType()].Count > 0, "{0} must have one or more states.", Id); - Assert(StateStack.Peek() != null, "{0} must not have a null current state.", Id); + Assert(CurrentState != null, "{0} must not have a null current state.", Id); } /// @@ -1026,36 +857,6 @@ public enum Type } } - /// - /// A struct used to track event handlers that are pushed or popped on the StateStack. - /// - private struct HandlerInfo - { - /// - /// The state that provided this EventHandler. - /// - public State State; - - /// - /// Records where this State is in the StateStack. This information is needed to implement WildCardEvent - /// semantics. A specific Handler closest to the top of the stack (higher StackDepth) wins over a - /// WildCardEvent further down the stack (lower StackDepth). - /// - public int StackDepth; - - /// - /// The event handler for a given event Type defined by the State. - /// - public EventHandlerDeclaration Handler; - - public HandlerInfo(State state, int depth, EventHandlerDeclaration handler) - { - State = state; - StackDepth = depth; - Handler = handler; - } - } - /// /// Abstract class representing a state. /// @@ -1074,11 +875,6 @@ public abstract class State /// internal string ExitAction { get; private set; } - /// - /// Map containing all event handler declarations. - /// - internal Dictionary InheritableEventHandlers; - /// /// Map containing all non-inheritable event handler declarations. /// @@ -1102,8 +898,6 @@ protected State() internal void InitializeState() { IsStart = false; - - InheritableEventHandlers = new Dictionary(); EventHandlers = new Dictionary(); if (GetType().GetCustomAttribute(typeof(OnEntryAttribute), true) is OnEntryAttribute entryAttribute) @@ -1126,7 +920,6 @@ internal void InitializeState() // Install event handlers. InstallGotoTransitions(handledEvents); - InstallPushTransitions(handledEvents); InstallActionBindings(handledEvents); InstallIgnoreHandlers(handledEvents); InstallDeferHandlers(handledEvents); @@ -1155,105 +948,6 @@ private void InstallGotoTransitions(HashSet handledEvents) handledEvents.Add(attr.Event); } - - InheritGotoTransitions(GetType().BaseType, handledEvents); - } - - /// - /// Inherits goto event handlers from a base state, if there is one. - /// - private void InheritGotoTransitions(Type baseState, HashSet handledEvents) - { - if (!baseState.IsSubclassOf(typeof(State))) - { - return; - } - - var gotoAttributesInherited = baseState.GetCustomAttributes(typeof(OnEventGotoStateAttribute), false) - as OnEventGotoStateAttribute[]; - - var gotoTransitionsInherited = new Dictionary(); - foreach (var attr in gotoAttributesInherited) - { - if (EventHandlers.ContainsKey(attr.Event)) - { - continue; - } - - CheckEventHandlerAlreadyInherited(attr.Event, baseState, handledEvents); - - if (attr.Action is null) - { - gotoTransitionsInherited.Add(attr.Event, new GotoStateTransition(attr.State)); - } - else - { - gotoTransitionsInherited.Add(attr.Event, new GotoStateTransition(attr.State, attr.Action)); - } - - handledEvents.Add(attr.Event); - } - - foreach (var kvp in gotoTransitionsInherited) - { - EventHandlers.Add(kvp.Key, kvp.Value); - } - - InheritGotoTransitions(baseState.BaseType, handledEvents); - } - - /// - /// Declares push event handlers, if there are any. - /// - private void InstallPushTransitions(HashSet handledEvents) - { - var pushAttributes = GetType().GetCustomAttributes(typeof(OnEventPushStateAttribute), false) - as OnEventPushStateAttribute[]; - - foreach (var attr in pushAttributes) - { - CheckEventHandlerAlreadyDeclared(attr.Event, handledEvents); - - EventHandlers.Add(attr.Event, new PushStateTransition(attr.State)); - handledEvents.Add(attr.Event); - } - - InheritPushTransitions(GetType().BaseType, handledEvents); - } - - /// - /// Inherits push event handlers from a base state, if there is one. - /// - private void InheritPushTransitions(Type baseState, HashSet handledEvents) - { - if (!baseState.IsSubclassOf(typeof(State))) - { - return; - } - - var pushAttributesInherited = baseState.GetCustomAttributes(typeof(OnEventPushStateAttribute), false) - as OnEventPushStateAttribute[]; - - var pushTransitionsInherited = new Dictionary(); - foreach (var attr in pushAttributesInherited) - { - if (EventHandlers.ContainsKey(attr.Event)) - { - continue; - } - - CheckEventHandlerAlreadyInherited(attr.Event, baseState, handledEvents); - - pushTransitionsInherited.Add(attr.Event, new PushStateTransition(attr.State)); - handledEvents.Add(attr.Event); - } - - foreach (var kvp in pushTransitionsInherited) - { - EventHandlers.Add(kvp.Key, kvp.Value); - } - - InheritPushTransitions(baseState.BaseType, handledEvents); } /// @@ -1268,48 +962,11 @@ private void InstallActionBindings(HashSet handledEvents) { CheckEventHandlerAlreadyDeclared(attr.Event, handledEvents); - InheritableEventHandlers.Add(attr.Event, new ActionEventHandlerDeclaration(attr.Action)); - handledEvents.Add(attr.Event); - } - - InheritActionBindings(GetType().BaseType, handledEvents); - } - - /// - /// Inherits action bindings from a base state, if there is one. - /// - private void InheritActionBindings(Type baseState, HashSet handledEvents) - { - if (!baseState.IsSubclassOf(typeof(State))) - { - return; - } - - var doAttributesInherited = baseState.GetCustomAttributes(typeof(OnEventDoActionAttribute), false) - as OnEventDoActionAttribute[]; - - var actionBindingsInherited = new Dictionary(); - foreach (var attr in doAttributesInherited) - { - if (InheritableEventHandlers.ContainsKey(attr.Event)) - { - continue; - } - - CheckEventHandlerAlreadyInherited(attr.Event, baseState, handledEvents); - - actionBindingsInherited.Add(attr.Event, new ActionEventHandlerDeclaration(attr.Action)); + EventHandlers.Add(attr.Event, new ActionEventHandlerDeclaration(attr.Action)); handledEvents.Add(attr.Event); } - - foreach (var kvp in actionBindingsInherited) - { - InheritableEventHandlers.Add(kvp.Key, kvp.Value); - } - - InheritActionBindings(baseState.BaseType, handledEvents); } - + /// /// Declares ignore event handlers, if there are any. /// @@ -1322,44 +979,13 @@ private void InstallIgnoreHandlers(HashSet handledEvents) { CheckEventHandlerAlreadyDeclared(e, handledEvents); - InheritableEventHandlers.Add(e, new IgnoreEventHandlerDeclaration()); + EventHandlers.Add(e, new IgnoreEventHandlerDeclaration()); ignoredEvents.Add(e); handledEvents.Add(e); } } - - InheritIgnoreHandlers(GetType().BaseType, handledEvents, ignoredEvents); - } - - /// - /// Inherits ignore event handlers from a base state, if there is one. - /// - private void InheritIgnoreHandlers(Type baseState, HashSet handledEvents, HashSet ignoredEvents) - { - if (!baseState.IsSubclassOf(typeof(State))) - { - return; - } - - if (baseState.GetCustomAttribute(typeof(IgnoreEventsAttribute), false) is IgnoreEventsAttribute ignoreEventsAttribute) - { - foreach (var e in ignoreEventsAttribute.Events) - { - if (ignoredEvents.Contains(e)) - { - continue; - } - - CheckEventHandlerAlreadyInherited(e, baseState, handledEvents); - - InheritableEventHandlers.Add(e, new IgnoreEventHandlerDeclaration()); - ignoredEvents.Add(e); - handledEvents.Add(e); - } - } - - InheritIgnoreHandlers(baseState.BaseType, handledEvents, ignoredEvents); } + /// /// Declares defer event handlers, if there are any. @@ -1372,7 +998,7 @@ private void InstallDeferHandlers(HashSet handledEvents) foreach (var e in deferEventsAttribute.Events) { CheckEventHandlerAlreadyDeclared(e, handledEvents); - InheritableEventHandlers.Add(e, new DeferEventHandlerDeclaration()); + EventHandlers.Add(e, new DeferEventHandlerDeclaration()); deferredEvents.Add(e); handledEvents.Add(e); } @@ -1399,9 +1025,8 @@ private void InheritDeferHandlers(Type baseState, HashSet handledEvents, H { continue; } - - CheckEventHandlerAlreadyInherited(e, baseState, handledEvents); - InheritableEventHandlers.Add(e, new DeferEventHandlerDeclaration()); + CheckEventHandlerAlreadyDeclared(e, handledEvents); + EventHandlers.Add(e, new DeferEventHandlerDeclaration()); deferredEvents.Add(e); handledEvents.Add(e); } @@ -1421,17 +1046,6 @@ private static void CheckEventHandlerAlreadyDeclared(Type e, HashSet handl } } - /// - /// Checks if an event handler has been already inherited. - /// - private static void CheckEventHandlerAlreadyInherited(Type e, Type baseState, HashSet handledEvents) - { - if (handledEvents.Contains(e)) - { - throw new InvalidOperationException($"inherited multiple handlers for event '{e}' from state '{baseState}'"); - } - } - /// /// Attribute for declaring the state that a state machine transitions upon creation. /// @@ -1529,35 +1143,6 @@ public OnEventGotoStateAttribute(Type eventType, Type stateType, string actionNa } } - /// - /// Attribute for declaring a push state transition when the state machine - /// is in the specified state and dequeues an event of the specified type. - /// - [AttributeUsage(AttributeTargets.Class, AllowMultiple = true)] - protected sealed class OnEventPushStateAttribute : Attribute - { - /// - /// The type of the dequeued event. - /// - internal Type Event; - - /// - /// The type of the state. - /// - internal Type State; - - /// - /// Initializes a new instance of the class. - /// - /// The type of the dequeued event. - /// The type of the state. - public OnEventPushStateAttribute(Type eventType, Type stateType) - { - Event = eventType; - State = stateType; - } - } - /// /// Attribute for declaring which action should be invoked when the state machine /// is in the specified state to handle a dequeued event of the specified type. @@ -1629,12 +1214,5 @@ public IgnoreEventsAttribute(params Type[] eventTypes) } } } - - /// - /// Abstract class used for representing a group of related states. - /// - public abstract class StateGroup - { - } } } \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs index 126e2ccec..ba5b6a81c 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs @@ -500,7 +500,7 @@ private EnqueueStatus EnqueueEvent(Actor actor, Event e, Actor sender, Guid opGr if (sender is StateMachine senderStateMachine) { originInfo = new EventOriginInfo(sender.Id, senderStateMachine.GetType().FullName, - NameResolver.GetStateNameForLogging(senderStateMachine.CurrentState)); + NameResolver.GetStateNameForLogging(senderStateMachine.CurrentState.GetType())); stateName = senderStateMachine.CurrentStateName; } else if (sender is Actor senderActor) diff --git a/Src/PChecker/CheckerCore/Testing/TestingProcess.cs b/Src/PChecker/CheckerCore/Testing/TestingProcess.cs index 61d884f69..68a06f48e 100644 --- a/Src/PChecker/CheckerCore/Testing/TestingProcess.cs +++ b/Src/PChecker/CheckerCore/Testing/TestingProcess.cs @@ -161,7 +161,7 @@ private void EmitTestReport() } Console.WriteLine(testReport.GetText(_checkerConfiguration, "...")); - Console.WriteLine($"... Elapsed {Profiler.Results()} sec."); + Console.WriteLine($"... Elapsed {Profiler.GetElapsedTime()} sec."); if (testReport.InternalErrors.Count > 0) {