Added test for generated PChecker logs

Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs

@@ -165,9 +165,7 @@ public override void Write(Utf8JsonWriter writer, Encoding value, JsonSerializer
         /// A guard for printing info.
         /// </summary>
         private int PrintGuard;
-
-        private StreamWriter TimelineFileStream;
-
+
 
         /// <summary>
         /// Creates a new systematic testing engine.
@@ -272,7 +270,6 @@ private TestingEngine(CheckerConfiguration checkerConfiguration, TestMethodInfo
 
             CancellationTokenSource = new CancellationTokenSource();
             PrintGuard = 1;
-            TimelineFileStream = new StreamWriter(checkerConfiguration.OutputDirectory + "timeline.txt");
             // Initialize a new instance of JsonVerboseLogs if running in verbose mode.
             if (checkerConfiguration.IsVerbose)
             {

Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs

@@ -11,7 +11,7 @@
 
 namespace Plang.Options
 {
-    internal sealed class PCheckerOptions
+    public sealed class PCheckerOptions
     {
         /// <summary>
         /// The command line parser to use.
@@ -21,7 +21,7 @@ internal sealed class PCheckerOptions
         /// <summary>
         /// Initializes a new instance of the <see cref="PCheckerOptions"/> class.
         /// </summary>
-        internal PCheckerOptions()
+        public PCheckerOptions()
         {
             Parser = new CommandLineArgumentParser("p check",
                 "The P checker enables systematic exploration of a specified P test case, it generates " +
@@ -87,7 +87,7 @@ internal PCheckerOptions()
         /// Parses the command line options and returns a checkerConfiguration.
         /// </summary>
         /// <returns>The CheckerConfiguration object populated with the parsed command line options.</returns>
-        internal CheckerConfiguration Parse(string[] args)
+        public CheckerConfiguration Parse(string[] args)
         {
             var configuration = CheckerConfiguration.Create();
             try

Tst/CorrectLogs/bugs2/Main.coverage.txt

@@ -0,0 +1,11 @@
+Total event coverage: 100.0%
+============================
+StateMachine: Main
+==================
+Event coverage: 100.0%
+
+	State: S
+		State event coverage: 100.0%
+		Events received: x
+		Events sent: a, x
+

Tst/CorrectLogs/bugs2/trace_0_0.trace.json

@@ -0,0 +1,103 @@
+[
+  {
+    "type": "CreateStateMachine",
+    "details": {
+      "log": "Main(1) was created by task \u00272\u0027.",
+      "id": "Main(1)",
+      "payload": "null",
+      "clock": {
+        "Main(1)": 1
+      }
+    }
+  },
+  {
+    "type": "StateTransition",
+    "details": {
+      "log": "Main(1) enters state \u0027S\u0027.",
+      "id": "Main(1)",
+      "state": "S",
+      "payload": "null",
+      "isEntry": true,
+      "clock": {
+        "Main(1)": 2
+      }
+    }
+  },
+  {
+    "type": "RaiseEvent",
+    "details": {
+      "log": "\u0027Main(1)\u0027 raised event \u0027x with payload (\u003Ca,3,\u003E)\u0027 in state \u0027S\u0027.",
+      "id": "Main(1)",
+      "event": "x",
+      "state": "S",
+      "payload": {
+        "0": {},
+        "1": {}
+      },
+      "clock": {
+        "Main(1)": 3
+      }
+    }
+  },
+  {
+    "type": "RaiseEvent",
+    "details": {
+      "log": "\u0027Main(1)\u0027 raised event \u0027a with payload (3)\u0027 in state \u0027S\u0027.",
+      "id": "Main(1)",
+      "event": "a",
+      "state": "S",
+      "payload": 3,
+      "clock": {
+        "Main(1)": 4
+      }
+    }
+  },
+  {
+    "type": "StateTransition",
+    "details": {
+      "log": "Main(1) exits state \u0027S\u0027.",
+      "id": "Main(1)",
+      "state": "S",
+      "payload": "null",
+      "isEntry": false,
+      "clock": {
+        "Main(1)": 5
+      }
+    }
+  },
+  {
+    "type": "PopStateUnhandledEvent",
+    "details": {
+      "log": "Main(1) popped state S due to unhandled event \u0027a\u0027.",
+      "id": "Main(1)",
+      "event": "a",
+      "state": "S",
+      "payload": "null",
+      "clock": {
+        "Main(1)": 6
+      }
+    }
+  },
+  {
+    "type": "ExceptionThrown",
+    "details": {
+      "log": "Main(1) running action \u0027\u0027 in state \u0027S\u0027 threw exception \u0027UnhandledEventException\u0027.",
+      "id": "Main(1)",
+      "state": "S",
+      "payload": "null",
+      "action": "",
+      "exception": "UnhandledEventException",
+      "clock": {
+        "Main(1)": 7
+      }
+    }
+  },
+  {
+    "type": "AssertionFailure",
+    "details": {
+      "log": "Main(1) received event \u0027PImplementation.a\u0027 that cannot be handled.",
+      "error": "Main(1) received event \u0027PImplementation.a\u0027 that cannot be handled.",
+      "payload": "null"
+    }
+  }
+]

Tst/CorrectLogs/bugs2/trace_0_0.txt

@@ -0,0 +1,17 @@
+<TestLog> Running test 'DefaultImpl'.
+<CreateLog> Main(1) was created by task '2'.
+<StateLog> Main(1) enters state 'S'.
+<RaiseLog> 'Main(1)' raised event 'x with payload (<a,3,>)' in state 'S'.
+<RaiseLog> 'Main(1)' raised event 'a with payload (3)' in state 'S'.
+<StateLog> Main(1) exits state 'S'.
+<PopLog> Main(1) popped state S due to unhandled event 'a'.
+<ExceptionLog> Main(1) running action '' in state 'S' threw exception 'UnhandledEventException'.
+<ErrorLog> Main(1) received event 'PImplementation.a' that cannot be handled.
+<StrategyLog> Found bug using 'random' strategy.
+<StrategyLog> Checking statistics:
+<StrategyLog> Found 1 bug.
+<StrategyLog> Scheduling statistics:
+<StrategyLog> Explored 1 schedule
+<StrategyLog> Explored 1 timeline
+<StrategyLog> Found 100.00% buggy schedules.
+<StrategyLog> Number of scheduling points in terminating schedules: 2 (min), 2 (avg), 2 (max).

Tst/UnitTests/PCheckerLogGeneratorTests.cs

@@ -0,0 +1,125 @@
+using System;
+using System.Diagnostics;
+using System.IO;
+using System.Linq;
+using Newtonsoft.Json.Linq;
+using NUnit.Framework;
+using PChecker;
+using UnitTests.Core;
+using UnitTests.Runners;
+using Plang.Options;
+namespace UnitTests;
+
+[TestFixture]
+[Parallelizable(ParallelScope.Children)]
+public class PCheckerLogGeneratorTests
+{
+    [Test]
+    public void TestLogGenerator()
+    {
+        var tempDir = Directory.CreateDirectory(Path.Combine(Constants.ScratchParentDirectory, "TestLogGenerator"));
+        var srcPath = new FileInfo(Path.Combine(Constants.SolutionDirectory, "Tst", "RegressionTests",
+            "Feature1SMLevelDecls", "DynamicError", "bug2", "bug2.p"));
+        var dllPath = Path.Combine(Constants.ScratchParentDirectory, "TestLogGenerator", "CSharp", "net8.0", "Main.dll");
+        var expectedPath = Path.Combine(Constants.SolutionDirectory, "Tst", "CorrectLogs", "bugs2");
+
+        var runner = new PCheckerRunner([srcPath]);
+        runner.DoCompile(tempDir);
+
+        var configuration = new PCheckerOptions().Parse([dllPath, "-o", tempDir.ToString()]);
+        Checker.Run(configuration);
+
+        AssertLog(tempDir+"/BugFinding", expectedPath);
+    }
+
+    private void AssertLog(string generatedDir, string expectedDir)
+    {
+        if (!Directory.Exists(generatedDir) || !Directory.Exists(expectedDir))
+        {
+            Assert.Fail("One or both directories do not exist.");
+        }
+
+        var generatedFiles = Directory.GetFiles(generatedDir).Select(Path.GetFileName).ToHashSet();
+        var expectedFiles = Directory.GetFiles(expectedDir).Select(Path.GetFileName).ToHashSet();
+
+        foreach (var fileName in expectedFiles.Intersect(generatedFiles))
+        {
+            string generatedFilePath = Path.Combine(generatedDir, fileName);
+            string expectedFilePath = Path.Combine(expectedDir, fileName);
+
+            if (fileName == "trace_0_0.trace.json")
+            {
+                // Perform "Is JSON Included" check for this specific file
+                if (!IsJsonContentIncluded(generatedFilePath, expectedFilePath))
+                {
+                    Assert.Fail($"Test Failed \nContent of {expectedFilePath} is not fully included in {generatedFilePath}");
+                }
+            }
+            else
+            {
+                // Perform exact match for other files
+                if (!File.ReadAllBytes(generatedFilePath).SequenceEqual(File.ReadAllBytes(expectedFilePath)))
+                {
+                    Assert.Fail($"Test Failed \nFiles differ: {fileName}\nGenerated File: {generatedFilePath}\nExpected File: {expectedFilePath}");
+                }
+            }
+        }
+
+        // Check for missing files in generatedDir
+        foreach (var file in expectedFiles.Except(generatedFiles))
+        {
+            Assert.Fail($"Test Failed \nMissing expected file in {generatedDir}: {file}");
+        }
+        Console.WriteLine("Test Succeeded");
+    }
+
+    private static bool IsJsonContentIncluded(string generatedFilePath, string expectedFilePath)
+    {
+        var generatedJson = JToken.Parse(File.ReadAllText(generatedFilePath));
+        var expectedJson = JToken.Parse(File.ReadAllText(expectedFilePath));
+
+        return IsSubset(expectedJson, generatedJson);
+    }
+
+    private static bool IsSubset(JToken subset, JToken superset)
+    {
+        if (JToken.DeepEquals(subset, superset))
+        {
+            return true;
+        }
+
+        if (subset.Type == JTokenType.Object && superset.Type == JTokenType.Object)
+        {
+            var subsetObj = (JObject)subset;
+            var supersetObj = (JObject)superset;
+
+            foreach (var property in subsetObj.Properties())
+            {
+                if (!supersetObj.TryGetValue(property.Name, out var supersetValue) || !IsSubset(property.Value, supersetValue))
+                {
+                    return false;
+                }
+            }
+
+            return true;
+        }
+
+        if (subset.Type == JTokenType.Array && superset.Type == JTokenType.Array)
+        {
+            var subsetArray = (JArray)subset;
+            var supersetArray = (JArray)superset;
+
+            foreach (var subsetItem in subsetArray)
+            {
+                if (!supersetArray.Any(supersetItem => IsSubset(subsetItem, supersetItem)))
+                {
+                    return false;
+                }
+            }
+
+            return true;
+        }
+
+        return false;
+    }
+}

Tst/UnitTests/Runners/PCheckerRunner.cs

@@ -155,7 +155,7 @@ private int RunPChecker(string directory, string dllPath, out string stdout, out
             return ProcessHelper.RunWithOutput(directory, out stdout, out stderr, "dotnet", dllPath);
         }
 
-        private int DoCompile(DirectoryInfo scratchDirectory)
+        public int DoCompile(DirectoryInfo scratchDirectory)
         {
             var compiler = new Compiler();
             var outputStream = new TestExecutionStream(scratchDirectory);

Tst/UnitTests/TestAssertions.cs

@@ -22,8 +22,8 @@ public static void AssertTestCase(CompilerTestCase testCase)
             // Delete ONLY if inside the solution directory
             SafeDeleteDirectory(testCase.ScratchDirectory);
         }
-
-        private static void SafeDeleteDirectory(DirectoryInfo toDelete)
+        
+        public static void SafeDeleteDirectory(DirectoryInfo toDelete)
         {
             var safeBase = new DirectoryInfo(Constants.SolutionDirectory);
             for (var scratch = toDelete; scratch.Parent != null; scratch = scratch.Parent)

Tst/UnitTests/UnitTests.csproj

@@ -16,5 +16,6 @@
   <ItemGroup>
     <ProjectReference Include="..\..\Src\PChecker\CheckerCore\CheckerCore.csproj" />
     <ProjectReference Include="..\..\Src\PCompiler\CompilerCore\CompilerCore.csproj" />
+    <ProjectReference Include="..\..\Src\PCompiler\PCommandLine\PCommandLine.csproj" />
   </ItemGroup>
 </Project>