Symbolic model checkers: Change the checkXYZ methods to take a stateOfInterest argument

Additionally, provide more consistent JavaDoc/@Override annotations for these methods.

Often, we are only interested in a subset of the states. E.g., for the top-level
expression, PRISM by default only reports on the initial states; for filters, only
the filtered states are of interest, etc.

By providing a statesOfInterest set to the check methods, they can in principle
exploit this knowledge. One prominent candidate is the automata-based LTL model
checking, which can start the product construction only from the states of interest
instead of from all states. The statesOfInterest information is merely a hint, i.e.,
a checkXYZ method can return values for more states than those specified as the states
of interest. However, the caller should not rely on any results beyond those for
the statesOfInterest.

This commit only provides the basic infrastructure, i.e., adding the stateOfInterest
argument to the method signatures, passing this set to recursive method calls where
appropriate, etc, but does not yet exploit this information. Subsequent commits will
then begin to exploit this information.

The called checkXYZ method is responsible for dereferencing the JDDNode for the
statesOfInterest set. Generally, care should be taken that statesOfInterest is indeed
an MTBDD over the row-variables of the model and that it is a subset of the reachable
states of the model. If one is interested in results for all states, use
model.getReach().copy() as the statesOfInterest.

An analoguous mechanism already exists for the explicit engine.


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

prism/src/prism/LTLModelChecker.java

@@ -104,7 +104,7 @@ public class LTLModelChecker extends PrismComponent
 		// A state formula
 		if (expr.getType() instanceof TypeBool) {
 			// Model check
-			JDDNode dd = mc.checkExpressionDD(expr);
+			JDDNode dd = mc.checkExpressionDD(expr, model.getReach().copy());
 			// Detect special cases (true, false) for optimisation
 			if (dd.equals(JDD.ZERO)) {
 				JDD.Deref(dd);

prism/src/prism/ModelChecker.java

@@ -34,9 +34,32 @@ import parser.ast.*;
 
 public interface ModelChecker
 {
+	/**
+	 * Model check an expression, process, print and return the result.
+	 */
 	public Result check(Expression expr) throws PrismException;
-	public StateValues checkExpression(Expression expr) throws PrismException;
-	public JDDNode checkExpressionDD(Expression expr) throws PrismException;
+
+	/**
+	 * Model check an expression and return a vector of result values,
+	 * with valid results for at least all states of interest.
+	 *
+	 * @param expr the expression
+	 * @param statesOfInterest the states of interest.
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	public StateValues checkExpression(Expression expr, JDDNode statesOfInterest) throws PrismException;
+
+	/**
+	 * Model check expression, convert to symbolic form (if not already), return BDD.
+	 * <br>
+	 * Will have valid results at least for all states of interest.
+	 * @param expr the expression
+	 * @param statesOfInterest the states of interest
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	public JDDNode checkExpressionDD(Expression expr, JDDNode statesOfInterest) throws PrismException;
+
+	/** Get the constant values (both from the modules file and the properties file) */
 	public Values getConstantValues();
 }
 

prism/src/prism/Modules2MTBDD.java

@@ -1922,7 +1922,8 @@ public class Modules2MTBDD
 	private JDDNode translateExpression(Expression e) throws PrismException
 	{
 		// pass this work onto the Expression2MTBDD object
-		return expr2mtbdd.checkExpressionDD(e);
+		// states of interest = JDD.ONE = true = all possible states
+		return expr2mtbdd.checkExpressionDD(e, JDD.ONE.copy());
 	}
 
 	// build state and transition rewards

prism/src/prism/NonProbModelChecker.java

@@ -62,22 +62,22 @@ public class NonProbModelChecker extends StateModelChecker
 	// -----------------------------------------------------------------------------------
 
 	// Check expression (recursive)
-
-	public StateValues checkExpression(Expression expr) throws PrismException
+	@Override
+	public StateValues checkExpression(Expression expr, JDDNode statesOfInterest) throws PrismException
 	{
 		StateValues res;
 
 		// E operator
 		if (expr instanceof ExpressionExists) {
-			res = checkExpressionExists(((ExpressionExists) expr).getExpression());
+			res = checkExpressionExists(((ExpressionExists) expr).getExpression(), statesOfInterest);
 		}
 		// A operator
 		else if (expr instanceof ExpressionForAll) {
-			res = checkExpressionForAll(((ExpressionForAll) expr).getExpression());
+			res = checkExpressionForAll(((ExpressionForAll) expr).getExpression(), statesOfInterest);
 		}
 		// Otherwise, use the superclass
 		else {
-			res = super.checkExpression(expr);
+			res = super.checkExpression(expr, statesOfInterest);
 		}
 
 		// Filter out non-reachable states from solution
@@ -94,17 +94,21 @@ public class NonProbModelChecker extends StateModelChecker
 
 	/**
 	 * Model check a CTL exists (E) operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
 	 */
-	protected StateValues checkExpressionExists(Expression expr) throws PrismException
+	protected StateValues checkExpressionExists(Expression expr, JDDNode statesOfInterest) throws PrismException
 	{
 		StateValues res = null;
 
 		// Check whether this is a simple path formula (i.e. CTL, not LTL)
 		if (!expr.isSimplePathFormula()) {
+			JDD.Deref(statesOfInterest);
 			throw new PrismNotSupportedException("(Non-probabilistic) LTL model checking is not supported");
 		}
 
 		if (prism.getFairness()) {
+			JDD.Deref(statesOfInterest);
 			throw new PrismNotSupportedException("Non-probabilistic CTL model checking is not supported with fairness");
 		}
 
@@ -114,12 +118,12 @@ public class NonProbModelChecker extends StateModelChecker
 			// Parentheses
 			if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) {
 				// Recurse
-				res = checkExpressionExists(exprUnary.getOperand());
+				res = checkExpressionExists(exprUnary.getOperand(), statesOfInterest);
 			}
 			// Negation
 			else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) {
 				// Compute, then negate 
-				res = checkExpressionForAll(exprUnary.getOperand());
+				res = checkExpressionForAll(exprUnary.getOperand(), statesOfInterest);
 				res.subtractFromOne();
 			}
 		}
@@ -127,23 +131,24 @@ public class NonProbModelChecker extends StateModelChecker
 		else if (expr instanceof ExpressionTemporal) {
 			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
 			if (exprTemp.hasBounds()) {
+				JDD.Deref(statesOfInterest);
 				throw new PrismNotSupportedException("Model checking of bounded CTL operators is not supported");
 			}
 			// Next (EX)
 			if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
-				res = checkNext(exprTemp, false);
+				res = checkNext(exprTemp, false, statesOfInterest);
 			}
 			// Until (EU)
 			else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
-				res = checkExistsUntil(exprTemp);
+				res = checkExistsUntil(exprTemp, statesOfInterest);
 			}
 			// Globally (EG)
 			else if (exprTemp.getOperator() == ExpressionTemporal.P_G) {
-				res = checkExistsGlobally(exprTemp);
+				res = checkExistsGlobally(exprTemp, statesOfInterest);
 			}
 			// Anything else - convert to until and recurse
 			else {
-				res = checkExpressionExists(exprTemp.convertToUntilForm());
+				res = checkExpressionExists(exprTemp.convertToUntilForm(), statesOfInterest);
 			}
 		}
 
@@ -155,17 +160,21 @@ public class NonProbModelChecker extends StateModelChecker
 
 	/**
 	 * Model check a CTL forall (A) operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
 	 */
-	protected StateValues checkExpressionForAll(Expression expr) throws PrismException
+	protected StateValues checkExpressionForAll(Expression expr, JDDNode statesOfInterest) throws PrismException
 	{
 		StateValues res = null;
 
 		// Check whether this is a simple path formula (i.e. CTL, not LTL)
 		if (!expr.isSimplePathFormula()) {
+			JDD.Deref(statesOfInterest);
 			throw new PrismNotSupportedException("(Non-probabilistic) LTL model checking is not supported");
 		}
 
 		if (prism.getFairness()) {
+			JDD.Deref(statesOfInterest);
 			throw new PrismNotSupportedException("Non-probabilistic CTL model checking is not supported with fairness");
 		}
 
@@ -175,12 +184,12 @@ public class NonProbModelChecker extends StateModelChecker
 			// Parentheses
 			if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) {
 				// Recurse
-				res = checkExpressionForAll(exprUnary.getOperand());
+				res = checkExpressionForAll(exprUnary.getOperand(), statesOfInterest);
 			}
 			// Negation
 			else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) {
 				// Compute, then negate 
-				res = checkExpressionExists(exprUnary.getOperand());
+				res = checkExpressionExists(exprUnary.getOperand(), statesOfInterest);
 				res.subtractFromOne();
 			}
 		}
@@ -188,11 +197,12 @@ public class NonProbModelChecker extends StateModelChecker
 		else if (expr instanceof ExpressionTemporal) {
 			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
 			if (exprTemp.hasBounds()) {
+				JDD.Deref(statesOfInterest);
 				throw new PrismNotSupportedException("Model checking of bounded CTL operators is not supported");
 			}
 			// Next (AX)
 			if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
-				res = checkNext(exprTemp, true);
+				res = checkNext(exprTemp, true, statesOfInterest);
 			}
 			// Until (AU)
 			else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
@@ -205,7 +215,7 @@ public class NonProbModelChecker extends StateModelChecker
 				Expression rhs = new ExpressionTemporal(ExpressionTemporal.P_G, null, notPhi2);
 				rhs = Expression.Not(new ExpressionExists(rhs));
 				Expression enf = Expression.And(lhs, rhs);
-				res = checkExpression(enf);
+				res = checkExpression(enf, statesOfInterest);
 			}
 			// Eventually (AF)
 			else if (exprTemp.getOperator() == ExpressionTemporal.P_F) {
@@ -213,12 +223,12 @@ public class NonProbModelChecker extends StateModelChecker
 				ExpressionTemporal exprCopy = (ExpressionTemporal) exprTemp.deepCopy();
 				exprCopy.setOperator(ExpressionTemporal.P_G);
 				exprCopy.setOperand2(Expression.Not(exprCopy.getOperand2()));
-				res = checkExpressionExists(exprCopy);
+				res = checkExpressionExists(exprCopy, statesOfInterest);
 				res.subtractFromOne();
 			}
 			// Anything else - convert to until and recurse
 			else {
-				res = checkExpressionForAll(exprTemp.convertToUntilForm());
+				res = checkExpressionForAll(exprTemp.convertToUntilForm(), statesOfInterest);
 			}
 		}
 
