From fd0304af0c684b494e20dc042540866627b59d55 Mon Sep 17 00:00:00 2001 From: Christine Zhou Date: Sun, 8 Sep 2024 11:33:49 -0700 Subject: [PATCH 1/3] [Cleanup] Remove GodMachine, reformat PChecker folder, add assert false after raise test case --- .../Monitoring/CodeCoverageMonitor.cs | 134 ------------------ .../CheckerCore/PRuntime/GodMachine.cs | 31 ---- .../{ => PRuntime}/Runtime/CoyoteRuntime.cs | 0 .../{ => PRuntime}/Runtime/ICoyoteRuntime.cs | 0 .../Runtime/OnFailureHandler.cs | 0 .../{ => PRuntime}/Runtime/RuntimeFactory.cs | 0 .../Specifications/CachedDelegate.cs | 0 .../{ => PRuntime}/Specifications/Monitor.cs | 0 .../EventQueues/DequeueStatus.cs | 0 .../EventQueues/EnqueueStatus.cs | 0 .../StateMachines/EventQueues/EventQueue.cs | 0 .../StateMachines/EventQueues/IEventQueue.cs | 0 .../StateMachines/Events/DefaultEvent.cs | 0 .../StateMachines/Events/Event.cs | 0 .../StateMachines/Events/EventInfo.cs | 0 .../StateMachines/Events/EventOriginInfo.cs | 0 .../StateMachines/Events/GotoStateEvent.cs | 0 .../StateMachines/Events/HaltEvent.cs | 0 .../StateMachines/Events/QuiescentEvent.cs | 0 .../StateMachines/Events/WildcardEvent.cs | 0 .../ActionExceptionFilterException.cs | 0 .../Exceptions/OnEventDroppedHandler.cs | 0 .../Exceptions/OnExceptionOutcome.cs | 0 .../Exceptions/UnhandledEventException.cs | 0 .../Handlers/ActionEventHandlerDeclaration.cs | 0 .../StateMachines/Handlers/CachedDelegate.cs | 0 .../Handlers/DeferEventHandlerDeclaration.cs | 0 .../Handlers/EventHandlerDeclaration.cs | 0 .../Handlers/IgnoreEventHandlerDeclaration.cs | 0 .../StateMachines/IStateMachineRuntime.cs | 0 .../Logging/IStateMachineRuntimeLog.cs | 0 .../StateMachines/Logging/JsonWriter.cs | 0 .../StateMachines/Logging/LogWriter.cs | 0 .../Logging/PCheckerLogJsonFormatter.cs | 23 +-- .../Logging/PCheckerLogTextFormatter.cs | 21 +-- .../Logging/PCheckerLogXmlFormatter.cs | 0 .../Managers/IStateMachineManager.cs | 0 .../Managers/StateMachineManager.cs | 0 .../StateMachines/NameResolver.cs | 0 .../StateMachines/StateMachine.cs | 1 + .../StateMachines/StateMachineFactory.cs | 0 .../StateMachines/StateMachineId.cs | 0 .../StateTransitions/GotoStateTransition.cs | 0 .../StateTransitions/PushStateTransition.cs | 0 .../ExhaustiveSearch.cs | 0 .../Backend/CSharp/CSharpCodeGenerator.cs | 2 +- .../Feature2Stmts/Correct/raise1/raise1.p | 1 + .../Feature2Stmts/Correct/raise2/raise2.p | 1 + 48 files changed, 6 insertions(+), 208 deletions(-) delete mode 100644 Src/PChecker/CheckerCore/Monitoring/CodeCoverageMonitor.cs delete mode 100644 Src/PChecker/CheckerCore/PRuntime/GodMachine.cs rename Src/PChecker/CheckerCore/{ => PRuntime}/Runtime/CoyoteRuntime.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/Runtime/ICoyoteRuntime.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/Runtime/OnFailureHandler.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/Runtime/RuntimeFactory.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/Specifications/CachedDelegate.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/Specifications/Monitor.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/EventQueues/DequeueStatus.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/EventQueues/EnqueueStatus.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/EventQueues/EventQueue.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/EventQueues/IEventQueue.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Events/DefaultEvent.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Events/Event.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Events/EventInfo.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Events/EventOriginInfo.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Events/GotoStateEvent.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Events/HaltEvent.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Events/QuiescentEvent.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Events/WildcardEvent.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Exceptions/ActionExceptionFilterException.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Exceptions/OnEventDroppedHandler.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Exceptions/OnExceptionOutcome.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Exceptions/UnhandledEventException.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Handlers/ActionEventHandlerDeclaration.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Handlers/CachedDelegate.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Handlers/DeferEventHandlerDeclaration.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Handlers/EventHandlerDeclaration.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Handlers/IgnoreEventHandlerDeclaration.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/IStateMachineRuntime.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Logging/IStateMachineRuntimeLog.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Logging/JsonWriter.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Logging/LogWriter.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Logging/PCheckerLogJsonFormatter.cs (96%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Logging/PCheckerLogTextFormatter.cs (94%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Logging/PCheckerLogXmlFormatter.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Managers/IStateMachineManager.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/Managers/StateMachineManager.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/NameResolver.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/StateMachine.cs (99%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/StateMachineFactory.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/StateMachineId.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/StateTransitions/GotoStateTransition.cs (100%) rename Src/PChecker/CheckerCore/{ => PRuntime}/StateMachines/StateTransitions/PushStateTransition.cs (100%) rename Src/PChecker/CheckerCore/{ExhaustiveSearch => SystematicTesting}/ExhaustiveSearch.cs (100%) diff --git a/Src/PChecker/CheckerCore/Monitoring/CodeCoverageMonitor.cs b/Src/PChecker/CheckerCore/Monitoring/CodeCoverageMonitor.cs deleted file mode 100644 index 0f2a11d5e2..0000000000 --- a/Src/PChecker/CheckerCore/Monitoring/CodeCoverageMonitor.cs +++ /dev/null @@ -1,134 +0,0 @@ -// Copyright (c) Microsoft Corporation. -// Licensed under the MIT License. - -#if NETFRAMEWORK -using System; -using System.Diagnostics; -using System.IO; -using System.Threading; - -using Microsoft.Coyote.IO; - -namespace Microsoft.Coyote.SystematicTesting -{ - /// - /// Monitors the program being tested for code coverage. - /// - internal static class CodeCoverageMonitor - { - /// - /// CheckerConfiguration. - /// - private static CheckerConfiguration CheckerConfiguration; - - /// - /// Monitoring process is running. - /// - internal static bool IsRunning; - - /// - /// Starts the code coverage monitor. - /// - /// CheckerConfiguration - internal static void Start(CheckerConfiguration checkerConfiguration) - { - if (IsRunning) - { - throw new InvalidOperationException("Process has already started."); - } - - CheckerConfiguration = checkerConfiguration; - RunMonitorProcess(true); - IsRunning = true; - } - - /// - /// Stops the code coverage monitor. - /// - internal static void Stop() - { - if (CheckerConfiguration is null) - { - throw new InvalidOperationException("Process has not been configured."); - } - - if (!IsRunning) - { - throw new InvalidOperationException("Process is not running."); - } - - RunMonitorProcess(false); - IsRunning = false; - } - - private static void RunMonitorProcess(bool isStarting) - { - var error = string.Empty; - var exitCode = 0; - var outputFile = GetOutputName(); - var arguments = isStarting ? $"/start:coverage /output:{outputFile}" : "/shutdown"; - var timedOut = false; - using (var monitorProc = new Process()) - { - monitorProc.StartInfo.FileName = CodeCoverageInstrumentation.GetToolPath("VSPerfCmdToolPath", "VSPerfCmd"); - monitorProc.StartInfo.Arguments = arguments; - monitorProc.StartInfo.UseShellExecute = false; - monitorProc.StartInfo.RedirectStandardOutput = true; - monitorProc.StartInfo.RedirectStandardError = true; - monitorProc.Start(); - - Console.WriteLine($"... {(isStarting ? "Starting" : "Shutting down")} code coverage monitor"); - - // timedOut can only become true on shutdown (non-infinite timeout value) - timedOut = !monitorProc.WaitForExit(isStarting ? Timeout.Infinite : 5000); - if (!timedOut) - { - exitCode = monitorProc.ExitCode; - if (exitCode != 0) - { - error = monitorProc.StandardError.ReadToEnd(); - } - } - } - - if (exitCode != 0 || error.Length > 0) - { - if (error.Length == 0) - { - error = ""; - } - - Console.WriteLine($"Warning: 'VSPerfCmd {arguments}' exit code {exitCode}: {error}"); - } - - if (!isStarting) - { - if (timedOut) - { - Console.WriteLine($"Warning: VsPerfCmd timed out on shutdown"); - } - - if (File.Exists(outputFile)) - { - var fileInfo = new FileInfo(outputFile); - Console.WriteLine($"..... Created {outputFile}"); - } - else - { - Console.WriteLine($"Warning: Code coverage output file {outputFile} was not created"); - } - } - } - - /// - /// Returns the output name. - /// - private static string GetOutputName() - { - string file = Path.GetFileNameWithoutExtension(CheckerConfiguration.AssemblyToBeAnalyzed); - string directory = CodeCoverageInstrumentation.OutputDirectory; - return $"{directory}{file}.coverage"; - } - } -} -#endif \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/PRuntime/GodMachine.cs b/Src/PChecker/CheckerCore/PRuntime/GodMachine.cs deleted file mode 100644 index 76fbfeb866..0000000000 --- a/Src/PChecker/CheckerCore/PRuntime/GodMachine.cs +++ /dev/null @@ -1,31 +0,0 @@ -using System; -using PChecker.StateMachines; -using PChecker.StateMachines.Events; - -namespace PChecker.PRuntime -{ - public class _GodMachine : StateMachine - { - private void InitOnEntry(Event e) - { - var mainMachine = (e as Config).MainMachine; - CreateStateMachine(mainMachine, mainMachine.Name); - } - - public class Config : Event - { - public Type MainMachine; - - public Config(Type main) - { - MainMachine = main; - } - } - - [Start] - [OnEntry(nameof(InitOnEntry))] - private class Init : State - { - } - } -} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Runtime/CoyoteRuntime.cs b/Src/PChecker/CheckerCore/PRuntime/Runtime/CoyoteRuntime.cs similarity index 100% rename from Src/PChecker/CheckerCore/Runtime/CoyoteRuntime.cs rename to Src/PChecker/CheckerCore/PRuntime/Runtime/CoyoteRuntime.cs diff --git a/Src/PChecker/CheckerCore/Runtime/ICoyoteRuntime.cs b/Src/PChecker/CheckerCore/PRuntime/Runtime/ICoyoteRuntime.cs similarity index 100% rename from Src/PChecker/CheckerCore/Runtime/ICoyoteRuntime.cs rename to Src/PChecker/CheckerCore/PRuntime/Runtime/ICoyoteRuntime.cs diff --git a/Src/PChecker/CheckerCore/Runtime/OnFailureHandler.cs b/Src/PChecker/CheckerCore/PRuntime/Runtime/OnFailureHandler.cs similarity index 100% rename from Src/PChecker/CheckerCore/Runtime/OnFailureHandler.cs rename to Src/PChecker/CheckerCore/PRuntime/Runtime/OnFailureHandler.cs diff --git a/Src/PChecker/CheckerCore/Runtime/RuntimeFactory.cs b/Src/PChecker/CheckerCore/PRuntime/Runtime/RuntimeFactory.cs similarity index 100% rename from Src/PChecker/CheckerCore/Runtime/RuntimeFactory.cs rename to Src/PChecker/CheckerCore/PRuntime/Runtime/RuntimeFactory.cs diff --git a/Src/PChecker/CheckerCore/Specifications/CachedDelegate.cs b/Src/PChecker/CheckerCore/PRuntime/Specifications/CachedDelegate.cs similarity index 100% rename from Src/PChecker/CheckerCore/Specifications/CachedDelegate.cs rename to Src/PChecker/CheckerCore/PRuntime/Specifications/CachedDelegate.cs diff --git a/Src/PChecker/CheckerCore/Specifications/Monitor.cs b/Src/PChecker/CheckerCore/PRuntime/Specifications/Monitor.cs similarity index 100% rename from Src/PChecker/CheckerCore/Specifications/Monitor.cs rename to Src/PChecker/CheckerCore/PRuntime/Specifications/Monitor.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/EventQueues/DequeueStatus.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/EventQueues/DequeueStatus.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/EventQueues/DequeueStatus.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/EventQueues/DequeueStatus.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/EventQueues/EnqueueStatus.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/EventQueues/EnqueueStatus.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/EventQueues/EnqueueStatus.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/EventQueues/EnqueueStatus.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/EventQueues/EventQueue.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/EventQueues/EventQueue.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/EventQueues/EventQueue.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/EventQueues/EventQueue.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/EventQueues/IEventQueue.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/EventQueues/IEventQueue.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/EventQueues/IEventQueue.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/EventQueues/IEventQueue.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Events/DefaultEvent.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Events/DefaultEvent.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Events/DefaultEvent.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Events/DefaultEvent.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Events/Event.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Events/Event.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Events/Event.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Events/Event.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Events/EventInfo.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Events/EventInfo.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Events/EventInfo.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Events/EventInfo.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Events/EventOriginInfo.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Events/EventOriginInfo.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Events/EventOriginInfo.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Events/EventOriginInfo.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Events/GotoStateEvent.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Events/GotoStateEvent.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Events/GotoStateEvent.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Events/GotoStateEvent.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Events/HaltEvent.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Events/HaltEvent.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Events/HaltEvent.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Events/HaltEvent.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Events/QuiescentEvent.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Events/QuiescentEvent.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Events/QuiescentEvent.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Events/QuiescentEvent.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Events/WildcardEvent.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Events/WildcardEvent.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Events/WildcardEvent.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Events/WildcardEvent.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Exceptions/ActionExceptionFilterException.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Exceptions/ActionExceptionFilterException.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Exceptions/ActionExceptionFilterException.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Exceptions/ActionExceptionFilterException.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Exceptions/OnEventDroppedHandler.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Exceptions/OnEventDroppedHandler.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Exceptions/OnEventDroppedHandler.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Exceptions/OnEventDroppedHandler.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Exceptions/OnExceptionOutcome.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Exceptions/OnExceptionOutcome.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Exceptions/OnExceptionOutcome.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Exceptions/OnExceptionOutcome.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Exceptions/UnhandledEventException.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Exceptions/UnhandledEventException.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Exceptions/UnhandledEventException.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Exceptions/UnhandledEventException.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Handlers/ActionEventHandlerDeclaration.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Handlers/ActionEventHandlerDeclaration.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Handlers/ActionEventHandlerDeclaration.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Handlers/ActionEventHandlerDeclaration.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Handlers/CachedDelegate.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Handlers/CachedDelegate.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Handlers/CachedDelegate.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Handlers/CachedDelegate.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Handlers/DeferEventHandlerDeclaration.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Handlers/DeferEventHandlerDeclaration.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Handlers/DeferEventHandlerDeclaration.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Handlers/DeferEventHandlerDeclaration.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Handlers/EventHandlerDeclaration.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Handlers/EventHandlerDeclaration.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Handlers/EventHandlerDeclaration.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Handlers/EventHandlerDeclaration.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Handlers/IgnoreEventHandlerDeclaration.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Handlers/IgnoreEventHandlerDeclaration.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Handlers/IgnoreEventHandlerDeclaration.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Handlers/IgnoreEventHandlerDeclaration.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/IStateMachineRuntime.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/IStateMachineRuntime.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/IStateMachineRuntime.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/IStateMachineRuntime.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Logging/IStateMachineRuntimeLog.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/IStateMachineRuntimeLog.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Logging/IStateMachineRuntimeLog.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/IStateMachineRuntimeLog.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Logging/JsonWriter.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/JsonWriter.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Logging/JsonWriter.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/JsonWriter.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Logging/LogWriter.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/LogWriter.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Logging/LogWriter.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/LogWriter.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogJsonFormatter.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/PCheckerLogJsonFormatter.cs similarity index 96% rename from Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogJsonFormatter.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/PCheckerLogJsonFormatter.cs index fbe857f3b3..36b6d72ed6 100644 --- a/Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogJsonFormatter.cs +++ b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/PCheckerLogJsonFormatter.cs @@ -114,11 +114,6 @@ public void OnAssertionFailure(string error) /// public void OnCreateStateMachine(StateMachineId id, string creatorName, string creatorType) { - if (id.Name.Contains("GodMachine") || creatorName.Contains("GodMachine")) - { - return; - } - var source = creatorName ?? $"task '{Task.CurrentId}'"; var log = $"{id} was created by {source}."; @@ -147,11 +142,6 @@ public void OnDefaultEventHandler(StateMachineId id, string stateName) public void OnDequeueEvent(StateMachineId id, string stateName, Event e) { - if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine")) - { - return; - } - var eventName = GetEventNameWithPayload(e); var log = stateName is null ? $"'{id}' dequeued event '{eventName}'." @@ -221,11 +211,6 @@ public void OnExecuteAction(StateMachineId id, string handlingStateName, string /// public void OnGotoState(StateMachineId id, string currentStateName, string newStateName) { - if (currentStateName.Contains("__InitState__") || id.Name.Contains("GodMachine")) - { - return; - } - currentStateName = GetShortName(currentStateName); newStateName = GetShortName(newStateName); @@ -304,8 +289,7 @@ public void OnRaiseEvent(StateMachineId id, string stateName, Event e) stateName = GetShortName(stateName); string eventName = GetEventNameWithPayload(e); - if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine") || - eventName.Contains("GotoStateEvent")) + if (eventName.Contains("GotoStateEvent")) { return; } @@ -371,11 +355,6 @@ public void OnSendEvent(StateMachineId targetStateMachineId, string senderName, /// public void OnStateTransition(StateMachineId id, string stateName, bool isEntry) { - if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine")) - { - return; - } - stateName = GetShortName(stateName); var direction = isEntry ? "enters" : "exits"; var log = $"{id} {direction} state '{stateName}'."; diff --git a/Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogTextFormatter.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/PCheckerLogTextFormatter.cs similarity index 94% rename from Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogTextFormatter.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/PCheckerLogTextFormatter.cs index 06b94318f2..96f8078f51 100644 --- a/Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogTextFormatter.cs +++ b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/PCheckerLogTextFormatter.cs @@ -57,10 +57,6 @@ public void OnAssertionFailure(string error) /// public void OnCreateStateMachine(StateMachineId id, string creatorName, string creatorType) { - if (id.Name.Contains("GodMachine") || creatorName.Contains("GodMachine")) - { - return; - } var source = creatorName ?? $"task '{Task.CurrentId}'"; var text = $" {id} was created by {source}."; Logger.WriteLine(text); @@ -69,11 +65,6 @@ public void OnCreateStateMachine(StateMachineId id, string creatorName, string c /// public void OnStateTransition(StateMachineId id, string stateName, bool isEntry) { - if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine")) - { - return; - } - var direction = isEntry ? "enters" : "exits"; var text = $" {id} {direction} state '{stateName}'."; Logger.WriteLine(text); @@ -188,11 +179,6 @@ public void OnMonitorProcessEvent(string monitorType, string stateName, string s /// public void OnDequeueEvent(StateMachineId id, string stateName, Event e) { - if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine")) - { - return; - } - stateName = GetShortName(stateName); var eventName = GetEventNameWithPayload(e); string text = null; @@ -213,7 +199,7 @@ public void OnRaiseEvent(StateMachineId id, string stateName, Event e) { stateName = GetShortName(stateName); var eventName = GetEventNameWithPayload(e); - if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine") || eventName.Contains("GotoStateEvent")) + if (eventName.Contains("GotoStateEvent")) { return; } @@ -277,11 +263,6 @@ public void OnSendEvent(StateMachineId targetStateMachineId, string senderName, /// public void OnGotoState(StateMachineId id, string currStateName, string newStateName) { - if (currStateName.Contains("__InitState__") || id.Name.Contains("GodMachine")) - { - return; - } - var text = $" {id} is transitioning from state '{currStateName}' to state '{newStateName}'."; Logger.WriteLine(text); } diff --git a/Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogXmlFormatter.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/PCheckerLogXmlFormatter.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogXmlFormatter.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/PCheckerLogXmlFormatter.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Managers/IStateMachineManager.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Managers/IStateMachineManager.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Managers/IStateMachineManager.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Managers/IStateMachineManager.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/Managers/StateMachineManager.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Managers/StateMachineManager.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/Managers/StateMachineManager.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Managers/StateMachineManager.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/NameResolver.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/NameResolver.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/NameResolver.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/NameResolver.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/StateMachine.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachine.cs similarity index 99% rename from Src/PChecker/CheckerCore/StateMachines/StateMachine.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachine.cs index 25245a3c86..5dda0c7fb5 100644 --- a/Src/PChecker/CheckerCore/StateMachines/StateMachine.cs +++ b/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachine.cs @@ -966,6 +966,7 @@ public void RaiseEvent(Event e) Assert(e != null, "{0} is raising a null event.", Id); CheckDanglingTransition(); PendingTransition = new Transition(Transition.Type.RaiseEvent, default, e); + throw new PNonStandardReturnException { ReturnKind = NonStandardReturn.Raise }; } /// diff --git a/Src/PChecker/CheckerCore/StateMachines/StateMachineFactory.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachineFactory.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/StateMachineFactory.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachineFactory.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/StateMachineId.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachineId.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/StateMachineId.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachineId.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/StateTransitions/GotoStateTransition.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateTransitions/GotoStateTransition.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/StateTransitions/GotoStateTransition.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/StateTransitions/GotoStateTransition.cs diff --git a/Src/PChecker/CheckerCore/StateMachines/StateTransitions/PushStateTransition.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateTransitions/PushStateTransition.cs similarity index 100% rename from Src/PChecker/CheckerCore/StateMachines/StateTransitions/PushStateTransition.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/StateTransitions/PushStateTransition.cs diff --git a/Src/PChecker/CheckerCore/ExhaustiveSearch/ExhaustiveSearch.cs b/Src/PChecker/CheckerCore/SystematicTesting/ExhaustiveSearch.cs similarity index 100% rename from Src/PChecker/CheckerCore/ExhaustiveSearch/ExhaustiveSearch.cs rename to Src/PChecker/CheckerCore/SystematicTesting/ExhaustiveSearch.cs diff --git a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs index eaaf86a259..02226f40c6 100644 --- a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs +++ b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs @@ -395,7 +395,7 @@ private void WriteTestFunction(CompilationContext context, StringWriter output, context.WriteLine(output, "InitializeMonitorMap(runtime);"); context.WriteLine(output, "InitializeMonitorObserves();"); context.WriteLine(output, - $"runtime.CreateStateMachine(typeof(_GodMachine), new _GodMachine.Config(typeof({main})));"); + $"runtime.CreateStateMachine(typeof({main}), \"{main}\");"); context.WriteLine(output, "}"); } diff --git a/Tst/RegressionTests/Feature2Stmts/Correct/raise1/raise1.p b/Tst/RegressionTests/Feature2Stmts/Correct/raise1/raise1.p index 234e066eea..4455a9db44 100644 --- a/Tst/RegressionTests/Feature2Stmts/Correct/raise1/raise1.p +++ b/Tst/RegressionTests/Feature2Stmts/Correct/raise1/raise1.p @@ -8,6 +8,7 @@ start state Init { entry { raise E1, 1000; + assert false; } on E1 do (payload: int) { assert (payload == 1000), format ("Expected payload to be 1000, actual payload is {0}", payload); diff --git a/Tst/RegressionTests/Feature2Stmts/Correct/raise2/raise2.p b/Tst/RegressionTests/Feature2Stmts/Correct/raise2/raise2.p index a433e06b11..0f80187bfd 100644 --- a/Tst/RegressionTests/Feature2Stmts/Correct/raise2/raise2.p +++ b/Tst/RegressionTests/Feature2Stmts/Correct/raise2/raise2.p @@ -18,6 +18,7 @@ start state Init { on E1 do { raise E2, 1000; + assert false; } on E2 do (payload: int) { assert (payload == 1000), format ("Expected payload to be 1000, actual payload is {0}", payload); From c599395dbde8267752ef8569e245a2810ce79675 Mon Sep 17 00:00:00 2001 From: Christine Zhou Date: Mon, 9 Sep 2024 11:50:18 -0700 Subject: [PATCH 2/3] [Cleanup] Remove IStateMachineRuntime, ICyoteRuntime, CyoteRuntime --- Src/PChecker/CheckerCore/PRuntime/PModule.cs | 4 +- .../PRuntime/Runtime/CoyoteRuntime.cs | 300 ------------------ .../PRuntime/Runtime/ICoyoteRuntime.cs | 136 -------- .../PRuntime/Runtime/OnFailureHandler.cs | 2 +- .../PRuntime/Runtime/RuntimeFactory.cs | 20 +- .../Exceptions/OnEventDroppedHandler.cs | 2 +- .../StateMachines/IStateMachineRuntime.cs | 158 --------- .../Logging/IStateMachineRuntimeLog.cs | 2 +- .../StateMachines/Logging/JsonWriter.cs | 2 +- .../StateMachines/Logging/LogWriter.cs | 2 +- .../PRuntime/StateMachines/StateMachineId.cs | 2 +- Src/PChecker/CheckerCore/Random/Generator.cs | 6 +- .../Random/IRandomValueGenerator.cs | 2 +- .../SystematicTesting/ControlledRuntime.cs | 212 ++++++++++--- .../SystematicTesting/TaskController.cs | 8 +- .../SystematicTesting/TestMethodInfo.cs | 20 +- .../SystematicTesting/TestingEngine.cs | 18 +- .../Tasks/AsyncTaskMethodBuilder.cs | 4 +- Src/PChecker/CheckerCore/Tasks/Task.cs | 28 +- .../CheckerCore/Tasks/TaskCompletionSource.cs | 2 +- .../Backend/CSharp/CSharpCodeGenerator.cs | 5 +- .../CompilerCore/Backend/CSharp/Constants.cs | 2 +- 22 files changed, 236 insertions(+), 701 deletions(-) delete mode 100644 Src/PChecker/CheckerCore/PRuntime/Runtime/CoyoteRuntime.cs delete mode 100644 Src/PChecker/CheckerCore/PRuntime/Runtime/ICoyoteRuntime.cs delete mode 100644 Src/PChecker/CheckerCore/PRuntime/StateMachines/IStateMachineRuntime.cs 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 deleted file mode 100644 index 73d26fc39d..0000000000 --- a/Src/PChecker/CheckerCore/PRuntime/Runtime/CoyoteRuntime.cs +++ /dev/null @@ -1,300 +0,0 @@ -// Copyright (c) Microsoft Corporation. -// Licensed under the MIT License. - -using System; -using System.Collections.Generic; -using System.Globalization; -using System.IO; -using System.Threading; -using System.Threading.Tasks; -using PChecker.StateMachines.Events; -using PChecker.Exceptions; -using PChecker.Random; -using Monitor = PChecker.Specifications.Monitors.Monitor; - -namespace PChecker.Runtime -{ - /// - /// Runtime for executing asynchronous operations. - /// - internal abstract class CoyoteRuntime : ICoyoteRuntime - { - /// - /// Provides access to the runtime associated with each asynchronous control flow. - /// - /// - /// In testing mode, each testing schedule uses a unique runtime instance. To safely - /// retrieve it from static methods, we store it in each asynchronous control flow. - /// - private static readonly AsyncLocal AsyncLocalInstance = new AsyncLocal(); - - /// - /// The currently executing runtime. - /// - internal static CoyoteRuntime Current => AsyncLocalInstance.Value ?? - (IsExecutionControlled ? throw new InvalidOperationException(string.Format(CultureInfo.InvariantCulture, - "Uncontrolled task '{0}' invoked a runtime method. Please make sure to avoid using concurrency APIs " + - "(e.g. 'Task.Run', 'Task.Delay' or 'Task.Yield' from the 'System.Threading.Tasks' namespace) inside " + - "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); - - /// - /// If true, the program execution is controlled by the runtime to - /// explore interleavings and sources of nondeterminism, else false. - /// - internal static bool IsExecutionControlled { get; private protected set; } = false; - - /// - /// The checkerConfiguration used by the runtime. - /// - protected internal readonly CheckerConfiguration CheckerConfiguration; - - /// - /// List of monitors in the program. - /// - protected readonly List Monitors; - - /// - /// Responsible for generating random values. - /// - protected readonly IRandomValueGenerator ValueGenerator; - - /// - /// Monotonically increasing operation id counter. - /// - private long OperationIdCounter; - - /// - /// Records if the runtime is running. - /// - protected internal volatile bool IsRunning; - - /// - /// Used to log text messages. Use - /// to replace the logger with a custom one. - /// - public abstract TextWriter Logger { get; } - - /// - /// Callback that is fired when the Coyote program throws an exception which includes failed assertions. - /// - public event OnFailureHandler OnFailure; - - /// - /// Initializes a new instance of the class. - /// - protected CoyoteRuntime(CheckerConfiguration checkerConfiguration, IRandomValueGenerator valueGenerator) - { - CheckerConfiguration = checkerConfiguration; - Monitors = new List(); - ValueGenerator = valueGenerator; - OperationIdCounter = 0; - IsRunning = true; - } - - /// - /// Registers a new specification monitor of the specified . - /// - public void RegisterMonitor() - where T : Monitor => - TryCreateMonitor(typeof(T)); - - /// - /// Invokes the specified monitor with the specified . - /// - public void Monitor(Event e) - where T : Monitor - { - // If the event is null then report an error and exit. - Assert(e != null, "Cannot monitor a null event."); - Monitor(typeof(T), e, null, null, null); - } - - /// - /// Returns a nondeterministic boolean choice, that can be controlled - /// during analysis or testing. - /// - public bool RandomBoolean() => GetNondeterministicBooleanChoice(2, null, null); - - /// - /// Returns a nondeterministic boolean choice, that can be controlled - /// during analysis or testing. The value is used to generate a number - /// in the range [0..maxValue), where 0 triggers true. - /// - public bool RandomBoolean(int maxValue) => GetNondeterministicBooleanChoice(maxValue, null, null); - - /// - /// Returns a nondeterministic integer, that can be controlled during - /// analysis or testing. The value is used to generate an integer in - /// the range [0..maxValue). - /// - public int RandomInteger(int maxValue) => GetNondeterministicIntegerChoice(maxValue, null, null); - - /// - /// Returns the next available unique operation id. - /// - /// Value representing the next available unique operation id. - internal ulong GetNextOperationId() => - // Atomically increments and safely wraps the value into an unsigned long. - (ulong)Interlocked.Increment(ref OperationIdCounter) - 1; - - /// - /// Tries to create a new of the specified . - /// - internal abstract void TryCreateMonitor(Type type); - - /// - /// Invokes the specified with the specified . - /// - internal virtual void Monitor(Type type, Event e, string senderName, string senderType, string senderState) - { - Monitor monitor = null; - - lock (Monitors) - { - foreach (var m in Monitors) - { - if (m.GetType() == type) - { - monitor = m; - break; - } - } - } - - if (monitor != null) - { - lock (monitor) - { - monitor.MonitorEvent(e, senderName, senderType, senderState); - } - } - } - - /// - /// Checks if the assertion holds, and if not, throws an exception. - /// - public virtual void Assert(bool predicate) - { - if (!predicate) - { - throw new AssertionFailureException("Detected an assertion failure."); - } - } - - /// - /// Checks if the assertion holds, and if not, throws an exception. - /// - public virtual void Assert(bool predicate, string s, object arg0) - { - if (!predicate) - { - throw new AssertionFailureException(string.Format(CultureInfo.InvariantCulture, s, arg0?.ToString())); - } - } - - /// - /// Checks if the assertion holds, and if not, throws an exception. - /// - public virtual void Assert(bool predicate, string s, object arg0, object arg1) - { - if (!predicate) - { - throw new AssertionFailureException(string.Format(CultureInfo.InvariantCulture, s, arg0?.ToString(), arg1?.ToString())); - } - } - - /// - /// Checks if the assertion holds, and if not, throws an exception. - /// - public virtual void Assert(bool predicate, string s, object arg0, object arg1, object arg2) - { - if (!predicate) - { - throw new AssertionFailureException(string.Format(CultureInfo.InvariantCulture, s, arg0?.ToString(), arg1?.ToString(), arg2?.ToString())); - } - } - - /// - /// Checks if the assertion holds, and if not, throws an exception. - /// - public virtual void Assert(bool predicate, string s, params object[] args) - { - if (!predicate) - { - throw new AssertionFailureException(string.Format(CultureInfo.InvariantCulture, s, args)); - } - } - - /// - /// Returns a controlled nondeterministic boolean choice. - /// - internal abstract bool GetNondeterministicBooleanChoice(int maxValue, string callerName, string callerType); - - /// - /// Returns a controlled nondeterministic integer choice. - /// - internal abstract int GetNondeterministicIntegerChoice(int maxValue, string callerName, string callerType); - - /// - /// Assigns the specified runtime as the default for the current asynchronous control flow. - /// - internal static void AssignAsyncControlFlowRuntime(CoyoteRuntime runtime) => AsyncLocalInstance.Value = runtime; - - /// - /// Use this method to override the default for logging messages. - /// - public abstract TextWriter SetLogger(TextWriter logger); - - /// - /// Raises the event with the specified . - /// - protected internal virtual void RaiseOnFailureEvent(Exception exception) - { - OnFailure?.Invoke(exception); - } - - /// - /// Throws an exception - /// containing the specified exception. - /// - internal virtual void WrapAndThrowException(Exception exception, string s, params object[] args) - { - var msg = string.Format(CultureInfo.InvariantCulture, s, args); - var message = string.Format(CultureInfo.InvariantCulture, - "Exception '{0}' was thrown in {1}: {2}\n" + - "from location '{3}':\n" + - "The stack trace is:\n{4}", - exception.GetType(), msg, exception.Message, exception.Source, exception.StackTrace); - - throw new AssertionFailureException(message, exception); - } - - /// - /// Terminates the runtime and notifies each active state machine to halt execution. - /// - public void Stop() => IsRunning = false; - - /// - /// Disposes runtime resources. - /// - protected virtual void Dispose(bool disposing) - { - if (disposing) - { - OperationIdCounter = 0; - } - } - - /// - /// Disposes runtime resources. - /// - public void Dispose() - { - Dispose(true); - GC.SuppressFinalize(this); - } - } -} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/PRuntime/Runtime/ICoyoteRuntime.cs b/Src/PChecker/CheckerCore/PRuntime/Runtime/ICoyoteRuntime.cs deleted file mode 100644 index e5b72ff206..0000000000 --- a/Src/PChecker/CheckerCore/PRuntime/Runtime/ICoyoteRuntime.cs +++ /dev/null @@ -1,136 +0,0 @@ -// Copyright (c) Microsoft Corporation. -// Licensed under the MIT License. - -using System; -using System.IO; -using PChecker.StateMachines.Events; -using PChecker.Exceptions; -using PChecker.Specifications.Monitors; - -namespace PChecker.Runtime -{ - /// - /// Interface that exposes base runtime methods for Coyote. - /// - public interface ICoyoteRuntime : IDisposable - { - /// - /// Used to log messages. Use - /// to replace the logger with a custom one. - /// - /// - /// See Logging for more information. - /// - TextWriter Logger { get; } - - /// - /// Callback that is fired when the runtime throws an exception which includes failed assertions. - /// - event OnFailureHandler OnFailure; - - /// - /// Registers a new specification monitor of the specified . - /// - /// Type of the monitor. - void RegisterMonitor() - where T : Monitor; - - /// - /// Invokes the specified monitor with the specified . - /// - /// Type of the monitor. - /// Event to send to the monitor. - void Monitor(Event e) - where T : Monitor; - - /// - /// Returns a nondeterministic boolean choice, that can be controlled - /// during analysis or testing. - /// - /// The nondeterministic boolean choice. - /// - /// See Program non-determinism - /// for more information. - /// - bool RandomBoolean(); - - /// - /// Returns a nondeterministic boolean choice, that can be controlled - /// during analysis or testing. The value is used to generate a number - /// in the range [0..maxValue), where 0 triggers true. - /// - /// The max value. - /// The nondeterministic boolean choice. - /// - /// See Program non-determinism - /// for more information. - /// - bool RandomBoolean(int maxValue); - - /// - /// Returns a nondeterministic integer choice, that can be - /// controlled during analysis or testing. The value is used - /// to generate an integer in the range [0..maxValue). - /// - /// The max value. - /// The nondeterministic integer choice. - /// - /// See Program non-determinism - /// for more information. - /// - int RandomInteger(int maxValue); - - /// - /// Checks if the assertion holds, and if not, throws an exception. - /// - /// The predicate to check. - void Assert(bool predicate); - - /// - /// Checks if the assertion holds, and if not, throws an exception. - /// - /// The predicate to check. - /// The message to print if the assertion fails. - /// The first argument. - void Assert(bool predicate, string s, object arg0); - - /// - /// Checks if the assertion holds, and if not, throws an exception. - /// - /// The predicate to check. - /// The message to print if the assertion fails. - /// The first argument. - /// The second argument. - void Assert(bool predicate, string s, object arg0, object arg1); - - /// - /// Checks if the assertion holds, and if not, throws an exception. - /// - /// The predicate to check. - /// The message to print if the assertion fails. - /// The first argument. - /// The second argument. - /// The third argument. - void Assert(bool predicate, string s, object arg0, object arg1, object arg2); - - /// - /// Checks if the assertion holds, and if not, throws an exception. - /// - /// The predicate to check. - /// The message to print if the assertion fails. - /// The message arguments. - void Assert(bool predicate, string s, params object[] args); - - /// - /// Use this method to override the default for logging messages. - /// - /// The logger to install. - /// The previously installed logger. - TextWriter SetLogger(TextWriter logger); - - /// - /// Terminates the runtime and notifies each active state machine to halt execution. - /// - void Stop(); - } -} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/PRuntime/Runtime/OnFailureHandler.cs b/Src/PChecker/CheckerCore/PRuntime/Runtime/OnFailureHandler.cs index 4c2e7f36bf..97acb4614e 100644 --- a/Src/PChecker/CheckerCore/PRuntime/Runtime/OnFailureHandler.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Runtime/OnFailureHandler.cs @@ -6,7 +6,7 @@ namespace PChecker.Runtime { /// - /// Handles the event. + /// Handles the event. /// public delegate void OnFailureHandler(Exception ex); } \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/PRuntime/Runtime/RuntimeFactory.cs b/Src/PChecker/CheckerCore/PRuntime/Runtime/RuntimeFactory.cs index f7c03b7b43..107ad79e7b 100644 --- a/Src/PChecker/CheckerCore/PRuntime/Runtime/RuntimeFactory.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Runtime/RuntimeFactory.cs @@ -9,14 +9,14 @@ namespace PChecker.Runtime { /// - /// Provides methods for creating a runtime. + /// Provides methods for creating a runtime. /// public static class RuntimeFactory { /// /// The installed runtime instance. /// - internal static CoyoteRuntime InstalledRuntime { get; private set; } = CreateWithConfiguration(default); + internal static ControlledRuntime InstalledRuntime { get; private set; } = CreateWithConfiguration(default); /// /// Protects access to the installed runtime. @@ -24,17 +24,17 @@ public static class RuntimeFactory private static readonly object SyncObject = new object(); /// - /// Creates a new Coyote runtime. + /// 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 ICoyoteRuntime Create() => CreateAndInstall(default); + public static ControlledRuntime Create() => CreateAndInstall(default); /// - /// Creates a new Coyote runtime with the specified . + /// Creates a new ControlledRuntime with the specified . /// /// The runtime checkerConfiguration to use. /// The created task runtime. @@ -42,13 +42,13 @@ public static class RuntimeFactory /// Only one task runtime can be created per process. If you create a new task /// runtime it replaces the previously installed one. /// - public static ICoyoteRuntime Create(CheckerConfiguration checkerConfiguration) => CreateAndInstall(checkerConfiguration); + public static ControlledRuntime Create(CheckerConfiguration checkerConfiguration) => CreateAndInstall(checkerConfiguration); /// - /// Creates a new Coyote runtime with the specified and sets + /// 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 CoyoteRuntime CreateAndInstall(CheckerConfiguration checkerConfiguration) + private static ControlledRuntime CreateAndInstall(CheckerConfiguration checkerConfiguration) { lock (SyncObject) { @@ -58,9 +58,9 @@ private static CoyoteRuntime CreateAndInstall(CheckerConfiguration checkerConfig } /// - /// Creates a new Coyote runtime with the specified . + /// Creates a new ControlledRuntime with the specified . /// - private static CoyoteRuntime CreateWithConfiguration(CheckerConfiguration checkerConfiguration) + private static ControlledRuntime CreateWithConfiguration(CheckerConfiguration checkerConfiguration) { if (checkerConfiguration is null) { 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/IStateMachineRuntime.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/IStateMachineRuntime.cs deleted file mode 100644 index c1b3ae7518..0000000000 --- a/Src/PChecker/CheckerCore/PRuntime/StateMachines/IStateMachineRuntime.cs +++ /dev/null @@ -1,158 +0,0 @@ -// Copyright (c) Microsoft Corporation. -// Licensed under the MIT License. - -using System; -using System.Threading.Tasks; -using PChecker.StateMachines.Events; -using PChecker.StateMachines.Exceptions; -using PChecker.StateMachines.Logging; -using PChecker.Runtime; - -namespace PChecker.StateMachines -{ - /// - /// Interface that exposes runtime methods for creating and executing state machines. - /// - public interface IStateMachineRuntime : ICoyoteRuntime - { - /// - /// Callback that is fired when an event is dropped. - /// - event OnEventDroppedHandler OnEventDropped; - - /// - /// Creates a fresh state machine id that has not yet been bound to any state machine. - /// - /// Type of the state machine. - /// Optional name used for logging. - /// The result is the state machine id. - StateMachineId CreateStateMachineId(Type type, string name = null); - - /// - /// Creates a state machine id that is uniquely tied to the specified unique name. The - /// returned state machine id can either be a fresh id (not yet bound to any state machine), or - /// it can be bound to a previously created state machine. In the second case, this state machine - /// id can be directly used to communicate with the corresponding state machine. - /// - /// Type of the state machine. - /// Unique name used to create or get the state machine id. - /// The result is the state machine id. - StateMachineId CreateStateMachineIdFromName(Type type, string name); - - /// - /// Creates a new state machine of the specified and with the specified - /// optional . This event can only be used to access its payload, - /// and cannot be handled. - /// - /// Type of the state machine. - /// Optional event used during initialization. - /// Optional id that can be used to identify this operation. - /// The result is the state machine id. - StateMachineId CreateStateMachine(Type type, Event initialEvent = null, Guid opGroupId = default); - - /// - /// Creates a new state machine of the specified and name, and with the - /// specified optional . This event can only be used to access - /// its payload, and cannot be handled. - /// - /// Type of the state machine. - /// Optional name used for logging. - /// Optional event used during initialization. - /// Optional id that can be used to identify this operation. - /// The result is the state machine id. - StateMachineId CreateStateMachine(Type type, string name, Event initialEvent = null, Guid opGroupId = default); - - /// - /// Creates a new state machine of the specified type, using the specified . - /// This method optionally passes an to the new state machine, which can only - /// be used to access its payload, and cannot be handled. - /// - /// Unbound state machine id. - /// Type of the state machine. - /// Optional event used during initialization. - /// Optional id that can be used to identify this operation. - /// The result is the state machine id. - StateMachineId CreateStateMachine(StateMachineId id, Type type, Event initialEvent = null, Guid opGroupId = default); - - /// - /// Creates a new state machine of the specified and with the specified - /// optional . This event can only be used to access its payload, - /// and cannot be handled. The method returns only when the state machine is initialized and - /// the (if any) is handled. - /// - /// Type of the state machine. - /// Optional event used during initialization. - /// Optional id that can be used to identify this operation. - /// Task that represents the asynchronous operation. The task result is the state machine id. - Task CreateStateMachineAndExecuteAsync(Type type, Event initialEvent = null, Guid opGroupId = default); - - /// - /// Creates a new state machine of the specified and name, and with the - /// specified optional . This event can only be used to access - /// its payload, and cannot be handled. The method returns only when the state machine is - /// initialized and the (if any) is handled. - /// - /// Type of the state machine. - /// Optional name used for logging. - /// Optional event used during initialization. - /// Optional id that can be used to identify this operation. - /// Task that represents the asynchronous operation. The task result is the state machine id. - Task CreateStateMachineAndExecuteAsync(Type type, string name, Event initialEvent = null, - Guid opGroupId = default); - - /// - /// Creates a new state machine of the specified , using the specified unbound - /// state machine id, and passes the specified optional . This event can only - /// be used to access its payload, and cannot be handled. The method returns only when - /// the state machine is initialized and the (if any) - /// is handled. - /// - /// Unbound state machine id. - /// Type of the state machine. - /// Optional event used during initialization. - /// Optional id that can be used to identify this operation. - /// Task that represents the asynchronous operation. The task result is the state machine id. - Task CreateStateMachineAndExecuteAsync(StateMachineId id, Type type, Event initialEvent = null, - Guid opGroupId = default); - - /// - /// Sends an asynchronous to an state machine. - /// - /// The id of the target. - /// The event to send. - /// Optional id that can be used to identify this operation. - void SendEvent(StateMachineId targetId, Event e, Guid opGroupId = default); - - /// - /// Sends an to an state machine. Returns immediately if the target was already - /// running. Otherwise blocks until the target handles the event and reaches quiescense. - /// - /// The id of the target. - /// The event to send. - /// Optional id that can be used to identify this operation. - /// Task that represents the asynchronous operation. The task result is true if - /// the event was handled, false if the event was only enqueued. - Task SendEventAndExecuteAsync(StateMachineId targetId, Event e, Guid opGroupId = default); - - /// - /// Returns the operation group id of the state machine with the specified id. Returns - /// if the id is not set, or if the is not associated with this runtime. During - /// testing, the runtime asserts that the specified state machine is currently executing. - /// - /// The id of the currently executing state machine. - /// The unique identifier. - Guid GetCurrentOperationGroupId(StateMachineId currentStateMachineId); - - /// - /// Use this method to register an . - /// - /// The log writer to register. - void RegisterLog(IStateMachineRuntimeLog log); - - /// - /// Use this method to unregister a previously registered . - /// - /// The previously registered log writer to unregister. - void RemoveLog(IStateMachineRuntimeLog log); - } -} \ 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/Generator.cs b/Src/PChecker/CheckerCore/Random/Generator.cs index 358c50bc7a..aa7cbaeea9 100644 --- a/Src/PChecker/CheckerCore/Random/Generator.cs +++ b/Src/PChecker/CheckerCore/Random/Generator.cs @@ -2,7 +2,7 @@ // Licensed under the MIT License. using System.Runtime.CompilerServices; -using PChecker.Runtime; +using PChecker.SystematicTesting; namespace PChecker.Random { @@ -21,14 +21,14 @@ public class Generator /// /// The runtime associated with this random value generator. /// - internal readonly CoyoteRuntime Runtime; + internal readonly ControlledRuntime Runtime; /// /// Initializes a new instance of the class. /// private Generator() { - Runtime = CoyoteRuntime.Current; + Runtime = ControlledRuntime.Current; } /// 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..322b3daebe 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs @@ -10,6 +10,7 @@ using System.Linq; using System.Linq.Expressions; using System.Reflection; +using System.Threading; using System.Threading.Tasks; using PChecker.StateMachines; using PChecker.StateMachines.EventQueues; @@ -25,13 +26,13 @@ using PChecker.PRuntime.Values; using PChecker.Random; using PChecker.Runtime; -using PChecker.Specifications.Monitors; using PChecker.SystematicTesting.Operations; using PChecker.SystematicTesting.Strategies; using PChecker.SystematicTesting.Strategies.Liveness; using PChecker.SystematicTesting.Traces; using Debug = PChecker.IO.Debugging.Debug; using EventInfo = PChecker.StateMachines.Events.EventInfo; +using Monitor = PChecker.Specifications.Monitors.Monitor; using PMachineValue = PChecker.PRuntime.Values.PMachineValue; namespace PChecker.SystematicTesting @@ -39,14 +40,65 @@ namespace PChecker.SystematicTesting /// /// Runtime for controlling asynchronous operations. /// - internal sealed class ControlledRuntime : CoyoteRuntime, IStateMachineRuntime + public sealed class ControlledRuntime : IDisposable { + /// + /// Provides access to the runtime associated with each asynchronous control flow. + /// + /// + /// In testing mode, each testing schedule uses a unique runtime instance. To safely + /// retrieve it from static methods, we store it in each asynchronous control flow. + /// + private static readonly AsyncLocal AsyncLocalInstance = new AsyncLocal(); /// /// The currently executing runtime. /// - internal static new ControlledRuntime Current => CoyoteRuntime.Current as ControlledRuntime; + internal static new ControlledRuntime Current => AsyncLocalInstance.Value ?? + (IsExecutionControlled ? throw new InvalidOperationException(string.Format(CultureInfo.InvariantCulture, + "Uncontrolled task '{0}' invoked a runtime method. Please make sure to avoid using concurrency APIs " + + "(e.g. 'Task.Run', 'Task.Delay' or 'Task.Yield' from the 'System.Threading.Tasks' namespace) inside " + + "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); + + /// + /// If true, the program execution is controlled by the runtime to + /// explore interleavings and sources of nondeterminism, else false. + /// + internal static bool IsExecutionControlled { get; private protected set; } = false; + + /// + /// The checkerConfiguration used by the runtime. + /// + protected internal readonly CheckerConfiguration CheckerConfiguration; + /// + /// List of monitors in the program. + /// + protected readonly List Monitors; + + /// + /// Responsible for generating random values. + /// + protected readonly IRandomValueGenerator ValueGenerator; + + /// + /// Monotonically increasing operation id counter. + /// + private long OperationIdCounter; + + /// + /// Records if the runtime is running. + /// + protected internal volatile bool IsRunning; + + /// + /// Callback that is fired when the Coyote program throws an exception which includes failed assertions. + /// + public event OnFailureHandler OnFailure; + /// /// The asynchronous operation scheduler. /// @@ -94,10 +146,10 @@ internal sealed class ControlledRuntime : CoyoteRuntime, IStateMachineRuntime protected internal LogWriter LogWriter { get; private set; } /// - /// Used to log text messages. Use + /// Used to log text messages. Use /// to replace the logger with a custom one. /// - public override TextWriter Logger => LogWriter.Logger; + public TextWriter Logger => LogWriter.Logger; /// /// Used to log json trace outputs. @@ -166,8 +218,13 @@ internal int GetHashedProgramState() /// internal ControlledRuntime(CheckerConfiguration checkerConfiguration, ISchedulingStrategy strategy, IRandomValueGenerator valueGenerator) - : base(checkerConfiguration, valueGenerator) { + CheckerConfiguration = checkerConfiguration; + Monitors = new List(); + ValueGenerator = valueGenerator; + OperationIdCounter = 0; + IsRunning = true; + StateMachineMap = new ConcurrentDictionary(); LogWriter = new LogWriter(checkerConfiguration); @@ -197,7 +254,6 @@ internal ControlledRuntime(CheckerConfiguration checkerConfiguration, ISchedulin /// internal ControlledRuntime(CheckerConfiguration checkerConfiguration, IRandomValueGenerator valueGenerator) - : base(checkerConfiguration, valueGenerator) { StateMachineMap = new ConcurrentDictionary(); LogWriter = new LogWriter(checkerConfiguration); @@ -214,6 +270,11 @@ internal ControlledRuntime(CheckerConfiguration checkerConfiguration, AssignAsyncControlFlowRuntime(this); } + /// + /// Assigns the specified runtime as the default for the current asynchronous control flow. + /// + internal static void AssignAsyncControlFlowRuntime(ControlledRuntime runtime) => AsyncLocalInstance.Value = runtime; + /// /// Creates a fresh state machine id that has not yet been bound to any state machine. /// @@ -349,7 +410,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 +418,7 @@ internal void RunTest(Delegate testMethod, string testName) { action(); } - else if (testMethod is Func functionWithRuntime) + else if (testMethod is Func functionWithRuntime) { await functionWithRuntime(this); } @@ -386,6 +447,14 @@ internal void RunTest(Delegate testMethod, string testName) task.Start(); Scheduler.WaitOperationStart(op); } + + /// + /// Returns the next available unique operation id. + /// + /// Value representing the next available unique operation id. + internal ulong GetNextOperationId() => + // Atomically increments and safely wraps the value into an unsigned long. + (ulong)Interlocked.Increment(ref OperationIdCounter) - 1; /// /// Creates a new state machine of the specified and name, using the specified @@ -734,9 +803,29 @@ private void ProcessUnhandledExceptionInOperation(AsyncOperation op, Exception e Scheduler.NotifyAssertionFailure(message, killTasks: true, cancelExecution: false); } } + + /// + /// Registers a new specification monitor of the specified . + /// + public void RegisterMonitor() + where T : Monitor => + TryCreateMonitor(typeof(T)); - /// - internal override void TryCreateMonitor(Type type) + /// + /// Invokes the specified monitor with the specified . + /// + public void Monitor(Event e) + where T : Monitor + { + // If the event is null then report an error and exit. + Assert(e != null, "Cannot monitor a null event."); + Monitor(typeof(T), e, null, null, null); + } + + /// + /// Tries to create a new of the specified . + /// + internal void TryCreateMonitor(Type type) { if (Monitors.Any(m => m.GetType() == type)) { @@ -762,8 +851,10 @@ internal override void TryCreateMonitor(Type type) monitor.GotoStartState(); } - /// - internal override void Monitor(Type type, Event e, string senderName, string senderType, string senderStateName) + /// + /// Invokes the specified with the specified . + /// + internal void Monitor(Type type, Event e, string senderName, string senderType, string senderStateName) { foreach (var monitor in Monitors) { @@ -775,11 +866,13 @@ internal override void Monitor(Type type, Event e, string senderName, string sen } } - /// + /// + /// Checks if the assertion holds, and if not, throws an exception. + /// #if !DEBUG [DebuggerHidden] #endif - public override void Assert(bool predicate) + public void Assert(bool predicate) { if (!predicate) { @@ -787,11 +880,13 @@ public override void Assert(bool predicate) } } - /// + /// + /// Checks if the assertion holds, and if not, throws an exception. + /// #if !DEBUG [DebuggerHidden] #endif - public override void Assert(bool predicate, string s, object arg0) + public void Assert(bool predicate, string s, object arg0) { if (!predicate) { @@ -800,11 +895,13 @@ public override void Assert(bool predicate, string s, object arg0) } } - /// + /// + /// Checks if the assertion holds, and if not, throws an exception. + /// #if !DEBUG [DebuggerHidden] #endif - public override void Assert(bool predicate, string s, object arg0, object arg1) + public void Assert(bool predicate, string s, object arg0, object arg1) { if (!predicate) { @@ -813,11 +910,13 @@ public override void Assert(bool predicate, string s, object arg0, object arg1) } } - /// + /// + /// Checks if the assertion holds, and if not, throws an exception. + /// #if !DEBUG [DebuggerHidden] #endif - public override void Assert(bool predicate, string s, object arg0, object arg1, object arg2) + public void Assert(bool predicate, string s, object arg0, object arg1, object arg2) { if (!predicate) { @@ -826,11 +925,13 @@ public override void Assert(bool predicate, string s, object arg0, object arg1, } } - /// + /// + /// Checks if the assertion holds, and if not, throws an exception. + /// #if !DEBUG [DebuggerHidden] #endif - public override void Assert(bool predicate, string s, params object[] args) + public void Assert(bool predicate, string s, params object[] args) { if (!predicate) { @@ -889,9 +990,19 @@ internal void CheckNoMonitorInHotStateAtTermination() } } } + + /// + /// Returns a nondeterministic boolean choice, that can be controlled + /// during analysis or testing. + /// + public bool RandomBoolean() => GetNondeterministicBooleanChoice(2, null, null); - /// - internal override bool GetNondeterministicBooleanChoice(int maxValue, string callerName, string callerType) + /// + /// Returns a nondeterministic boolean choice, that can be controlled + /// during analysis or testing. The value is used to generate a number + /// in the range [0..maxValue), where 0 triggers true. + /// + internal bool GetNondeterministicBooleanChoice(int maxValue, string callerName, string callerType) { var caller = Scheduler.GetExecutingOperation()?.StateMachine; if (caller != null) @@ -904,8 +1015,12 @@ internal override bool GetNondeterministicBooleanChoice(int maxValue, string cal return choice; } - /// - internal override int GetNondeterministicIntegerChoice(int maxValue, string callerName, string callerType) + /// + /// Returns a nondeterministic integer, that can be controlled during + /// analysis or testing. The value is used to generate an integer in + /// the range [0..maxValue). + /// + internal int GetNondeterministicIntegerChoice(int maxValue, string callerName, string callerType) { var caller = Scheduler.GetExecutingOperation()?.StateMachine; if (caller != null) @@ -1189,7 +1304,7 @@ internal void NotifyMonitorError(Monitor monitor) internal void TryHandleDroppedEvent(Event e, StateMachineId id) => OnEventDropped?.Invoke(e, id); /// - public override TextWriter SetLogger(TextWriter logger) => LogWriter.SetLogger(logger); + public TextWriter SetLogger(TextWriter logger) => LogWriter.SetLogger(logger); /// /// Sets the JsonLogger in LogWriter.cs @@ -1326,9 +1441,12 @@ internal int GetProgramState() } } - /// + /// + /// Throws an exception + /// containing the specified exception. + /// [DebuggerStepThrough] - internal override void WrapAndThrowException(Exception exception, string s, params object[] args) + internal void WrapAndThrowException(Exception exception, string s, params object[] args) { var msg = string.Format(CultureInfo.InvariantCulture, s, args); var message = string.Format(CultureInfo.InvariantCulture, @@ -1349,9 +1467,16 @@ internal async Task WaitAsync() await Scheduler.WaitAsync(); IsRunning = false; } + + /// + /// Terminates the runtime and notifies each active state machine to halt execution. + /// + public void Stop() => IsRunning = false; - /// - protected internal override void RaiseOnFailureEvent(Exception exception) + /// + /// Raises the event with the specified . + /// + protected internal void RaiseOnFailureEvent(Exception exception) { if (exception is ExecutionCanceledException || (exception is ActionExceptionFilterException ae && ae.InnerException is ExecutionCanceledException)) @@ -1360,12 +1485,14 @@ protected internal override void RaiseOnFailureEvent(Exception exception) return; } - base.RaiseOnFailureEvent(exception); + OnFailure?.Invoke(exception); } - /// + /// + /// Disposes runtime resources. + /// [DebuggerStepThrough] - protected override void Dispose(bool disposing) + protected void Dispose(bool disposing) { if (disposing) { @@ -1373,7 +1500,20 @@ protected override void Dispose(bool disposing) StateMachineMap.Clear(); } - base.Dispose(disposing); + if (disposing) + { + OperationIdCounter = 0; + } + } + + /// + /// Disposes runtime resources. + /// + [DebuggerStepThrough] + public void Dispose() + { + Dispose(true); + GC.SuppressFinalize(this); } } } \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TaskController.cs b/Src/PChecker/CheckerCore/SystematicTesting/TaskController.cs index 7869bfb6f0..c09e99ead6 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TaskController.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TaskController.cs @@ -58,7 +58,7 @@ public Task ScheduleAction(Action action, System.Threading.Tasks.Task predecesso { // Update the current asynchronous control flow with the current runtime instance, // allowing future retrieval in the same asynchronous call stack. - CoyoteRuntime.AssignAsyncControlFlowRuntime(Runtime); + ControlledRuntime.AssignAsyncControlFlowRuntime(Runtime); OperationScheduler.StartOperation(op); if (predecessor != null) @@ -118,7 +118,7 @@ public Task ScheduleFunction(Func function, System.Threading.Tasks.Task pr { // Update the current asynchronous control flow with the current runtime instance, // allowing future retrieval in the same asynchronous call stack. - CoyoteRuntime.AssignAsyncControlFlowRuntime(Runtime); + ControlledRuntime.AssignAsyncControlFlowRuntime(Runtime); OperationScheduler.StartOperation(op); if (predecessor != null) @@ -177,7 +177,7 @@ public Tasks.Task ScheduleFunction(Func> f { // Update the current asynchronous control flow with the current runtime instance, // allowing future retrieval in the same asynchronous call stack. - CoyoteRuntime.AssignAsyncControlFlowRuntime(Runtime); + ControlledRuntime.AssignAsyncControlFlowRuntime(Runtime); OperationScheduler.StartOperation(op); if (predecessor != null) @@ -235,7 +235,7 @@ public Tasks.Task ScheduleDelegate(Delegate work, System.Threa { // Update the current asynchronous control flow with the current runtime instance, // allowing future retrieval in the same asynchronous call stack. - CoyoteRuntime.AssignAsyncControlFlowRuntime(Runtime); + ControlledRuntime.AssignAsyncControlFlowRuntime(Runtime); OperationScheduler.StartOperation(op); if (predecessor != null) diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestMethodInfo.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestMethodInfo.cs index 0a7e1e6cbb..1868ac8ba7 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TestMethodInfo.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TestMethodInfo.cs @@ -164,8 +164,8 @@ 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 hasTaskInputParameters = testParams.Length is 1 && testParams[0].ParameterType == typeof(ICoyoteRuntime); + var hasStateMachineInputParameters = testParams.Length is 1 && testParams[0].ParameterType == typeof(ControlledRuntime); + var hasTaskInputParameters = testParams.Length is 1 && testParams[0].ParameterType == typeof(ControlledRuntime); if (!((hasVoidReturnType || hasAsyncReturnType) && (hasNoInputParameters || hasStateMachineInputParameters || hasTaskInputParameters) && !testMethod.IsAbstract && !testMethod.IsVirtual && !testMethod.IsConstructor && @@ -176,15 +176,15 @@ private static (Delegate testMethod, string testName) GetTestMethod(Assembly ass $" [{typeof(TestAttribute).FullName}]\n" + $" public static void {testMethod.Name}() {{ ... }}\n\n" + $" [{typeof(TestAttribute).FullName}]\n" + - $" public static void {testMethod.Name}(ICoyoteRuntime runtime) {{ ... }}\n\n" + + $" public static void {testMethod.Name}(ControlledRuntime 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" + + $" public static async {typeof(Task).FullName} {testMethod.Name}(ControlledRuntime 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,11 +192,11 @@ 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) { - test = Delegate.CreateDelegate(typeof(Func), testMethod); + test = Delegate.CreateDelegate(typeof(Func), testMethod); } else { @@ -207,11 +207,11 @@ 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) { - test = Delegate.CreateDelegate(typeof(Action), testMethod); + test = Delegate.CreateDelegate(typeof(Action), testMethod); } else { diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs index a18300000a..e4ff17006a 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs @@ -213,17 +213,11 @@ public static TestingEngine Create(CheckerConfiguration checkerConfiguration, As /// public static TestingEngine Create(CheckerConfiguration checkerConfiguration, Action test) => new TestingEngine(checkerConfiguration, test); - - /// - /// Creates a new systematic testing engine. - /// - public static TestingEngine Create(CheckerConfiguration checkerConfiguration, Action test) => - new TestingEngine(checkerConfiguration, test); - + /// /// 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); /// @@ -235,13 +229,7 @@ public static TestingEngine Create(CheckerConfiguration checkerConfiguration, Fu /// /// Creates a new systematic testing engine. /// - public static TestingEngine Create(CheckerConfiguration checkerConfiguration, Func test) => - new TestingEngine(checkerConfiguration, test); - - /// - /// 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/PChecker/CheckerCore/Tasks/AsyncTaskMethodBuilder.cs b/Src/PChecker/CheckerCore/Tasks/AsyncTaskMethodBuilder.cs index ca915b4daa..d9fa104de9 100644 --- a/Src/PChecker/CheckerCore/Tasks/AsyncTaskMethodBuilder.cs +++ b/Src/PChecker/CheckerCore/Tasks/AsyncTaskMethodBuilder.cs @@ -85,7 +85,7 @@ private AsyncTaskMethodBuilder(TaskController taskManager) [DebuggerHidden] public static AsyncTaskMethodBuilder Create() { - if (CoyoteRuntime.IsExecutionControlled) + if (ControlledRuntime.IsExecutionControlled) { return new AsyncTaskMethodBuilder(ControlledRuntime.Current.TaskController); } @@ -245,7 +245,7 @@ private AsyncTaskMethodBuilder(TaskController taskManager) [DebuggerHidden] public static AsyncTaskMethodBuilder Create() { - if (CoyoteRuntime.IsExecutionControlled) + if (ControlledRuntime.IsExecutionControlled) { return new AsyncTaskMethodBuilder(ControlledRuntime.Current.TaskController); } diff --git a/Src/PChecker/CheckerCore/Tasks/Task.cs b/Src/PChecker/CheckerCore/Tasks/Task.cs index 261b063ab5..7d9ab2b9f4 100644 --- a/Src/PChecker/CheckerCore/Tasks/Task.cs +++ b/Src/PChecker/CheckerCore/Tasks/Task.cs @@ -165,7 +165,7 @@ public static Task FromException(Exception exception) => [MethodImpl(MethodImplOptions.AggressiveInlining)] public static Task Run(Action action, CancellationToken cancellationToken) { - if (CoyoteRuntime.IsExecutionControlled) + if (ControlledRuntime.IsExecutionControlled) { return ControlledRuntime.Current.TaskController.ScheduleAction(action, null, cancellationToken); } @@ -193,7 +193,7 @@ public static Task Run(Action action, CancellationToken cancellationToken) [MethodImpl(MethodImplOptions.AggressiveInlining)] public static Task Run(Func function, CancellationToken cancellationToken) { - if (CoyoteRuntime.IsExecutionControlled) + if (ControlledRuntime.IsExecutionControlled) { return ControlledRuntime.Current.TaskController.ScheduleFunction(function, null, cancellationToken); } @@ -223,7 +223,7 @@ public static Task Run(Func function, CancellationToken cancellationToken) [MethodImpl(MethodImplOptions.AggressiveInlining)] public static Task Run(Func> function, CancellationToken cancellationToken) { - if (CoyoteRuntime.IsExecutionControlled) + if (ControlledRuntime.IsExecutionControlled) { return ControlledRuntime.Current.TaskController.ScheduleFunction(function, null, cancellationToken); } @@ -252,7 +252,7 @@ public static Task Run(Func> function, Cancellat [MethodImpl(MethodImplOptions.AggressiveInlining)] public static Task Run(Func function, CancellationToken cancellationToken) { - if (CoyoteRuntime.IsExecutionControlled) + if (ControlledRuntime.IsExecutionControlled) { return ControlledRuntime.Current.TaskController.ScheduleDelegate(function, null, cancellationToken); } @@ -281,7 +281,7 @@ public static Task Run(Func function, CancellationTok [MethodImpl(MethodImplOptions.AggressiveInlining)] public static Task Delay(int millisecondsDelay, CancellationToken cancellationToken) { - if (CoyoteRuntime.IsExecutionControlled) + if (ControlledRuntime.IsExecutionControlled) { return ControlledRuntime.Current.TaskController.ScheduleDelay(TimeSpan.FromMilliseconds(millisecondsDelay), cancellationToken); } @@ -312,7 +312,7 @@ public static Task Delay(int millisecondsDelay, CancellationToken cancellationTo [MethodImpl(MethodImplOptions.AggressiveInlining)] public static Task Delay(TimeSpan delay, CancellationToken cancellationToken) { - if (CoyoteRuntime.IsExecutionControlled) + if (ControlledRuntime.IsExecutionControlled) { return ControlledRuntime.Current.TaskController.ScheduleDelay(delay, cancellationToken); } @@ -347,7 +347,7 @@ public static Task Delay(TimeSpan delay, CancellationToken cancellationToken) [MethodImpl(MethodImplOptions.AggressiveInlining)] private static Task WhenAllTasksCompleteAsync(IEnumerable tasks) { - if (CoyoteRuntime.IsExecutionControlled) + if (ControlledRuntime.IsExecutionControlled) { return ControlledRuntime.Current.TaskController.WhenAllTasksCompleteAsync(tasks); } @@ -385,7 +385,7 @@ private static Task WhenAllTasksCompleteAsync(IEnumerable tasks) [MethodImpl(MethodImplOptions.AggressiveInlining)] private static Task WhenAllTasksCompleteAsync(IEnumerable> tasks) { - if (CoyoteRuntime.IsExecutionControlled) + if (ControlledRuntime.IsExecutionControlled) { return ControlledRuntime.Current.TaskController.WhenAllTasksCompleteAsync(tasks); } @@ -417,7 +417,7 @@ private static Task WhenAllTasksCompleteAsync(IEnumerable WhenAnyTaskCompletesAsync(IEnumerable tasks) { - if (CoyoteRuntime.IsExecutionControlled) + if (ControlledRuntime.IsExecutionControlled) { return ControlledRuntime.Current.TaskController.WhenAnyTaskCompletesAsync(tasks); } @@ -462,7 +462,7 @@ public static Task> WhenAny(IEnumerable> ta [MethodImpl(MethodImplOptions.AggressiveInlining)] public static Task> WhenAnyTaskCompletesAsync(IEnumerable> tasks) { - if (CoyoteRuntime.IsExecutionControlled) + if (ControlledRuntime.IsExecutionControlled) { return ControlledRuntime.Current.TaskController.WhenAnyTaskCompletesAsync(tasks); } @@ -542,7 +542,7 @@ public static void WaitAll(Task[] tasks, CancellationToken cancellationToken) => [MethodImpl(MethodImplOptions.AggressiveInlining)] public static bool WaitAll(Task[] tasks, int millisecondsTimeout, CancellationToken cancellationToken) { - if (CoyoteRuntime.IsExecutionControlled) + if (ControlledRuntime.IsExecutionControlled) { return ControlledRuntime.Current.TaskController.WaitAllTasksComplete(tasks); } @@ -612,7 +612,7 @@ public static int WaitAny(Task[] tasks, TimeSpan timeout) [MethodImpl(MethodImplOptions.AggressiveInlining)] public static int WaitAny(Task[] tasks, int millisecondsTimeout, CancellationToken cancellationToken) { - if (CoyoteRuntime.IsExecutionControlled) + if (ControlledRuntime.IsExecutionControlled) { return ControlledRuntime.Current.TaskController.WaitAnyTaskCompletes(tasks); } @@ -626,7 +626,7 @@ public static int WaitAny(Task[] tasks, int millisecondsTimeout, CancellationTok [MethodImpl(MethodImplOptions.AggressiveInlining)] public static YieldAwaitable Yield() { - if (CoyoteRuntime.IsExecutionControlled) + if (ControlledRuntime.IsExecutionControlled) { return new YieldAwaitable(ControlledRuntime.Current.TaskController); } @@ -719,7 +719,7 @@ public ConfiguredTaskAwaitable ConfigureAwait(bool continueOnCapturedContext) => [MethodImpl(MethodImplOptions.AggressiveInlining)] public static void ExploreContextSwitch() { - if (CoyoteRuntime.IsExecutionControlled) + if (ControlledRuntime.IsExecutionControlled) { ControlledRuntime.Current.ScheduleNextOperation(AsyncOperationType.Default); } diff --git a/Src/PChecker/CheckerCore/Tasks/TaskCompletionSource.cs b/Src/PChecker/CheckerCore/Tasks/TaskCompletionSource.cs index 2a109f05ca..b7bf8d3a14 100644 --- a/Src/PChecker/CheckerCore/Tasks/TaskCompletionSource.cs +++ b/Src/PChecker/CheckerCore/Tasks/TaskCompletionSource.cs @@ -22,7 +22,7 @@ public static class TaskCompletionSource /// /// The type of the result value assocatied with this task completion source. /// The task completion source. - public static TaskCompletionSource Create() => CoyoteRuntime.IsExecutionControlled ? + public static TaskCompletionSource Create() => ControlledRuntime.IsExecutionControlled ? new Mock() : new TaskCompletionSource(new System.Threading.Tasks.TaskCompletionSource()); /// 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) From 39411b7e74b9b4940b0132c269d3efef9a0ac138 Mon Sep 17 00:00:00 2001 From: Christine Zhou Date: Mon, 9 Sep 2024 16:38:30 -0700 Subject: [PATCH 3/3] [Cleanup] Fixing monitor Raise statement + unit tests --- .../Runtime}/ControlledRuntime.cs | 0 .../PRuntime/Specifications/Monitor.cs | 8 +++++ ...xhaustiveSearch.cs => ExhaustiveEngine.cs} | 0 .../Feature2Stmts/Correct/goto4/goto4.p | 33 +++++++++++++++++++ .../Feature2Stmts/Correct/raise3/raise3.p | 32 ++++++++++++++++++ .../Feature2Stmts/DynamicError/goto4/goto4.p | 33 +++++++++++++++++++ .../DynamicError/raise3/raise3.p | 32 ++++++++++++++++++ 7 files changed, 138 insertions(+) rename Src/PChecker/CheckerCore/{SystematicTesting => PRuntime/Runtime}/ControlledRuntime.cs (100%) rename Src/PChecker/CheckerCore/SystematicTesting/{ExhaustiveSearch.cs => ExhaustiveEngine.cs} (100%) create mode 100644 Tst/RegressionTests/Feature2Stmts/Correct/goto4/goto4.p create mode 100644 Tst/RegressionTests/Feature2Stmts/Correct/raise3/raise3.p create mode 100644 Tst/RegressionTests/Feature2Stmts/DynamicError/goto4/goto4.p create mode 100644 Tst/RegressionTests/Feature2Stmts/DynamicError/raise3/raise3.p diff --git a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs b/Src/PChecker/CheckerCore/PRuntime/Runtime/ControlledRuntime.cs similarity index 100% rename from Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs rename to Src/PChecker/CheckerCore/PRuntime/Runtime/ControlledRuntime.cs diff --git a/Src/PChecker/CheckerCore/PRuntime/Specifications/Monitor.cs b/Src/PChecker/CheckerCore/PRuntime/Specifications/Monitor.cs index 7c81cd433f..2aeb515c85 100644 --- a/Src/PChecker/CheckerCore/PRuntime/Specifications/Monitor.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Specifications/Monitor.cs @@ -16,6 +16,7 @@ using PChecker.StateMachines.Logging; using PChecker.StateMachines.StateTransitions; using PChecker.Exceptions; +using PChecker.PRuntime.Exceptions; using PChecker.SystematicTesting; namespace PChecker.Specifications.Monitors @@ -204,6 +205,7 @@ public void RaiseEvent(Event e) Assert(e != null, "{0} is raising a null event.", GetType().FullName); CheckDanglingTransition(); PendingTransition = new Transition(Transition.Type.Raise, default, e); + throw new PNonStandardReturnException { ReturnKind = NonStandardReturn.Raise }; } /// @@ -250,6 +252,7 @@ public void RaiseGotoStateEvent(object payload = null) where S : State { gotoPayload = payload; RaiseGotoStateEvent(typeof(S)); + throw new PNonStandardReturnException { ReturnKind = NonStandardReturn.Goto }; } /// @@ -493,6 +496,11 @@ private void ExecuteAction(CachedDelegate cachedAction, Event e) innerException = innerException.InnerException; } + if (innerException is PNonStandardReturnException) + { + return; + } + if (innerException is AggregateException) { innerException = innerException.InnerException; diff --git a/Src/PChecker/CheckerCore/SystematicTesting/ExhaustiveSearch.cs b/Src/PChecker/CheckerCore/SystematicTesting/ExhaustiveEngine.cs similarity index 100% rename from Src/PChecker/CheckerCore/SystematicTesting/ExhaustiveSearch.cs rename to Src/PChecker/CheckerCore/SystematicTesting/ExhaustiveEngine.cs diff --git a/Tst/RegressionTests/Feature2Stmts/Correct/goto4/goto4.p b/Tst/RegressionTests/Feature2Stmts/Correct/goto4/goto4.p new file mode 100644 index 0000000000..054ea467d3 --- /dev/null +++ b/Tst/RegressionTests/Feature2Stmts/Correct/goto4/goto4.p @@ -0,0 +1,33 @@ +/******************** + * This example tests raise with payload on monitor + * ******************/ + + event E1; + + machine Main { + start state Init { + entry { + send this, E1; + } + on E1 do { + } + } +} + spec M observes E1 { + start state Init { + on E1 do { + testFunc(); + assert false; + } + } + state S { + entry (payload: int) { + assert (payload == 1000), format ("Expected payload to be 1000, actual payload is {0}", payload); + } + } + fun testFunc() { + goto S, 1000; + } +} + +test DefaultImpl [main=Main]: assert M in { Main }; \ No newline at end of file diff --git a/Tst/RegressionTests/Feature2Stmts/Correct/raise3/raise3.p b/Tst/RegressionTests/Feature2Stmts/Correct/raise3/raise3.p new file mode 100644 index 0000000000..9846dcbc22 --- /dev/null +++ b/Tst/RegressionTests/Feature2Stmts/Correct/raise3/raise3.p @@ -0,0 +1,32 @@ +/******************** + * This example tests raise with payload on monitor + * ******************/ + + event E1; + event E2: int; + + machine Main { + start state Init { + entry { + send this, E1; + } + on E1 do { + } + } +} + spec M observes E1, E2 { + start state Init { + on E1 do { + testFunc(); + assert false; + } + on E2 do (payload: int) { + assert (payload == 1000), format ("Expected payload to be 1000, actual payload is {0}", payload); + } + } + fun testFunc() { + raise E2, 1000; + } +} + +test DefaultImpl [main=Main]: assert M in { Main }; \ No newline at end of file diff --git a/Tst/RegressionTests/Feature2Stmts/DynamicError/goto4/goto4.p b/Tst/RegressionTests/Feature2Stmts/DynamicError/goto4/goto4.p new file mode 100644 index 0000000000..a407985420 --- /dev/null +++ b/Tst/RegressionTests/Feature2Stmts/DynamicError/goto4/goto4.p @@ -0,0 +1,33 @@ +/******************** + * This example tests raise with payload on monitor + * ******************/ + + event E1; + + machine Main { + start state Init { + entry { + send this, E1; + } + on E1 do { + } + } +} + spec M observes E1 { + start state Init { + on E1 do { + testFunc(); + assert false; + } + } + state S { + entry (payload: int) { + assert (payload != 1000), format ("Expected payload to be 1000, actual payload is {0}", payload); + } + } + fun testFunc() { + goto S, 1000; + } +} + +test DefaultImpl [main=Main]: assert M in { Main }; \ No newline at end of file diff --git a/Tst/RegressionTests/Feature2Stmts/DynamicError/raise3/raise3.p b/Tst/RegressionTests/Feature2Stmts/DynamicError/raise3/raise3.p new file mode 100644 index 0000000000..712da9b7d3 --- /dev/null +++ b/Tst/RegressionTests/Feature2Stmts/DynamicError/raise3/raise3.p @@ -0,0 +1,32 @@ +/******************** + * This example tests raise with payload on monitor + * ******************/ + + event E1; + event E2: int; + + machine Main { + start state Init { + entry { + send this, E1; + } + on E1 do { + } + } +} + spec M observes E1, E2 { + start state Init { + on E1 do { + testFunc(); + assert false; + } + on E2 do (payload: int) { + assert (payload != 1000), format ("Expected payload to be 1000, actual payload is {0}", payload); + } + } + fun testFunc() { + raise E2, 1000; + } +} + +test DefaultImpl [main=Main]: assert M in { Main }; \ No newline at end of file