Add syntax checks on existence of observables...endobservables block.

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.