@@ -230,13 +240,18 @@ public class NonProbModelChecker extends StateModelChecker
 
 	/**
 	 * Model check a CTL exists/forall next (EX/AX) operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
 	 */
-	protected StateValues checkNext(ExpressionTemporal expr, boolean forall) throws PrismException
+	protected StateValues checkNext(ExpressionTemporal expr, boolean forall, JDDNode statesOfInterest) throws PrismException
 	{
 		JDDNode b, transRel, pre;
 
-		// Model check operand first
-		b = checkExpressionDD(expr.getOperand2());
+		// currently, ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
+
+		// Model check operands first, statesOfInterest = all
+		b = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
 
 		// Get transition relation
 		if (model.getModelType() == ModelType.MDP) {
@@ -265,8 +280,10 @@ public class NonProbModelChecker extends StateModelChecker
 
 	/**
 	 * Model check a CTL exists until (EU) operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
 	 */
-	protected StateValues checkExistsUntil(ExpressionTemporal expr) throws PrismException
+	protected StateValues checkExistsUntil(ExpressionTemporal expr, JDDNode statesOfInterest) throws PrismException
 	{
 		JDDNode b1, b2, transRel, tmp, tmp2, tmp3, init = null;
 		ArrayList<JDDNode> cexDDs = null;
@@ -276,10 +293,13 @@ public class NonProbModelChecker extends StateModelChecker
 		int iters, i;
 		long l;
 
-		// Model check operands first
-		b1 = checkExpressionDD(expr.getOperand1());
+		// currently, ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
+
+		// Model check operands first, statesOfInterest = all
+		b1 = checkExpressionDD(expr.getOperand1(), model.getReach().copy());
 		try {
-			b2 = checkExpressionDD(expr.getOperand2());
+			b2 = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
 		} catch (PrismException e) {
 			JDD.Deref(b1);
 			throw e;
@@ -425,8 +445,10 @@ public class NonProbModelChecker extends StateModelChecker
 
 	/**
 	 * Model check a CTL exists globally (EG) operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
 	 */
-	protected StateValues checkExistsGlobally(ExpressionTemporal expr) throws PrismException
+	protected StateValues checkExistsGlobally(ExpressionTemporal expr, JDDNode statesOfInterest) throws PrismException
 	{
 		JDDNode b2, transRel, tmp, tmp2;
 		boolean done;
@@ -437,8 +459,11 @@ public class NonProbModelChecker extends StateModelChecker
 		JDDNode notInSCCs = null;
 		int numSCCs = 0;
 
-		// Model check operand first
-		b2 = checkExpressionDD(expr.getOperand2());
+		// currently, ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
+
+		// Model check operand first, statesOfInterest = all
+		b2 = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
 
 		l = System.currentTimeMillis();
 

prism/src/prism/NondetModelChecker.java

@@ -143,36 +143,36 @@ public class NondetModelChecker extends NonProbModelChecker
 	// Model checking functions
 
 	@Override
-	public StateValues checkExpression(Expression expr) throws PrismException
+	public StateValues checkExpression(Expression expr, JDDNode statesOfInterest) throws PrismException
 	{
 		StateValues res;
 
 		// <<>> or [[]] operator
 		if (expr instanceof ExpressionStrategy) {
-			res = checkExpressionStrategy((ExpressionStrategy) expr);
+			res = checkExpressionStrategy((ExpressionStrategy) expr, statesOfInterest);
 		}
 		// P operator
 		else if (expr instanceof ExpressionProb) {
-			res = checkExpressionProb((ExpressionProb) expr);
+			res = checkExpressionProb((ExpressionProb) expr, statesOfInterest);
 		}
 		// R operator
 		else if (expr instanceof ExpressionReward) {
-			res = checkExpressionReward((ExpressionReward) expr);
+			res = checkExpressionReward((ExpressionReward) expr, statesOfInterest);
 		}
 		// Multi-objective
 		else if (expr instanceof ExpressionFunc) {
 			// Detect "multi" function
 			if (((ExpressionFunc) expr).getName().equals("multi")) {
-				res = checkExpressionMultiObjective((ExpressionFunc) expr);
+				res = checkExpressionMultiObjective((ExpressionFunc) expr, statesOfInterest);
 			}
 			// For any other function, check as normal
 			else {
-				res = super.checkExpression(expr);
+				res = super.checkExpression(expr, statesOfInterest);
 			}
 		}
 		// Otherwise, use the superclass
 		else {
-			res = super.checkExpression(expr);
+			res = super.checkExpression(expr, statesOfInterest);
 		}
 
 		// Filter out non-reachable states from solution
@@ -184,9 +184,11 @@ public class NondetModelChecker extends NonProbModelChecker
 	}
 
 	/**
-	 * Model check a <<>> or [[]] operator expression and return the values for all states.
+	 * Model check a <<>> or [[]] operator expression.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
 	 */
-	protected StateValues checkExpressionStrategy(ExpressionStrategy expr) throws PrismException
+	protected StateValues checkExpressionStrategy(ExpressionStrategy expr, JDDNode statesOfInterest) throws PrismException
 	{
 		// Will we be quantifying universally or existentially over strategies/adversaries?
 		boolean forAll = !expr.isThereExists();
@@ -207,34 +209,39 @@ public class NondetModelChecker extends NonProbModelChecker
 		// Pass onto relevant method:
 		// Single P operator
 		if (exprs.size() == 1 && exprs.get(0) instanceof ExpressionProb) {
-			return checkExpressionProb((ExpressionProb) exprs.get(0), forAll);
+			return checkExpressionProb((ExpressionProb) exprs.get(0), forAll, statesOfInterest);
 		}
 		// Single R operator
 		else if (exprs.size() == 1 && exprs.get(0) instanceof ExpressionReward) {
-			return checkExpressionReward((ExpressionReward) exprs.get(0), forAll);
+			return checkExpressionReward((ExpressionReward) exprs.get(0), forAll, statesOfInterest);
 		}
 		// Anything else is treated as multi-objective 
 		else {
-			return checkExpressionMultiObjective(exprs, forAll);
+			return checkExpressionMultiObjective(exprs, forAll, statesOfInterest);
 		}
 	}
 	
 	/**
-	 * Model check a P operator expression and return the values for all states.
+	 * Model check a P operator expression.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
 	 */
-	protected StateValues checkExpressionProb(ExpressionProb expr) throws PrismException
+	protected StateValues checkExpressionProb(ExpressionProb expr, JDDNode statesOfInterest) throws PrismException
 	{
 		// Use the default semantics for a standalone P operator
 		// (i.e. quantification over all strategies)
-		return checkExpressionProb(expr, true);
+		return checkExpressionProb(expr, true, statesOfInterest);
 	}
 	
 	/**
-	 * Model check a P operator expression and return the values for all states.
+	 * Model check a P operator expression.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 *
 	 * @param expr The P operator expression
-	 * @param forAll Are we checking "for all strategies" (true) or "there exists a strategy" (false)? [irrelevant for numerical (=?) queries] 
+	 * @param forAll Are we checking "for all strategies" (true) or "there exists a strategy" (false)? [irrelevant for numerical (=?) queries]
 	 */
-	protected StateValues checkExpressionProb(ExpressionProb expr, boolean forAll) throws PrismException
+	protected StateValues checkExpressionProb(ExpressionProb expr, boolean forAll, JDDNode statesOfInterest) throws PrismException
 	{
 		// Get info from P operator
 		OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues);
@@ -244,15 +251,17 @@ public class NondetModelChecker extends NonProbModelChecker
 		if (opInfo.isTriviallyTrue()) {
 			mainLog.printWarning("Checking for probability " + opInfo.relOpBoundString() + " - formula trivially satisfies all states");
 			JDD.Ref(reach);
+			JDD.Deref(statesOfInterest);
 			return new StateValuesMTBDD(reach, model);
 		} else if (opInfo.isTriviallyFalse()) {
 			mainLog.printWarning("Checking for probability " + opInfo.relOpBoundString() + " - formula trivially satisfies no states");
+			JDD.Deref(statesOfInterest);
 			return new StateValuesMTBDD(JDD.Constant(0), model);
 		}
 
 		// Compute probabilities
 		boolean qual = opInfo.isQualitative() && precomp && prob0 && prob1;
-		StateValues probs = checkProbPathFormula(expr.getExpression(), qual, minMax.isMin());
+		StateValues probs = checkProbPathFormula(expr.getExpression(), qual, minMax.isMin(), statesOfInterest);
 
 		// Print out probabilities
 		if (verbose) {
@@ -277,21 +286,26 @@ public class NondetModelChecker extends NonProbModelChecker
 	}
 
 	/**
-	 * Model check n R operator expression and return the values for all states.
+	 * Model check an R operator expression.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
 	 */
-	protected StateValues checkExpressionReward(ExpressionReward expr) throws PrismException
+	protected StateValues checkExpressionReward(ExpressionReward expr, JDDNode statesOfInterest) throws PrismException
 	{
 		// Use the default semantics for a standalone R operator
 		// (i.e. quantification over all strategies)
-		return checkExpressionReward(expr, true);
+	    return checkExpressionReward(expr, true, statesOfInterest);
 	}
 	
 	/**
-	 * Model check an R operator expression and return the values for all states.
+	 * Model check an R operator expression.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 *
 	 * @param expr The R operator expression
-	 * @param forAll Are we checking "for all strategies" (true) or "there exists a strategy" (false)? [irrelevant for numerical (=?) queries] 
+	 * @param forAll Are we checking "for all strategies" (true) or "there exists a strategy" (false)? [irrelevant for numerical (=?) queries]
 	 */
-	protected StateValues checkExpressionReward(ExpressionReward expr, boolean forAll) throws PrismException
+	protected StateValues checkExpressionReward(ExpressionReward expr, boolean forAll, JDDNode statesOfInterest) throws PrismException
 	{
 		// Get info from R operator
 		OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues);
@@ -310,17 +324,17 @@ public class NondetModelChecker extends NonProbModelChecker
 			switch (exprTemp.getOperator()) {
 			case ExpressionTemporal.R_C:
 				if (exprTemp.hasBounds()) {
-					rewards = checkRewardCumul(exprTemp, stateRewards, transRewards, minMax.isMin());
+					rewards = checkRewardCumul(exprTemp, stateRewards, transRewards, minMax.isMin(), statesOfInterest);
 				} else {
-					rewards = checkRewardTotal(exprTemp, stateRewards, transRewards, minMax.isMin());
+					rewards = checkRewardTotal(exprTemp, stateRewards, transRewards, minMax.isMin(), statesOfInterest);
 				}
 				break;
 			case ExpressionTemporal.R_I:
-				rewards = checkRewardInst(exprTemp, stateRewards, transRewards, minMax.isMin());
+				rewards = checkRewardInst(exprTemp, stateRewards, transRewards, minMax.isMin(), statesOfInterest);
 				break;
 			}
 		} else if (expr2.getType() instanceof TypePathBool || expr2.getType() instanceof TypeBool) {
-			rewards = checkRewardPathFormula(expr2, stateRewards, transRewards, minMax.isMin());
+			rewards = checkRewardPathFormula(expr2, stateRewards, transRewards, minMax.isMin(), statesOfInterest);
 		}
 
 		if (rewards == null)
@@ -352,13 +366,17 @@ public class NondetModelChecker extends NonProbModelChecker
 	 * Model check a multi-objective query (from the contents of a strategy operator).
 	 * Return the result as a StateValues object (usually this gives values for all states,
 	 * but for a multi-objective query, we just give a single value, usually for the initial state).
+	 *
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
 	 * @param exprs The list of Expressions specifying the objectives
-	 * @param forAll Are we checking "for all strategies" (true) or "there exists a strategy" (false)? [irrelevant for numerical (=?) queries] 
+	 * @param forAll Are we checking "for all strategies" (true) or "there exists a strategy" (false)? [irrelevant for numerical (=?) queries]
+	 * @param statesOfInterest the states of interest
 	 */
-	protected StateValues checkExpressionMultiObjective(List<Expression> exprs, boolean forAll) throws PrismException
+	protected StateValues checkExpressionMultiObjective(List<Expression> exprs, boolean forAll, JDDNode statesOfInterest) throws PrismException
 	{
 		// For now, just support a single expression (which may encode a Boolean combination of objectives)
 		if (exprs.size() > 1) {
+			JDD.Deref(statesOfInterest);
 			throw new PrismException("Cannot currently check strategy operators with lists of expressions");
 		}
 		Expression exprSub = exprs.get(0);
@@ -380,6 +398,7 @@ public class NondetModelChecker extends NonProbModelChecker
 						prop = ((ExpressionUnaryOp) prop).getOperand();
 					}
 					if (!(prop instanceof ExpressionQuant)) {
+						JDD.Deref(statesOfInterest);
 						throw new PrismException("Expression " + prop + " is not allowed in a multi-objective query");
 					}
 				}
@@ -400,6 +419,7 @@ public class NondetModelChecker extends NonProbModelChecker
 
 			// Only handle a single disjunct for now
 			if (dnf.size() > 1) {
+				JDD.Deref(statesOfInterest);
 				throw new PrismException("Multi-objective model checking of multiple disjuncts not yet supported");
 			}
 			// Convert to multi(...)
@@ -409,13 +429,14 @@ public class NondetModelChecker extends NonProbModelChecker
 			}
 			// Handle negation
 			if (forAll) {
-				return checkExpression(Expression.Not(exprMulti));
+				return checkExpression(Expression.Not(exprMulti), statesOfInterest);
 			} else {
-				return checkExpressionMultiObjective(exprMulti);
+				return checkExpressionMultiObjective(exprMulti, statesOfInterest);
 			}
 		} else if (exprSub.getType() instanceof TypeDouble) {
-			return checkExpressionMultiObjective(exprs);
+			return checkExpressionMultiObjective(exprs, statesOfInterest);
 		} else {
+			JDD.Deref(statesOfInterest);
 			throw new PrismException("Multi-objective model checking not supported for: " + exprSub);
 		}
 	}
