diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index 7fda7680..4a20463a 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/prism/src/parser/ast/ModulesFile.java @@ -816,6 +816,8 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato // is non-null; methods before this point cannot) finaliseModelType(); + // Check observables + checkObservables(); // Various semantic checks doSemanticChecks(); // Type checking @@ -1097,6 +1099,19 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato } } + /** + * Check "observables...endobservables" construct + */ + private void checkObservables() throws PrismLangException + { + if (getModelType().partiallyObservable() && !hasObservables) { + throw new PrismLangException(getModelType() + "s must specify observables"); + } + if (hasObservables() && !getModelType().partiallyObservable()) { + throw new PrismLangException(getModelType() + "s cannot specify observables"); + } + } + /** * Perform any required semantic checks. * These checks are done *before* any undefined constants have been defined.