From 79d58daf4b820c5e156c33c80a5ba32292b0e19b Mon Sep 17 00:00:00 2001 From: Christine Zhou Date: Thu, 10 Oct 2024 14:49:35 -0700 Subject: [PATCH] Fixing warnings and errors --- .../Logging/PCheckerLogJsonFormatter.cs | 2 +- .../SystematicTesting/ControlledRuntime.cs | 14 +-- .../Backend/CSharp/CSharpCodeGenerator.cs | 13 ++- .../CompilerCore/Backend/CSharp/Constants.cs | 2 +- .../BugFinding1/generatedOutput.coverage.txt | 25 ----- .../BugFinding1/generatedOutput.dgml | 44 -------- .../BugFinding1/generatedOutput.sci | 1 - .../BugFinding1/generatedOutput_0_0.dgml | 44 -------- .../BugFinding1/generatedOutput_0_0.schedule | 6 -- .../generatedOutput_0_0.trace.json | 101 ------------------ .../BugFinding1/generatedOutput_0_0.txt | 15 --- .../generatedOutput_pchecker_summary.txt | 5 - 12 files changed, 15 insertions(+), 257 deletions(-) delete mode 100644 Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput.coverage.txt delete mode 100644 Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput.dgml delete mode 100644 Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput.sci delete mode 100644 Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_0_0.dgml delete mode 100644 Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_0_0.schedule delete mode 100644 Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_0_0.trace.json delete mode 100644 Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_0_0.txt delete mode 100644 Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_pchecker_summary.txt diff --git a/Src/PChecker/CheckerCore/Runtime/Logging/PCheckerLogJsonFormatter.cs b/Src/PChecker/CheckerCore/Runtime/Logging/PCheckerLogJsonFormatter.cs index 578e1863ba..c37b679a3c 100644 --- a/Src/PChecker/CheckerCore/Runtime/Logging/PCheckerLogJsonFormatter.cs +++ b/Src/PChecker/CheckerCore/Runtime/Logging/PCheckerLogJsonFormatter.cs @@ -29,7 +29,7 @@ protected PCheckerLogJsonFormatter() } /// - /// Removes the '<' and '>' tags for a log text. + /// Removes the "<" and ">" tags for a log text. /// /// The text log /// New string with the tag removed or just the string itself if there is no tag. diff --git a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs index e6f0894a16..9f1cd05283 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs @@ -60,7 +60,7 @@ private static ControlledRuntime CreateWithConfiguration(CheckerConfiguration ch /// /// The currently executing runtime. /// - internal static new ControlledRuntime Current => AsyncLocalInstance.Value ?? + internal static ControlledRuntime Current => AsyncLocalInstance.Value ?? 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 " + @@ -71,12 +71,12 @@ private static ControlledRuntime CreateWithConfiguration(CheckerConfiguration ch /// /// The checkerConfiguration used by the runtime. /// - protected internal readonly CheckerConfiguration CheckerConfiguration; + internal readonly CheckerConfiguration CheckerConfiguration; /// /// List of monitors in the program. /// - protected readonly List Monitors; + readonly List Monitors; /// /// Monotonically increasing operation id counter. @@ -86,7 +86,7 @@ private static ControlledRuntime CreateWithConfiguration(CheckerConfiguration ch /// /// Records if the runtime is running. /// - protected internal volatile bool IsRunning; + internal volatile bool IsRunning; /// /// Callback that is fired when the program throws an exception which includes failed assertions. @@ -137,7 +137,7 @@ private static ControlledRuntime CreateWithConfiguration(CheckerConfiguration ch /// /// Responsible for writing to all registered objects. /// - protected internal LogWriter LogWriter { get; private set; } + internal LogWriter LogWriter { get; private set; } /// /// Used to log text messages. Use @@ -1421,7 +1421,7 @@ internal async Task WaitAsync() /// /// Raises the event with the specified . /// - protected internal void RaiseOnFailureEvent(Exception exception) + internal void RaiseOnFailureEvent(Exception exception) { if (exception is ExecutionCanceledException || (exception is ActionExceptionFilterException ae && ae.InnerException is ExecutionCanceledException)) @@ -1437,7 +1437,7 @@ protected internal void RaiseOnFailureEvent(Exception exception) /// Disposes runtime resources. /// [DebuggerStepThrough] - protected void Dispose(bool disposing) + void Dispose(bool disposing) { if (disposing) { diff --git a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs index 978e69a295..d7b935872c 100644 --- a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs +++ b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs @@ -150,20 +150,19 @@ private void WriteInitializeInterfaces(CompilationContext context, StringWriter private void WriteSourcePrologue(CompilationContext context, StringWriter output) { context.WriteLine(output, "using PChecker;"); - context.WriteLine(output, "using PChecker.StateMachines;"); - context.WriteLine(output, "using PChecker.StateMachines.Events;"); context.WriteLine(output, "using PChecker.Runtime;"); - context.WriteLine(output, "using PChecker.Specifications;"); - context.WriteLine(output, "using Monitor = PChecker.Specifications.Monitors.Monitor;"); + context.WriteLine(output, "using PChecker.Runtime.StateMachines;"); + context.WriteLine(output, "using PChecker.Runtime.Events;"); + context.WriteLine(output, "using PChecker.Runtime.Exceptions;"); + context.WriteLine(output, "using PChecker.Runtime.Values;"); + context.WriteLine(output, "using PChecker.Runtime.Specifications;"); + context.WriteLine(output, "using Monitor = PChecker.Runtime.Specifications.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;"); context.WriteLine(output, "using System.IO;"); - context.WriteLine(output, "using PChecker.Runtime.Values;"); - context.WriteLine(output, "using PChecker.Runtime;"); - context.WriteLine(output, "using PChecker.Runtime.Exceptions;"); context.WriteLine(output, "using System.Threading;"); context.WriteLine(output, "using System.Threading.Tasks;"); context.WriteLine(output); diff --git a/Src/PCompiler/CompilerCore/Backend/CSharp/Constants.cs b/Src/PCompiler/CompilerCore/Backend/CSharp/Constants.cs index c2f8208ac3..1094d641e7 100644 --- a/Src/PCompiler/CompilerCore/Backend/CSharp/Constants.cs +++ b/Src/PCompiler/CompilerCore/Backend/CSharp/Constants.cs @@ -26,7 +26,7 @@ internal class Constants using System; using System.IO; using System.Linq; -using PChecker.StateMachines; +using PChecker.Runtime.StateMachines; namespace PImplementation { diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput.coverage.txt b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput.coverage.txt deleted file mode 100644 index 8fe3514eca..0000000000 --- a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput.coverage.txt +++ /dev/null @@ -1,25 +0,0 @@ -Total event coverage: 100.0% -============================ -StateMachine: _GodMachine -========================= -Event coverage: 100.0% - - State: Init - State has no expected events, so coverage is 100% - -StateMachine: Main -================== -Event coverage: 100.0% - - State: __InitState__ - State event coverage: 100.0% - Events received: Main+ConstructorEvent - Events sent: Main+ConstructorEvent - Next states: S - - State: S - State event coverage: 100.0% - Events received: x - Events sent: a, x - Previous states: __InitState__ - diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput.dgml b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput.dgml deleted file mode 100644 index 06241b5f23..0000000000 --- a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput.dgml +++ /dev/null @@ -1,44 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput.sci b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput.sci deleted file mode 100644 index 025408688b..0000000000 --- a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput.sci +++ /dev/null @@ -1 +0,0 @@ -PImplementation.Main.__InitState__->PImplementation.Main.S(0)ConstructorEventPImplementation.Main.__InitState__->PImplementation.Main.S(ConstructorEvent)0PChecker.PRuntime._GodMachine->PChecker.PRuntime._GodMachine.InitContainsPImplementation.Main->PImplementation.Main.__InitState__PImplementation.Main->PImplementation.Main.SPImplementation.Main.__InitState__->PImplementation.Main.S(0)EventIdPImplementation.Main+ConstructorEvent0PImplementation.Main.__InitState__->PImplementation.Main.S0PImplementation.Main.__InitState__PImplementation.Main.SPImplementation.xPImplementation.Main.__InitState__PImplementation.Main.SPImplementation.aSPImplementation.Main.__InitState__PImplementation.Main.S \ No newline at end of file diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_0_0.dgml b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_0_0.dgml deleted file mode 100644 index 06241b5f23..0000000000 --- a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_0_0.dgml +++ /dev/null @@ -1,44 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_0_0.schedule b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_0_0.schedule deleted file mode 100644 index d507e9ea98..0000000000 --- a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_0_0.schedule +++ /dev/null @@ -1,6 +0,0 @@ ---fair-scheduling ---liveness-temperature-threshold:50000 -(0) -(1) -(1) -(2) \ No newline at end of file diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_0_0.trace.json b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_0_0.trace.json deleted file mode 100644 index 70a7df9b78..0000000000 --- a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_0_0.trace.json +++ /dev/null @@ -1,101 +0,0 @@ -[ - { - "type": "StateTransition", - "details": { - "log": "Main(2) enters state \u0027S\u0027.", - "id": "Main(2)", - "state": "S", - "payload": "null", - "isEntry": true, - "clock": { - "Main(2)": 1 - } - } - }, - { - "type": "RaiseEvent", - "details": { - "log": "\u0027Main(2)\u0027 raised event \u0027x with payload (\u003Ca,3,\u003E)\u0027 in state \u0027S\u0027.", - "id": "Main(2)", - "event": "x", - "state": "S", - "payload": { - "0": {}, - "1": {} - }, - "clock": { - "Main(2)": 2 - } - } - }, - { - "type": "RaiseEvent", - "details": { - "log": "\u0027Main(2)\u0027 raised event \u0027a with payload (3)\u0027 in state \u0027S\u0027.", - "id": "Main(2)", - "event": "a", - "state": "S", - "payload": 3, - "clock": { - "Main(2)": 3 - } - } - }, - { - "type": "StateTransition", - "details": { - "log": "Main(2) exits state \u0027S\u0027.", - "id": "Main(2)", - "state": "S", - "payload": "null", - "isEntry": false, - "clock": { - "Main(2)": 4 - } - } - }, - { - "type": "PopStateUnhandledEvent", - "details": { - "log": "Main(2) popped state S due to unhandled event \u0027a\u0027.", - "id": "Main(2)", - "event": "a", - "state": "S", - "payload": "null", - "clock": { - "Main(2)": 5 - } - } - }, - { - "type": "ExceptionThrown", - "details": { - "log": "Main(2) running action \u0027\u0027 in state \u0027S\u0027 threw exception \u0027UnhandledEventException\u0027.", - "id": "Main(2)", - "state": "S", - "payload": "null", - "action": "", - "exception": "UnhandledEventException", - "clock": { - "Main(2)": 6 - } - } - }, - { - "type": "AssertionFailure", - "details": { - "log": "Main(2) received event \u0027PImplementation.a\u0027 that cannot be handled.", - "error": "Main(2) received event \u0027PImplementation.a\u0027 that cannot be handled.", - "payload": "null" - } - }, - { - "type": "StrategyDescription", - "details": { - "log": "Found bug using \u0027random\u0027 strategy.", - "payload": "null", - "strategy": "random", - "strategyDescription": "random[seed \u0027769371342\u0027]" - } - } -] \ No newline at end of file diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_0_0.txt b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_0_0.txt deleted file mode 100644 index a07342a6b5..0000000000 --- a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_0_0.txt +++ /dev/null @@ -1,15 +0,0 @@ - Running test 'DefaultImpl'. - Main(2) enters state 'S'. - 'Main(2)' raised event 'x with payload ()' in state 'S'. - 'Main(2)' raised event 'a with payload (3)' in state 'S'. - Main(2) exits state 'S'. - Main(2) popped state S due to unhandled event 'PImplementation.a'. - Main(2) running action '' in state 'S' threw exception 'UnhandledEventException'. - Main(2) received event 'PImplementation.a' that cannot be handled. - Found bug using 'random' strategy. - Checking statistics: - Found 1 bug. - Scheduling statistics: - Explored 1 schedule - Found 100.00% buggy schedules. - Number of scheduling points in terminating schedules: 4 (min), 4 (avg), 4 (max). \ No newline at end of file diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_pchecker_summary.txt b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_pchecker_summary.txt deleted file mode 100644 index 1f66d9ba9f..0000000000 --- a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_pchecker_summary.txt +++ /dev/null @@ -1,5 +0,0 @@ -bugs:1 -schedules:1 -max_depth:4 -time_seconds:0.12 -memory_max_mb:0 \ No newline at end of file