[Cleanup] Remove IStateMachineRuntime

p-org · Sep 9, 2024 · 9aed4f3 · 9aed4f3
1 parent fd0304a
commit 9aed4f3
Show file tree

Hide file tree

Showing 13 changed files with 23 additions and 22 deletions.
diff --git a/Src/PChecker/CheckerCore/PRuntime/PModule.cs b/Src/PChecker/CheckerCore/PRuntime/PModule.cs
@@ -1,6 +1,6 @@
 using System;
 using System.Collections.Generic;
-using PChecker.StateMachines;
+using PChecker.SystematicTesting;
 
 namespace PChecker.PRuntime
 {
@@ -13,6 +13,6 @@ public class PModule
         public static IDictionary<string, Dictionary<string, string>> linkMap =
             new Dictionary<string, Dictionary<string, string>>();
 
-        public static IStateMachineRuntime runtime;
+        public static ControlledRuntime runtime;
     }
 }
diff --git a/Src/PChecker/CheckerCore/PRuntime/Runtime/CoyoteRuntime.cs b/Src/PChecker/CheckerCore/PRuntime/Runtime/CoyoteRuntime.cs
@@ -17,7 +17,7 @@ namespace PChecker.Runtime
     /// <summary>
     /// Runtime for executing asynchronous operations.
     /// </summary>
