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