Merge Recent Bug Fixes

Src/PChecker/CheckerCore/CheckerConfiguration.cs

@@ -229,7 +229,7 @@ public int MaxSchedulingSteps
         /// Defaults to true.
         /// </summary>
         [DataMember]
-        public bool IsJsonLogEnabled { get; set; } = true;
+        public bool IsJsonLogEnabled { get; set; } = false;
 
         /// <summary>
         /// If specified, requests a custom runtime log to be used instead of the default.

Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs

@@ -105,7 +105,7 @@ public class TestReport
         /// Set of hashes of timelines discovered by the scheduler.
         /// </summary>
         [DataMember]
-        public HashSet<int> ExploredTimelines = new();
+        public Dictionary<int, int> ExploredTimelines = new();
 
         /// <summary>
         /// Number of schedulings that satisfies the pattern.

Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs

@@ -68,12 +68,12 @@
         /// <summary>
         /// Pattern coverage observer if pattern is provided
         /// </summary>
         private EventPatternObserver? _eventPatternObserver;
 
         /// <summary>
         /// Monitors conflict operations used by the POS Strategy.
         /// </summary>
         private ConflictOpMonitor? _conflictOpObserver;
 
         /// <summary>
         /// Random value generator used by the scheduling strategies.
@@ -113,9 +113,25 @@
         {
             DefaultIgnoreCondition = JsonIgnoreCondition.WhenWritingNull,
             PropertyNamingPolicy = JsonNamingPolicy.CamelCase,
-            WriteIndented = true
+            WriteIndented = true,
+            Converters = { new EncodingConverter() }
         };
 
+        internal class EncodingConverter : JsonConverter<Encoding>
+        {
+            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);
+            }
+        }
+
         /// <summary>
         /// The profiler.
         /// </summary>
@@ -751,12 +767,18 @@
             {
                 return "null";
             }
-
-            if (obj is Dictionary<string, object> dictionary)
-            {
+            if (obj is Dictionary<string, object> dictionaryStr) {
                 var newDictionary = new Dictionary<string, object>();
-                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<int, object> dictionaryInt) {
+                var newDictionary = new Dictionary<int, object>();
+                foreach (var item in dictionaryInt) {
                     var newVal = RecursivelyReplaceNullWithString(item.Value);
                     if (newVal != null)
                         newDictionary[item.Key] = newVal;
@@ -1016,8 +1038,9 @@
                 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 @@
             ErrorReporter.Logger = logger;
         }
     }
-}
+}

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!]";
+        }
     }
 }

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);
     }
 }

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

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)

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 {
+
+	}
+}