explicit/symbolic: refactor checkExpressionLabel to use getLabelList()

For symbolic checkExpressionLabel, additionally ensure that no NullPointerException
is thrown if propertiesFile is null.


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

prism/src/explicit/StateModelChecker.java

@@ -836,18 +836,9 @@ public class StateModelChecker extends PrismComponent
 			if (bs != null) {
 				return StateValues.createFromBitSet((BitSet) bs.clone(), model);
 			}
-			// Failing that, look in the properties file (if possible)
-			if (propertiesFile != null) {
-				ll = propertiesFile.getCombinedLabelList();
-				i = ll.getLabelIndex(expr.getName());
-				if (i != -1) {
-					// check recursively
-					return checkExpression(model, ll.getLabel(i), statesOfInterest);
-				}
-			}
-			// Or just the model file
-			else {
-				ll = modulesFile.getLabelList();
+			// Failing that, look in the label list (from properties file / modules file)
+			ll = getLabelList();
+			if (ll != null) {
 				i = ll.getLabelIndex(expr.getName());
 				if (i != -1) {
 					// check recursively

prism/src/prism/StateModelChecker.java

@@ -989,8 +989,10 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 			return new StateValuesMTBDD(dd.copy(), model);
 		} else {
 			// get expression associated with label
-			ll = propertiesFile.getCombinedLabelList();
-			i = ll.getLabelIndex(expr.getName());
+			ll = getLabelList();
+			i = -1;
+			if (ll != null)
+				i = ll.getLabelIndex(expr.getName());
 			if (i == -1)
 				throw new PrismException("Unknown label \"" + expr.getName() + "\" in property");
 			// check recursively