Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Added test for generated logs
Browse files Browse the repository at this point in the history
Christine Zhou committed Jan 23, 2025

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
1 parent db51c8e commit 0179067
Showing 9 changed files with 263 additions and 10 deletions.
5 changes: 1 addition & 4 deletions Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs
Original file line number Diff line number Diff line change
@@ -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)
{
6 changes: 3 additions & 3 deletions Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs
Original file line number Diff line number Diff line change
@@ -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
11 changes: 11 additions & 0 deletions Tst/CorrectLogs/bugs2/Main.coverage.txt
Original file line number Diff line number Diff line change
@@ -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

103 changes: 103 additions & 0 deletions Tst/CorrectLogs/bugs2/trace_0_0.trace.json
Original file line number Diff line number Diff line change
@@ -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"
}
}
]
17 changes: 17 additions & 0 deletions Tst/CorrectLogs/bugs2/trace_0_0.txt
Original file line number Diff line number Diff line change
@@ -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).
124 changes: 124 additions & 0 deletions Tst/UnitTests/PCheckerLogGeneratorTests.cs
Original file line number Diff line number Diff line change
@@ -0,0 +1,124 @@
using System;
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);
TestAssertions.SafeDeleteDirectory(tempDir);
}

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

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;
}
}
2 changes: 1 addition & 1 deletion Tst/UnitTests/Runners/PCheckerRunner.cs
Original file line number Diff line number Diff line change
@@ -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);
4 changes: 2 additions & 2 deletions Tst/UnitTests/TestAssertions.cs
Original file line number Diff line number Diff line change
@@ -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)
1 change: 1 addition & 0 deletions Tst/UnitTests/UnitTests.csproj
Original file line number Diff line number Diff line change
@@ -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>

0 comments on commit 0179067

Please sign in to comment.