From c68f93f1ece510495909d4924134e0e0bf91e2c1 Mon Sep 17 00:00:00 2001 From: Ankush Desai Date: Wed, 28 Feb 2024 11:47:43 -0800 Subject: [PATCH 001/185] Removed the C backend completely in the P 2.1 --- Src/PChecker/CheckerCore/Actors/Actor.cs | 6 +- .../CheckerCore/Actors/ActorFactory.cs | 2 +- Src/PChecker/CheckerCore/Actors/ActorId.cs | 2 +- .../CheckerCore/Actors/ActorRuntime.cs | 2 +- .../Actors/EventQueues/DequeueStatus.cs | 2 +- .../Actors/EventQueues/EnqueueStatus.cs | 2 +- .../Actors/EventQueues/EventQueue.cs | 2 +- .../Actors/EventQueues/IEventQueue.cs | 2 +- .../EventQueues/Mocks/MockEventQueue.cs | 2 +- .../CheckerCore/Actors/Events/DefaultEvent.cs | 2 +- .../CheckerCore/Actors/Events/Event.cs | 2 +- .../CheckerCore/Actors/Events/EventInfo.cs | 2 +- .../Actors/Events/EventOriginInfo.cs | 2 +- .../Actors/Events/GotoStateEvent.cs | 2 +- .../CheckerCore/Actors/Events/HaltEvent.cs | 2 +- .../Actors/Events/QuiescentEvent.cs | 2 +- .../Actors/Events/WildcardEvent.cs | 2 +- .../ActionExceptionFilterException.cs | 2 +- .../Exceptions/OnEventDroppedHandler.cs | 2 +- .../Actors/Exceptions/OnExceptionOutcome.cs | 2 +- .../Exceptions/UnhandledEventException.cs | 2 +- .../Handlers/ActionEventHandlerDeclaration.cs | 2 +- .../Actors/Handlers/CachedDelegate.cs | 2 +- .../Handlers/DeferEventHandlerDeclaration.cs | 2 +- .../Handlers/EventHandlerDeclaration.cs | 2 +- .../Handlers/IgnoreEventHandlerDeclaration.cs | 2 +- .../CheckerCore/Actors/IActorRuntime.cs | 2 +- .../Logging/ActorRuntimeLogTextFormatter.cs | 2 +- .../Logging/ActorRuntimeLogXmlFormatter.cs | 2 +- .../Actors/Logging/IActorRuntimeLog.cs | 2 +- .../CheckerCore/Actors/Logging/JsonWriter.cs | 4 +- .../CheckerCore/Actors/Logging/LogWriter.cs | 2 +- .../Actors/Managers/ActorManager.cs | 2 +- .../Actors/Managers/IActorManager.cs | 2 +- .../Actors/Managers/Mocks/MockActorManager.cs | 2 +- .../Managers/Mocks/MockStateMachineManager.cs | 2 +- .../Actors/Managers/StateMachineManager.cs | 2 +- .../CheckerCore/Actors/NameResolver.cs | 2 +- .../CheckerCore/Actors/RuntimeFactory.cs | 2 +- .../CheckerCore/Actors/SendOptions.cs | 2 +- .../CheckerCore/Actors/StateMachine.cs | 22 +- .../StateTransitions/GotoStateTransition.cs | 2 +- .../StateTransitions/PushStateTransition.cs | 2 +- .../Actors/UnitTesting/ActorTestKit.cs | 4 +- .../UnitTesting/ActorUnitTestingRuntime.cs | 2 +- .../CheckerCore/CheckerConfiguration.cs | 3 +- .../Coverage/ActivityCoverageReporter.cs | 2 +- .../Coverage/ActorRuntimeLogEventCoverage.cs | 2 +- .../Coverage/ActorRuntimeLogGraphBuilder.cs | 4 +- .../CheckerCore/Coverage/CoverageInfo.cs | 2 +- .../Exceptions/AssertionFailureException.cs | 2 +- .../Exceptions/ExecutionCanceledException.cs | 2 +- .../Exceptions/RuntimeException.cs | 2 +- .../ExhaustiveSearch/ExhaustiveSearch.cs | 8 +- .../CheckerCore/IO/Debugging/Debug.cs | 2 +- .../CheckerCore/IO/Debugging/Error.cs | 2 +- Src/PChecker/CheckerCore/IO/ErrorReporter.cs | 2 +- .../CheckerCore/IO/Logging/ConsoleLogger.cs | 2 +- .../CheckerCore/IO/Logging/InMemoryLogger.cs | 2 +- .../Monitoring/CodeCoverageMonitor.cs | 2 +- Src/PChecker/CheckerCore/Random/Generator.cs | 2 +- .../Random/IRandomValueGenerator.cs | 2 +- .../Random/RandomValueGenerator.cs | 2 +- .../CheckerCore/Runtime/CoyoteRuntime.cs | 16 +- .../CheckerCore/Runtime/ICoyoteRuntime.cs | 2 +- .../CheckerCore/Runtime/OnFailureHandler.cs | 2 +- .../CheckerCore/Runtime/RuntimeFactory.cs | 2 +- .../Scheduling/TestingProcessScheduler.cs | 2 +- .../Specifications/Monitors/CachedDelegate.cs | 2 +- .../Specifications/Monitors/Monitor.cs | 35 +- .../Specifications/Specification.cs | 2 +- .../SystematicTesting/ControlledRuntime.cs | 7 +- .../SystematicTesting/OperationScheduler.cs | 19 +- .../Operations/ActorOperation.cs | 2 +- .../Operations/AsyncOperation.cs | 2 +- .../Operations/AsyncOperationStatus.cs | 2 +- .../Operations/AsyncOperationType.cs | 2 +- .../Operations/IAsyncOperation.cs | 2 +- .../Operations/TaskOperation.cs | 2 +- .../CheckerCore/SystematicTesting/Resource.cs | 2 +- .../Strategies/Exhaustive/DFSStrategy.cs | 2 +- .../Strategies/ISchedulingStrategy.cs | 2 +- .../Liveness/LivenessCheckingStrategy.cs | 2 +- .../Liveness/TemperatureCheckingStrategy.cs | 2 +- .../Strategies/Probabilistic/PCTStrategy.cs | 6 +- .../ProbabilisticRandomStrategy.cs | 2 +- .../Probabilistic/QLearningStrategy.cs | 7 +- .../Probabilistic/RandomStrategy.cs | 2 +- .../Strategies/Special/ComboStrategy.cs | 2 +- .../Strategies/Special/ReplayStrategy.cs | 2 +- .../SystematicTesting/TaskController.cs | 102 +- .../SystematicTesting/TestAttributes.cs | 2 +- .../SystematicTesting/TestMethodInfo.cs | 48 +- .../SystematicTesting/TestReport.cs | 7 +- .../SystematicTesting/TestingEngine.cs | 32 +- .../SystematicTesting/Traces/ScheduleStep.cs | 2 +- .../Traces/ScheduleStepType.cs | 2 +- .../SystematicTesting/Traces/ScheduleTrace.cs | 2 +- .../Tasks/AsyncTaskMethodBuilder.cs | 36 +- .../Tasks/ConfiguredTaskAwaitable.cs | 12 +- .../CheckerCore/Tasks/Locks/AsyncLock.cs | 2 +- .../CheckerCore/Tasks/Locks/Semaphore.cs | 2 +- Src/PChecker/CheckerCore/Tasks/Task.cs | 2 +- Src/PChecker/CheckerCore/Tasks/TaskAwaiter.cs | 12 +- .../CheckerCore/Tasks/TaskCompletionSource.cs | 4 +- .../CheckerCore/Tasks/TaskExtensions.cs | 2 +- .../CheckerCore/Tasks/YieldAwaitable.cs | 8 +- .../CheckerCore/Testing/TestingPortfolio.cs | 2 +- .../CheckerCore/Testing/TestingProcess.cs | 4 +- .../Testing/TestingProcessFactory.cs | 6 +- .../CheckerCore/Utilities/ExitCode.cs | 2 +- .../CheckerCore/Utilities/Profiler.cs | 2 +- .../CheckerCore/Utilities/Reporter.cs | 6 +- .../CompilerCore/Backend/C/CCodeGenerator.cs | 1807 ----------------- .../CompilerCore/Backend/C/CNameManager.cs | 228 --- .../Backend/C/CTranslationUtils.cs | 148 -- .../Backend/C/CompilationContext.cs | 137 -- .../Backend/C/ValueInternmentManager.cs | 46 - .../Backend/CSharp/CSharpCodeGenerator.cs | 70 +- .../Backend/CSharp/CSharpNameManager.cs | 8 +- .../CompilerCore/Backend/CSharp/Constants.cs | 2 +- .../CompilerCore/Backend/ICodeGenerator.cs | 2 +- .../CompilerCore/Backend/IRTransformer.cs | 16 +- .../Backend/Java/CompilationContext.cs | 2 +- .../CompilerCore/Backend/Java/Constants.cs | 2 +- .../Backend/Java/EventGenerator.cs | 2 +- .../Backend/Java/FFIStubGenerator.cs | 2 +- .../CompilerCore/Backend/Java/JavaCompiler.cs | 2 +- .../Backend/Java/JavaSourceGenerator.cs | 2 +- .../Backend/Java/MachineGenerator.cs | 8 +- .../CompilerCore/Backend/Java/NameManager.cs | 2 +- .../CompilerCore/Backend/Java/TypeManager.cs | 98 +- .../Backend/Java/TypesGenerator.cs | 2 +- .../Backend/Stately/StatelyCodeGenerator.cs | 3 +- .../Backend/Symbolic/CompilationContext.cs | 2 +- .../Backend/Symbolic/Constants.cs | 2 +- .../Backend/Symbolic/Continuation.cs | 2 +- .../Backend/Symbolic/ReceiveSplitStmt.cs | 2 +- .../Backend/Symbolic/SymbolicCodeGenerator.cs | 337 ++- .../Backend/Symbolic/TransformASTPass.cs | 1210 +++++------ .../Backend/Symbolic/WhileFunction.cs | 2 +- .../CompilerCore/Backend/TargetLanguage.cs | 4 +- Src/PCompiler/CompilerCore/Compiler.cs | 2 +- Src/PCompiler/CompilerCore/CompilerOutput.cs | 2 +- .../TypeChecker/AST/Declarations/Function.cs | 2 +- .../TypeChecker/AST/Expressions/BinOpType.cs | 2 +- .../CompilerCore/TypeChecker/Analyzer.cs | 2 +- .../TypeChecker/DeclarationVisitor.cs | 2 +- .../CompilerCore/TypeChecker/ExprVisitor.cs | 72 +- .../TypeChecker/MachineChecker.cs | 17 +- .../TypeChecker/ModuleSystemTypeChecker.cs | 84 +- .../TypeChecker/Types/NamedTupleType.cs | 10 +- .../TypeChecker/Types/TupleType.cs | 2 +- .../PCommandLine/Options/PCheckerOptions.cs | 66 +- .../PCommandLine/Options/PCompilerOptions.cs | 37 +- .../Parser/CommandLineArgumentParser.cs | 2 +- .../PCommandLine/Parser/ParsePProjectFile.cs | 3 +- .../UnknownNamedTupleFieldAccess.cs | 2 +- .../PCSharpRuntime/PJsonFormatter.cs | 3 +- Src/PRuntimes/PCSharpRuntime/PLogFormatter.cs | 2 +- Src/PRuntimes/PCSharpRuntime/PMachine.cs | 16 +- .../PCSharpRuntime/Values/IPrtValue.cs | 3 +- Src/PRuntimes/PCSharpRuntime/Values/PrtMap.cs | 2 +- Src/PRuntimes/PCSharpRuntime/Values/PrtSeq.cs | 2 +- Src/PRuntimes/PCSharpRuntime/Values/PrtSet.cs | 2 +- .../PCSharpRuntime/Values/PrtString.cs | 3 +- .../PCSharpRuntime/Values/PrtTuple.cs | 2 +- Tst/UnitTests/CSharpBackendTests.cs | 4 +- Tst/UnitTests/Core/TestCaseFactory.cs | 2 +- Tst/UnitTests/Core/TestCaseLoader.cs | 10 +- Tst/UnitTests/RegressionTests.cs | 4 +- Tst/UnitTests/Runners/CompileOnlyRunner.cs | 2 +- Tst/UnitTests/Runners/PCheckerRunner.cs | 3 +- Tst/UnitTests/TestAssertions.cs | 4 +- Tst/UnitTests/TypeCheckingUtilsTest.cs | 37 +- global.json | 7 + 176 files changed, 1380 insertions(+), 3779 deletions(-) delete mode 100644 Src/PCompiler/CompilerCore/Backend/C/CCodeGenerator.cs delete mode 100644 Src/PCompiler/CompilerCore/Backend/C/CNameManager.cs delete mode 100644 Src/PCompiler/CompilerCore/Backend/C/CTranslationUtils.cs delete mode 100644 Src/PCompiler/CompilerCore/Backend/C/CompilationContext.cs delete mode 100644 Src/PCompiler/CompilerCore/Backend/C/ValueInternmentManager.cs create mode 100644 global.json diff --git a/Src/PChecker/CheckerCore/Actors/Actor.cs b/Src/PChecker/CheckerCore/Actors/Actor.cs index be36535572..03b77089c1 100644 --- a/Src/PChecker/CheckerCore/Actors/Actor.cs +++ b/Src/PChecker/CheckerCore/Actors/Actor.cs @@ -14,8 +14,8 @@ using PChecker.Actors.Events; using PChecker.Actors.Exceptions; using PChecker.Actors.Handlers; -using PChecker.Actors.Managers; using PChecker.Actors.Logging; +using PChecker.Actors.Managers; using PChecker.Exceptions; using PChecker.IO.Debugging; using EventInfo = PChecker.Actors.Events.EventInfo; @@ -789,7 +789,7 @@ private void AssertActionValidity(MethodInfo action) var actionType = action.DeclaringType; var parameters = action.GetParameters(); Assert(parameters.Length is 0 || - (parameters.Length is 1 && parameters[0].ParameterType == typeof(Event)), + (parameters.Length is 1 && parameters[0].ParameterType == typeof(Event)), "Action '{0}' in '{1}' must either accept no parameters or a single parameter of type 'Event'.", action.Name, actionType.Name); @@ -1003,4 +1003,4 @@ public OnEventDoActionAttribute(Type eventType, string actionName) } } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/ActorFactory.cs b/Src/PChecker/CheckerCore/Actors/ActorFactory.cs index 4f3494e820..7f6929b45f 100644 --- a/Src/PChecker/CheckerCore/Actors/ActorFactory.cs +++ b/Src/PChecker/CheckerCore/Actors/ActorFactory.cs @@ -45,4 +45,4 @@ public static Actor Create(Type type) return constructor(); } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/ActorId.cs b/Src/PChecker/CheckerCore/Actors/ActorId.cs index f67a845c04..5c48c481f0 100644 --- a/Src/PChecker/CheckerCore/Actors/ActorId.cs +++ b/Src/PChecker/CheckerCore/Actors/ActorId.cs @@ -155,4 +155,4 @@ public override int GetHashCode() int IComparable.CompareTo(ActorId other) => string.Compare(Name, other?.Name); } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/ActorRuntime.cs b/Src/PChecker/CheckerCore/Actors/ActorRuntime.cs index 67c1a50524..7aaab2e56d 100644 --- a/Src/PChecker/CheckerCore/Actors/ActorRuntime.cs +++ b/Src/PChecker/CheckerCore/Actors/ActorRuntime.cs @@ -726,4 +726,4 @@ protected override void Dispose(bool disposing) base.Dispose(disposing); } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/EventQueues/DequeueStatus.cs b/Src/PChecker/CheckerCore/Actors/EventQueues/DequeueStatus.cs index b18cb4f9ee..6482634a40 100644 --- a/Src/PChecker/CheckerCore/Actors/EventQueues/DequeueStatus.cs +++ b/Src/PChecker/CheckerCore/Actors/EventQueues/DequeueStatus.cs @@ -28,4 +28,4 @@ internal enum DequeueStatus /// NotAvailable } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/EventQueues/EnqueueStatus.cs b/Src/PChecker/CheckerCore/Actors/EventQueues/EnqueueStatus.cs index 7dd9c5c755..57aab56ab6 100644 --- a/Src/PChecker/CheckerCore/Actors/EventQueues/EnqueueStatus.cs +++ b/Src/PChecker/CheckerCore/Actors/EventQueues/EnqueueStatus.cs @@ -33,4 +33,4 @@ internal enum EnqueueStatus /// Dropped } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/EventQueues/EventQueue.cs b/Src/PChecker/CheckerCore/Actors/EventQueues/EventQueue.cs index df2fe259e1..fa35a4758f 100644 --- a/Src/PChecker/CheckerCore/Actors/EventQueues/EventQueue.cs +++ b/Src/PChecker/CheckerCore/Actors/EventQueues/EventQueue.cs @@ -292,4 +292,4 @@ public void Dispose() GC.SuppressFinalize(this); } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/EventQueues/IEventQueue.cs b/Src/PChecker/CheckerCore/Actors/EventQueues/IEventQueue.cs index 5e7f9bcaf0..20026e59c9 100644 --- a/Src/PChecker/CheckerCore/Actors/EventQueues/IEventQueue.cs +++ b/Src/PChecker/CheckerCore/Actors/EventQueues/IEventQueue.cs @@ -62,4 +62,4 @@ internal interface IEventQueue : IDisposable /// void Close(); } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/EventQueues/Mocks/MockEventQueue.cs b/Src/PChecker/CheckerCore/Actors/EventQueues/Mocks/MockEventQueue.cs index 4a773c5f0c..a1e8d11720 100644 --- a/Src/PChecker/CheckerCore/Actors/EventQueues/Mocks/MockEventQueue.cs +++ b/Src/PChecker/CheckerCore/Actors/EventQueues/Mocks/MockEventQueue.cs @@ -346,4 +346,4 @@ public void Dispose() GC.SuppressFinalize(this); } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Events/DefaultEvent.cs b/Src/PChecker/CheckerCore/Actors/Events/DefaultEvent.cs index fd417724fa..bf430e673a 100644 --- a/Src/PChecker/CheckerCore/Actors/Events/DefaultEvent.cs +++ b/Src/PChecker/CheckerCore/Actors/Events/DefaultEvent.cs @@ -25,4 +25,4 @@ private DefaultEvent() { } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Events/Event.cs b/Src/PChecker/CheckerCore/Actors/Events/Event.cs index ff1afd639c..a33f298172 100644 --- a/Src/PChecker/CheckerCore/Actors/Events/Event.cs +++ b/Src/PChecker/CheckerCore/Actors/Events/Event.cs @@ -12,4 +12,4 @@ namespace PChecker.Actors.Events public abstract class Event { } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Events/EventInfo.cs b/Src/PChecker/CheckerCore/Actors/Events/EventInfo.cs index 3a9cab1792..05d37caeb5 100644 --- a/Src/PChecker/CheckerCore/Actors/Events/EventInfo.cs +++ b/Src/PChecker/CheckerCore/Actors/Events/EventInfo.cs @@ -60,4 +60,4 @@ internal EventInfo(Event e, EventOriginInfo originInfo) OriginInfo = originInfo; } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Events/EventOriginInfo.cs b/Src/PChecker/CheckerCore/Actors/Events/EventOriginInfo.cs index aca32397fc..8aea77ed51 100644 --- a/Src/PChecker/CheckerCore/Actors/Events/EventOriginInfo.cs +++ b/Src/PChecker/CheckerCore/Actors/Events/EventOriginInfo.cs @@ -39,4 +39,4 @@ internal EventOriginInfo(ActorId senderActorId, string senderMachineName, string SenderStateName = senderStateName; } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Events/GotoStateEvent.cs b/Src/PChecker/CheckerCore/Actors/Events/GotoStateEvent.cs index 51cb144924..ef8eadf02b 100644 --- a/Src/PChecker/CheckerCore/Actors/Events/GotoStateEvent.cs +++ b/Src/PChecker/CheckerCore/Actors/Events/GotoStateEvent.cs @@ -27,4 +27,4 @@ public GotoStateEvent(Type s) State = s; } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Events/HaltEvent.cs b/Src/PChecker/CheckerCore/Actors/Events/HaltEvent.cs index a24bc7c323..e1dcc6e064 100644 --- a/Src/PChecker/CheckerCore/Actors/Events/HaltEvent.cs +++ b/Src/PChecker/CheckerCore/Actors/Events/HaltEvent.cs @@ -24,4 +24,4 @@ private HaltEvent() { } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Events/QuiescentEvent.cs b/Src/PChecker/CheckerCore/Actors/Events/QuiescentEvent.cs index 838d36fadb..9b0649273c 100644 --- a/Src/PChecker/CheckerCore/Actors/Events/QuiescentEvent.cs +++ b/Src/PChecker/CheckerCore/Actors/Events/QuiescentEvent.cs @@ -25,4 +25,4 @@ public QuiescentEvent(ActorId id) ActorId = id; } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Events/WildcardEvent.cs b/Src/PChecker/CheckerCore/Actors/Events/WildcardEvent.cs index 39d93b5fcd..bba77fd07d 100644 --- a/Src/PChecker/CheckerCore/Actors/Events/WildcardEvent.cs +++ b/Src/PChecker/CheckerCore/Actors/Events/WildcardEvent.cs @@ -19,4 +19,4 @@ public WildCardEvent() { } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Exceptions/ActionExceptionFilterException.cs b/Src/PChecker/CheckerCore/Actors/Exceptions/ActionExceptionFilterException.cs index 50ad7accab..dcb74df948 100644 --- a/Src/PChecker/CheckerCore/Actors/Exceptions/ActionExceptionFilterException.cs +++ b/Src/PChecker/CheckerCore/Actors/Exceptions/ActionExceptionFilterException.cs @@ -30,4 +30,4 @@ internal ActionExceptionFilterException(string message, Exception innerException { } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Exceptions/OnEventDroppedHandler.cs b/Src/PChecker/CheckerCore/Actors/Exceptions/OnEventDroppedHandler.cs index 07c510e8ae..a96ad02dc0 100644 --- a/Src/PChecker/CheckerCore/Actors/Exceptions/OnEventDroppedHandler.cs +++ b/Src/PChecker/CheckerCore/Actors/Exceptions/OnEventDroppedHandler.cs @@ -9,4 +9,4 @@ namespace PChecker.Actors.Exceptions /// Handles the event. /// public delegate void OnEventDroppedHandler(Event e, ActorId target); -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Exceptions/OnExceptionOutcome.cs b/Src/PChecker/CheckerCore/Actors/Exceptions/OnExceptionOutcome.cs index 832a039545..dfa5bea2e3 100644 --- a/Src/PChecker/CheckerCore/Actors/Exceptions/OnExceptionOutcome.cs +++ b/Src/PChecker/CheckerCore/Actors/Exceptions/OnExceptionOutcome.cs @@ -23,4 +23,4 @@ public enum OnExceptionOutcome /// Halt = 2 } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Exceptions/UnhandledEventException.cs b/Src/PChecker/CheckerCore/Actors/Exceptions/UnhandledEventException.cs index c3f3a7d306..97a1891bab 100644 --- a/Src/PChecker/CheckerCore/Actors/Exceptions/UnhandledEventException.cs +++ b/Src/PChecker/CheckerCore/Actors/Exceptions/UnhandledEventException.cs @@ -36,4 +36,4 @@ internal UnhandledEventException(Event unhandledEvent, string currentStateName, UnhandledEvent = unhandledEvent; } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Handlers/ActionEventHandlerDeclaration.cs b/Src/PChecker/CheckerCore/Actors/Handlers/ActionEventHandlerDeclaration.cs index 82d32d665f..eb8a3aa1dc 100644 --- a/Src/PChecker/CheckerCore/Actors/Handlers/ActionEventHandlerDeclaration.cs +++ b/Src/PChecker/CheckerCore/Actors/Handlers/ActionEventHandlerDeclaration.cs @@ -23,4 +23,4 @@ public ActionEventHandlerDeclaration(string actionName) internal override bool Inheritable => true; } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Handlers/CachedDelegate.cs b/Src/PChecker/CheckerCore/Actors/Handlers/CachedDelegate.cs index 06eb081db1..1d69e9511b 100644 --- a/Src/PChecker/CheckerCore/Actors/Handlers/CachedDelegate.cs +++ b/Src/PChecker/CheckerCore/Actors/Handlers/CachedDelegate.cs @@ -48,4 +48,4 @@ internal CachedDelegate(MethodInfo method, object caller) MethodInfo = method; } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Handlers/DeferEventHandlerDeclaration.cs b/Src/PChecker/CheckerCore/Actors/Handlers/DeferEventHandlerDeclaration.cs index 6cc2230e88..428426ed4a 100644 --- a/Src/PChecker/CheckerCore/Actors/Handlers/DeferEventHandlerDeclaration.cs +++ b/Src/PChecker/CheckerCore/Actors/Handlers/DeferEventHandlerDeclaration.cs @@ -10,4 +10,4 @@ internal sealed class DeferEventHandlerDeclaration : EventHandlerDeclaration { internal override bool Inheritable => true; } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Handlers/EventHandlerDeclaration.cs b/Src/PChecker/CheckerCore/Actors/Handlers/EventHandlerDeclaration.cs index d0f6cf50fb..870fae0ca7 100644 --- a/Src/PChecker/CheckerCore/Actors/Handlers/EventHandlerDeclaration.cs +++ b/Src/PChecker/CheckerCore/Actors/Handlers/EventHandlerDeclaration.cs @@ -10,4 +10,4 @@ internal abstract class EventHandlerDeclaration { internal abstract bool Inheritable { get; } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Handlers/IgnoreEventHandlerDeclaration.cs b/Src/PChecker/CheckerCore/Actors/Handlers/IgnoreEventHandlerDeclaration.cs index f6d1f2708b..0486c36c04 100644 --- a/Src/PChecker/CheckerCore/Actors/Handlers/IgnoreEventHandlerDeclaration.cs +++ b/Src/PChecker/CheckerCore/Actors/Handlers/IgnoreEventHandlerDeclaration.cs @@ -10,4 +10,4 @@ internal sealed class IgnoreEventHandlerDeclaration : EventHandlerDeclaration { internal override bool Inheritable => true; } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/IActorRuntime.cs b/Src/PChecker/CheckerCore/Actors/IActorRuntime.cs index a0820f15de..84f4ecdf38 100644 --- a/Src/PChecker/CheckerCore/Actors/IActorRuntime.cs +++ b/Src/PChecker/CheckerCore/Actors/IActorRuntime.cs @@ -157,4 +157,4 @@ Task CreateActorAndExecuteAsync(ActorId id, Type type, Event initialEve /// The previously registered log writer to unregister. void RemoveLog(IActorRuntimeLog log); } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogTextFormatter.cs b/Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogTextFormatter.cs index b5bbac851e..1fd02e2ac3 100644 --- a/Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogTextFormatter.cs +++ b/Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogTextFormatter.cs @@ -373,4 +373,4 @@ public virtual void OnCompleted() { } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogXmlFormatter.cs b/Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogXmlFormatter.cs index 4043281b46..ebc7fb18d1 100644 --- a/Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogXmlFormatter.cs +++ b/Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogXmlFormatter.cs @@ -537,4 +537,4 @@ public void OnStrategyDescription(string strategyName, string description) Writer.WriteEndElement(); } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Logging/IActorRuntimeLog.cs b/Src/PChecker/CheckerCore/Actors/Logging/IActorRuntimeLog.cs index bc4f84bcf5..49e92e4f0e 100644 --- a/Src/PChecker/CheckerCore/Actors/Logging/IActorRuntimeLog.cs +++ b/Src/PChecker/CheckerCore/Actors/Logging/IActorRuntimeLog.cs @@ -248,4 +248,4 @@ void OnMonitorProcessEvent(string monitorType, string stateName, string senderNa /// void OnCompleted(); } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs b/Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs index 35b38176a3..76bd274e97 100644 --- a/Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs +++ b/Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs @@ -1,10 +1,10 @@ #nullable enable using System; using System.Collections; -using System.Linq; -using System.Text; using System.Collections.Generic; +using System.Linq; using System.Security.Cryptography; +using System.Text; namespace PChecker.Actors.Logging { diff --git a/Src/PChecker/CheckerCore/Actors/Logging/LogWriter.cs b/Src/PChecker/CheckerCore/Actors/Logging/LogWriter.cs index 3f97398a77..f92e5d13e6 100644 --- a/Src/PChecker/CheckerCore/Actors/Logging/LogWriter.cs +++ b/Src/PChecker/CheckerCore/Actors/Logging/LogWriter.cs @@ -640,4 +640,4 @@ internal void RemoveLog(IActorRuntimeLog log) } } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Managers/ActorManager.cs b/Src/PChecker/CheckerCore/Actors/Managers/ActorManager.cs index 39a837f5d5..3ec125adcd 100644 --- a/Src/PChecker/CheckerCore/Actors/Managers/ActorManager.cs +++ b/Src/PChecker/CheckerCore/Actors/Managers/ActorManager.cs @@ -117,4 +117,4 @@ public void Assert(bool predicate, string s, object arg0, object arg1, object ar [MethodImpl(MethodImplOptions.AggressiveInlining)] public void Assert(bool predicate, string s, params object[] args) => Runtime.Assert(predicate, s, args); } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Managers/IActorManager.cs b/Src/PChecker/CheckerCore/Actors/Managers/IActorManager.cs index a63bbd07c4..bc2ec7ab8e 100644 --- a/Src/PChecker/CheckerCore/Actors/Managers/IActorManager.cs +++ b/Src/PChecker/CheckerCore/Actors/Managers/IActorManager.cs @@ -93,4 +93,4 @@ internal interface IActorManager /// void Assert(bool predicate, string s, params object[] args); } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Managers/Mocks/MockActorManager.cs b/Src/PChecker/CheckerCore/Actors/Managers/Mocks/MockActorManager.cs index fbb00f4222..01c1d5de6c 100644 --- a/Src/PChecker/CheckerCore/Actors/Managers/Mocks/MockActorManager.cs +++ b/Src/PChecker/CheckerCore/Actors/Managers/Mocks/MockActorManager.cs @@ -150,4 +150,4 @@ public void Assert(bool predicate, string s, object arg0, object arg1, object ar [MethodImpl(MethodImplOptions.AggressiveInlining)] public void Assert(bool predicate, string s, params object[] args) => Runtime.Assert(predicate, s, args); } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Managers/Mocks/MockStateMachineManager.cs b/Src/PChecker/CheckerCore/Actors/Managers/Mocks/MockStateMachineManager.cs index eb8de3d865..9e647666b0 100644 --- a/Src/PChecker/CheckerCore/Actors/Managers/Mocks/MockStateMachineManager.cs +++ b/Src/PChecker/CheckerCore/Actors/Managers/Mocks/MockStateMachineManager.cs @@ -140,4 +140,4 @@ public void Assert(bool predicate, string s, object arg0, object arg1, object ar [MethodImpl(MethodImplOptions.AggressiveInlining)] public void Assert(bool predicate, string s, params object[] args) => Runtime.Assert(predicate, s, args); } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Managers/StateMachineManager.cs b/Src/PChecker/CheckerCore/Actors/Managers/StateMachineManager.cs index 0ad29505db..91e28f0b71 100644 --- a/Src/PChecker/CheckerCore/Actors/Managers/StateMachineManager.cs +++ b/Src/PChecker/CheckerCore/Actors/Managers/StateMachineManager.cs @@ -119,4 +119,4 @@ public void Assert(bool predicate, string s, object arg0, object arg1, object ar [MethodImpl(MethodImplOptions.AggressiveInlining)] public void Assert(bool predicate, string s, params object[] args) => Runtime.Assert(predicate, s, args); } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/NameResolver.cs b/Src/PChecker/CheckerCore/Actors/NameResolver.cs index 8f9e714843..501876bafd 100644 --- a/Src/PChecker/CheckerCore/Actors/NameResolver.cs +++ b/Src/PChecker/CheckerCore/Actors/NameResolver.cs @@ -56,4 +56,4 @@ internal static string GetQualifiedStateName(Type state) /// internal static string GetStateNameForLogging(Type state) => state is null ? "None" : GetQualifiedStateName(state); } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/RuntimeFactory.cs b/Src/PChecker/CheckerCore/Actors/RuntimeFactory.cs index 89a2f5a19c..852ebcd667 100644 --- a/Src/PChecker/CheckerCore/Actors/RuntimeFactory.cs +++ b/Src/PChecker/CheckerCore/Actors/RuntimeFactory.cs @@ -43,4 +43,4 @@ public static IActorRuntime Create(CheckerConfiguration checkerConfiguration) return runtime; } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/SendOptions.cs b/Src/PChecker/CheckerCore/Actors/SendOptions.cs index 985efae6dc..ff0dbb1ec0 100644 --- a/Src/PChecker/CheckerCore/Actors/SendOptions.cs +++ b/Src/PChecker/CheckerCore/Actors/SendOptions.cs @@ -47,4 +47,4 @@ public override string ToString() => string.Format("SendOptions[MustHandle='{0}', Assert='{1}', HashedState='{2}']", MustHandle, Assert, HashedState); } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/StateMachine.cs b/Src/PChecker/CheckerCore/Actors/StateMachine.cs index eb041e353a..27e5d910da 100644 --- a/Src/PChecker/CheckerCore/Actors/StateMachine.cs +++ b/Src/PChecker/CheckerCore/Actors/StateMachine.cs @@ -365,7 +365,7 @@ private async Task ExecuteCurrentStateOnExitAsync(string eventHandlerExitActionN await InvokeActionAsync(exitAction, e); var transition = PendingTransition; Assert(transition.TypeValue is Transition.Type.None || - transition.TypeValue is Transition.Type.Halt, + transition.TypeValue is Transition.Type.Halt, "{0} has performed a '{1}' transition from an OnExit action.", Id, transition.TypeValue); await ApplyEventHandlerTransitionAsync(transition, e); @@ -380,7 +380,7 @@ private async Task ExecuteCurrentStateOnExitAsync(string eventHandlerExitActionN await InvokeActionAsync(eventHandlerExitAction, e); var transition = PendingTransition; Assert(transition.TypeValue is Transition.Type.None || - transition.TypeValue is Transition.Type.Halt, + transition.TypeValue is Transition.Type.Halt, "{0} has performed a '{1}' transition from an OnExit action.", Id, transition.TypeValue); await ApplyEventHandlerTransitionAsync(transition, e); @@ -716,8 +716,8 @@ internal override void SetupEventHandlers() while (baseType != typeof(StateMachine)) { foreach (var s in baseType.GetNestedTypes(BindingFlags.Instance | - BindingFlags.NonPublic | BindingFlags.Public | - BindingFlags.DeclaredOnly)) + BindingFlags.NonPublic | BindingFlags.Public | + BindingFlags.DeclaredOnly)) { ExtractStateTypes(s); } @@ -745,8 +745,8 @@ internal override void SetupEventHandlers() // type. This type can be then used to create the state constructor. var declaringType = GetType(); while (!declaringType.IsGenericType || - !type.DeclaringType.FullName.Equals(declaringType.FullName.Substring( - 0, declaringType.FullName.IndexOf('[')))) + !type.DeclaringType.FullName.Equals(declaringType.FullName.Substring( + 0, declaringType.FullName.IndexOf('[')))) { declaringType = declaringType.BaseType; } @@ -862,8 +862,8 @@ private void ExtractStateTypes(Type type) { // Adds the contents of the group of states to the stack. foreach (var t in nextType.GetNestedTypes(BindingFlags.Instance | - BindingFlags.NonPublic | BindingFlags.Public | - BindingFlags.DeclaredOnly)) + BindingFlags.NonPublic | BindingFlags.Public | + BindingFlags.DeclaredOnly)) { Assert(t.IsSubclassOf(typeof(StateGroup)) || t.IsSubclassOf(typeof(State)), "'{0}' is neither a group of states nor a state.", t.Name); @@ -911,8 +911,8 @@ internal HashSet> GetAllStateEventPairs() foreach (var state in StateInstanceCache[GetType()]) { foreach (var binding in from b in state.InheritableEventHandlers.Concat(state.EventHandlers) - where IncludeInCoverage(b.Value) - select b) + where IncludeInCoverage(b.Value) + select b) { pairs.Add(Tuple.Create(NameResolver.GetQualifiedStateName(state.GetType()), binding.Key.FullName)); } @@ -1637,4 +1637,4 @@ public abstract class StateGroup { } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/StateTransitions/GotoStateTransition.cs b/Src/PChecker/CheckerCore/Actors/StateTransitions/GotoStateTransition.cs index d63c1e035f..2b41829acc 100644 --- a/Src/PChecker/CheckerCore/Actors/StateTransitions/GotoStateTransition.cs +++ b/Src/PChecker/CheckerCore/Actors/StateTransitions/GotoStateTransition.cs @@ -45,4 +45,4 @@ public GotoStateTransition(Type targetState) internal override bool Inheritable => false; } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/StateTransitions/PushStateTransition.cs b/Src/PChecker/CheckerCore/Actors/StateTransitions/PushStateTransition.cs index dcb38c42e5..da0f64c517 100644 --- a/Src/PChecker/CheckerCore/Actors/StateTransitions/PushStateTransition.cs +++ b/Src/PChecker/CheckerCore/Actors/StateTransitions/PushStateTransition.cs @@ -27,4 +27,4 @@ public PushStateTransition(Type targetState) internal override bool Inheritable => false; } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/UnitTesting/ActorTestKit.cs b/Src/PChecker/CheckerCore/Actors/UnitTesting/ActorTestKit.cs index 998475c907..67b47922ec 100644 --- a/Src/PChecker/CheckerCore/Actors/UnitTesting/ActorTestKit.cs +++ b/Src/PChecker/CheckerCore/Actors/UnitTesting/ActorTestKit.cs @@ -163,7 +163,7 @@ private MethodInfo GetMethod(string methodName, bool isAsync, Type[] parameterTy methodName, ActorInstance.Id)); Runtime.Assert(method.GetCustomAttribute(typeof(AsyncStateMachineAttribute)) is null != isAsync, string.Format("Must invoke {0}method '{1}' of {2} using '{3}'.", - isAsync ? string.Empty : "async ", methodName, ActorInstance.Id, isAsync ? "Invoke" : "InvokeAsync")); + isAsync ? string.Empty : "async ", methodName, ActorInstance.Id, isAsync ? "Invoke" : "InvokeAsync")); return method; } @@ -257,4 +257,4 @@ public void AssertInboxSize(int numEvents) ActorInstance.Id, Runtime.ActorInbox.Size); } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/UnitTesting/ActorUnitTestingRuntime.cs b/Src/PChecker/CheckerCore/Actors/UnitTesting/ActorUnitTestingRuntime.cs index 43aa5d251c..dff8b32b33 100644 --- a/Src/PChecker/CheckerCore/Actors/UnitTesting/ActorUnitTestingRuntime.cs +++ b/Src/PChecker/CheckerCore/Actors/UnitTesting/ActorUnitTestingRuntime.cs @@ -250,4 +250,4 @@ internal override void NotifyWaitEvent(Actor actor, IEnumerable eventTypes QuiescenceCompletionSource.SetResult(true); } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/CheckerConfiguration.cs b/Src/PChecker/CheckerCore/CheckerConfiguration.cs index 3463c73572..0c983a7c80 100644 --- a/Src/PChecker/CheckerCore/CheckerConfiguration.cs +++ b/Src/PChecker/CheckerCore/CheckerConfiguration.cs @@ -5,7 +5,6 @@ using System.Collections.Generic; using System.IO; using System.Runtime.Serialization; -using PChecker.Actors.Logging; using PChecker.Utilities; namespace PChecker @@ -557,4 +556,4 @@ public void SetOutputDirectory() } } #pragma warning restore CA1724 // Type names should not match namespaces -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Coverage/ActivityCoverageReporter.cs b/Src/PChecker/CheckerCore/Coverage/ActivityCoverageReporter.cs index 0550b7ab46..6401efb0b5 100644 --- a/Src/PChecker/CheckerCore/Coverage/ActivityCoverageReporter.cs +++ b/Src/PChecker/CheckerCore/Coverage/ActivityCoverageReporter.cs @@ -365,4 +365,4 @@ private static string GetSanitizedName(string name) return name; } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Coverage/ActorRuntimeLogEventCoverage.cs b/Src/PChecker/CheckerCore/Coverage/ActorRuntimeLogEventCoverage.cs index 0e2b4d4c71..8d13857018 100644 --- a/Src/PChecker/CheckerCore/Coverage/ActorRuntimeLogEventCoverage.cs +++ b/Src/PChecker/CheckerCore/Coverage/ActorRuntimeLogEventCoverage.cs @@ -311,4 +311,4 @@ private static string GetLabel(string actorId, string fullyQualifiedName) return fullyQualifiedName; } } -} +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Coverage/ActorRuntimeLogGraphBuilder.cs b/Src/PChecker/CheckerCore/Coverage/ActorRuntimeLogGraphBuilder.cs index bccac80e9d..752570a510 100644 --- a/Src/PChecker/CheckerCore/Coverage/ActorRuntimeLogGraphBuilder.cs +++ b/Src/PChecker/CheckerCore/Coverage/ActorRuntimeLogGraphBuilder.cs @@ -903,7 +903,7 @@ public void WriteDgml(TextWriter writer, bool includeDefaultStyles) if (includeDefaultStyles) { writer.WriteLine( -@" + @"