Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 7 additions & 6 deletions Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs
Original file line number Diff line number Diff line change
Expand Up @@ -241,12 +241,13 @@ public string GetText(CheckerConfiguration checkerConfiguration, string prefix =
totalExploredSchedules,
totalExploredSchedules == 1 ? string.Empty : "s");

report.AppendLine();
report.AppendFormat(
"{0} Explored {1} timeline{2}",
prefix.Equals("...") ? "....." : prefix,
ExploredTimelines.Count,
ExploredTimelines.Count == 1 ? string.Empty : "s");
// Comment out this part until feedback strategy error is fixed
// report.AppendLine();
// report.AppendFormat(
// "{0} Explored {1} timeline{2}",
// prefix.Equals("...") ? "....." : prefix,
// ExploredTimelines.Count,
// ExploredTimelines.Count == 1 ? string.Empty : "s");

if (totalExploredSchedules > 0 &&
NumOfFoundBugs > 0)
Expand Down
4 changes: 0 additions & 4 deletions Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs
Original file line number Diff line number Diff line change
Expand Up @@ -629,10 +629,6 @@ private void RunNextIteration(int schedule)
}

ConstructReproducableTrace(runtime);
if (_checkerConfiguration.OutputDirectory != null)
{
TryEmitTraces(_checkerConfiguration.OutputDirectory, "trace_0");
}
}
}
finally
Expand Down
18 changes: 18 additions & 0 deletions Src/PChecker/CheckerCore/Testing/TestingProcess.cs
Original file line number Diff line number Diff line change
Expand Up @@ -87,6 +87,11 @@ private async Task RunAsync()
Console.WriteLine($"Checker found a bug.");
}

if ((!_checkerConfiguration.PerformFullExploration && TestingEngine.TestReport.NumOfFoundBugs > 0))
{
await EmitTraces();
}

// Closes the remote notification listener.
if (_checkerConfiguration.IsVerbose)
{
Expand Down Expand Up @@ -115,6 +120,19 @@ private TestingProcess(CheckerConfiguration checkerConfiguration)
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.
/// </summary>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,5 @@
<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).
2 changes: 1 addition & 1 deletion Tst/UnitTests/PCheckerLogGeneratorTests.cs
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ private void AssertLog(string generatedDir, string expectedDir)
string generatedFilePath = Path.Combine(generatedDir, fileName);
string expectedFilePath = Path.Combine(expectedDir, fileName);

if (fileName == "trace_0_0.trace.json")
if (fileName == "Main_0_0.trace.json")
{
// Perform "Is JSON Included" check for this specific file
if (!IsJsonContentIncluded(generatedFilePath, expectedFilePath))
Expand Down
Loading