From ec76c264689e87a8ce470ea5d47c997702738eeb Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 29 Dec 2020 23:54:31 +0000
Subject: [PATCH] Add syntax checks on existence of
 observables...endobservables block.

---
 prism/src/parser/ast/ModulesFile.java | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

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.