Skip to content

Commit 775d875

Browse files
author
Christine Zhou
committed
Removing dgml and sci file generation
1 parent 10dd56e commit 775d875

File tree

8 files changed

+1
-59
lines changed

8 files changed

+1
-59
lines changed

Docs/docs/advanced/debuggingerror.md

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -20,13 +20,10 @@ p check -tc tcAbstractServer -s 100
2020
... Emitting traces:
2121
..... Writing PCheckerOutput/BugFinding/ClientServer_0_0.txt
2222
..... Writing PCheckerOutput/BugFinding/ClientServer_0_0.trace.json
23-
..... Writing PCheckerOutput/BugFinding/ClientServer_0_0.dgml
2423
..... Writing PCheckerOutput/BugFinding/ClientServer_0_0.schedule
2524
... Elapsed 0.2196562 sec.
2625
... Emitting coverage reports:
27-
..... Writing PCheckerOutput/BugFinding/ClientServer.dgml
2826
..... Writing PCheckerOutput/BugFinding/ClientServer.coverage.txt
29-
..... Writing PCheckerOutput/BugFinding/ClientServer.sci
3027
... Checking statistics:
3128
..... Found 1 bug.
3229
... Scheduling statistics:

Docs/docs/getstarted/usingP.md

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -245,9 +245,7 @@ p check -tc tcSingleClient -s 100
245245
..... Schedule #90
246246
..... Schedule #100
247247
... Emitting coverage reports:
248-
..... Writing PCheckerOutput/BugFinding/ClientServer.dgml
249248
..... Writing PCheckerOutput/BugFinding/ClientServer.coverage.txt
250-
..... Writing PCheckerOutput/BugFinding/ClientServer.sci
251249
... Checking statistics:
252250
..... Found 0 bugs.
253251
... Scheduling statistics:
@@ -278,13 +276,10 @@ p check -tc tcAbstractServer -s 100
278276
... Emitting traces:
279277
..... Writing PCheckerOutput/BugFinding/ClientServer_0_0.txt
280278
..... Writing PCheckerOutput/BugFinding/ClientServer_0_0.trace.json
281-
..... Writing PCheckerOutput/BugFinding/ClientServer_0_0.dgml
282279
..... Writing PCheckerOutput/BugFinding/ClientServer_0_0.schedule
283280
... Elapsed 0.2264114 sec.
284281
... Emitting coverage reports:
285-
..... Writing PCheckerOutput/BugFinding/ClientServer.dgml
286282
..... Writing PCheckerOutput/BugFinding/ClientServer.coverage.txt
287-
..... Writing PCheckerOutput/BugFinding/ClientServer.sci
288283
... Checking statistics:
289284
..... Found 1 bug.
290285
... Scheduling statistics:

Docs/docs/manual/foriegntypesfunctions.md

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -123,9 +123,7 @@ p check -v
123123
<PrintLog> --------------
124124
... ### Process 0 is terminating
125125
... Emitting coverage reports:
126-
..... Writing PCheckerOutput/BugFinding/PriorityQueue.dgml
127126
..... Writing PCheckerOutput/BugFinding/PriorityQueue.coverage.txt
128-
..... Writing PCheckerOutput/BugFinding/PriorityQueue.sci
129127
... Checking statistics:
130128
..... Found 0 bugs.
131129
... Scheduling statistics:

Src/PChecker/CheckerCore/CheckerConfiguration.cs

Lines changed: 0 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -204,20 +204,6 @@ public int MaxSchedulingSteps
204204
/// </summary>
205205
public bool DebugActivityCoverage;
206206

207-
/// <summary>
208-
/// Is DGML graph showing all test schedules or just one "bug" schedule.
209-
/// False means all, and True means only the schedule containing a bug.
210-
/// </summary>
211-
[DataMember]
212-
public bool IsDgmlBugGraph;
213-
214-
/// <summary>
215-
/// If specified, requests a DGML graph of the schedule that contains a bug, if a bug is found.
216-
/// This is different from a coverage activity graph, as it will also show state machine instances.
217-
/// </summary>
218-
[DataMember]
219-
public bool IsDgmlGraphEnabled { get; set; }
220-
221207
/// <summary>
222208
/// Produce an XML formatted runtime log file.
223209
/// </summary>
@@ -489,16 +475,6 @@ public CheckerConfiguration WithActivityCoverageEnabled(bool isEnabled = true)
489475
return this;
490476
}
491477