@@ -423,8 +444,9 @@ public class NondetModelChecker extends NonProbModelChecker
 	/**
 	 * Model check a multi-objective expression and return the result.
 	 * For multi-objective queries, we only find the value for one state.
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
 	 */
-	protected StateValues checkExpressionMultiObjective(ExpressionFunc expr) throws PrismException
+	protected StateValues checkExpressionMultiObjective(ExpressionFunc expr, JDDNode statesOfInterest) throws PrismException
 	{
 		// Extract objective list from 'multi' function
 		List<Expression> exprs = new ArrayList<Expression>();
@@ -432,14 +454,15 @@ public class NondetModelChecker extends NonProbModelChecker
 		for (int i = 0; i < n; i++) {
 			exprs.add(expr.getOperand(i));
 		}
-		return checkExpressionMultiObjective(exprs);
+		return checkExpressionMultiObjective(exprs, statesOfInterest);
 	}
 	
 	/**
 	 * Model check a multi-objective expression and return the result.
 	 * For multi-objective queries, we only find the value for one state.
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
 	 */
-	protected StateValues checkExpressionMultiObjective(List<Expression> exprs) throws PrismException
+	protected StateValues checkExpressionMultiObjective(List<Expression> exprs, JDDNode statesOfInterest) throws PrismException
 	{
 		// Objective/target info
 		List<JDDNode> multitargetDDs = null;
@@ -459,6 +482,10 @@ public class NondetModelChecker extends NonProbModelChecker
 		boolean hasMaxReward = false;
 		//boolean hasLTLconstraint = false;
 
+		// currently, ignore statesOfInterest
+		// TODO: switch singleton check below to use statesOfInterest 
+		JDD.Deref(statesOfInterest);
+
 		// Make sure we are only expected to compute a value for a single state
 		// Assuming yes, determine index of state of interest and build BDD
 		JDDNode ddStateIndex = null;
@@ -488,6 +515,7 @@ public class NondetModelChecker extends NonProbModelChecker
 		//currently we do 1 numerical subject to booleans, or multiple numericals only 
 		if (opsAndBounds.numberOfNumerical() > 1 &&
 				opsAndBounds.numberOfNumerical() < opsAndBounds.probSize() + opsAndBounds.rewardSize()) {
+			JDD.Deref(stateOfInterest);
 			throw new PrismException("Multiple min/max queries cannot be combined with boolean queries.");
 		}
 		
@@ -604,7 +632,7 @@ public class NondetModelChecker extends NonProbModelChecker
 				// (not used currently)
 				// Fixme: maybe not efficient
 				if (pathFormulas.get(i) != null) {
-					JDDNode dd = checkExpressionDD(pathFormulas.get(i));
+					JDDNode dd = checkExpressionDD(pathFormulas.get(i), model.getReach().copy());
 					JDD.Ref(modelProduct.getReach());
 					dd = JDD.And(dd, modelProduct.getReach());
 					targetDDs.add(dd);
@@ -847,8 +875,10 @@ public class NondetModelChecker extends NonProbModelChecker
 	
 	/**
 	 * Compute probabilities for the contents of a P operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
 	 */
-	protected StateValues checkProbPathFormula(Expression expr, boolean qual, boolean min) throws PrismException
+	protected StateValues checkProbPathFormula(Expression expr, boolean qual, boolean min, JDDNode statesOfInterest) throws PrismException
 	{
 		// Test whether this is a simple path formula (i.e. PCTL)
 		// and whether we want to use the corresponding algorithms
@@ -863,16 +893,18 @@ public class NondetModelChecker extends NonProbModelChecker
 		}
 
 		if (useSimplePathAlgo) {
-			return checkProbPathFormulaSimple(expr, qual, min);
+			return checkProbPathFormulaSimple(expr, qual, min, statesOfInterest);
 		} else {
-			return checkProbPathFormulaLTL(expr, qual, min);
+			return checkProbPathFormulaLTL(expr, qual, min, statesOfInterest);
 		}
 	}
 
 	/**
 	 * Compute probabilities for a simple, non-LTL path operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
 	 */
-	protected StateValues checkProbPathFormulaSimple(Expression expr, boolean qual, boolean min) throws PrismException
+	protected StateValues checkProbPathFormulaSimple(Expression expr, boolean qual, boolean min, JDDNode statesOfInterest) throws PrismException
 	{
 		boolean negated = false;
 		StateValues probs = null;
@@ -892,14 +924,14 @@ public class NondetModelChecker extends NonProbModelChecker
 			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
 			// Next
 			if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
-				probs = checkProbNext(exprTemp, min);
+				probs = checkProbNext(exprTemp, min, statesOfInterest);
 			}
 			// Until
 			else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
 				if (exprTemp.hasBounds()) {
-					probs = checkProbBoundedUntil(exprTemp, min);
+					probs = checkProbBoundedUntil(exprTemp, min, statesOfInterest);
 				} else {
-					probs = checkProbUntil(exprTemp, qual, min);
+					probs = checkProbUntil(exprTemp, qual, min, statesOfInterest);
 				}
 			}
 		}
@@ -917,14 +949,19 @@ public class NondetModelChecker extends NonProbModelChecker
 
 	/**
 	 * Compute probabilities for a next operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
 	 */
