diff --git a/Src/PChecker/CheckerCore/CheckerConfiguration.cs b/Src/PChecker/CheckerCore/CheckerConfiguration.cs
index 57706a2b4..b1f183180 100644
--- a/Src/PChecker/CheckerCore/CheckerConfiguration.cs
+++ b/Src/PChecker/CheckerCore/CheckerConfiguration.cs
@@ -229,7 +229,7 @@ public int MaxSchedulingSteps
/// Defaults to true.
///
[DataMember]
- public bool IsJsonLogEnabled { get; set; } = true;
+ public bool IsJsonLogEnabled { get; set; } = false;
///
/// If specified, requests a custom runtime log to be used instead of the default.
diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs
index 24fd70057..36b59c305 100644
--- a/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs
+++ b/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs
@@ -105,7 +105,7 @@ public class TestReport
/// Set of hashes of timelines discovered by the scheduler.
///
[DataMember]
- public HashSet ExploredTimelines = new();
+ public Dictionary ExploredTimelines = new();
///
/// Number of schedulings that satisfies the pattern.
diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs
index 876873d3e..5d8088d73 100644
--- a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs
+++ b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs
@@ -113,9 +113,25 @@ public class TestingEngine
{
DefaultIgnoreCondition = JsonIgnoreCondition.WhenWritingNull,
PropertyNamingPolicy = JsonNamingPolicy.CamelCase,
- WriteIndented = true
+ WriteIndented = true,
+ Converters = { new EncodingConverter() }
};
+ internal class EncodingConverter : JsonConverter
+ {
+ public override Encoding Read(ref Utf8JsonReader reader, Type typeToConvert, JsonSerializerOptions options)
+ {
+ var name = reader.GetString();
+ if (name == null)
+ return null;
+ return Encoding.GetEncoding(name);
+ }
+ public override void Write(Utf8JsonWriter writer, Encoding value, JsonSerializerOptions options)
+ {
+ writer.WriteStringValue(value.WebName);
+ }
+ }
+
///
/// The profiler.
///
@@ -751,12 +767,18 @@ public object RecursivelyReplaceNullWithString(object obj)
{
return "null";
}
-
- if (obj is Dictionary dictionary)
- {
+ if (obj is Dictionary dictionaryStr) {
var newDictionary = new Dictionary();
- foreach (var item in dictionary)
- {
+ foreach (var item in dictionaryStr) {
+ var newVal = RecursivelyReplaceNullWithString(item.Value);
+ if (newVal != null)
+ newDictionary[item.Key] = newVal;
+ }
+ return newDictionary;
+ }
+ else if (obj is Dictionary dictionaryInt) {
+ var newDictionary = new Dictionary();
+ foreach (var item in dictionaryInt) {
var newVal = RecursivelyReplaceNullWithString(item.Value);
if (newVal != null)
newDictionary[item.Key] = newVal;
@@ -1016,8 +1038,9 @@ private void GatherTestingStatistics(ControlledRuntime runtime, TimelineObserver
var coverageInfo = runtime.GetCoverageInfo();
report.CoverageInfo.Merge(coverageInfo);
TestReport.Merge(report);
-
- TestReport.ExploredTimelines.Add(timelineObserver.GetTimelineHash());
+ var timelineHash = timelineObserver.GetTimelineHash();
+ TestReport.ExploredTimelines[timelineHash] =
+ TestReport.ExploredTimelines.GetValueOrDefault(timelineHash, 0) + 1;
// Also save the graph snapshot of the last iteration, if there is one.
Graph = coverageInfo.CoverageGraph;
// Also save the graph snapshot of the last schedule, if there is one.
@@ -1156,4 +1179,4 @@ public void SetLogger(TextWriter logger)
ErrorReporter.Logger = logger;
}
}
-}
\ No newline at end of file
+}
diff --git a/Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs b/Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs
index ccacf6fcf..4aef965ae 100644
--- a/Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs
+++ b/Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs
@@ -334,5 +334,10 @@ private string DeclarationName(IPDecl method)
{
return method.Name.Length > 0 ? method.Name : $"at {locationResolver.GetLocation(method.SourceLocation)}";
}
+
+ public string SpecObservesSetIncompleteWarning(ParserRuleContext ctx, PEvent ev, Machine machine)
+ {
+ return $"[!Warning!]\n[{locationResolver.GetLocation(ctx, ctx.start)}] Event {ev.Name} is not in the observes list of the spec machine {machine.Name}. The event-handler is never triggered as the event is not observed by the spec.\n[!Warning!]";
+ }
}
}
\ No newline at end of file
diff --git a/Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs b/Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs
index 00e12c244..402a5fc5d 100644
--- a/Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs
+++ b/Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs
@@ -117,5 +117,7 @@ Exception DuplicateStartState(
Exception IllegalChooseSubExprType(PParser.ChooseExprContext context, PLanguageType subExprType);
Exception IllegalFunctionUsedInSpecMachine(Function function, Machine callerOwner);
+
+ String SpecObservesSetIncompleteWarning(ParserRuleContext loc, PEvent ev, Machine machine);
}
}
\ No newline at end of file
diff --git a/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs b/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs
index aac694afb..2257d5a6a 100644
--- a/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs
+++ b/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs
@@ -20,7 +20,7 @@ public static Scope AnalyzeCompilationUnit(ICompilerConfiguration config,
// Step 2: Validate machine specifications
foreach (var machine in globalScope.Machines)
{
- MachineChecker.Validate(handler, machine);
+ MachineChecker.Validate(handler, machine, config);
}
// Step 3: Fill function bodies
diff --git a/Src/PCompiler/CompilerCore/TypeChecker/MachineChecker.cs b/Src/PCompiler/CompilerCore/TypeChecker/MachineChecker.cs
index 628d9cac5..b8f0a5cdd 100644
--- a/Src/PCompiler/CompilerCore/TypeChecker/MachineChecker.cs
+++ b/Src/PCompiler/CompilerCore/TypeChecker/MachineChecker.cs
@@ -11,13 +11,34 @@ namespace Plang.Compiler.TypeChecker
{
public static class MachineChecker
{
- public static void Validate(ITranslationErrorHandler handler, Machine machine)
+ public static void Validate(ITranslationErrorHandler handler, Machine machine, ICompilerConfiguration job)
{
var startState = FindStartState(machine, handler);
var startStatePayloadType = GetStatePayload(startState);
Debug.Assert(startStatePayloadType.IsSameTypeAs(machine.PayloadType));
ValidateHandlers(handler, machine);
ValidateTransitions(handler, machine);
+ // special validation for monitors:
+ // ensure that each eventhandler is in the observe set.
+ ValidateSpecObservesList(handler, machine, job);
+ }
+
+ private static void ValidateSpecObservesList(ITranslationErrorHandler handler, Machine machine, ICompilerConfiguration job)
+ {
+ if (machine.IsSpec)
+ {
+ foreach (var state in machine.AllStates())
+ {
+ foreach (var pair in state.AllEventHandlers)
+ {
+ if (!machine.Observes.Events.Contains(pair.Key))
+ {
+ job.Output.WriteWarning(
+ handler.SpecObservesSetIncompleteWarning(pair.Value.SourceLocation, pair.Key, machine));
+ }
+ }
+ }
+ }
}
private static void ValidateHandlers(ITranslationErrorHandler handler, Machine machine)
diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/Correct/monitorobserves/observes.p b/Tst/RegressionTests/Feature1SMLevelDecls/Correct/monitorobserves/observes.p
new file mode 100644
index 000000000..03855f714
--- /dev/null
+++ b/Tst/RegressionTests/Feature1SMLevelDecls/Correct/monitorobserves/observes.p
@@ -0,0 +1,14 @@
+event e1;
+event e2;
+
+spec Invariant1 observes e1 {
+ start state Init {
+ on e2 goto Init;
+ }
+}
+
+machine Main {
+ start state Init {
+
+ }
+}
\ No newline at end of file