diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs index 0c7fb0bca..3a54d5e47 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs @@ -97,9 +97,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. /// @@ -618,9 +634,18 @@ public object RecursivelyReplaceNullWithString(object obj) { if (obj == null) { 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; 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 050be18cc..97ee4dabd 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