Movatterモバイル変換

[0]ホーム
URL:

Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly

 Sign up
Appearance settings
/PPublic

Commit27a1d2f

Browse files
ChristineZh0uChristine Zhou
and
Christine Zhou
authored
Added test for generated PChecker logs (#815)
Co-authored-by: Christine Zhou <zhouchrs@amazon.com>
1 parentdb51c8e commit27a1d2f

File tree

9 files changed

+264
-10
lines changed

9 files changed

+264
-10
lines changed

‎Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -165,9 +165,7 @@ public override void Write(Utf8JsonWriter writer, Encoding value, JsonSerializer
165165
/// A guard for printing info.
166166
/// </summary>
167167
privateintPrintGuard;
168-
169-
privateStreamWriterTimelineFileStream;
170-
168+
171169

172170
/// <summary>
173171
/// Creates a new systematic testing engine.
@@ -272,7 +270,6 @@ private TestingEngine(CheckerConfiguration checkerConfiguration, TestMethodInfo
272270

273271
CancellationTokenSource=newCancellationTokenSource();
274272
PrintGuard=1;
275-
TimelineFileStream=newStreamWriter(checkerConfiguration.OutputDirectory+"timeline.txt");
276273
// Initialize a new instance of JsonVerboseLogs if running in verbose mode.
277274
if(checkerConfiguration.IsVerbose)
278275
{

‎Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@
1111

1212
namespacePlang.Options
1313
{
14-
internalsealedclassPCheckerOptions
14+
publicsealedclassPCheckerOptions
1515
{
1616
/// <summary>
1717
/// The command line parser to use.
@@ -21,7 +21,7 @@ internal sealed class PCheckerOptions
2121
/// <summary>
2222
/// Initializes a new instance of the <see cref="PCheckerOptions"/> class.
2323
/// </summary>
24-
internalPCheckerOptions()
24+
publicPCheckerOptions()
2525
{
2626
Parser=newCommandLineArgumentParser("p check",
2727
"The P checker enables systematic exploration of a specified P test case, it generates "+
@@ -87,7 +87,7 @@ internal PCheckerOptions()
8787
/// Parses the command line options and returns a checkerConfiguration.
8888
/// </summary>
8989
/// <returns>The CheckerConfiguration object populated with the parsed command line options.</returns>
90-
internalCheckerConfigurationParse(string[]args)
90+
publicCheckerConfigurationParse(string[]args)
9191
{
9292
varconfiguration=CheckerConfiguration.Create();
9393
try
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
Total event coverage: 100.0%
2+
============================
3+
StateMachine: Main
4+
==================
5+
Event coverage: 100.0%
6+
7+
State: S
8+
State event coverage: 100.0%
9+
Events received: x
10+
Events sent: a, x
11+
Lines changed: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,103 @@
1+
[
2+
{
3+
"type":"CreateStateMachine",
4+
"details": {
5+
"log":"Main(1) was created by task\u00272\u0027.",
6+
"id":"Main(1)",
7+
"payload":"null",
8+
"clock": {
9+
"Main(1)":1
10+
}
11+
}
12+
},
13+
{
14+
"type":"StateTransition",
15+
"details": {
16+
"log":"Main(1) enters state\u0027S\u0027.",
17+
"id":"Main(1)",
18+
"state":"S",
19+
"payload":"null",
20+
"isEntry":true,
21+
"clock": {
22+
"Main(1)":2
23+
}
24+
}
25+
},
26+
{
27+
"type":"RaiseEvent",
28+
"details": {
29+
"log":"\u0027Main(1)\u0027 raised event\u0027x with payload (\u003Ca,3,\u003E)\u0027 in state\u0027S\u0027.",
30+
"id":"Main(1)",
31+
"event":"x",
32+
"state":"S",
33+
"payload": {
34+
"0": {},
35+
"1": {}
36+
},
37+
"clock": {
38+
"Main(1)":3
39+
}
40+
}
41+
},
42+
{
43+
"type":"RaiseEvent",
44+
"details": {
45+
"log":"\u0027Main(1)\u0027 raised event\u0027a with payload (3)\u0027 in state\u0027S\u0027.",
46+
"id":"Main(1)",
47+
"event":"a",
48+
"state":"S",
49+
"payload":3,
50+
"clock": {
51+
"Main(1)":4
52+
}
53+
}
54+
},
55+
{
56+
"type":"StateTransition",
57+
"details": {
58+
"log":"Main(1) exits state\u0027S\u0027.",
59+
"id":"Main(1)",
60+
"state":"S",
61+
"payload":"null",
62+
"isEntry":false,
63+
"clock": {
64+
"Main(1)":5
65+
}
66+
}
67+
},
68+
{
69+
"type":"PopStateUnhandledEvent",
70+
"details": {
71+
"log":"Main(1) popped state S due to unhandled event\u0027a\u0027.",
72+
"id":"Main(1)",
73+
"event":"a",
74+
"state":"S",
75+
"payload":"null",
76+
"clock": {
77+
"Main(1)":6
78+
}
79+
}
80+
},
81+
{
82+
"type":"ExceptionThrown",
83+
"details": {
84+
"log":"Main(1) running action\u0027\u0027 in state\u0027S\u0027 threw exception\u0027UnhandledEventException\u0027.",
85+
"id":"Main(1)",
86+
"state":"S",
87+
"payload":"null",
88+
"action":"",
89+
"exception":"UnhandledEventException",
90+
"clock": {
91+
"Main(1)":7
92+
}
93+
}
94+
},
95+
{
96+
"type":"AssertionFailure",
97+
"details": {
98+
"log":"Main(1) received event\u0027PImplementation.a\u0027 that cannot be handled.",
99+
"error":"Main(1) received event\u0027PImplementation.a\u0027 that cannot be handled.",
100+
"payload":"null"
101+
}
102+
}
103+
]
Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
<TestLog> Running test 'DefaultImpl'.
2+
<CreateLog> Main(1) was created by task '2'.
3+
<StateLog> Main(1) enters state 'S'.
4+
<RaiseLog> 'Main(1)' raised event 'x with payload (<a,3,>)' in state 'S'.
5+
<RaiseLog> 'Main(1)' raised event 'a with payload (3)' in state 'S'.
6+
<StateLog> Main(1) exits state 'S'.
7+
<PopLog> Main(1) popped state S due to unhandled event 'a'.
8+
<ExceptionLog> Main(1) running action '' in state 'S' threw exception 'UnhandledEventException'.
9+
<ErrorLog> Main(1) received event 'PImplementation.a' that cannot be handled.
10+
<StrategyLog> Found bug using 'random' strategy.
11+
<StrategyLog> Checking statistics:
12+
<StrategyLog> Found 1 bug.
13+
<StrategyLog> Scheduling statistics:
14+
<StrategyLog> Explored 1 schedule
15+
<StrategyLog> Explored 1 timeline
16+
<StrategyLog> Found 100.00% buggy schedules.
17+
<StrategyLog> Number of scheduling points in terminating schedules: 2 (min), 2 (avg), 2 (max).
Lines changed: 125 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,125 @@
1+
usingSystem;
2+
usingSystem.Diagnostics;
3+
usingSystem.IO;
4+
usingSystem.Linq;
5+
usingNewtonsoft.Json.Linq;
6+
usingNUnit.Framework;
7+
usingPChecker;
8+
usingUnitTests.Core;
9+
usingUnitTests.Runners;
10+
usingPlang.Options;
11+
namespaceUnitTests;
12+
13+
[TestFixture]
14+
[Parallelizable(ParallelScope.Children)]
15+
publicclassPCheckerLogGeneratorTests
16+
{
17+
[Test]
18+
publicvoidTestLogGenerator()
19+
{
20+
vartempDir=Directory.CreateDirectory(Path.Combine(Constants.ScratchParentDirectory,"TestLogGenerator"));
21+
varsrcPath=newFileInfo(Path.Combine(Constants.SolutionDirectory,"Tst","RegressionTests",
22+
"Feature1SMLevelDecls","DynamicError","bug2","bug2.p"));
23+
vardllPath=Path.Combine(Constants.ScratchParentDirectory,"TestLogGenerator","CSharp","net8.0","Main.dll");
24+
varexpectedPath=Path.Combine(Constants.SolutionDirectory,"Tst","CorrectLogs","bugs2");
25+
26+
varrunner=newPCheckerRunner([srcPath]);
27+
runner.DoCompile(tempDir);
28+
29+
varconfiguration=newPCheckerOptions().Parse([dllPath,"-o",tempDir.ToString()]);
30+
Checker.Run(configuration);
31+
32+
AssertLog(tempDir+"/BugFinding",expectedPath);
33+
}
34+
35+
privatevoidAssertLog(stringgeneratedDir,stringexpectedDir)
36+
{
37+
if(!Directory.Exists(generatedDir)||!Directory.Exists(expectedDir))
38+
{
39+
Assert.Fail("One or both directories do not exist.");
40+
}
41+
42+
vargeneratedFiles=Directory.GetFiles(generatedDir).Select(Path.GetFileName).ToHashSet();
43+
varexpectedFiles=Directory.GetFiles(expectedDir).Select(Path.GetFileName).ToHashSet();
44+
45+
foreach(varfileNameinexpectedFiles.Intersect(generatedFiles))
46+
{
47+
stringgeneratedFilePath=Path.Combine(generatedDir,fileName);
48+
stringexpectedFilePath=Path.Combine(expectedDir,fileName);
49+
50+
if(fileName=="trace_0_0.trace.json")
51+
{
52+
// Perform "Is JSON Included" check for this specific file
53+
if(!IsJsonContentIncluded(generatedFilePath,expectedFilePath))
54+
{
55+
Assert.Fail($"Test Failed\nContent of{expectedFilePath} is not fully included in{generatedFilePath}");
56+
}
57+
}
58+
else
59+
{
60+
// Perform exact match for other files
61+
if(!File.ReadAllBytes(generatedFilePath).SequenceEqual(File.ReadAllBytes(expectedFilePath)))
62+
{
63+
Assert.Fail($"Test Failed\nFiles differ:{fileName}\nGenerated File:{generatedFilePath}\nExpected File:{expectedFilePath}");
64+
}
65+
}
66+
}
67+
68+
// Check for missing files in generatedDir
69+
foreach(varfileinexpectedFiles.Except(generatedFiles))
70+
{
71+
Assert.Fail($"Test Failed\nMissing expected file in{generatedDir}:{file}");
72+
}
73+
Console.WriteLine("Test Succeeded");
74+
}
75+
76+
privatestaticboolIsJsonContentIncluded(stringgeneratedFilePath,stringexpectedFilePath)
77+
{
78+
vargeneratedJson=JToken.Parse(File.ReadAllText(generatedFilePath));
79+
varexpectedJson=JToken.Parse(File.ReadAllText(expectedFilePath));
80+
81+
returnIsSubset(expectedJson,generatedJson);
82+
}
83+
84+
privatestaticboolIsSubset(JTokensubset,JTokensuperset)
85+
{
86+
if(JToken.DeepEquals(subset,superset))
87+
{
88+
returntrue;
89+
}
90+
91+
if(subset.Type==JTokenType.Object&&superset.Type==JTokenType.Object)
92+
{
93+
varsubsetObj=(JObject)subset;
94+
varsupersetObj=(JObject)superset;
95+
96+
foreach(varpropertyinsubsetObj.Properties())
97+
{
98+
if(!supersetObj.TryGetValue(property.Name,outvarsupersetValue)||!IsSubset(property.Value,supersetValue))
99+
{
100+
returnfalse;
101+
}
102+
}
103+
104+
returntrue;
105+
}
106+
107+
if(subset.Type==JTokenType.Array&&superset.Type==JTokenType.Array)
108+
{
109+
varsubsetArray=(JArray)subset;
110+
varsupersetArray=(JArray)superset;
111+
112+
foreach(varsubsetIteminsubsetArray)
113+
{
114+
if(!supersetArray.Any(supersetItem=>IsSubset(subsetItem,supersetItem)))
115+
{
116+
returnfalse;
117+
}
118+
}
119+
120+
returntrue;
121+
}
122+
123+
returnfalse;
124+
}
125+
}

‎Tst/UnitTests/Runners/PCheckerRunner.cs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -155,7 +155,7 @@ private int RunPChecker(string directory, string dllPath, out string stdout, out
155155
returnProcessHelper.RunWithOutput(directory,outstdout,outstderr,"dotnet",dllPath);
156156
}
157157

158-
privateintDoCompile(DirectoryInfoscratchDirectory)
158+
publicintDoCompile(DirectoryInfoscratchDirectory)
159159
{
160160
varcompiler=newCompiler();
161161
varoutputStream=newTestExecutionStream(scratchDirectory);

‎Tst/UnitTests/TestAssertions.cs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,8 @@ public static void AssertTestCase(CompilerTestCase testCase)
2222
// Delete ONLY if inside the solution directory
2323
SafeDeleteDirectory(testCase.ScratchDirectory);
2424
}
25-
26-
privatestaticvoidSafeDeleteDirectory(DirectoryInfotoDelete)
25+
26+
publicstaticvoidSafeDeleteDirectory(DirectoryInfotoDelete)
2727
{
2828
varsafeBase=newDirectoryInfo(Constants.SolutionDirectory);
2929
for(varscratch=toDelete;scratch.Parent!=null;scratch=scratch.Parent)

‎Tst/UnitTests/UnitTests.csproj‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,5 +16,6 @@
1616
<ItemGroup>
1717
<ProjectReferenceInclude="..\..\Src\PChecker\CheckerCore\CheckerCore.csproj" />
1818
<ProjectReferenceInclude="..\..\Src\PCompiler\CompilerCore\CompilerCore.csproj" />
19+
<ProjectReferenceInclude="..\..\Src\PCompiler\PCommandLine\PCommandLine.csproj" />
1920
</ItemGroup>
2021
</Project>

0 commit comments

Comments
 (0)
[8]ページ先頭
©2009-2025 Movatter.jp