From 753d0d470a64fa0fd7c6706d8830aee5e16a1ec1 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 30 Dec 2014 01:31:35 +0000
Subject: [PATCH] Re-factoring in multi-objective model checking.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9469 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/NondetModelChecker.java | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java
index 8648930a..f897ac55 100644
--- a/prism/src/prism/NondetModelChecker.java
+++ b/prism/src/prism/NondetModelChecker.java
@@ -257,10 +257,8 @@ public class NondetModelChecker extends NonProbModelChecker
 	protected StateValues checkExpressionMultiObjective(ExpressionFunc expr) throws PrismException
 	{
 		// Objective/target info
-		List<Expression> targetExprs;
 		List<JDDNode> multitargetDDs = null;
 		List<Integer> multitargetIDs = null;
-		OpsAndBoundsList opsAndBounds;
 
 		// LTL/product model stuff
 		NondetModel modelProduct, modelNew;
@@ -295,11 +293,11 @@ public class NondetModelChecker extends NonProbModelChecker
 
 		// Check format and extract bounds/etc.
 		int numObjectives = expr.getNumOperands();
-		opsAndBounds = new OpsAndBoundsList();
+		OpsAndBoundsList opsAndBounds = new OpsAndBoundsList();
 		List<JDDNode> rewards = new ArrayList<JDDNode>(numObjectives);
 		List<JDDNode> rewardsIndex = new ArrayList<JDDNode>(numObjectives);
 		ArrayList<String> targetName = new ArrayList<String>();
-		targetExprs = new ArrayList<Expression>(numObjectives);
+		List<Expression> targetExprs = new ArrayList<Expression>(numObjectives);
 		for (int i = 0; i < numObjectives; i++) {
 			extractInfoFromMultiObjectiveOperand(expr.getOperand(i), opsAndBounds, rewardsIndex, targetName, targetExprs);
 		}
@@ -532,8 +530,7 @@ public class NondetModelChecker extends NonProbModelChecker
 			//check if there are state rewards and display a warning
 			if (stateRewards != null && !stateRewards.equals(JDD.ZERO))
 				throw new PrismException("Multi-objective model checking does not support state rewards; please convert to transition rewards");
-			if (transRewards == null)
-				throw new PrismException("Invalid reward structure index \"" + rs + "\"");
+			
 			rewardsIndex.add(transRewards);
 		} else {
 			throw new PrismException("Multi-objective properties can only contain P and R operators");