Fixed json log generation bug (#812)

Co-authored-by: Christine Zhou <[email protected]>
p-org · Jan 16, 2025 · db51c8e · db51c8e
1 parent a7bbb1f
commit db51c8e
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 24 deletions.
diff --git a/Src/PChecker/CheckerCore/Runtime/Logging/PCheckerLogJsonFormatter.cs b/Src/PChecker/CheckerCore/Runtime/Logging/PCheckerLogJsonFormatter.cs
@@ -23,7 +23,7 @@ public class PCheckerLogJsonFormatter : IControlledRuntimeLog
         /// <summary>
         /// Initializes a new instance of the <see cref="PCheckerLogJsonFormatter"/> class.
         /// </summary>
-        protected PCheckerLogJsonFormatter()
+        public PCheckerLogJsonFormatter()
         {
             Writer = new JsonWriter();
         }

diff --git a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs
@@ -449,7 +449,6 @@ internal StateMachineId CreateStateMachine(StateMachineId id, Type type, string
             AssertExpectedCallerStateMachine(creator, "CreateStateMachine");
 
             var stateMachine = CreateStateMachine(id, type, name, creator);
-            LogWriter.LogCreateStateMachine(stateMachine.Id, creator?.Id.Name, creator?.Id.Type);
             RunStateMachineEventHandler(stateMachine, initialEvent, true, null);
             return stateMachine.Id;
         }

diff --git a/Src/PChecker/CheckerCore/Testing/TestingProcess.cs b/Src/PChecker/CheckerCore/Testing/TestingProcess.cs
@@ -86,14 +86,7 @@ private async Task RunAsync()
             {
                 Console.WriteLine($"Checker found a bug.");
             }
-
-            // we want the graph generation even if doing full exploration.
-            if ((!_checkerConfiguration.PerformFullExploration && TestingEngine.TestReport.NumOfFoundBugs > 0) ||
-                (_checkerConfiguration.IsDgmlGraphEnabled && !_checkerConfiguration.IsDgmlBugGraph))
-            {
-                await EmitTraces();
-            }
-
+
             // Closes the remote notification listener.
             if (_checkerConfiguration.IsVerbose)
             {
@@ -121,20 +114,6 @@ private TestingProcess(CheckerConfiguration checkerConfiguration)
             Profiler = new Profiler();
             IsProcessCanceled = false;
         }
-
-
-        /// <summary>
-        /// Emits the testing traces.
-        /// </summary>
-        private Task EmitTraces()
-        {
-            var file = Path.GetFileNameWithoutExtension(_checkerConfiguration.AssemblyToBeAnalyzed);
-            file += "_" + _checkerConfiguration.TestingProcessId;
-
-            Console.WriteLine($"... Emitting traces:");
-            TestingEngine.TryEmitTraces(_checkerConfiguration.OutputDirectory, file);
-            return Task.CompletedTask;
-        }
 
         /// <summary>
         /// Emits the test report.

diff --git a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs
@@ -154,6 +154,7 @@ private void WriteSourcePrologue(CompilationContext context, StringWriter output
             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.Logging;");
             context.WriteLine(output, "using PChecker.Runtime.Values;");
             context.WriteLine(output, "using PChecker.Runtime.Specifications;");
             context.WriteLine(output, "using Monitor = PChecker.Runtime.Specifications.Monitor;");
@@ -387,6 +388,8 @@ private void WriteTestFunction(CompilationContext context, StringWriter output,
             context.WriteLine(output);
             context.WriteLine(output, "[PChecker.SystematicTesting.Test]");
             context.WriteLine(output, "public static void Execute(ControlledRuntime runtime) {");
+            context.WriteLine(output, "runtime.RegisterLog(new PCheckerLogTextFormatter());");
+            context.WriteLine(output, "runtime.RegisterLog(new PCheckerLogJsonFormatter());");
             context.WriteLine(output, "PModule.runtime = runtime;");
             context.WriteLine(output, "PHelper.InitializeInterfaces();");
             context.WriteLine(output, "PHelper.InitializeEnums();");