-	protected StateValues checkProbNext(ExpressionTemporal expr, boolean min) throws PrismException
+	protected StateValues checkProbNext(ExpressionTemporal expr, boolean min, JDDNode statesOfInterest) throws PrismException
 	{
 		JDDNode b;
 		StateValues probs = null;
 
-		// model check operand first
-		b = checkExpressionDD(expr.getOperand2());
+		// currently, ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
+
+		// model check operand first, statesOfInterest = all
+		b = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
 
 		// print out some info about num states
 		// mainLog.print("\nb = " + JDD.GetNumMintermsString(b,
@@ -941,8 +978,10 @@ public class NondetModelChecker extends NonProbModelChecker
 
 	/**
 	 * Compute probabilities for a bounded until operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
 	 */
-	protected StateValues checkProbBoundedUntil(ExpressionTemporal expr, boolean min) throws PrismException
+	protected StateValues checkProbBoundedUntil(ExpressionTemporal expr, boolean min, JDDNode statesOfInterest) throws PrismException
 	{
 		JDDNode b1, b2;
 		StateValues probs = null;
@@ -950,13 +989,16 @@ public class NondetModelChecker extends NonProbModelChecker
 		IntegerBound bounds;
 		int i;
 
+		// currently, ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
+
 		// get and check bounds information
 		bounds = IntegerBound.fromExpressionTemporal(expr, constantValues, true);
 
-		// model check operands first
-		b1 = checkExpressionDD(expr.getOperand1());
+		// model check operands first, statesOfInterest = all
+		b1 = checkExpressionDD(expr.getOperand1(), model.getReach().copy());
 		try {
-			b2 = checkExpressionDD(expr.getOperand2());
+			b2 = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
 		} catch (PrismException e) {
 			JDD.Deref(b1);
 			throw e;
@@ -1022,16 +1064,21 @@ public class NondetModelChecker extends NonProbModelChecker
 	/**
 	 * Compute probabilities for an (unbounded) until operator.
 	 * Note: This method is split into two steps so that the LTL model checker can use the second part directly.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
 	 */
-	protected StateValues checkProbUntil(ExpressionTemporal expr, boolean qual, boolean min) throws PrismException
+	protected StateValues checkProbUntil(ExpressionTemporal expr, boolean qual, boolean min, JDDNode statesOfInterest) throws PrismException
 	{
 		JDDNode b1, b2;
 		StateValues probs = null;
 
+		// currently, ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
+
 		// model check operands first
-		b1 = checkExpressionDD(expr.getOperand1());
+		b1 = checkExpressionDD(expr.getOperand1(), model.getReach().copy());
 		try {
-			b2 = checkExpressionDD(expr.getOperand2());
+			b2 = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
 		} catch (PrismException e) {
 			JDD.Deref(b1);
 			throw e;
@@ -1059,7 +1106,10 @@ public class NondetModelChecker extends NonProbModelChecker
 	}
 
 	/**
-	 * Compute probabilities for an (unbounded) until operator.
+	 * Compute probabilities for an (unbounded) until operator (b1 U b2).
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 *
 	 * @param b1 Remain in these states
 	 * @param b2 Target states
 	 * @param qual True if only qualititative (0/1) results are needed
@@ -1141,8 +1191,10 @@ public class NondetModelChecker extends NonProbModelChecker
 
 	/**
 	 * Compute probabilities for an LTL path formula
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
 	 */
-	protected StateValues checkProbPathFormulaLTL(Expression expr, boolean qual, boolean min) throws PrismException
+	protected StateValues checkProbPathFormulaLTL(Expression expr, boolean qual, boolean min, JDDNode statesOfInterest) throws PrismException
 	{
 		LTLModelChecker mcLtl;
 		StateValues probsProduct = null, probs = null;
@@ -1155,6 +1207,9 @@ public class NondetModelChecker extends NonProbModelChecker
 		int i;
 		long l;
 
+		// currently, ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
+
 		// For min probabilities, need to negate the formula
 		// (But check fairness setting since this may affect min/max)
 		// (add parentheses to allow re-parsing if required)
@@ -1260,12 +1315,17 @@ public class NondetModelChecker extends NonProbModelChecker
 
 	/**
 	 * Compute rewards for a cumulative reward operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
 	 */
-	protected StateValues checkRewardCumul(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException
+	protected StateValues checkRewardCumul(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min, JDDNode statesOfInterest) throws PrismException
 	{
 		int time; // time
 		StateValues rewards = null;
 
+		// currently, ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
+
 		// check that there is an upper time bound
 		if (expr.getUpperBound() == null) {
 			throw new PrismException("Cumulative reward operator without time bound (C) is only allowed for multi-objective queries");
@@ -1294,21 +1354,30 @@ public class NondetModelChecker extends NonProbModelChecker
 
 	/**
 	 * Compute rewards for a total reward operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
 	 */
-	protected StateValues checkRewardTotal(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException
+	protected StateValues checkRewardTotal(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min, JDDNode statesOfInterest) throws PrismException
 	{
+		// currently, ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
 		StateValues rewards = computeTotalRewards(trans, trans01, transActions, stateRewards, transRewards, min);
 		return rewards;
 	}
 
 	/**
 	 * Compute rewards for an instantaneous reward operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
 	 */
-	protected StateValues checkRewardInst(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException
+	protected StateValues checkRewardInst(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min, JDDNode statesOfInterest) throws PrismException
 	{
 		int time; // time bound
 		StateValues rewards = null;
 
+		// currently, ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
+
 		// get info from bounded until
 		time = expr.getUpperBound().evaluateInt(constantValues);
 		if (time < 0) {
@@ -1322,33 +1391,42 @@ public class NondetModelChecker extends NonProbModelChecker
 	}
 
 	/**
-	 * Compute rewards for a reachability reward operator.
+	 * Compute rewards for a reachability reward operator (either simple reachability or co-safe LTL).
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
 	 */
-	protected StateValues checkRewardPathFormula(Expression expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException
+	protected StateValues checkRewardPathFormula(Expression expr, JDDNode stateRewards, JDDNode transRewards, boolean min, JDDNode statesOfInterest) throws PrismException
 	{
 		if (Expression.isReach(expr)) {
-			return checkRewardReach((ExpressionTemporal) expr, stateRewards, transRewards, min);
+			return checkRewardReach((ExpressionTemporal) expr, stateRewards, transRewards, min, statesOfInterest);
 		}
 		else if (Expression.isCoSafeLTLSyntactic(expr, true)) {
-			return checkRewardCoSafeLTL(expr, stateRewards, transRewards, min);
+			return checkRewardCoSafeLTL(expr, stateRewards, transRewards, min, statesOfInterest);
 		}
+		JDD.Deref(statesOfInterest);
 		throw new PrismException("R operator contains a path formula that is not syntactically co-safe: " + expr);
 	}
-	
-	// reach reward
 
-	protected StateValues checkRewardReach(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException
+	/**
+	 * Compute rewards for a reachability reward operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkRewardReach(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min, JDDNode statesOfInterest) throws PrismException
 	{
 		JDDNode b;
 		StateValues rewards = null;
 
+		// currently, ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
+
 		// No time bounds allowed
 		if (expr.hasBounds()) {
 			throw new PrismNotSupportedException("R operator cannot contain a bounded F operator: " + expr);
 		}
 		
-		// model check operand first
-		b = checkExpressionDD(expr.getOperand2());
+		// model check operand first, statesOfInterest = all
+		b = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
 
 		// print out some info about num states
 		// mainLog.print("\nb = " + JDD.GetNumMintermsString(b,
@@ -1368,9 +1446,12 @@ public class NondetModelChecker extends NonProbModelChecker
 		return rewards;
 	}
 
-	// co-safe LTL reward
-
-	protected StateValues checkRewardCoSafeLTL(Expression expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException
+	/**
+	 * Compute rewards for a co-safe LTL reward operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkRewardCoSafeLTL(Expression expr, JDDNode stateRewards, JDDNode transRewards, boolean min, JDDNode statesOfInterest) throws PrismException
 	{
 		LTLModelChecker mcLtl;
 		StateValues rewardsProduct = null, rewards = null;
@@ -1384,6 +1465,9 @@ public class NondetModelChecker extends NonProbModelChecker
 		int i;
 		long l;
 
+		// currently, ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
+
 		if (Expression.containsTemporalTimeBounds(expr)) {
 			if (model.getModelType().continuousTime()) {
 				throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");

prism/src/prism/ProbModelChecker.java

@@ -124,26 +124,26 @@ public class ProbModelChecker extends NonProbModelChecker
 	// -----------------------------------------------------------------------------------
 
 	// Check expression (recursive)
-
-	public StateValues checkExpression(Expression expr) throws PrismException
+	@Override
+	public StateValues checkExpression(Expression expr, JDDNode statesOfInterest) throws PrismException
 	{
 		StateValues res;
 
 		// P operator
 		if (expr instanceof ExpressionProb) {
-			res = checkExpressionProb((ExpressionProb) expr);
+			res = checkExpressionProb((ExpressionProb) expr, statesOfInterest);
 		}
 		// R operator
 		else if (expr instanceof ExpressionReward) {
-			res = checkExpressionReward((ExpressionReward) expr);
+			res = checkExpressionReward((ExpressionReward) expr, statesOfInterest);
 		}
 		// S operator
 		else if (expr instanceof ExpressionSS) {
-			res = checkExpressionSteadyState((ExpressionSS) expr);
+			res = checkExpressionSteadyState((ExpressionSS) expr, statesOfInterest);
 		}
 		// Otherwise, use the superclass
 		else {
-			res = super.checkExpression(expr);
+			res = super.checkExpression(expr, statesOfInterest);
 		}
 
 		// Filter out non-reachable states from solution
@@ -160,7 +160,12 @@ public class ProbModelChecker extends NonProbModelChecker
 
 	// P operator
 
-	protected StateValues checkExpressionProb(ExpressionProb expr) throws PrismException
+	/**
+	 * Check a P (probability) operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkExpressionProb(ExpressionProb expr, JDDNode statesOfInterest) throws PrismException
 	{
 		// Get info from P operator
 		OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues);
@@ -169,9 +174,11 @@ public class ProbModelChecker extends NonProbModelChecker
 		if (opInfo.isTriviallyTrue()) {
 			mainLog.printWarning("Checking for probability " + opInfo.relOpBoundString() + " - formula trivially satisfies all states");
 			JDD.Ref(reach);
+			JDD.Deref(statesOfInterest);
 			return new StateValuesMTBDD(reach, model);
 		} else if (opInfo.isTriviallyFalse()) {
 			mainLog.printWarning("Checking for probability " + opInfo.relOpBoundString() + " - formula trivially satisfies no states");
+			JDD.Deref(statesOfInterest);
 			return new StateValuesMTBDD(JDD.Constant(0), model);
 		}
 
@@ -182,7 +189,7 @@ public class ProbModelChecker extends NonProbModelChecker
 
 		// Compute probabilities
 		boolean qual = opInfo.isQualitative() && precomp && prob0 && prob1;
-		StateValues probs = checkProbPathFormula(expr.getExpression(), qual);
+		StateValues probs = checkProbPathFormula(expr.getExpression(), qual, statesOfInterest);
 
 		// Print out probabilities
 		if (prism.getVerbose()) {
@@ -207,8 +214,13 @@ public class ProbModelChecker extends NonProbModelChecker
 	}
 
 	// R operator
-
-	protected StateValues checkExpressionReward(ExpressionReward expr) throws PrismException
+	
+	/**
+	 * Check an R (reward) operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkExpressionReward(ExpressionReward expr, JDDNode statesOfInterest) throws PrismException
 	{
 		// Get info from R operator
 		OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues);
@@ -231,20 +243,20 @@ public class ProbModelChecker extends NonProbModelChecker
 			switch (exprTemp.getOperator()) {
 			case ExpressionTemporal.R_C:
 				if (exprTemp.hasBounds()) {
-					rewards = checkRewardCumul(exprTemp, stateRewards, transRewards);
+					rewards = checkRewardCumul(exprTemp, stateRewards, transRewards, statesOfInterest);
 				} else {
-					rewards = checkRewardTotal(exprTemp, stateRewards, transRewards);
+					rewards = checkRewardTotal(exprTemp, stateRewards, transRewards, statesOfInterest);
 				}
 				break;
 			case ExpressionTemporal.R_I:
-				rewards = checkRewardInst(exprTemp, stateRewards, transRewards);
+				rewards = checkRewardInst(exprTemp, stateRewards, transRewards, statesOfInterest);
 				break;
 			case ExpressionTemporal.R_S:
-				rewards = checkRewardSS(exprTemp, stateRewards, transRewards);
+				rewards = checkRewardSS(exprTemp, stateRewards, transRewards, statesOfInterest);
 				break;
 			}
 		} else if (expr2.getType() instanceof TypePathBool || expr2.getType() instanceof TypeBool) {
-			rewards = checkRewardPathFormula(expr2, stateRewards, transRewards);
+			rewards = checkRewardPathFormula(expr2, stateRewards, transRewards, statesOfInterest);
 		}
 		
 		if (rewards == null)
@@ -274,7 +286,12 @@ public class ProbModelChecker extends NonProbModelChecker
 
 	// S operator
 
-	protected StateValues checkExpressionSteadyState(ExpressionSS expr) throws PrismException
+	/**
+	 * Check an S (steady-state) operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkExpressionSteadyState(ExpressionSS expr, JDDNode statesOfInterest) throws PrismException
 	{
 		// BSCC stuff
 		List<JDDNode> bsccs = null;
@@ -286,6 +303,8 @@ public class ProbModelChecker extends NonProbModelChecker
 		int i, numBSCCs = 0;
 		double d, probBSCCs[];
 
+		JDD.Deref(statesOfInterest);
+
 		// Get info from S operator
 		OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues);
 
@@ -300,8 +319,8 @@ public class ProbModelChecker extends NonProbModelChecker
 		}
 
 		try {
-			// Model check argument
-			b = checkExpressionDD(expr.getExpression());
+			// Model check argument with stateOfInterest = all
+			b = checkExpressionDD(expr.getExpression(), model.getReach().copy());
 
 			// Compute bottom strongly connected components (BSCCs)
 			if (bsccComp) {
@@ -438,7 +457,14 @@ public class ProbModelChecker extends NonProbModelChecker
 
 	// Contents of a P operator
 
-	protected StateValues checkProbPathFormula(Expression expr, boolean qual) throws PrismException
+	/**
+	 * Check a P operator path formula.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 *
+	 * @param qual perform qualitative model checking
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkProbPathFormula(Expression expr, boolean qual, JDDNode statesOfInterest) throws PrismException
 	{
 		// Test whether this is a simple path formula (i.e. PCTL)
 		// and whether we want to use the corresponding algorithms
@@ -453,13 +479,20 @@ public class ProbModelChecker extends NonProbModelChecker
 		}
 
 		if (useSimplePathAlgo) {
-			return checkProbPathFormulaSimple(expr, qual);
+			return checkProbPathFormulaSimple(expr, qual, statesOfInterest);
 		} else {
-			return checkProbPathFormulaLTL(expr, qual);
+			return checkProbPathFormulaLTL(expr, qual, statesOfInterest);
 		}
 	}
 
-	protected StateValues checkProbPathFormulaSimple(Expression expr, boolean qual) throws PrismException
+	/**
+	 * Check a P operator simple path formula (single, non-nested temporal operator).
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 *
+	 * @param qual perform qualitative model checking
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkProbPathFormulaSimple(Expression expr, boolean qual, JDDNode statesOfInterest) throws PrismException
 	{
 		boolean negated = false;
 		StateValues probs = null;
@@ -477,14 +510,14 @@ public class ProbModelChecker extends NonProbModelChecker
 			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
 			// Next
 			if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
-				probs = checkProbNext(exprTemp);
+				probs = checkProbNext(exprTemp, statesOfInterest);
 			}
 			// Until
 			else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
 				if (exprTemp.hasBounds()) {
-					probs = checkProbBoundedUntil(exprTemp);
+					probs = checkProbBoundedUntil(exprTemp, statesOfInterest);
 				} else {
-					probs = checkProbUntil(exprTemp, qual);
+					probs = checkProbUntil(exprTemp, qual, statesOfInterest);
 				}
 			}
 		}
@@ -500,9 +533,14 @@ public class ProbModelChecker extends NonProbModelChecker
 		return probs;
 	}
 
-	// LTL-like path formula for P operator
-
-	protected StateValues checkProbPathFormulaLTL(Expression expr, boolean qual) throws PrismException
+	/**
+	 * Check a P operator LTL-like path formula.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 *
+	 * @param qual perform qualitative model checking
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkProbPathFormulaLTL(Expression expr, boolean qual, JDDNode statesOfInterest) throws PrismException
 	{
 		LTLModelChecker mcLtl;
 		StateValues probsProduct = null, probs = null;
@@ -514,6 +552,9 @@ public class ProbModelChecker extends NonProbModelChecker
 		JDDVars daDDRowVars, daDDColVars;
 		int i;
 
+		// TODO: take statesOfInterest into account for product construction
+		JDD.Deref(statesOfInterest);
+
 		AcceptanceType[] allowedAcceptance = {
 				AcceptanceType.RABIN,
 				AcceptanceType.REACH,
@@ -587,15 +628,20 @@ public class ProbModelChecker extends NonProbModelChecker
 		return probs;
 	}
 
-	// next
-
-	protected StateValues checkProbNext(ExpressionTemporal expr) throws PrismException
+	/**
+	 * Check a P operator with a next operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkProbNext(ExpressionTemporal expr, JDDNode statesOfInterest) throws PrismException
 	{
 		JDDNode b;
 		StateValues probs = null;
 
-		// model check operand first
-		b = checkExpressionDD(expr.getOperand2());
+		JDD.Deref(statesOfInterest);
+
+		// model check operand first, stateOfInterest = all
+		b = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
 
 		// print out some info about num states
 		// mainLog.print("\nb = " + JDD.GetNumMintermsString(b,
@@ -610,9 +656,12 @@ public class ProbModelChecker extends NonProbModelChecker
 		return probs;
 	}
 
-	// bounded until
-
-	protected StateValues checkProbBoundedUntil(ExpressionTemporal expr) throws PrismException
+	/**
+	 * Check a P operator with a bounded until operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkProbBoundedUntil(ExpressionTemporal expr, JDDNode statesOfInterest) throws PrismException
 	{
 		JDDNode b1, b2;
 		StateValues probs = null;
@@ -620,13 +669,16 @@ public class ProbModelChecker extends NonProbModelChecker
 		IntegerBound bounds;
 		int i;
 
+		// currently, we ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
+
 		// get and check bounds information
 		bounds = IntegerBound.fromExpressionTemporal(expr, constantValues, true);
 
-		// model check operands first
-		b1 = checkExpressionDD(expr.getOperand1());
+		// model check operands first, statesOfInterest = all
+		b1 = checkExpressionDD(expr.getOperand1(), model.getReach().copy());
 		try {
-			b2 = checkExpressionDD(expr.getOperand2());
+			b2 = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
 		} catch (PrismException e) {
 			JDD.Deref(b1);
 			throw e;
@@ -689,19 +741,24 @@ public class ProbModelChecker extends NonProbModelChecker
 		return probs;
 	}
 
-	// until (unbounded)
-
+	/**
+	 * Check a P operator with an unbounded until operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
 	// this method is split into two steps so that the LTL model checker can use the second part directly
-
-	protected StateValues checkProbUntil(ExpressionTemporal expr, boolean qual) throws PrismException
+	protected StateValues checkProbUntil(ExpressionTemporal expr, boolean qual, JDDNode statesOfInterest) throws PrismException
 	{
 		JDDNode b1, b2;
 		StateValues probs = null;
 
-		// model check operands first
-		b1 = checkExpressionDD(expr.getOperand1());
+		// currently, ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
+
+		// model check operands first, statesOfInterest = all
+		b1 = checkExpressionDD(expr.getOperand1(), model.getReach().copy());
 		try {
-			b2 = checkExpressionDD(expr.getOperand2());
+			b2 = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
 		} catch (PrismException e) {
 			JDD.Deref(b1);
 			throw e;
@@ -728,8 +785,11 @@ public class ProbModelChecker extends NonProbModelChecker
 		return probs;
 	}
 
-	// until (unbounded): b1/b2 are bdds for until operands
-
+	/**
+	 * Check a P operator with an unbounded until operator (b1 U b2)
+	 * @param qual perform qualitative model checking?
+	 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
+	 */
 	protected StateValues checkProbUntil(JDDNode b1, JDDNode b2, boolean qual) throws PrismException
 	{
 		StateValues probs = null;
@@ -750,13 +810,19 @@ public class ProbModelChecker extends NonProbModelChecker
 		return probs;
 	}
 
-	// cumulative reward
-
-	protected StateValues checkRewardCumul(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards) throws PrismException
+	/**
+	 * Check a cumulative reward operator (C<=t).
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkRewardCumul(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, JDDNode statesOfInterest) throws PrismException
 	{
 		int time; // time
 		StateValues rewards = null;
 
+		// currently, ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
+
 		// check that there is an upper time bound
 		if (expr.getUpperBound() == null) {
 			throw new PrismException("Cumulative reward operator without time bound (C) is only allowed for multi-objective queries");
@@ -785,21 +851,33 @@ public class ProbModelChecker extends NonProbModelChecker
 		return rewards;
 	}
 
-	// cumulative reward
-
-	protected StateValues checkRewardTotal(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards) throws PrismException
+	/**
+	 * Check a total reward operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkRewardTotal(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, JDDNode statesOfInterest) throws PrismException
 	{
+		// currently, we ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
+
 		StateValues rewards = computeTotalRewards(trans, trans01, stateRewards, transRewards);
 		return rewards;
 	}
 
-	// inst reward
-
-	protected StateValues checkRewardInst(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards) throws PrismException
+	/**
+	 * Check an instantaneous reward operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkRewardInst(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, JDDNode statesOfInterest) throws PrismException
 	{
 		int time; // time
 		StateValues rewards = null;
 
+		// currently, we ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
+
 		// get info from inst reward
 		time = expr.getUpperBound().evaluateInt(constantValues);
 		if (time < 0) {
@@ -813,33 +891,42 @@ public class ProbModelChecker extends NonProbModelChecker
 	}
 
 	/**
-	 * Compute rewards for a reachability reward operator.
+	 * Check a reachability reward operator (either simple or using co-safety LTL).
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
 	 */
-	protected StateValues checkRewardPathFormula(Expression expr, JDDNode stateRewards, JDDNode transRewards) throws PrismException
+	protected StateValues checkRewardPathFormula(Expression expr, JDDNode stateRewards, JDDNode transRewards, JDDNode statesOfInterest) throws PrismException
 	{
 		if (Expression.isReach(expr)) {
-			return checkRewardReach((ExpressionTemporal) expr, stateRewards, transRewards);
+			return checkRewardReach((ExpressionTemporal) expr, stateRewards, transRewards, statesOfInterest);
 		}
 		else if (Expression.isCoSafeLTLSyntactic(expr, true)) {
-			return checkRewardCoSafeLTL(expr, stateRewards, transRewards);
+			return checkRewardCoSafeLTL(expr, stateRewards, transRewards, statesOfInterest);
 		}
+		JDD.Deref(statesOfInterest);
 		throw new PrismException("R operator contains a path formula that is not syntactically co-safe: " + expr);
 	}
-	
-	// reach reward
 
-	protected StateValues checkRewardReach(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards) throws PrismException
+	/**
+	 * Check a reachability reward operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkRewardReach(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, JDDNode statesOfInterest) throws PrismException
 	{
 		JDDNode b;
 		StateValues rewards = null;
 
+		// currently, we ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
+
 		// No time bounds allowed
 		if (expr.hasBounds()) {
 			throw new PrismNotSupportedException("R operator cannot contain a bounded F operator: " + expr);
 		}
 		
 		// model check operand first
-		b = checkExpressionDD(expr.getOperand2());
+		b = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
 
 		// print out some info about num states
 		// mainLog.print("\nb = " + JDD.GetNumMintermsString(b,
@@ -859,9 +946,12 @@ public class ProbModelChecker extends NonProbModelChecker
 		return rewards;
 	}
 
-	// co-safe LTL reward
-
-	protected StateValues checkRewardCoSafeLTL(Expression expr, JDDNode stateRewards, JDDNode transRewards) throws PrismException
+	/**
+	 * Check a co-safe LTL reward operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkRewardCoSafeLTL(Expression expr, JDDNode stateRewards, JDDNode transRewards, JDDNode statesOfInterest) throws PrismException
 	{
 		LTLModelChecker mcLtl;
 		StateValues rewardsProduct = null, rewards = null;
@@ -875,6 +965,9 @@ public class ProbModelChecker extends NonProbModelChecker
 		int i;
 		long l;
 
+		// currently, ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
+
 		if (Expression.containsTemporalTimeBounds(expr)) {
 			if (model.getModelType().continuousTime()) {
 				throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
@@ -995,9 +1088,12 @@ public class ProbModelChecker extends NonProbModelChecker
 		return rewards;
 	}
 
-	// steady state reward
-
-	protected StateValues checkRewardSS(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards) throws PrismException
+	/**
+	 * Check a steady-state reward operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkRewardSS(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, JDDNode statesOfInterest) throws PrismException
 	{
 		// bscc stuff
 		List<JDDNode> vectBSCCs;
@@ -1009,6 +1105,9 @@ public class ProbModelChecker extends NonProbModelChecker
 		int i, numBSCCs;
 		double d, rewBSCCs[];
 
+		// currently, ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
+
 		// compute rewards corresponding to each state
 		JDD.Ref(trans);
 		JDD.Ref(transRewards);

prism/src/prism/StateModelChecker.java

@@ -191,9 +191,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		model.clear();
 	}
 
-	/**
-	 * Model check an expression, process and return the result.
-	 */
+	@Override
 	public Result check(Expression expr) throws PrismException
 	{
 		long timer = 0;
@@ -217,7 +215,8 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		
 		// Do model checking and store result vector
 		timer = System.currentTimeMillis();
-		vals = checkExpression(expr);
+		// check expression, statesOfInterest = all reachable states
+		vals = checkExpression(expr, model.getReach().copy());
 		timer = System.currentTimeMillis() - timer;
 		mainLog.println("\nTime for model checking: " + timer / 1000.0 + " seconds.");
 
@@ -235,28 +234,26 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		return result;
 	}
 
-	/**
-	 * Model check an expression and return a vector result values over all states.
-	 */
-	public StateValues checkExpression(Expression expr) throws PrismException
+	@Override
+	public StateValues checkExpression(Expression expr, JDDNode statesOfInterest) throws PrismException
 	{
 		StateValues res;
 
 		// If-then-else
 		if (expr instanceof ExpressionITE) {
-			res = checkExpressionITE((ExpressionITE) expr);
+			res = checkExpressionITE((ExpressionITE) expr, statesOfInterest);
 		}
 		// Binary ops
 		else if (expr instanceof ExpressionBinaryOp) {
-			res = checkExpressionBinaryOp((ExpressionBinaryOp) expr);
+			res = checkExpressionBinaryOp((ExpressionBinaryOp) expr, statesOfInterest);
 		}
 		// Unary ops
 		else if (expr instanceof ExpressionUnaryOp) {
-			res = checkExpressionUnaryOp((ExpressionUnaryOp) expr);
+			res = checkExpressionUnaryOp((ExpressionUnaryOp) expr, statesOfInterest);
 		}
 		// Functions
 		else if (expr instanceof ExpressionFunc) {
-			res = checkExpressionFunc((ExpressionFunc) expr);
+			res = checkExpressionFunc((ExpressionFunc) expr, statesOfInterest);
 		}
 		// Identifiers
 		else if (expr instanceof ExpressionIdent) {
@@ -265,38 +262,39 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		}
 		// Literals
 		else if (expr instanceof ExpressionLiteral) {
-			res = checkExpressionLiteral((ExpressionLiteral) expr);
+			res = checkExpressionLiteral((ExpressionLiteral) expr, statesOfInterest);
 		}
 		// Constants
 		else if (expr instanceof ExpressionConstant) {
-			res = checkExpressionConstant((ExpressionConstant) expr);
+			res = checkExpressionConstant((ExpressionConstant) expr, statesOfInterest);
 		}
 		// Formulas
 		else if (expr instanceof ExpressionFormula) {
 			// This should have been defined or expanded by now.
 			if (((ExpressionFormula) expr).getDefinition() != null)
-				return checkExpression(((ExpressionFormula) expr).getDefinition());
+				return checkExpression(((ExpressionFormula) expr).getDefinition(), statesOfInterest);
 			else
 				throw new PrismException("Unexpanded formula \"" + ((ExpressionFormula) expr).getName() + "\"");
 		}
 		// Variables
 		else if (expr instanceof ExpressionVar) {
-			res = checkExpressionVar((ExpressionVar) expr);
+			res = checkExpressionVar((ExpressionVar) expr, statesOfInterest);
 		}
 		// Labels
 		else if (expr instanceof ExpressionLabel) {
-			res = checkExpressionLabel((ExpressionLabel) expr);
+			res = checkExpressionLabel((ExpressionLabel) expr, statesOfInterest);
 		}
 		// Property refs
 		else if (expr instanceof ExpressionProp) {
-			res = checkExpressionProp((ExpressionProp) expr);
+			res = checkExpressionProp((ExpressionProp) expr, statesOfInterest);
 		}
 		// Filter
 		else if (expr instanceof ExpressionFilter) {
-			res = checkExpressionFilter((ExpressionFilter) expr);
+			res = checkExpressionFilter((ExpressionFilter) expr, statesOfInterest);
 		}
 		// Anything else - error
 		else {
+			JDD.Deref(statesOfInterest);
 			throw new PrismException("Couldn't check " + expr.getClass());
 		}
 
@@ -309,11 +307,10 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		return res;
 	}
 
-	// Check expression, convert to symbolic form (if not already), return BDD
-
-	public JDDNode checkExpressionDD(Expression expr) throws PrismException
+	@Override
+	public JDDNode checkExpressionDD(Expression expr, JDDNode statesOfInterest) throws PrismException
 	{
-		return checkExpression(expr).convertToStateValuesMTBDD().getJDDNode();
+		return checkExpression(expr, statesOfInterest).convertToStateValuesMTBDD().getJDDNode();
 	}
 
 	// -----------------------------------------------------------------------------------
@@ -348,8 +345,12 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 	 * properties, the vector will be stored symbolically since values are Booleans. 
 	 */
 
-	// Check an 'if-then-else'
-	protected StateValues checkExpressionITE(ExpressionITE expr) throws PrismException
+	/**
+	 * Check an 'if-then-else' expression.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkExpressionITE(ExpressionITE expr, JDDNode statesOfInterest) throws PrismException
 	{
 		StateValues res1 = null, res2 = null, res3 = null;
 		JDDNode dd, dd1, dd2, dd3;
@@ -357,15 +358,17 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 
 		// Check operands recursively
 		try {
-			res1 = checkExpression(expr.getOperand1());
-			res2 = checkExpression(expr.getOperand2());
-			res3 = checkExpression(expr.getOperand3());
+			res1 = checkExpression(expr.getOperand1(), statesOfInterest.copy());
+			res2 = checkExpression(expr.getOperand2(), statesOfInterest.copy());
+			res3 = checkExpression(expr.getOperand3(), statesOfInterest.copy());
 		} catch (PrismException e) {
 			if (res1 != null)
 				res1.clear();
 			if (res2 != null)
 				res2.clear();
 			throw e;
+		} finally {
+			JDD.Deref(statesOfInterest);
 		}
 
 		// Operand 1 is boolean so should be symbolic
@@ -392,9 +395,12 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		}
 	}
 
-	// Check a binary operator
-
-	protected StateValues checkExpressionBinaryOp(ExpressionBinaryOp expr) throws PrismException
+	/**
+	 * Check a binary operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkExpressionBinaryOp(ExpressionBinaryOp expr, JDDNode statesOfInterest) throws PrismException
 	{
 		StateValues res1 = null, res2 = null;
 		JDDNode dd, dd1, dd2;
@@ -404,17 +410,19 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		// Optimisations are possible for relational operators
 		// (note dubious use of knowledge that op IDs are consecutive)
 		if (op >= ExpressionBinaryOp.EQ && op <= ExpressionBinaryOp.LE) {
-			return checkExpressionRelOp(op, expr.getOperand1(), expr.getOperand2());
+			return checkExpressionRelOp(op, expr.getOperand1(), expr.getOperand2(), statesOfInterest);
 		}
 
 		// Check operands recursively
 		try {
-			res1 = checkExpression(expr.getOperand1());
-			res2 = checkExpression(expr.getOperand2());
+			res1 = checkExpression(expr.getOperand1(), statesOfInterest.copy());
+			res2 = checkExpression(expr.getOperand2(), statesOfInterest.copy());
 		} catch (PrismException e) {
 			if (res1 != null)
 				res1.clear();
 			throw e;
+		} finally {
+			JDD.Deref(statesOfInterest);
 		}
 
 		// If both operands are symbolic, result will be symbolic
@@ -490,9 +498,12 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		}
 	}
 
-	// Check a relational operator (=, !=, >, >=, < <=)
-
-	protected StateValues checkExpressionRelOp(int op, Expression expr1, Expression expr2) throws PrismException
+	/**
+	 * Check a relational operator (=, !=, >, >=, < <=).
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkExpressionRelOp(int op, Expression expr1, Expression expr2, JDDNode statesOfInterest) throws PrismException
 	{
 		StateValues res1 = null, res2 = null;
 		JDDNode dd, dd1, dd2;
@@ -503,6 +514,8 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 
 		// var relop int
 		if (expr1 instanceof ExpressionVar && expr2.isConstant() && expr2.getType() instanceof TypeInt) {
+			JDD.Deref(statesOfInterest);
+
 			ExpressionVar e1;
 			Expression e2;
 			int i, j, l, h, v;
@@ -553,6 +566,8 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		}
 		// int relop var
 		else if (expr1.isConstant() && expr1.getType() instanceof TypeInt && expr2 instanceof ExpressionVar) {
+			JDD.Deref(statesOfInterest);
+
 			Expression e1;
 			ExpressionVar e2;
 			int i, j, l, h, v;
@@ -607,12 +622,14 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		// just convert both operands to MTBDDs first. Optimisations would be possible here.
 		// Check operands recursively
 		try {
-			res1 = checkExpression(expr1);
-			res2 = checkExpression(expr2);
+			res1 = checkExpression(expr1, statesOfInterest.copy());
+			res2 = checkExpression(expr2, statesOfInterest.copy());
 		} catch (PrismException e) {
 			if (res1 != null)
 				res1.clear();
 			throw e;
+		} finally {
+			JDD.Deref(statesOfInterest);
 		}
 		dd1 = res1.convertToStateValuesMTBDD().getJDDNode();
 		dd2 = res2.convertToStateValuesMTBDD().getJDDNode();
@@ -641,9 +658,12 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		return new StateValuesMTBDD(dd, model);
 	}
 
-	// Check a unary operator
-
-	protected StateValues checkExpressionUnaryOp(ExpressionUnaryOp expr) throws PrismException
+	/**
+	 * Check a unary operator.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkExpressionUnaryOp(ExpressionUnaryOp expr, JDDNode statesOfInterest) throws PrismException
 	{
 		StateValues res1 = null;
 		JDDNode dd, dd1;
@@ -651,7 +671,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		int i, n, op = expr.getOperator();
 
 		// Check operand recursively
-		res1 = checkExpression(expr.getOperand());
+		res1 = checkExpression(expr.getOperand(), statesOfInterest);
 
 		// Parentheses are easy - nothing to do:
 		if (op == ExpressionUnaryOp.PARENTH)
@@ -693,29 +713,39 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		}
 	}
 
-	// Check a 'function'
-
-	protected StateValues checkExpressionFunc(ExpressionFunc expr) throws PrismException
+	/**
+	 * Check a 'function'.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkExpressionFunc(ExpressionFunc expr, JDDNode statesOfInterest) throws PrismException
 	{
 		switch (expr.getNameCode()) {
 		case ExpressionFunc.MIN:
 		case ExpressionFunc.MAX:
-			return checkExpressionFuncNary(expr);
+			return checkExpressionFuncNary(expr, statesOfInterest);
 		case ExpressionFunc.FLOOR:
 		case ExpressionFunc.CEIL:
-			return checkExpressionFuncUnary(expr);
+			return checkExpressionFuncUnary(expr, statesOfInterest);
 		case ExpressionFunc.POW:
 		case ExpressionFunc.MOD:
 		case ExpressionFunc.LOG:
-			return checkExpressionFuncBinary(expr);
+			return checkExpressionFuncBinary(expr, statesOfInterest);
 		case ExpressionFunc.MULTI:
+			JDD.Deref(statesOfInterest);
 			throw new PrismException("Multi-objective model checking is not supported for " + model.getModelType() + "s");
 		default:
+			JDD.Deref(statesOfInterest);
 			throw new PrismException("Unrecognised function \"" + expr.getName() + "\"");
 		}
 	}
 
-	protected StateValues checkExpressionFuncUnary(ExpressionFunc expr) throws PrismException
+	/**
+	 * Check a unary 'function'.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkExpressionFuncUnary(ExpressionFunc expr, JDDNode statesOfInterest) throws PrismException
 	{
 		StateValues res1 = null;
 		JDDNode dd1;
@@ -723,7 +753,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		int i, n, op = expr.getNameCode();
 
 		// Check operand recursively
-		res1 = checkExpression(expr.getOperand(0));
+		res1 = checkExpression(expr.getOperand(0), statesOfInterest);
 		// Symbolic
 		if (res1 instanceof StateValuesMTBDD) {
 			dd1 = ((StateValuesMTBDD) res1).getJDDNode();
@@ -759,7 +789,12 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		}
 	}
 
-	protected StateValues checkExpressionFuncBinary(ExpressionFunc expr) throws PrismException
+	/**
+	 * Check a binary 'function'.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkExpressionFuncBinary(ExpressionFunc expr, JDDNode statesOfInterest) throws PrismException
 	{
 		StateValues res1 = null, res2 = null;
 		JDDNode dd = null, dd1, dd2;
@@ -769,12 +804,14 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 
 		// Check operands recursively
 		try {
-			res1 = checkExpression(expr.getOperand(0));
-			res2 = checkExpression(expr.getOperand(1));
+			res1 = checkExpression(expr.getOperand(0), statesOfInterest.copy());
+			res2 = checkExpression(expr.getOperand(1), statesOfInterest.copy());
 		} catch (PrismException e) {
 			if (res1 != null)
 				res1.clear();
 			throw e;
+		} finally {
+			JDD.Deref(statesOfInterest);
 		}
 		// If both operands are symbolic, result will be symbolic
 		if (res1 instanceof StateValuesMTBDD && res2 instanceof StateValuesMTBDD) {
@@ -849,7 +886,12 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		}
 	}
 
-	protected StateValues checkExpressionFuncNary(ExpressionFunc expr) throws PrismException
+	/**
+	 * Check an n-ary 'function'.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkExpressionFuncNary(ExpressionFunc expr, JDDNode statesOfInterest) throws PrismException
 	{
 		StateValues res1 = null, res2 = null;
 		JDDNode dd1, dd2;
@@ -858,17 +900,18 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		boolean symbolic;
 
 		// Check first operand recursively
-		res1 = checkExpression(expr.getOperand(0));
+		res1 = checkExpression(expr.getOperand(0), statesOfInterest.copy());
 		// Go through remaining operands
 		// Switch to explicit as soon as an operand is explicit
 		n = expr.getNumOperands();
 		symbolic = (res1 instanceof StateValuesMTBDD);
 		for (i = 1; i < n; i++) {
 			try {
-				res2 = checkExpression(expr.getOperand(i));
+				res2 = checkExpression(expr.getOperand(i), statesOfInterest.copy());
 			} catch (PrismException e) {
 				if (res2 != null)
 					res2.clear();
+				JDD.Deref(statesOfInterest);
 				throw e;
 			}
 			// Explicit
@@ -906,14 +949,24 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 			}
 		}
 
+		JDD.Deref(statesOfInterest);
 		return res1;
 	}
 
-	// Check a literal
-
-	protected StateValues checkExpressionLiteral(ExpressionLiteral expr) throws PrismException
+	/**
+	 * Check a literal.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkExpressionLiteral(ExpressionLiteral expr, JDDNode statesOfInterest) throws PrismException
 	{
 		JDDNode dd;
+
+		// it's more efficient to return the constant node
+		// instead of a MTBDD function for ITE(statesOfInterest, value, 0),
+		// so we ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
+
 		try {
 			dd = JDD.Constant(expr.evaluateDouble());
 		} catch (PrismLangException e) {
@@ -922,13 +975,21 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		return new StateValuesMTBDD(dd, model);
 	}
 
-	// Check a constant
-
-	protected StateValues checkExpressionConstant(ExpressionConstant expr) throws PrismException
+	/**
+	 * Check a constant.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkExpressionConstant(ExpressionConstant expr, JDDNode statesOfInterest) throws PrismException
 	{
 		int i;
 		JDDNode dd;
 
+		// it's more efficient to return the constant node
+		// instead of a MTBDD function for ITE(statesOfInterest, value, 0),
+		// so we ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
+
 		i = constantValues.getIndexOf(expr.getName());
 		if (i == -1)
 			throw new PrismException("Couldn't evaluate constant \"" + expr.getName() + "\"");
@@ -941,14 +1002,21 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		return new StateValuesMTBDD(dd, model);
 	}
 
-	// Check a variable reference
-
-	protected StateValues checkExpressionVar(ExpressionVar expr) throws PrismException
+	/**
+	 * Check a variable reference.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkExpressionVar(ExpressionVar expr, JDDNode statesOfInterest) throws PrismException
 	{
 		String s;
 		int v, l, h, i;
 		JDDNode dd;
 
+		// it's generally more efficient not to restrict to statesOfInterest here
+		// so we ignore statesOfInterest
+		JDD.Deref(statesOfInterest);
+
 		s = expr.getName();
 		// get the variable's index
 		v = varList.getIndex(s);
@@ -967,9 +1035,12 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		return new StateValuesMTBDD(dd, model);
 	}
 
-	// Check label
-
-	protected StateValues checkExpressionLabel(ExpressionLabel expr) throws PrismException
+	/**
+	 * Check a label.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkExpressionLabel(ExpressionLabel expr, JDDNode statesOfInterest) throws PrismException
 	{
 		LabelList ll;
 		JDDNode dd;
@@ -977,14 +1048,17 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 
 		// treat special cases
 		if (expr.isDeadlockLabel()) {
+			JDD.Deref(statesOfInterest);
 			dd = model.getDeadlocks();
 			JDD.Ref(dd);
 			return new StateValuesMTBDD(dd, model);
 		} else if (expr.isInitLabel()) {
+			JDD.Deref(statesOfInterest);
 			dd = start;
 			JDD.Ref(dd);
 			return new StateValuesMTBDD(dd, model);
 		} else if (model.hasLabelDD(expr.getName())) {
+			JDD.Deref(statesOfInterest);
 			dd = model.getLabelDD(expr.getName());
 			return new StateValuesMTBDD(dd.copy(), model);
 		} else {
@@ -996,27 +1070,35 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 			if (i == -1)
 				throw new PrismException("Unknown label \"" + expr.getName() + "\" in property");
 			// check recursively
-			return checkExpression(ll.getLabel(i));
+			return checkExpression(ll.getLabel(i), statesOfInterest);
 		}
 	}
 
-	// Check property ref
 
-	protected StateValues checkExpressionProp(ExpressionProp expr) throws PrismException
+	/**
+	 * Check a property reference.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkExpressionProp(ExpressionProp expr, JDDNode statesOfInterest) throws PrismException
 	{
 		// Look up property and check recursively
 		Property prop = propertiesFile.lookUpPropertyObjectByName(expr.getName());
 		if (prop != null) {
 			mainLog.println("\nModel checking : " + prop);
-			return checkExpression(prop.getExpression());
+			return checkExpression(prop.getExpression(), statesOfInterest);
 		} else {
+			JDD.Deref(statesOfInterest);
 			throw new PrismException("Unknown property reference " + expr);
 		}
 	}
 
-	// Check filter
-
-	protected StateValues checkExpressionFilter(ExpressionFilter expr) throws PrismException
+	/**
+	 * Check a filter.
+	 * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+	 * <br>[ REFS: <i>result</i>, DEREFS: statesOfInterest ]
+	 */
+	protected StateValues checkExpressionFilter(ExpressionFilter expr, JDDNode statesOfInterest) throws PrismException
 	{
 		// Translate filter
 		Expression filter = expr.getFilter();
@@ -1027,7 +1109,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		boolean filterTrue = Expression.isTrue(filter);
 		// Store some more info
 		String filterStatesString = filterTrue ? "all states" : "states satisfying filter";
-		JDDNode ddFilter = checkExpressionDD(filter);
+		JDDNode ddFilter = checkExpressionDD(filter, statesOfInterest.copy());
 		StateListMTBDD statesFilter = new StateListMTBDD(ddFilter, model);
 		// Check if filter state set is empty; we treat this as an error
 		if (ddFilter.equals(JDD.ZERO)) {
@@ -1057,10 +1139,11 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 
 		StateValues vals = null;
 		try {
-			// Check operand recursively
-			vals = checkExpression(expr.getOperand());
+			// Check operand recursively, using the filter as the states of interest
+			vals = checkExpression(expr.getOperand(), ddFilter.copy());
 		} catch (PrismException e) {
 			JDD.Deref(ddFilter);
+			JDD.Deref(statesOfInterest);
 			throw e;
 		}
 
@@ -1364,6 +1447,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		}
 		// Other derefs
 		JDD.Deref(ddFilter);
+		JDD.Deref(statesOfInterest);
 
 		return resVals;
 	}
@@ -1416,7 +1500,6 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		return transRewards; 
 	}
 
-	/** Get the constant values (both from the modules file and the properties file) */
 	@Override
 	public Values getConstantValues()
 	{
@@ -1466,7 +1549,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		int numLabels = labelNames.size();
 		JDDNode labels[] = new JDDNode[numLabels];
 		for (int i = 0; i < numLabels; i++) {
-			labels[i] = checkExpressionDD(new ExpressionLabel(labelNames.get(i)));
+			labels[i] = checkExpressionDD(new ExpressionLabel(labelNames.get(i)), model.getReach().copy());
 		}
 
 		// Export them using the MTBDD engine

prism/src/prism/StochModelChecker.java

@@ -78,14 +78,16 @@ public class StochModelChecker extends ProbModelChecker
 	// -----------------------------------------------------------------------------------
 
 	// bounded until
-
-	protected StateValues checkProbBoundedUntil(ExpressionTemporal expr) throws PrismException
+	@Override
+	protected StateValues checkProbBoundedUntil(ExpressionTemporal expr, JDDNode statesOfInterest) throws PrismException
 	{
 		double lTime, uTime; // time bounds
 		Expression exprTmp;
 		JDDNode b1, b2, tmp;
 		StateValues tmpProbs = null, probs = null;
 
+		JDD.Deref(statesOfInterest);
+
 		// get info from bounded until
 
 		// lower bound is 0 if not specified
@@ -115,10 +117,10 @@ public class StochModelChecker extends ProbModelChecker
 			uTime = -1;
 		}
 
-		// model check operands first
-		b1 = checkExpressionDD(expr.getOperand1());
+		// model check operands first, statesOfInterest = all
+		b1 = checkExpressionDD(expr.getOperand1(), model.getReach().copy());
 		try {
-			b2 = checkExpressionDD(expr.getOperand2());
+			b2 = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
 		} catch (PrismException e) {
 			JDD.Deref(b1);
 			throw e;
@@ -228,13 +230,15 @@ public class StochModelChecker extends ProbModelChecker
 	}
 
 	// cumulative reward
-
-	protected StateValues checkRewardCumul(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards)
+	@Override
+	protected StateValues checkRewardCumul(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, JDDNode statesOfInterest)
 			throws PrismException
 	{
 		double time; // time
 		StateValues rewards = null;
 
+		JDD.Deref(statesOfInterest);
+
 		// get info from inst reward
 		time = expr.getUpperBound().evaluateDouble(constantValues);
 		if (time < 0) {
@@ -260,12 +264,15 @@ public class StochModelChecker extends ProbModelChecker
 
 	// inst reward
 
-	protected StateValues checkRewardInst(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards)
+	@Override
+	protected StateValues checkRewardInst(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, JDDNode statesOfInterest)
 			throws PrismException
 	{
 		double time; // time
 		StateValues sr = null, rewards = null;
 
+		JDD.Deref(statesOfInterest);
+
 		// get info from inst reward
 		time = expr.getUpperBound().evaluateDouble(constantValues);
 		if (time < 0) {
@@ -391,7 +398,7 @@ public class StochModelChecker extends ProbModelChecker
 	// -----------------------------------------------------------------------------------
 
 	// compute probabilities for next
-
+	@Override
 	protected StateValues computeNextProbs(JDDNode tr, JDDNode b)
 	{
 		JDDNode diags, emb;
@@ -491,7 +498,7 @@ public class StochModelChecker extends ProbModelChecker
 	}
 
 	// compute probabilities for until (general case)
-
+	@Override
 	protected StateValues computeUntilProbs(JDDNode tr, JDDNode tr01, JDDNode b1, JDDNode b2) throws PrismException
 	{
 		JDDNode diags, emb;
@@ -555,6 +562,7 @@ public class StochModelChecker extends ProbModelChecker
 
 	// compute total rewards
 
+	@Override
 	protected StateValues computeTotalRewards(JDDNode tr, JDDNode tr01, JDDNode sr, JDDNode trr) throws PrismException
 	{
 		JDDNode diags, emb, srNew;
@@ -587,7 +595,7 @@ public class StochModelChecker extends ProbModelChecker
 	}
 	
 	// compute rewards for reach reward
-
+	@Override
 	protected StateValues computeReachRewards(JDDNode tr, JDDNode tr01, JDDNode sr, JDDNode trr, JDDNode b)
 			throws PrismException
 	{