From 502faa6a263db29a73bc93ef62471ba8f0e85250 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Wed, 14 Sep 2016 11:33:42 +0000
Subject: [PATCH] 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 | 15 +++------------
 prism/src/prism/StateModelChecker.java    |  6 ++++--
 2 files changed, 7 insertions(+), 14 deletions(-)

diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java
index 1868914a..b705009d 100644
--- a/prism/src/explicit/StateModelChecker.java
+++ b/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
diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java
index 652ba4ff..57f3642e 100644
--- a/prism/src/prism/StateModelChecker.java
+++ b/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