-    internal abstract class CoyoteRuntime : ICoyoteRuntime
+    public abstract class CoyoteRuntime : ICoyoteRuntime
     {
         /// <summary>
         /// Provides access to the runtime associated with each asynchronous control flow.

diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Exceptions/OnEventDroppedHandler.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Exceptions/OnEventDroppedHandler.cs
@@ -6,7 +6,7 @@
 namespace PChecker.StateMachines.Exceptions
 {
     /// <summary>
-    /// Handles the <see cref="IStateMachineRuntime.OnEventDropped"/> event.
+    /// Handles the <see cref="ControlledRuntime.OnEventDropped"/> event.
     /// </summary>
     public delegate void OnEventDroppedHandler(Event e, StateMachineId target);
 }
diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/IStateMachineRuntimeLog.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/IStateMachineRuntimeLog.cs
@@ -8,7 +8,7 @@ namespace PChecker.StateMachines.Logging
 {
     /// <summary>
     /// Interface that allows an external module to track what
-    /// is happening in the <see cref="IStateMachineRuntime"/>.
+    /// is happening in the <see cref="ControlledRuntime"/>.
     /// </summary>
     public interface IStateMachineRuntimeLog
     {

diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/JsonWriter.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/JsonWriter.cs
@@ -349,7 +349,7 @@ public LogEntry()
     /// Enum representing the possible attributes in the details dictionary,
     /// which represents the data associated with a specific log type. All of
     /// the following are available or expanded parameters associated with an
-    /// IStateMachineRuntime method. Naming for them is mostly the same except some
+    /// ControlledRuntime method. Naming for them is mostly the same except some
     /// are changed for simplicity.
     /// I.e., for OnRaiseEvent(StateMachineId id, string, stateName, Event e), it
     /// will have attributes id, state (simplified from stateName, event

diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/LogWriter.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/LogWriter.cs
@@ -15,7 +15,7 @@ namespace PChecker.StateMachines.Logging
     /// Manages the installed <see cref="TextWriter"/> and all registered
     /// <see cref="IStateMachineRuntimeLog"/> objects.
     /// </summary>
-    internal sealed class LogWriter
+    public sealed class LogWriter
     {
         /// <summary>
         /// The set of registered log writers.

diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachineId.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachineId.cs
@@ -18,7 +18,7 @@ public sealed class StateMachineId : IEquatable<StateMachineId>, IComparable<Sta
         /// <summary>
         /// The runtime that executes the state machine with this id.
         /// </summary>
-        public IStateMachineRuntime Runtime { get; private set; }
+        internal ControlledRuntime Runtime { get; private set; }
 
         /// <summary>
         /// Unique id, when <see cref="NameValue"/> is empty.

diff --git a/Src/PChecker/CheckerCore/Random/IRandomValueGenerator.cs b/Src/PChecker/CheckerCore/Random/IRandomValueGenerator.cs
@@ -6,7 +6,7 @@ namespace PChecker.Random
     /// <summary>
     /// Interface for random value generators.
     /// </summary>
-    internal interface IRandomValueGenerator
+    public interface IRandomValueGenerator
     {
         /// <summary>
         /// The seed currently used by the generator.

diff --git a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs
@@ -39,7 +39,7 @@ namespace PChecker.SystematicTesting
     /// <summary>
     /// Runtime for controlling asynchronous operations.
     /// </summary>
-    internal sealed class ControlledRuntime : CoyoteRuntime, IStateMachineRuntime
+    public sealed class ControlledRuntime : CoyoteRuntime
     {
 
         /// <summary>
@@ -349,15 +349,15 @@ internal void RunTest(Delegate testMethod, string testName)
 
                     OperationScheduler.StartOperation(op);
 
-                    if (testMethod is Action<IStateMachineRuntime> actionWithRuntime)
+                    if (testMethod is Action<ControlledRuntime> actionWithRuntime)
                     {
                         actionWithRuntime(this);
                     }
                     else if (testMethod is Action action)
                     {
                         action();
                     }
-                    else if (testMethod is Func<IStateMachineRuntime, Tasks.Task> functionWithRuntime)
+                    else if (testMethod is Func<ControlledRuntime, Tasks.Task> functionWithRuntime)
                     {
                         await functionWithRuntime(this);
                     }

diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestMethodInfo.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestMethodInfo.cs
@@ -164,7 +164,7 @@ private static (Delegate testMethod, string testName) GetTestMethod(Assembly ass
                                      testMethod.GetCustomAttribute(typeof(AsyncStateMachineAttribute)) != null;
 
             var hasNoInputParameters = testParams.Length is 0;
-            var hasStateMachineInputParameters = testParams.Length is 1 && testParams[0].ParameterType == typeof(IStateMachineRuntime);
+            var hasStateMachineInputParameters = testParams.Length is 1 && testParams[0].ParameterType == typeof(ControlledRuntime);
             var hasTaskInputParameters = testParams.Length is 1 && testParams[0].ParameterType == typeof(ICoyoteRuntime);
 
             if (!((hasVoidReturnType || hasAsyncReturnType) && (hasNoInputParameters || hasStateMachineInputParameters || hasTaskInputParameters) &&
@@ -178,21 +178,21 @@ private static (Delegate testMethod, string testName) GetTestMethod(Assembly ass
                                     $"  [{typeof(TestAttribute).FullName}]\n" +
                                     $"  public static void {testMethod.Name}(ICoyoteRuntime runtime) {{ ... }}\n\n" +
                                     $"  [{typeof(TestAttribute).FullName}]\n" +
-                                    $"  public static void {testMethod.Name}(IStateMachineRuntime runtime) {{ ... }}\n\n" +
+                                    $"  public static void {testMethod.Name}(ControlledRuntime runtime) {{ ... }}\n\n" +
                                     $"  [{typeof(TestAttribute).FullName}]\n" +
                                     $"  public static async {typeof(Task).FullName} {testMethod.Name}() {{ ... await ... }}\n\n" +
                                     $"  [{typeof(TestAttribute).FullName}]\n" +
                                     $"  public static async {typeof(Task).FullName} {testMethod.Name}(ICoyoteRuntime runtime) {{ ... await ... }}\n\n" +
                                     $"  [{typeof(TestAttribute).FullName}]\n" +
-                                    $"  public static async {typeof(Task).FullName} {testMethod.Name}(IStateMachineRuntime runtime) {{ ... await ... }}");
+                                    $"  public static async {typeof(Task).FullName} {testMethod.Name}(ControlledRuntime runtime) {{ ... await ... }}");
             }
 
             Delegate test;
             if (hasAsyncReturnType)
             {
                 if (hasStateMachineInputParameters)
                 {
-                    test = Delegate.CreateDelegate(typeof(Func<IStateMachineRuntime, Task>), testMethod);
+                    test = Delegate.CreateDelegate(typeof(Func<ControlledRuntime, Task>), testMethod);
                 }
                 else if (hasTaskInputParameters)
                 {
@@ -207,7 +207,7 @@ private static (Delegate testMethod, string testName) GetTestMethod(Assembly ass
             {
                 if (hasStateMachineInputParameters)
                 {
-                    test = Delegate.CreateDelegate(typeof(Action<IStateMachineRuntime>), testMethod);
+                    test = Delegate.CreateDelegate(typeof(Action<ControlledRuntime>), testMethod);
                 }
                 else if (hasTaskInputParameters)
                 {

diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs
@@ -223,7 +223,7 @@ public static TestingEngine Create(CheckerConfiguration checkerConfiguration, Ac
         /// <summary>
         /// Creates a new systematic testing engine.
         /// </summary>
-        public static TestingEngine Create(CheckerConfiguration checkerConfiguration, Action<IStateMachineRuntime> test) =>
+        public static TestingEngine Create(CheckerConfiguration checkerConfiguration, Action<ControlledRuntime> test) =>
             new TestingEngine(checkerConfiguration, test);
 
         /// <summary>
@@ -241,7 +241,7 @@ public static TestingEngine Create(CheckerConfiguration checkerConfiguration, Fu
         /// <summary>
         /// Creates a new systematic testing engine.
         /// </summary>
-        public static TestingEngine Create(CheckerConfiguration checkerConfiguration, Func<IStateMachineRuntime, Task> test) =>
+        internal static TestingEngine Create(CheckerConfiguration checkerConfiguration, Func<ControlledRuntime, Task> test) =>
             new TestingEngine(checkerConfiguration, test);
 
         /// <summary>

diff --git a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs
@@ -156,6 +156,7 @@ private void WriteSourcePrologue(CompilationContext context, StringWriter output
             context.WriteLine(output, "using PChecker.Specifications;");
             context.WriteLine(output, "using Monitor = PChecker.Specifications.Monitors.Monitor;");
             context.WriteLine(output, "using System;");
+            context.WriteLine(output, "using PChecker.SystematicTesting;");
             context.WriteLine(output, "using System.Runtime;");
             context.WriteLine(output, "using System.Collections.Generic;");
             context.WriteLine(output, "using System.Linq;");
@@ -386,7 +387,7 @@ private void WriteTestFunction(CompilationContext context, StringWriter output,
         {
             context.WriteLine(output);
             context.WriteLine(output, "[PChecker.SystematicTesting.Test]");
-            context.WriteLine(output, "public static void Execute(IStateMachineRuntime runtime) {");
+            context.WriteLine(output, "public static void Execute(ControlledRuntime runtime) {");
             context.WriteLine(output, "PModule.runtime = runtime;");
             context.WriteLine(output, "PHelper.InitializeInterfaces();");
             context.WriteLine(output, "PHelper.InitializeEnums();");
@@ -417,7 +418,7 @@ private void WriteInitializeMonitorMap(CompilationContext context, StringWriter
                 }
             }
 
-            context.WriteLine(output, "public static void InitializeMonitorMap(IStateMachineRuntime runtime) {");
+            context.WriteLine(output, "public static void InitializeMonitorMap(ControlledRuntime runtime) {");
             context.WriteLine(output, "PModule.monitorMap.Clear();");
             foreach (var machine in machineMap)
             {

diff --git a/Src/PCompiler/CompilerCore/Backend/CSharp/Constants.cs b/Src/PCompiler/CompilerCore/Backend/CSharp/Constants.cs
@@ -39,7 +39,7 @@ public static void Main(string[] args)
             // update the path to the schedule file.
             string schedule = File.ReadAllText(""absolute path to *.schedule file"");
             configuration.WithReplayStrategy(schedule);
-            TestingEngine engine = TestingEngine.Create(configuration, (Action<IStateMachineRuntime>)PImplementation.<Name of the test case>.Execute);
+            TestingEngine engine = TestingEngine.Create(configuration, (Action<ControlledRuntime>)PImplementation.<Name of the test case>.Execute);
             engine.Run();
             string bug = engine.TestReport.BugReports.FirstOrDefault();
                 if (bug != null)