From 9aed4f331de4955b586571f497d373a144075e2a Mon Sep 17 00:00:00 2001 From: Christine Zhou Date: Mon, 9 Sep 2024 11:50:18 -0700 Subject: [PATCH] [Cleanup] Remove IStateMachineRuntime --- Src/PChecker/CheckerCore/PRuntime/PModule.cs | 4 ++-- .../CheckerCore/PRuntime/Runtime/CoyoteRuntime.cs | 2 +- .../StateMachines/Exceptions/OnEventDroppedHandler.cs | 2 +- .../StateMachines/Logging/IStateMachineRuntimeLog.cs | 2 +- .../PRuntime/StateMachines/Logging/JsonWriter.cs | 2 +- .../PRuntime/StateMachines/Logging/LogWriter.cs | 2 +- .../PRuntime/StateMachines/StateMachineId.cs | 2 +- .../CheckerCore/Random/IRandomValueGenerator.cs | 2 +- .../CheckerCore/SystematicTesting/ControlledRuntime.cs | 6 +++--- .../CheckerCore/SystematicTesting/TestMethodInfo.cs | 10 +++++----- .../CheckerCore/SystematicTesting/TestingEngine.cs | 4 ++-- .../CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs | 5 +++-- Src/PCompiler/CompilerCore/Backend/CSharp/Constants.cs | 2 +- 13 files changed, 23 insertions(+), 22 deletions(-) diff --git a/Src/PChecker/CheckerCore/PRuntime/PModule.cs b/Src/PChecker/CheckerCore/PRuntime/PModule.cs index d86cbc528d..115f99f3df 100644 --- 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> linkMap = new Dictionary>(); - public static IStateMachineRuntime runtime; + public static ControlledRuntime runtime; } } \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/PRuntime/Runtime/CoyoteRuntime.cs b/Src/PChecker/CheckerCore/PRuntime/Runtime/CoyoteRuntime.cs index 73d26fc39d..4d47ea19da 100644 --- a/Src/PChecker/CheckerCore/PRuntime/Runtime/CoyoteRuntime.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Runtime/CoyoteRuntime.cs @@ -17,7 +17,7 @@ namespace PChecker.Runtime /// /// Runtime for executing asynchronous operations. /// - internal abstract class CoyoteRuntime : ICoyoteRuntime + public abstract class CoyoteRuntime : ICoyoteRuntime { /// /// 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 index df4b14eaea..32a0599565 100644 --- 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 { /// - /// Handles the event. + /// Handles the event. /// public delegate void OnEventDroppedHandler(Event e, StateMachineId target); } \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/IStateMachineRuntimeLog.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/IStateMachineRuntimeLog.cs index 32d2b4ad17..aa933288ac 100644 --- 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 { /// /// Interface that allows an external module to track what - /// is happening in the . + /// is happening in the . /// public interface IStateMachineRuntimeLog { diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/JsonWriter.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/JsonWriter.cs index cb2a9490b1..7602b8afcb 100644 --- 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 index 58fa631bb8..bedd74a389 100644 --- 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 and all registered /// objects. /// - internal sealed class LogWriter + public sealed class LogWriter { /// /// The set of registered log writers. diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachineId.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachineId.cs index 113481c542..2ef8053d07 100644 --- 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, IComparable /// The runtime that executes the state machine with this id. /// - public IStateMachineRuntime Runtime { get; private set; } + internal ControlledRuntime Runtime { get; private set; } /// /// Unique id, when is empty. diff --git a/Src/PChecker/CheckerCore/Random/IRandomValueGenerator.cs b/Src/PChecker/CheckerCore/Random/IRandomValueGenerator.cs index 8e3084ced9..60cd4b0847 100644 --- a/Src/PChecker/CheckerCore/Random/IRandomValueGenerator.cs +++ b/Src/PChecker/CheckerCore/Random/IRandomValueGenerator.cs @@ -6,7 +6,7 @@ namespace PChecker.Random /// /// Interface for random value generators. /// - internal interface IRandomValueGenerator + public interface IRandomValueGenerator { /// /// The seed currently used by the generator. diff --git a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs index aa622f75de..370690989d 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs @@ -39,7 +39,7 @@ namespace PChecker.SystematicTesting /// /// Runtime for controlling asynchronous operations. /// - internal sealed class ControlledRuntime : CoyoteRuntime, IStateMachineRuntime + public sealed class ControlledRuntime : CoyoteRuntime { /// @@ -349,7 +349,7 @@ internal void RunTest(Delegate testMethod, string testName) OperationScheduler.StartOperation(op); - if (testMethod is Action actionWithRuntime) + if (testMethod is Action actionWithRuntime) { actionWithRuntime(this); } @@ -357,7 +357,7 @@ internal void RunTest(Delegate testMethod, string testName) { action(); } - else if (testMethod is Func functionWithRuntime) + else if (testMethod is Func functionWithRuntime) { await functionWithRuntime(this); } diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestMethodInfo.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestMethodInfo.cs index 0a7e1e6cbb..a03ab2889e 100644 --- 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,13 +178,13 @@ 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; @@ -192,7 +192,7 @@ private static (Delegate testMethod, string testName) GetTestMethod(Assembly ass { if (hasStateMachineInputParameters) { - test = Delegate.CreateDelegate(typeof(Func), testMethod); + test = Delegate.CreateDelegate(typeof(Func), testMethod); } else if (hasTaskInputParameters) { @@ -207,7 +207,7 @@ private static (Delegate testMethod, string testName) GetTestMethod(Assembly ass { if (hasStateMachineInputParameters) { - test = Delegate.CreateDelegate(typeof(Action), testMethod); + test = Delegate.CreateDelegate(typeof(Action), testMethod); } else if (hasTaskInputParameters) { diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs index a18300000a..3854568242 100644 --- 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 /// /// Creates a new systematic testing engine. /// - public static TestingEngine Create(CheckerConfiguration checkerConfiguration, Action test) => + public static TestingEngine Create(CheckerConfiguration checkerConfiguration, Action test) => new TestingEngine(checkerConfiguration, test); /// @@ -241,7 +241,7 @@ public static TestingEngine Create(CheckerConfiguration checkerConfiguration, Fu /// /// Creates a new systematic testing engine. /// - public static TestingEngine Create(CheckerConfiguration checkerConfiguration, Func test) => + internal static TestingEngine Create(CheckerConfiguration checkerConfiguration, Func test) => new TestingEngine(checkerConfiguration, test); /// diff --git a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs index 02226f40c6..19be808ec8 100644 --- 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 index b63f3cd462..c2f8208ac3 100644 --- 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)PImplementation..Execute); + TestingEngine engine = TestingEngine.Create(configuration, (Action)PImplementation..Execute); engine.Run(); string bug = engine.TestReport.BugReports.FirstOrDefault(); if (bug != null)