Skip to content
Closed
Show file tree
Hide file tree
Changes from 1 commit
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
3 changes: 0 additions & 3 deletions Docs/docs/advanced/debuggingerror.md
Original file line number Diff line number Diff line change
Expand Up @@ -20,13 +20,10 @@ p check -tc tcAbstractServer -s 100
... Emitting traces:
..... Writing PCheckerOutput/BugFinding/ClientServer_0_0.txt
..... Writing PCheckerOutput/BugFinding/ClientServer_0_0.trace.json
..... Writing PCheckerOutput/BugFinding/ClientServer_0_0.dgml
..... Writing PCheckerOutput/BugFinding/ClientServer_0_0.schedule
... Elapsed 0.2196562 sec.
... Emitting coverage reports:
..... Writing PCheckerOutput/BugFinding/ClientServer.dgml
..... Writing PCheckerOutput/BugFinding/ClientServer.coverage.txt
..... Writing PCheckerOutput/BugFinding/ClientServer.sci
... Checking statistics:
..... Found 1 bug.
... Scheduling statistics:
Expand Down
5 changes: 0 additions & 5 deletions Docs/docs/getstarted/usingP.md
Original file line number Diff line number Diff line change
Expand Up @@ -245,9 +245,7 @@ p check -tc tcSingleClient -s 100
..... Schedule #90
..... Schedule #100
... Emitting coverage reports:
..... Writing PCheckerOutput/BugFinding/ClientServer.dgml
..... Writing PCheckerOutput/BugFinding/ClientServer.coverage.txt
..... Writing PCheckerOutput/BugFinding/ClientServer.sci
... Checking statistics:
..... Found 0 bugs.
... Scheduling statistics:
Expand Down Expand Up @@ -278,13 +276,10 @@ p check -tc tcAbstractServer -s 100
... Emitting traces:
..... Writing PCheckerOutput/BugFinding/ClientServer_0_0.txt
..... Writing PCheckerOutput/BugFinding/ClientServer_0_0.trace.json
..... Writing PCheckerOutput/BugFinding/ClientServer_0_0.dgml
..... Writing PCheckerOutput/BugFinding/ClientServer_0_0.schedule
... Elapsed 0.2264114 sec.
... Emitting coverage reports:
..... Writing PCheckerOutput/BugFinding/ClientServer.dgml
..... Writing PCheckerOutput/BugFinding/ClientServer.coverage.txt
..... Writing PCheckerOutput/BugFinding/ClientServer.sci
... Checking statistics:
..... Found 1 bug.
... Scheduling statistics:
Expand Down
2 changes: 0 additions & 2 deletions Docs/docs/manual/foriegntypesfunctions.md
Original file line number Diff line number Diff line change
Expand Up @@ -123,9 +123,7 @@ p check -v
<PrintLog> --------------
... ### Process 0 is terminating
... Emitting coverage reports:
..... Writing PCheckerOutput/BugFinding/PriorityQueue.dgml
..... Writing PCheckerOutput/BugFinding/PriorityQueue.coverage.txt
..... Writing PCheckerOutput/BugFinding/PriorityQueue.sci
... Checking statistics:
..... Found 0 bugs.
... Scheduling statistics:
Expand Down
24 changes: 0 additions & 24 deletions Src/PChecker/CheckerCore/CheckerConfiguration.cs
Original file line number Diff line number Diff line change
Expand Up @@ -204,20 +204,6 @@ public int MaxSchedulingSteps
/// </summary>
public bool DebugActivityCoverage;

/// <summary>
/// Is DGML graph showing all test schedules or just one "bug" schedule.
/// False means all, and True means only the schedule containing a bug.
/// </summary>
[DataMember]
public bool IsDgmlBugGraph;

/// <summary>
/// If specified, requests a DGML graph of the schedule that contains a bug, if a bug is found.
/// This is different from a coverage activity graph, as it will also show state machine instances.
/// </summary>
[DataMember]
public bool IsDgmlGraphEnabled { get; set; }

/// <summary>
/// Produce an XML formatted runtime log file.
/// </summary>
Expand Down Expand Up @@ -489,16 +475,6 @@ public CheckerConfiguration WithActivityCoverageEnabled(bool isEnabled = true)
return this;
}

