Skip to content

Commit 7d910aa

Browse files
ankushdesaiankushdesai
authored
Added better error messages for assertion and ran auto code cleanup. (#831)
1 parent 4762db7 commit 7d910aa

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

52 files changed

+294
-372
lines changed

‎Src/PChecker/CheckerCore/Checker.cs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ namespace PChecker;
99
/// <summary>
1010
/// Checker class that implements the run method which acts as the entry point into the P checker.
1111
/// </summary>
12-
public class Checker
12+
public static class Checker
1313
{
1414
/// <summary>
1515
/// Run the P checker for the given configuration

‎Src/PChecker/CheckerCore/CheckerConfiguration.cs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -379,8 +379,8 @@ public CheckerConfiguration WithPCTStrategy(bool isFair, uint numPrioritySwitchP
379379
/// </summary>
380380
public CheckerConfiguration WithRLStrategy()
381381
{
382-
this.SchedulingStrategy = "rl";
383-
this.IsProgramStateHashingEnabled = true;
382+
SchedulingStrategy = "rl";
383+
IsProgramStateHashingEnabled = true;
384384
return this;
385385
}
386386

@@ -530,7 +530,7 @@ public void SetOutputDirectory()
530530
Directory.Delete(older, true);
531531
}
532532

533-
if(this.SchedulingStrategy != "replay"){
533+
if(SchedulingStrategy != "replay"){
534534
for (var history = MaxHistory - 2; history >= 0; --history)
535535
{
536536
var newer = makeHistoryDirName(history);

‎Src/PChecker/CheckerCore/Coverage/ActivityCoverageReporter.cs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -66,7 +66,7 @@ private static IEnumerable<string> GetEventIds(GraphLink link)
6666
// a fully expanded edge graph has individual links for each event.
6767
if (link.Attributes.TryGetValue("EventId", out var eventId))
6868
{
69-
return new string[] { eventId };
69+
return new[] { eventId };
7070
}
7171

7272
return Array.Empty<string>();
@@ -154,7 +154,7 @@ internal void WriteCoverageText(TextWriter writer)
154154

155155
if (!CoverageInfo.MachinesToStates.ContainsKey(machine))
156156
{
157-
CoverageInfo.MachinesToStates[machine] = new HashSet<string>(new string[] { "ExternalState" });
157+
CoverageInfo.MachinesToStates[machine] = new HashSet<string>(new[] { "ExternalState" });
158158
}
159159

160160
// Per-state data.

‎Src/PChecker/CheckerCore/Coverage/ControlledRuntimeLogEventCoverage.cs

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -107,10 +107,6 @@ internal class ControlledRuntimeLogEventCoverage : IControlledRuntimeLog
107107
private readonly EventCoverage InternalEventCoverage = new EventCoverage();
108108
private Event Dequeued;
109109

110-
public ControlledRuntimeLogEventCoverage()
111-
{
112-
}
113-
114110
public EventCoverage EventCoverage => InternalEventCoverage;
115111

116112
public void OnAssertionFailure(string error)

‎Src/PChecker/CheckerCore/Coverage/ControlledRuntimeLogGraphBuilder.cs

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,6 @@
55
using System.Collections.Generic;
66
using System.IO;
77
using System.Runtime.Serialization;
8-
using System.Text;
9-
using System.Xml.Linq;
108
using PChecker.Runtime.Events;
119
using PChecker.Runtime.Logging;
1210
using PChecker.Runtime.StateMachines;
@@ -40,7 +38,7 @@ private class EventInfo
4038
private readonly Dictionary<string, List<EventInfo>> Inbox = new Dictionary<string, List<EventInfo>>();
4139
private static readonly Dictionary<string, string> EventAliases = new Dictionary<string, string>();
4240
private readonly HashSet<string> Namespaces = new HashSet<string>();
43-
private static readonly char[] TypeSeparators = new char[] { '.', '+' };
41+
private static readonly char[] TypeSeparators = new[] { '.', '+' };
4442

4543
private class DoActionEvent : Event
4644
{
@@ -238,7 +236,7 @@ public void OnHalt(StateMachineId id, int inboxSize)
238236
// Transition to the Halt state.
239237
var source = GetOrCreateChild(id?.Name, id?.Type, stateName);
240238
var target = GetOrCreateChild(id?.Name, id?.Type, "Halt", "Halt");
241-
GetOrCreateEventLink(source, target, new EventInfo() { Event = typeof(HaltEvent).FullName });
239+
GetOrCreateEventLink(source, target, new EventInfo { Event = typeof(HaltEvent).FullName });
242240
}
243241
}
244242

@@ -474,7 +472,7 @@ private EventInfo AddEvent(string targetName, string targetType, string senderNa
474472
Inbox[targetId] = inbox;
475473
}
476474

477-
info = new EventInfo()
475+
info = new EventInfo
478476
{
479477
Name = senderName ?? ExternalCodeName,
480478
Type = senderType ?? ExternalCodeName,

‎Src/PChecker/CheckerCore/Coverage/CoverageInfo.cs

Lines changed: 20 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -81,12 +81,13 @@ public void DeclareStateEvent(string machine, string state, string eventName)
8181

8282
private void InternalAddEvent(string key, string eventName)
8383
{
84-
if (!RegisteredEvents.ContainsKey(key))
84+
if (!RegisteredEvents.TryGetValue(key, out HashSet<string> value))
8585
{
86-
RegisteredEvents.Add(key, new HashSet<string>());
86+
value = new HashSet<string>();
87+
RegisteredEvents.Add(key, value);
8788
}
8889

89-
RegisteredEvents[key].Add(eventName);
90+
value.Add(eventName);
9091
}
9192

9293
/// <summary>
@@ -141,12 +142,13 @@ private void AddState(string machineName, string stateName)
141142
{
142143
Machines.Add(machineName);
143144

144-
if (!MachinesToStates.ContainsKey(machineName))
145+
if (!MachinesToStates.TryGetValue(machineName, out HashSet<string> value))
145146
{
146-
MachinesToStates.Add(machineName, new HashSet<string>());
147+
value = new HashSet<string>();
148+
MachinesToStates.Add(machineName, value);
147149
}
148150

149-
MachinesToStates[machineName].Add(stateName);
151+
value.Add(stateName);
150152
}
151153

152154
/// <summary>
@@ -156,16 +158,14 @@ private void AddState(string machineName, string stateName)
156158
/// <returns>The deserialized coverage info.</returns>
157159
public static CoverageInfo Load(string filename)
158160
{
159-
using (var fs = new FileStream(filename, FileMode.Open))
161+
using var fs = new FileStream(filename, FileMode.Open);
162+
using var reader = XmlDictionaryReader.CreateTextReader(fs, new XmlDictionaryReaderQuotas());
163+
var settings = new DataContractSerializerSettings
160164
{
161-
using (var reader = XmlDictionaryReader.CreateTextReader(fs, new XmlDictionaryReaderQuotas()))
162-
{
163-
var settings = new DataContractSerializerSettings();
164-
settings.PreserveObjectReferences = true;
165-
var ser = new DataContractSerializer(typeof(CoverageInfo), settings);
166-
return (CoverageInfo)ser.ReadObject(reader, true);
167-
}
168-
}
165+
PreserveObjectReferences = true
166+
};
167+
var ser = new DataContractSerializer(typeof(CoverageInfo), settings);
168+
return (CoverageInfo)ser.ReadObject(reader, true);
169169
}
170170

171171
/// <summary>
@@ -174,13 +174,11 @@ public static CoverageInfo Load(string filename)
174174
/// <param name="serFilePath">The path to the file to create.</param>
175175
public void Save(string serFilePath)
176176
{
177-
using (var fs = new FileStream(serFilePath, FileMode.Create))
178-
{
179-
var settings = new DataContractSerializerSettings();
180-
settings.PreserveObjectReferences = true;
181-
var ser = new DataContractSerializer(typeof(CoverageInfo), settings);
182-
ser.WriteObject(fs, this);
183-
}
177+
using var fs = new FileStream(serFilePath, FileMode.Create);
178+
var settings = new DataContractSerializerSettings();
179+
settings.PreserveObjectReferences = true;
180+
var ser = new DataContractSerializer(typeof(CoverageInfo), settings);
181+
ser.WriteObject(fs, this);
184182
}
185183
}
186184
}

‎Src/PChecker/CheckerCore/Exceptions/RuntimeException.cs

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@
33

44
using System;
55
using System.Diagnostics;
6-
using System.Runtime.Serialization;
76

87
namespace PChecker.Exceptions
98
{

‎Src/PChecker/CheckerCore/ExhaustiveEngine.cs

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ public class ExhaustiveEngine
2323
/// <summary>
2424
/// Logger.
2525
/// </summary>
26-
private TextWriter Logger;
26+
private TextWriter _logger;
2727

2828
/// <summary>
2929
/// The testing task cancellation token source.
@@ -44,14 +44,14 @@ public static ExhaustiveEngine Create(CheckerConfiguration checkerConfiguration)
4444
private ExhaustiveEngine(CheckerConfiguration checkerConfiguration)
4545
{
4646
_checkerConfiguration = checkerConfiguration;
47-
Logger = new ConsoleLogger();
47+
_logger = new ConsoleLogger();
4848
CancellationTokenSource = new CancellationTokenSource();
4949
}
5050

5151
/// <summary>
5252
/// Creates the set of arguments for the exhaustive engine.
5353
/// </summary>
54-
private String CreateArguments()
54+
private string CreateArguments()
5555
{
5656
var arguments = new StringBuilder();
5757

@@ -91,7 +91,7 @@ private String CreateArguments()
9191

9292
if (_checkerConfiguration.IsVerbose)
9393
{
94-
arguments.Append($"--verbose 1 ");
94+
arguments.Append("--verbose 1 ");
9595
}
9696

9797
arguments.Append($"--schedules {_checkerConfiguration.TestingIterations} ");
@@ -148,19 +148,19 @@ private async Task CreateTaskFromProcess(Process proc)
148148
switch (proc.ExitCode)
149149
{
150150
case 0:
151-
Logger.WriteLine($"... Checker run finished.");
151+
_logger.WriteLine("... Checker run finished.");
152152
break;
153153
case 2:
154-
Logger.WriteLine($"... Checker found a bug.");
154+
_logger.WriteLine("... Checker found a bug.");
155155
break;
156156
case 3:
157-
Logger.WriteLine($"... Checker timed out.");
157+
_logger.WriteLine("... Checker timed out.");
158158
break;
159159
case 4:
160-
Logger.WriteLine($"... Checker ran out of memory.");
160+
_logger.WriteLine("... Checker ran out of memory.");
161161
break;
162162
default:
163-
Logger.WriteLine($"... Checker run exited with code {proc.ExitCode}.");
163+
_logger.WriteLine($"... Checker run exited with code {proc.ExitCode}.");
164164
break;
165165
}
166166
}
@@ -182,7 +182,7 @@ public void Run()
182182

183183
if (_checkerConfiguration.IsVerbose)
184184
{
185-
Logger.WriteLine($"... Executing command: java {arguments}");
185+
_logger.WriteLine($"... Executing command: java {arguments}");
186186
}
187187

188188
var proc = CreateProcess(Directory.GetCurrentDirectory(), "java", arguments);
@@ -196,15 +196,15 @@ public void Run()
196196
interrupted = true;
197197
CancellationTokenSource.Cancel();
198198
Cleanup(proc, task);
199-
Logger.WriteLine($"... Checker run terminated.");
199+
_logger.WriteLine("... Checker run terminated.");
200200
};
201201

202202
Console.CancelKeyPress += delegate
203203
{
204204
interrupted = true;
205205
CancellationTokenSource.Cancel();
206206
Cleanup(proc, task);
207-
Logger.WriteLine($"... Checker run cancelled by user.");
207+
_logger.WriteLine("... Checker run cancelled by user.");
208208
};
209209

210210
try
@@ -217,14 +217,14 @@ public void Run()
217217
{
218218
if (!interrupted)
219219
{
220-
Logger.WriteLine($"... Checker run forcefully cancelled on timeout.");
220+
_logger.WriteLine("... Checker run forcefully cancelled on timeout.");
221221
}
222222
Error.Report($"{ex.Message}");
223223
}
224224
}
225225
catch (Exception ex)
226226
{
227-
Logger.WriteLine($"... Checker failed due to an internal error: {ex}");
227+
_logger.WriteLine($"... Checker failed due to an internal error: {ex}");
228228
Error.Report($"{ex.Message}");
229229
}
230230
finally

‎Src/PChecker/CheckerCore/Random/IRandomValueGenerator.cs

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
// Copyright (c) Microsoft Corporation.
22
// Licensed under the MIT License.
33

4-
using System;
5-
64
namespace PChecker.Random
75
{
86
/// <summary>

‎Src/PChecker/CheckerCore/Runtime/Events/Event.cs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ public virtual IPValue Clone()
3636

3737
public object ToDict()
3838
{
39-
return this.GetType().Name;
39+
return GetType().Name;
4040
}
4141

4242
public override bool Equals(object obj)

0 commit comments

Comments
 (0)