diff --git a/Src/PChecker/CheckerCore/PRuntime/Runtime/ControlledRuntime.cs b/Src/PChecker/CheckerCore/PRuntime/Runtime/ControlledRuntime.cs index 17fb6fbb5..a3525cca6 100644 --- a/Src/PChecker/CheckerCore/PRuntime/Runtime/ControlledRuntime.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Runtime/ControlledRuntime.cs @@ -51,6 +51,19 @@ public sealed class ControlledRuntime : IDisposable /// private static readonly AsyncLocal AsyncLocalInstance = new AsyncLocal(); + internal static ControlledRuntime InstalledRuntime { get; private set; } = CreateWithConfiguration(default); + + private static ControlledRuntime CreateWithConfiguration(CheckerConfiguration checkerConfiguration) + { + if (checkerConfiguration is null) + { + checkerConfiguration = CheckerConfiguration.Create(); + } + + var valueGenerator = new RandomValueGenerator(checkerConfiguration); + return new ControlledRuntime(checkerConfiguration, valueGenerator); + } + /// /// The currently executing runtime. /// @@ -61,7 +74,7 @@ public sealed class ControlledRuntime : IDisposable "state machine handlers or controlled tasks. If you are using external libraries that are executing concurrently, " + "you will need to mock them during testing.", Task.CurrentId.HasValue ? Task.CurrentId.Value.ToString() : "")) : - RuntimeFactory.InstalledRuntime); + InstalledRuntime); /// /// If true, the program execution is controlled by the runtime to @@ -514,13 +527,6 @@ private StateMachine CreateStateMachine(StateMachineId id, Type type, string nam { id = new StateMachineId(type, name, this); } - else - { - Assert(id.Runtime is null || id.Runtime == this, "Unbound state machine id '{0}' was created by another runtime.", id.Value); - Assert(id.Type == type.FullName, "Cannot bind state machine id '{0}' of type '{1}' to an state machine of type '{2}'.", - id.Value, id.Type, type.FullName); - id.Bind(this); - } var stateMachine = Create(type); IStateMachineManager stateMachineManager = new StateMachineManager(this, stateMachine); @@ -664,7 +670,7 @@ private EnqueueStatus EnqueueEvent(StateMachine stateMachine, Event e, StateMach { // Directly use sender as a StateMachine var originInfo = new EventOriginInfo(sender.Id, sender.GetType().FullName, - NameResolver.GetStateNameForLogging(sender.CurrentState.GetType())); + sender.CurrentState.GetType().Name); var eventInfo = new EventInfo(e, originInfo); diff --git a/Src/PChecker/CheckerCore/PRuntime/Runtime/RuntimeFactory.cs b/Src/PChecker/CheckerCore/PRuntime/Runtime/RuntimeFactory.cs deleted file mode 100644 index 107ad79e7..000000000 --- a/Src/PChecker/CheckerCore/PRuntime/Runtime/RuntimeFactory.cs +++ /dev/null @@ -1,74 +0,0 @@ -// Copyright (c) Microsoft Corporation. -// Licensed under the MIT License. - -using PChecker.StateMachines; -using PChecker.Random; -using PChecker.SystematicTesting; -using PChecker.SystematicTesting.Strategies.Probabilistic; - -namespace PChecker.Runtime -{ - /// - /// Provides methods for creating a runtime. - /// - public static class RuntimeFactory - { - /// - /// The installed runtime instance. - /// - internal static ControlledRuntime InstalledRuntime { get; private set; } = CreateWithConfiguration(default); - - /// - /// Protects access to the installed runtime. - /// - private static readonly object SyncObject = new object(); - - /// - /// Creates a new ControlledRuntime. - /// - /// The created task runtime. - /// - /// Only one task runtime can be created per process. If you create a new task - /// runtime it replaces the previously installed one. - /// - public static ControlledRuntime Create() => CreateAndInstall(default); - - /// - /// Creates a new ControlledRuntime with the specified . - /// - /// The runtime checkerConfiguration to use. - /// The created task runtime. - /// - /// Only one task runtime can be created per process. If you create a new task - /// runtime it replaces the previously installed one. - /// - public static ControlledRuntime Create(CheckerConfiguration checkerConfiguration) => CreateAndInstall(checkerConfiguration); - - /// - /// Creates a new ControlledRuntime with the specified and sets - /// it as the installed runtime, or returns the installed runtime if it already exists. - /// - private static ControlledRuntime CreateAndInstall(CheckerConfiguration checkerConfiguration) - { - lock (SyncObject) - { - // Assign the newly created runtime as the installed runtime. - return InstalledRuntime = CreateWithConfiguration(checkerConfiguration); - } - } - - /// - /// Creates a new ControlledRuntime with the specified . - /// - private static ControlledRuntime CreateWithConfiguration(CheckerConfiguration checkerConfiguration) - { - if (checkerConfiguration is null) - { - checkerConfiguration = CheckerConfiguration.Create(); - } - - var valueGenerator = new RandomValueGenerator(checkerConfiguration); - return new ControlledRuntime(checkerConfiguration, valueGenerator); - } - } -} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/PRuntime/Specifications/Monitor.cs b/Src/PChecker/CheckerCore/PRuntime/Specifications/Monitor.cs index b4d433743..71e93c300 100644 --- a/Src/PChecker/CheckerCore/PRuntime/Specifications/Monitor.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Specifications/Monitor.cs @@ -135,7 +135,7 @@ protected internal Type CurrentState /// internal string CurrentStateName { - get => NameResolver.GetQualifiedStateName(CurrentState); + get => CurrentState.Name; } /// @@ -985,7 +985,7 @@ internal HashSet GetAllStates() var allStates = new HashSet(); foreach (var state in StateMap[GetType()]) { - allStates.Add(NameResolver.GetQualifiedStateName(state.GetType())); + allStates.Add(state.GetType().Name); } return allStates; @@ -1003,7 +1003,7 @@ internal HashSet> GetAllStateEventPairs() { foreach (var binding in state.EventHandlers) { - pairs.Add(Tuple.Create(NameResolver.GetQualifiedStateName(state.GetType()), binding.Key.FullName)); + pairs.Add(Tuple.Create(state.GetType().Name, binding.Key.FullName)); } } diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/EventQueues/EventQueue.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/EventQueues/EventQueue.cs index c60673d41..314b83057 100644 --- a/Src/PChecker/CheckerCore/PRuntime/StateMachines/EventQueues/EventQueue.cs +++ b/Src/PChecker/CheckerCore/PRuntime/StateMachines/EventQueues/EventQueue.cs @@ -156,7 +156,7 @@ public EnqueueStatus Enqueue(Event e, EventInfo info) // TODO: check op-id of default event. // A default event handler exists. - var stateName = NameResolver.GetStateNameForLogging(StateMachine.CurrentState.GetType()); + var stateName = StateMachine.CurrentState.GetType().Name; var eventOrigin = new EventOriginInfo(StateMachine.Id, StateMachine.GetType().FullName, stateName); return (DequeueStatus.Default, DefaultEvent.Instance, new EventInfo(DefaultEvent.Instance, eventOrigin)); } @@ -208,7 +208,7 @@ public EnqueueStatus Enqueue(Event e, EventInfo info) /// public void RaiseEvent(Event e) { - var stateName = NameResolver.GetStateNameForLogging(StateMachine.CurrentState.GetType()); + var stateName = StateMachine.CurrentState.GetType().Name; var eventOrigin = new EventOriginInfo(StateMachine.Id, StateMachine.GetType().FullName, stateName); var info = new EventInfo(e, eventOrigin); RaisedEvent = (e, info); diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/NameResolver.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/NameResolver.cs deleted file mode 100644 index 3a32fe554..000000000 --- a/Src/PChecker/CheckerCore/PRuntime/StateMachines/NameResolver.cs +++ /dev/null @@ -1,54 +0,0 @@ -// Copyright (c) Microsoft Corporation. -// Licensed under the MIT License. - -using System; -using System.Collections.Concurrent; -using System.Globalization; - -namespace PChecker.StateMachines -{ - /// - /// Utility class for resolving names. - /// - internal static class NameResolver - { - /// - /// Cache of state names. - /// - private static readonly ConcurrentDictionary StateNamesCache = - new ConcurrentDictionary(); - - /// - /// Returns the qualified (i.e. ) name of the specified - /// state machine or monitor state, or the empty string if there is no such name. - /// - internal static string GetQualifiedStateName(Type state) - { - if (state is null) - { - return string.Empty; - } - - if (!StateNamesCache.TryGetValue(state, out var name)) - { - name = state.Name; - - var nextState = state; - while (nextState.DeclaringType != null) - { - name = string.Format(CultureInfo.InvariantCulture, "{0}.{1}", nextState.DeclaringType.Name, name); - nextState = nextState.DeclaringType; - } - - StateNamesCache.GetOrAdd(state, name); - } - - return name; - } - - /// - /// Returns the state name to be used for logging purposes. - /// - internal static string GetStateNameForLogging(Type state) => state is null ? "None" : GetQualifiedStateName(state); - } -} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachine.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachine.cs index 20987657f..be563d3c1 100644 --- a/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachine.cs +++ b/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachine.cs @@ -1038,7 +1038,7 @@ private protected async Task HandleEventAsync(Event e) break; } - var currentStateName = NameResolver.GetQualifiedStateName(currentState.GetType()); + var currentStateName = currentState.GetType().Name; await InvokeUserCallbackAsync(UserCallbackType.OnEventUnhandled, e, currentStateName); if (CurrentStatus is Status.Active) { @@ -1112,7 +1112,7 @@ private bool TryGetHandler(Type e, out EventHandlerDeclaration o) private async Task HandleEventAsync(Event e, State declaringState, EventHandlerDeclaration eventHandler) { - var handlingStateName = NameResolver.GetQualifiedStateName(declaringState.GetType()); + var handlingStateName = declaringState.GetType().Name; if (eventHandler is ActionEventHandlerDeclaration actionEventHandler) { var cachedAction = StateMachineActionMap[actionEventHandler.Name]; @@ -1265,7 +1265,7 @@ private void CheckDanglingTransition() private async Task GotoStateAsync(Type s, string onExitActionName, Event e) { Runtime.LogWriter.LogGotoState(Id, CurrentStateName, - $"{s.DeclaringType}.{NameResolver.GetStateNameForLogging(s)}"); + $"{s.DeclaringType}.{s.Name}"); // The state machine performs the on exit action of the current state. await ExecuteCurrentStateOnExitAsync(onExitActionName, e); @@ -1300,7 +1300,7 @@ private void DoStateTransition(State state) { EventHandlerMap = state.EventHandlers; // non-inheritable handlers. CurrentState = state; - CurrentStateName = NameResolver.GetQualifiedStateName(CurrentState.GetType()); + CurrentStateName = CurrentState.GetType().Name; } @@ -1542,7 +1542,7 @@ internal HashSet GetAllStates() var allStates = new HashSet(); foreach (var state in StateInstanceCache[GetType()]) { - allStates.Add(NameResolver.GetQualifiedStateName(state.GetType())); + allStates.Add(state.GetType().Name); } return allStates; @@ -1573,7 +1573,7 @@ internal HashSet> GetAllStateEventPairs() where IncludeInCoverage(b.Value) select b) { - pairs.Add(Tuple.Create(NameResolver.GetQualifiedStateName(state.GetType()), binding.Key.FullName)); + pairs.Add(Tuple.Create(state.GetType().Name, binding.Key.FullName)); } } diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachineFactory.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachineFactory.cs deleted file mode 100644 index f3c2b84e9..000000000 --- a/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachineFactory.cs +++ /dev/null @@ -1,48 +0,0 @@ -// Copyright (c) Microsoft Corporation. -// Licensed under the MIT License. - -using System; -using System.Collections.Generic; -using System.Linq.Expressions; - -namespace PChecker.StateMachines -{ - /// - /// Factory for creating state machine instances. - /// - internal static class StateMachineFactory - { - /// - /// Cache storing state machine constructors. - /// - private static readonly Dictionary> StateMachineConstructorCache = - new Dictionary>(); - - /// - /// Creates a new instance of the specified type. - /// - /// The type of the state machines. - /// The created state machine instance. - public static StateMachine Create(Type type) - { - Func constructor = null; - lock (StateMachineConstructorCache) - { - if (!StateMachineConstructorCache.TryGetValue(type, out constructor)) - { - var constructorInfo = type.GetConstructor(Type.EmptyTypes); - if (constructorInfo == null) - { - throw new Exception("Could not find empty constructor for type " + type.FullName); - } - - constructor = Expression.Lambda>( - Expression.New(constructorInfo)).Compile(); - StateMachineConstructorCache.Add(type, constructor); - } - } - - return constructor(); - } - } -} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachineId.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachineId.cs index 2ef8053d0..719c3c986 100644 --- a/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachineId.cs +++ b/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachineId.cs @@ -15,11 +15,6 @@ namespace PChecker.StateMachines [DataContract] public sealed class StateMachineId : IEquatable, IComparable { - /// - /// The runtime that executes the state machine with this id. - /// - internal ControlledRuntime Runtime { get; private set; } - /// /// Unique id, when is empty. /// @@ -44,18 +39,6 @@ public sealed class StateMachineId : IEquatable, IComparable - /// Generation of the runtime that created this state machine id. - /// - [DataMember] - public readonly ulong Generation; - - /// - /// Endpoint. - /// - [DataMember] - public readonly string Endpoint; - /// /// True if is used as the unique id, else false. /// @@ -66,22 +49,16 @@ public sealed class StateMachineId : IEquatable, IComparable internal StateMachineId(Type type, string name, ControlledRuntime runtime, bool useNameForHashing = false) { - Runtime = runtime; - Endpoint = string.Empty; if (useNameForHashing) { Value = 0; NameValue = name; - Runtime.Assert(!string.IsNullOrEmpty(NameValue), "The state machine name cannot be null when used as id."); } else { Value = runtime.GetNextOperationId(); NameValue = string.Empty; - - // Checks for overflow. - Runtime.Assert(Value != ulong.MaxValue, "Detected state machine id overflow."); } Type = type.FullName; @@ -96,14 +73,6 @@ internal StateMachineId(Type type, string name, ControlledRuntime runtime, bool } } - /// - /// Bind the state machine id. - /// - internal void Bind(ControlledRuntime runtime) - { - Runtime = runtime; - } - /// /// Determines whether the specified object is equal to the current object. /// @@ -118,8 +87,8 @@ public override bool Equals(object obj) } return IsNameUsedForHashing ? - NameValue.Equals(id.NameValue) && Generation == id.Generation : - Value == id.Value && Generation == id.Generation; + NameValue.Equals(id.NameValue) : + Value == id.Value; } return false; @@ -132,7 +101,6 @@ public override int GetHashCode() { var hash = 17; hash = (hash * 23) + (IsNameUsedForHashing ? NameValue.GetHashCode() : Value.GetHashCode()); - hash = (hash * 23) + Generation.GetHashCode(); return hash; }