/// <summary>
/// Updates the checkerConfiguration with DGML graph generation enabled or disabled.
/// </summary>
/// <param name="isEnabled">If true, then enables DGML graph generation.</param>
public CheckerConfiguration WithDgmlGraphEnabled(bool isEnabled = true)
{
IsDgmlGraphEnabled = isEnabled;
return this;
}

/// <summary>
/// Updates the checkerConfiguration with XML log generation enabled or disabled.
/// </summary>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -1281,7 +1281,7 @@ public CoverageInfo GetCoverageInfo()
var builder = LogWriter.GetLogsOfType<ControlledRuntimeLogGraphBuilder>().FirstOrDefault();
if (builder != null)
{
result.CoverageGraph = builder.SnapshotGraph(CheckerConfiguration.IsDgmlBugGraph);
result.CoverageGraph = builder.SnapshotGraph(true);
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why pass a true value?

}

var eventCoverage = LogWriter.GetLogsOfType<ControlledRuntimeLogEventCoverage>().FirstOrDefault();
Expand Down
6 changes: 1 addition & 5 deletions Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs
Original file line number Diff line number Diff line change
Expand Up @@ -838,17 +838,13 @@ private void InitializeCustomLogging(ControlledRuntime runtime)
}
}

if (_checkerConfiguration.IsDgmlGraphEnabled || _checkerConfiguration.ReportActivityCoverage)
if (_checkerConfiguration.ReportActivityCoverage)
{
// Registers an activity coverage graph builder.
runtime.RegisterLog(new ControlledRuntimeLogGraphBuilder(false)
{
CollapseMachineInstances = _checkerConfiguration.ReportActivityCoverage
});
}

if (_checkerConfiguration.ReportActivityCoverage)
{
// Need this additional logger to get the event coverage report correct
runtime.RegisterLog(new ControlledRuntimeLogEventCoverage());
}
Expand Down
4 changes: 0 additions & 4 deletions Src/PChecker/CheckerCore/Utilities/Reporter.cs
Original file line number Diff line number Diff line change
Expand Up @@ -77,10 +77,6 @@ private static void EmitTestingCoverageOutputFiles(TestReport report, string dir
var coverageFilePath = $"{filePath}.coverage.txt";
Console.WriteLine($"..... Writing {coverageFilePath}");
codeCoverageReporter.EmitCoverageReport(coverageFilePath);

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Lets keep the .sci file around. Only remove things related to dgml.

var serFilePath = $"{filePath}.sci";
Console.WriteLine($"..... Writing {serFilePath}");
report.CoverageInfo.Save(serFilePath);
}
}
}
10 changes: 0 additions & 10 deletions Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs
Original file line number Diff line number Diff line change
Expand Up @@ -76,8 +76,6 @@ public PCheckerOptions()
var advancedGroup = Parser.GetOrCreateGroup("advanced", "Advanced options");
advancedGroup.AddArgument("explore", null, "Keep testing until the bound (e.g. schedule or time) is reached", typeof(bool));
advancedGroup.AddArgument("seed", null, "Specify the random value generator seed", typeof(uint));
advancedGroup.AddArgument("graph-bug", null, "Output a DGML graph of the schedule that found a bug", typeof(bool));
advancedGroup.AddArgument("graph", null, "Output a DGML graph of all test schedules whether a bug was found or not", typeof(bool));
advancedGroup.AddArgument("xml-trace", null, "Specify a filename for XML runtime log output to be written to", typeof(bool));
advancedGroup.AddArgument("psym-args", null, "Specify a concatenated list of additional PSym-specific arguments to pass, each starting with a colon").IsHidden = true;
advancedGroup.AddArgument("jvm-args", null, "Specify a concatenated list of PSym-specific JVM arguments to pass, each starting with a colon").IsHidden = true;
Expand Down Expand Up @@ -272,14 +270,6 @@ private static void UpdateConfigurationWithParsedArgument(CheckerConfiguration c
case "schedules":
checkerConfiguration.TestingIterations = (int)(uint)option.Value;
break;
case "graph":
checkerConfiguration.IsDgmlGraphEnabled = true;
checkerConfiguration.IsDgmlBugGraph = false;
break;
case "graph-bug":
checkerConfiguration.IsDgmlGraphEnabled = true;
checkerConfiguration.IsDgmlBugGraph = true;
break;
case "xml-trace":
checkerConfiguration.IsXmlLogEnabled = true;
break;
Expand Down
Loading