492-
/// <summary>
493-
/// Updates the checkerConfiguration with DGML graph generation enabled or disabled.
494-
/// </summary>
495-
/// <param name="isEnabled">If true, then enables DGML graph generation.</param>
496-
public CheckerConfiguration WithDgmlGraphEnabled(bool isEnabled = true)
497-
{
498-
IsDgmlGraphEnabled = isEnabled;
499-
return this;
500-
}
501-
502478
/// <summary>
503479
/// Updates the checkerConfiguration with XML log generation enabled or disabled.
504480
/// </summary>

Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1278,12 +1278,6 @@ public CoverageInfo GetCoverageInfo()
12781278
var result = CoverageInfo;
12791279
if (result != null)
12801280
{
1281-
var builder = LogWriter.GetLogsOfType<ControlledRuntimeLogGraphBuilder>().FirstOrDefault();
1282-
if (builder != null)
1283-
{
1284-
result.CoverageGraph = builder.SnapshotGraph(CheckerConfiguration.IsDgmlBugGraph);
1285-
}
1286-
12871281
var eventCoverage = LogWriter.GetLogsOfType<ControlledRuntimeLogEventCoverage>().FirstOrDefault();
12881282
if (eventCoverage != null)
12891283
{

Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -838,17 +838,13 @@ private void InitializeCustomLogging(ControlledRuntime runtime)
838838
}
839839
}
840840

841-
if (_checkerConfiguration.IsDgmlGraphEnabled || _checkerConfiguration.ReportActivityCoverage)
841+
if (_checkerConfiguration.ReportActivityCoverage)
842842
{
843843
// Registers an activity coverage graph builder.
844844
runtime.RegisterLog(new ControlledRuntimeLogGraphBuilder(false)
845845
{
846846
CollapseMachineInstances = _checkerConfiguration.ReportActivityCoverage
847847
});
848-
}
849-
850-
if (_checkerConfiguration.ReportActivityCoverage)
851-
{
852848
// Need this additional logger to get the event coverage report correct
853849
runtime.RegisterLog(new ControlledRuntimeLogEventCoverage());
854850
}

Src/PChecker/CheckerCore/Utilities/Reporter.cs

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -77,10 +77,6 @@ private static void EmitTestingCoverageOutputFiles(TestReport report, string dir
7777
var coverageFilePath = $"{filePath}.coverage.txt";
7878
Console.WriteLine($"..... Writing {coverageFilePath}");
7979
codeCoverageReporter.EmitCoverageReport(coverageFilePath);
80-
81-
var serFilePath = $"{filePath}.sci";
82-
Console.WriteLine($"..... Writing {serFilePath}");
83-
report.CoverageInfo.Save(serFilePath);
8480
}
8581
}
8682
}

Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs

Lines changed: 0 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -76,8 +76,6 @@ public PCheckerOptions()
7676
var advancedGroup = Parser.GetOrCreateGroup("advanced", "Advanced options");
7777
advancedGroup.AddArgument("explore", null, "Keep testing until the bound (e.g. schedule or time) is reached", typeof(bool));
7878
advancedGroup.AddArgument("seed", null, "Specify the random value generator seed", typeof(uint));
79-
advancedGroup.AddArgument("graph-bug", null, "Output a DGML graph of the schedule that found a bug", typeof(bool));
80-
advancedGroup.AddArgument("graph", null, "Output a DGML graph of all test schedules whether a bug was found or not", typeof(bool));
8179
advancedGroup.AddArgument("xml-trace", null, "Specify a filename for XML runtime log output to be written to", typeof(bool));
8280
advancedGroup.AddArgument("psym-args", null, "Specify a concatenated list of additional PSym-specific arguments to pass, each starting with a colon").IsHidden = true;
8381
advancedGroup.AddArgument("jvm-args", null, "Specify a concatenated list of PSym-specific JVM arguments to pass, each starting with a colon").IsHidden = true;
@@ -272,14 +270,6 @@ private static void UpdateConfigurationWithParsedArgument(CheckerConfiguration c
272270
case "schedules":
273271
checkerConfiguration.TestingIterations = (int)(uint)option.Value;
274272
break;
275-
case "graph":
276-
checkerConfiguration.IsDgmlGraphEnabled = true;
277-
checkerConfiguration.IsDgmlBugGraph = false;
278-
break;
279-
case "graph-bug":
280-
checkerConfiguration.IsDgmlGraphEnabled = true;
281-
checkerConfiguration.IsDgmlBugGraph = true;
282-
break;
283273
case "xml-trace":
284274
checkerConfiguration.IsXmlLogEnabled = true;
285275
break;

0 commit comments

Comments
 (0)