[Cleanup] Remove state machine factory, runtime factory, and name resolver

Src/PChecker/CheckerCore/PRuntime/Runtime/ControlledRuntime.cs

@@ -51,6 +51,19 @@
         /// </remarks>
         private static readonly AsyncLocal<ControlledRuntime> AsyncLocalInstance = new AsyncLocal<ControlledRuntime>();
 
+        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);
+        }
+
         /// <summary>
         /// The currently executing runtime.
         /// </summary>
@@ -61,28 +74,28 @@
                                                                         "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() : "<unknown>")) :
-                                                                    RuntimeFactory.InstalledRuntime);
+                                                                    InstalledRuntime);
 
         /// <summary>
         /// If true, the program execution is controlled by the runtime to
         /// explore interleavings and sources of nondeterminism, else false.
         /// </summary>
         internal static bool IsExecutionControlled { get; private protected set; } = false;
 
         /// <summary>
         /// The checkerConfiguration used by the runtime.
         /// </summary>
         protected internal readonly CheckerConfiguration CheckerConfiguration;
 
         /// <summary>
         /// List of monitors in the program.
         /// </summary>
         protected readonly List<Monitor> Monitors;
 
         /// <summary>
         /// Responsible for generating random values.
         /// </summary>
         protected readonly IRandomValueGenerator ValueGenerator;
 
         /// <summary>
         /// Monotonically increasing operation id counter.
@@ -92,7 +105,7 @@
         /// <summary>
         /// Records if the runtime is running.
         /// </summary>
         protected internal volatile bool IsRunning;
 
         /// <summary>
         /// Callback that is fired when the program throws an exception which includes failed assertions.
@@ -514,13 +527,6 @@
             {
                 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 @@
         {
             // 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);
 
@@ -1440,7 +1446,7 @@
         /// <summary>
         /// Raises the <see cref="OnFailure"/> event with the specified <see cref="Exception"/>.
         /// </summary>
         protected internal void RaiseOnFailureEvent(Exception exception)
         {
             if (exception is ExecutionCanceledException ||
                 (exception is ActionExceptionFilterException ae && ae.InnerException is ExecutionCanceledException))

Src/PChecker/CheckerCore/PRuntime/Specifications/Monitor.cs

@@ -135,7 +135,7 @@ protected internal Type CurrentState
         /// </summary>
         internal string CurrentStateName
         {
-            get => NameResolver.GetQualifiedStateName(CurrentState);
+            get => CurrentState.Name;
         }
 
         /// <summary>
@@ -985,7 +985,7 @@ internal HashSet<string> GetAllStates()
             var allStates = new HashSet<string>();
             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<Tuple<string, string>> 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));
                 }
             }
 

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)
         /// <inheritdoc/>
         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);

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<string> GetAllStates()
             var allStates = new HashSet<string>();
             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<Tuple<string, string>> 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));
                 }
             }