Re-factoring in multi-objective model checking.

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

prism/src/parser/ast/ExpressionProb.java

@@ -33,7 +33,7 @@ import prism.OpRelOpBound;
 import prism.PrismException;
 import prism.PrismLangException;
 
-public class ExpressionProb extends Expression
+public class ExpressionProb extends Expression implements ExpressionQuant
 {
 	RelOp relOp = null;
 	Expression prob = null;

prism/src/parser/ast/ExpressionQuant.java

@@ -0,0 +1,44 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package parser.ast;
+
+import parser.Values;
+import prism.OpRelOpBound;
+import prism.PrismException;
+
+/**
+ * Interface containing (some) common features of "quantitative" operators (P,R,S),
+ * i.e., classes ExpressionProb, ExpressionReward, ExpressionSS
+ */
+public interface ExpressionQuant
+{
+	public RelOp getRelOp();
+	public Expression getExpression();
+	public OpRelOpBound getRelopBoundInfo(Values constantValues) throws PrismException;
+}
+
+//------------------------------------------------------------------------------

prism/src/parser/ast/ExpressionReward.java

@@ -33,7 +33,7 @@ import prism.OpRelOpBound;
 import prism.PrismException;
 import prism.PrismLangException;
 
-public class ExpressionReward extends Expression
+public class ExpressionReward extends Expression implements ExpressionQuant
 {
 	Object rewardStructIndex = null;
 	Object rewardStructIndexDiv = null;

prism/src/parser/ast/ExpressionSS.java

@@ -33,7 +33,7 @@ import prism.OpRelOpBound;
 import prism.PrismException;
 import prism.PrismLangException;
 
-public class ExpressionSS extends Expression
+public class ExpressionSS extends Expression implements ExpressionQuant
 {
 	RelOp relOp = null;
 	Expression prob = null;

prism/src/prism/MultiObjModelChecker.java

@@ -36,6 +36,7 @@ import java.util.List;
 import java.util.Vector;
 
 import parser.ast.Expression;
+import parser.ast.RelOp;
 
 import dv.DoubleVector;
 
@@ -257,11 +258,10 @@ public class MultiObjModelChecker extends PrismComponent
 
 					for (int i = 0; i < opsAndBounds.probSize(); i++) {
 						if (opsAndBounds.getProbOperator(i) != Operator.P_MAX) {
-							tmpOpsAndBounds.add(opsAndBounds.getProbOperator(i), opsAndBounds.getProbBound(i), opsAndBounds.getProbStepBound(i));
+							tmpOpsAndBounds.add(opsAndBounds.getOpRelOpBound(i), opsAndBounds.getProbOperator(i), opsAndBounds.getProbBound(i), opsAndBounds.getProbStepBound(i));
 						}
 					}
-
-					tmpOpsAndBounds.add(Operator.R_MAX, -1.0, -1);
+					tmpOpsAndBounds.add(new OpRelOpBound("R", RelOp.MAX, -1.0), Operator.R_MAX, -1.0, -1);
 
 					ArrayList<JDDNode> tmprewards = new ArrayList<JDDNode>(1);
 					tmprewards.add(rtarget);

prism/src/prism/NondetModelChecker.java

@@ -299,7 +299,7 @@ public class NondetModelChecker extends NonProbModelChecker
 		ArrayList<String> targetName = new ArrayList<String>();
 		List<Expression> targetExprs = new ArrayList<Expression>(numObjectives);
 		for (int i = 0; i < numObjectives; i++) {
-			extractInfoFromMultiObjectiveOperand(expr.getOperand(i), opsAndBounds, rewardsIndex, targetName, targetExprs);
+			extractInfoFromMultiObjectiveOperand((ExpressionQuant) expr.getOperand(i), opsAndBounds, rewardsIndex, targetName, targetExprs);
 		}
 
 		//currently we do 1 numerical subject to booleans, or multiple numericals only 
@@ -507,7 +507,7 @@ public class NondetModelChecker extends NonProbModelChecker
 	 * Extract the information from the operator defining one objective of a multi-objective query,
 	 * store the info in the passed in arrays and so some checks. 
 	 */
-	protected void extractInfoFromMultiObjectiveOperand(Expression operand, OpsAndBoundsList opsAndBounds, List<JDDNode> rewardsIndex, List<String> targetName,
+	protected void extractInfoFromMultiObjectiveOperand(ExpressionQuant exprQuant, OpsAndBoundsList opsAndBounds, List<JDDNode> rewardsIndex, List<String> targetName,
 			List<Expression> targetExprs) throws PrismException
 	{
 		int stepBound = 0;
@@ -515,12 +515,13 @@ public class NondetModelChecker extends NonProbModelChecker
 		ExpressionReward exprReward = null;
 		ExpressionTemporal exprTemp;
 		RelOp relOp;
-		if (operand instanceof ExpressionProb) {
-			exprProb = (ExpressionProb) operand;
+		
+		if (exprQuant instanceof ExpressionProb) {
+			exprProb = (ExpressionProb) exprQuant;
 			exprReward = null;
 			relOp = exprProb.getRelOp();
-		} else if (operand instanceof ExpressionReward) {
-			exprReward = (ExpressionReward) operand;
+		} else if (exprQuant instanceof ExpressionReward) {
+			exprReward = (ExpressionReward) exprQuant;
 			exprProb = null;
 			relOp = exprReward.getRelOp();
 			Object rs = exprReward.getRewardStructIndex();
@@ -567,9 +568,12 @@ public class NondetModelChecker extends NonProbModelChecker
 		}
 
 		// Get info from P/R operator
+		OpRelOpBound opInfo = exprQuant.getRelopBoundInfo(constantValues);
+		
 		// Store relational operator
-		if (relOp.isStrict())
+		if (opInfo.getRelOp().isStrict())
 			throw new PrismException("Multi-objective properties can not use strict inequalities on P/R operators");
+		
 		Operator op;
 		if (relOp == RelOp.MAX) {
 			op = (exprProb != null) ? Operator.P_MAX : Operator.R_MAX;
@@ -592,9 +596,9 @@ public class NondetModelChecker extends NonProbModelChecker
 			if (exprProb != null && relOp == RelOp.LEQ)
 				p = 1 - p;
 
-			opsAndBounds.add(op, p, stepBound);
+			opsAndBounds.add(opInfo, op, p, stepBound);
 		} else {
-			opsAndBounds.add(op, -1.0, stepBound);
+			opsAndBounds.add(opInfo, op, -1.0, stepBound);
 		}
 
 		// Now extract targets
@@ -615,7 +619,8 @@ public class NondetModelChecker extends NonProbModelChecker
 		for (JDDNode set : tmpecs)
 			acceptingStates = JDD.Or(acceptingStates, set);
 		targetDDs.add(acceptingStates);
-		opsAndBounds.add(Operator.P_GE, 0.0, -1);
+		OpRelOpBound opInfo = new OpRelOpBound("P", RelOp.GEQ, 0.0);
+		opsAndBounds.add(opInfo, Operator.P_GE, 0.0, -1);
 	}
 
 	//Prints info about the product model in multi-objective

prism/src/prism/OpsAndBoundsList.java

@@ -31,8 +31,7 @@ import java.util.BitSet;
 import java.util.List;
 
 /**
- * This class keeps lists of operators and bounds used in multi-objective
- * verification. 
+ * This class keeps lists of operators and bounds used in multi-objective verification. 
  *
  * The instance keeps an ordered instance of (operator,bound) values.
  * These are currently held in two separate lists internally. A tuple
@@ -52,6 +51,7 @@ public class OpsAndBoundsList
 	 */
 	private BitSet probNegated;
 	
+	protected List<OpRelOpBound> opInfos;
 	protected List<Operator> relOps, relOpsProb, relOpsReward;
 	protected List<Double> bounds,  boundsProb, boundsReward;
 	protected List<Integer> stepBounds,  stepBoundsProb, stepBoundsReward;
@@ -67,20 +67,21 @@ public class OpsAndBoundsList
 	/**
 	 * Creates an instance of the class in which the "big" lists
 	 * are allocated with size numTargets.
-	 * @param numTargets The expected number of elements that would be added to the list. 
+	 * @param numObjectives The expected number of elements that would be added to the list. 
 	 */
-	public OpsAndBoundsList(int numTargets)
+	public OpsAndBoundsList(int numObjectives)
 	{
 		probNegated = new BitSet();
-		relOps = new ArrayList<Operator>(numTargets);
-		bounds = new ArrayList<Double>(numTargets);
-		stepBounds = new ArrayList<Integer>(numTargets);
+		opInfos = new ArrayList<OpRelOpBound>(numObjectives);
+		relOps = new ArrayList<Operator>(numObjectives);
+		bounds = new ArrayList<Double>(numObjectives);
+		stepBounds = new ArrayList<Integer>(numObjectives);
 		relOpsProb = new ArrayList<Operator>();
 		boundsProb = new ArrayList<Double>();
-		stepBoundsProb = new ArrayList<Integer>(numTargets);
+		stepBoundsProb = new ArrayList<Integer>(numObjectives);
 		relOpsReward = new ArrayList<Operator>();
 		boundsReward = new ArrayList<Double>();
-		stepBoundsReward = new ArrayList<Integer>(numTargets);
+		stepBoundsReward = new ArrayList<Integer>(numObjectives);
 	}
 	
 	/**
@@ -89,8 +90,9 @@ public class OpsAndBoundsList
 	 * @param quantityBound
 	 * @param stepBound
 	 */
-	public void add(Operator op, double quantityBound, int stepBound)
+	public void add(OpRelOpBound opInfo, Operator op, double quantityBound, int stepBound)
 	{
+		opInfos.add(opInfo);
 		relOps.add(op);
 		bounds.add(quantityBound);
 		stepBounds.add(stepBound);
@@ -143,6 +145,14 @@ public class OpsAndBoundsList
 		return stepBounds.get(i);
 	}
 	
+	/**
+	 * Returns the operator/relop info at i-th position.
+	 */
+	public OpRelOpBound getOpRelOpBound(int i)
+	{
+		return opInfos.get(i);
+	}
+
 	/**
 	 * Returns the operator at i-th position in the subsequence containing only probabilistic
 	 * operators.