More fixes for bugs introduced in recent "improvements" to constant handling API:

- setSomeUndefinedConstants(null) call changed in PropertiesFile
- expandConstants() handles undefined constants cleanly


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4460 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/parser/ast/ModulesFile.java

@@ -504,9 +504,9 @@ public class ModulesFile extends ASTElement
 
 		// Various semantic checks 
 		semanticCheck(this);
-		
 		// Type checking
 		typeCheck();
+		
 		// If there are no undefined constants, set up values for constants
 		// (to avoid need for a later call to setUndefinedConstants).
 		// NB: Can't call setUndefinedConstants if there are undefined constants

prism/src/parser/ast/PropertiesFile.java

@@ -212,10 +212,6 @@ public class PropertiesFile extends ASTElement
 		// check constants for cyclic dependencies
 		constantList.findCycles();
 		
-		// Set up some values for constants
-		// (without assuming any info about undefined constants)
-		setSomeUndefinedConstants(null);
-		
 		// Check property names
 		checkPropertyNames();
 		
@@ -229,6 +225,10 @@ public class PropertiesFile extends ASTElement
 		semanticCheck(modulesFile, this);
 		// Type checking
 		typeCheck();
+		
+		// Set up some values for constants
+		// (without assuming any info about undefined constants)
+		setSomeUndefinedConstants(null);
 	}
 
 	// check formula identifiers

prism/src/parser/visitor/ExpandConstants.java

@@ -51,18 +51,25 @@ public class ExpandConstants extends ASTTraverseModify
 		// See if identifier corresponds to a constant
 		i = constantList.getConstantIndex(e.getName());
 		if (i != -1) {
-			// If so, replace it with the corresponding expression
-			expr = constantList.getConstant(i).deepCopy();
-			// But also recursively expand that
-			expr = (Expression)expr.expandConstants(constantList);
-			// Put in brackets so precedence is preserved
-			// (for display purposes only; in case of re-parse)
-			// This is being done after type-checking so also set type
-			t = expr.getType();
-			expr = Expression.Parenth(expr);
-			expr.setType(t);
-			// Return replacement expression
-			return expr;
+			// And check that the constant is defined
+			if (constantList.getConstant(i) != null) {
+				// If so, replace it with the corresponding expression
+				expr = constantList.getConstant(i).deepCopy();
+				// But also recursively expand that
+				expr = (Expression) expr.expandConstants(constantList);
+				// Put in brackets so precedence is preserved
+				// (for display purposes only; in case of re-parse)
+				// This is being done after type-checking so also set type
+				t = expr.getType();
+				expr = Expression.Parenth(expr);
+				expr.setType(t);
+				// Return replacement expression
+				return expr;
+			}
+			else {
+				// Error (should never happen)
+				throw new PrismLangException("Undefined constant", e);
+			}
 		}
 		else {
 			// Error (should never happen)