Improvements to StateValues class + it's use in explicit model checking.

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

prism/src/explicit/CTMCModelChecker.java

@@ -93,8 +93,8 @@ public class CTMCModelChecker extends DTMCModelChecker
 		}
 
 		// model check operands first
-		b1 = (BitSet) checkExpression(model, expr.getOperand1());
-		b2 = (BitSet) checkExpression(model, expr.getOperand2());
+		b1 = checkExpression(model, expr.getOperand1()).getBitSet();
+		b2 = checkExpression(model, expr.getOperand2()).getBitSet();
 
 		// compute probabilities
 

prism/src/explicit/CTMDPModelChecker.java

@@ -55,8 +55,8 @@ public class CTMDPModelChecker extends MDPModelChecker
 		}
 
 		// model check operands first
-		b1 = (BitSet) checkExpression(model, expr.getOperand1());
-		b2 = (BitSet) checkExpression(model, expr.getOperand2());
+		b1 = checkExpression(model, expr.getOperand1()).getBitSet();
+		b2 = checkExpression(model, expr.getOperand2()).getBitSet();
 
 		// compute probabilities
 

prism/src/explicit/DTMCModelChecker.java

@@ -104,8 +104,8 @@ public class DTMCModelChecker extends ProbModelChecker
 		}
 
 		// model check operands first
-		b1 = (BitSet) checkExpression(model, expr.getOperand1());
-		b2 = (BitSet) checkExpression(model, expr.getOperand2());
+		b1 = checkExpression(model, expr.getOperand1()).getBitSet();
+		b2 = checkExpression(model, expr.getOperand2()).getBitSet();
 
 		// compute probabilities
 
@@ -131,8 +131,8 @@ public class DTMCModelChecker extends ProbModelChecker
 		ModelCheckerResult res = null;
 
 		// model check operands first
-		b1 = (BitSet) checkExpression(model, expr.getOperand1());
-		b2 = (BitSet) checkExpression(model, expr.getOperand2());
+		b1 = checkExpression(model, expr.getOperand1()).getBitSet();
+		b2 = checkExpression(model, expr.getOperand2()).getBitSet();
 
 		// print out some info about num states
 		// mainLog.print("\nb1 = " + JDD.GetNumMintermsString(b1,
@@ -180,7 +180,7 @@ public class DTMCModelChecker extends ProbModelChecker
 		ModelCheckerResult res = null;
 
 		// model check operand first
-		b = (BitSet) checkExpression(model, expr.getOperand2());
+		b = checkExpression(model, expr.getOperand2()).getBitSet();
 
 		// print out some info about num states
 		// mainLog.print("\nb = " + JDD.GetNumMintermsString(b1,

prism/src/explicit/MDPModelChecker.java

@@ -107,8 +107,8 @@ public class MDPModelChecker extends ProbModelChecker
 		}
 
 		// model check operands first
-		b1 = (BitSet) checkExpression(model, expr.getOperand1());
-		b2 = (BitSet) checkExpression(model, expr.getOperand2());
+		b1 = checkExpression(model, expr.getOperand1()).getBitSet();
+		b2 = checkExpression(model, expr.getOperand2()).getBitSet();
 
 		// print out some info about num states
 		// mainLog.print("\nb1 = " + JDD.GetNumMintermsString(b1,
@@ -140,8 +140,8 @@ public class MDPModelChecker extends ProbModelChecker
 		ModelCheckerResult res = null;
 
 		// model check operands first
-		b1 = (BitSet) checkExpression(model, expr.getOperand1());
-		b2 = (BitSet) checkExpression(model, expr.getOperand2());
+		b1 = checkExpression(model, expr.getOperand1()).getBitSet();
+		b2 = checkExpression(model, expr.getOperand2()).getBitSet();
 
 		// print out some info about num states
 		// mainLog.print("\nb1 = " + JDD.GetNumMintermsString(b1,
@@ -189,7 +189,7 @@ public class MDPModelChecker extends ProbModelChecker
 		ModelCheckerResult res = null;
 
 		// model check operand first
-		b = (BitSet) checkExpression(model, expr.getOperand2());
+		b = checkExpression(model, expr.getOperand2()).getBitSet();
 
 		// print out some info about num states
 		// mainLog.print("\nb = " + JDD.GetNumMintermsString(b1,

prism/src/explicit/ProbModelChecker.java

@@ -47,9 +47,9 @@ public class ProbModelChecker extends StateModelChecker
 	// Model checking functions
 
 	@Override
-	public Object checkExpression(Model model, Expression expr) throws PrismException
+	public StateValues checkExpression(Model model, Expression expr) throws PrismException
 	{
-		Object res;
+		StateValues res;
 
 		// P operator
 		if (expr instanceof ExpressionProb) {
@@ -74,7 +74,7 @@ public class ProbModelChecker extends StateModelChecker
 	/**
 	 * Model check a P operator expression and return the values for all states.
 	 */
-	protected Object checkExpressionProb(Model model, ExpressionProb expr) throws PrismException
+	protected StateValues checkExpressionProb(Model model, ExpressionProb expr) throws PrismException
 	{
 		Expression pb; // Probability bound (expression)
 		double p = 0; // Probability bound (actual value)
@@ -141,14 +141,14 @@ public class ProbModelChecker extends StateModelChecker
 		else {
 			BitSet sol = probs.getBitSetFromInterval(relOp, p);
 			probs.clear();
-			return sol;
+			return StateValues.createFromBitSet(sol, model.getNumStates());
 		}
 	}
 	
 	/**
 	 * Model check an R operator expression and return the values for all states.
 	 */
-	protected Object checkExpressionReward(Model model, ExpressionReward expr) throws PrismException
+	protected StateValues checkExpressionReward(Model model, ExpressionReward expr) throws PrismException
 	{
 		Object rs; // Reward struct index
 		RewardStruct rewStruct = null; // Reward struct object
@@ -246,7 +246,7 @@ public class ProbModelChecker extends StateModelChecker
 		else {
 			BitSet sol = rews.getBitSetFromInterval(relOp, r);
 			rews.clear();
-			return sol;
+			return StateValues.createFromBitSet(sol, model.getNumStates());
 		}
 	}
 }

prism/src/explicit/STPGModelChecker.java

@@ -105,8 +105,8 @@ public class STPGModelChecker extends ProbModelChecker
 		}
 
 		// model check operands first
-		b1 = (BitSet) checkExpression(model, expr.getOperand1());
-		b2 = (BitSet) checkExpression(model, expr.getOperand2());
+		b1 = checkExpression(model, expr.getOperand1()).getBitSet();
+		b2 = checkExpression(model, expr.getOperand2()).getBitSet();
 
 		// print out some info about num states
 		// mainLog.print("\nb1 = " + JDD.GetNumMintermsString(b1,
@@ -138,8 +138,8 @@ public class STPGModelChecker extends ProbModelChecker
 		ModelCheckerResult res = null;
 
 		// model check operands first
-		b1 = (BitSet) checkExpression(model, expr.getOperand1());
-		b2 = (BitSet) checkExpression(model, expr.getOperand2());
+		b1 = checkExpression(model, expr.getOperand1()).getBitSet();
+		b2 = checkExpression(model, expr.getOperand2()).getBitSet();
 
 		// print out some info about num states
 		// mainLog.print("\nb1 = " + JDD.GetNumMintermsString(b1,
@@ -165,7 +165,7 @@ public class STPGModelChecker extends ProbModelChecker
 		ModelCheckerResult res = null;
 
 		// model check operands first
-		target = (BitSet) checkExpression(model, expr.getOperand2());
+		target = checkExpression(model, expr.getOperand2()).getBitSet();
 
 		res = computeReachRewards((STPG) model, rewards, target, min1, min2);
 		rews = StateValues.createFromDoubleArray(res.soln);

prism/src/explicit/StateModelChecker.java

@@ -32,7 +32,9 @@ import java.util.*;
 import parser.State;
 import parser.Values;
 import parser.ast.*;
+import parser.ast.ExpressionFilter.FilterOperator;
 import parser.type.*;
+import prism.Prism;
 import prism.PrismException;
 import prism.PrismLog;
 import prism.PrismPrintStreamLog;
@@ -336,7 +338,7 @@ public class StateModelChecker
 
 		// Do model checking and store result vector
 		timer = System.currentTimeMillis();
-		vals = checkExpression(model, expr);
+		valsSV = checkExpression(model, expr);
 		timer = System.currentTimeMillis() - timer;
 		mainLog.println("\nTime for model checking: " + timer / 1000.0 + " seconds.");
 
@@ -344,7 +346,7 @@ public class StateModelChecker
 		if (expr.getType() instanceof TypeBool) {
 
 			// Cast to Bitset
-			valsBitSet = (BitSet) vals;
+			valsBitSet = valsSV.getBitSet();
 			// And check how many states are satisfying
 			numSat = valsBitSet.cardinality();
 
@@ -403,9 +405,6 @@ public class StateModelChecker
 			// Result returned depends on the number of initial states
 			// and whether it is just a single value (e.g. from if the top-level operator is a filter)
 
-			// Cast to Bitset
-			valsSV = (StateValues) vals;
-
 			// Case where this is a single value (e.g. filter)
 			if (expr.returnsSingleValue()) {
 				// Get result for initial state (although it is the same for all states)
@@ -442,7 +441,7 @@ public class StateModelChecker
 				// If in "verbose" mode, print out result values to log
 				if (getVerbosity() > 5) {
 					mainLog.println("\nResults (non-zero only) for all states:");
-					mainLog.print(vals);
+					mainLog.print(valsSV);
 				}
 			}
 		}
@@ -470,9 +469,9 @@ public class StateModelChecker
 	 * {@link #setModulesFile} and {@link #setPropertiesFile}
 	 * to attach the original model/properties files.
 	 */
-	public Object checkExpression(Model model, Expression expr) throws PrismException
+	public StateValues checkExpression(Model model, Expression expr) throws PrismException
 	{
-		Object res = null;
+		StateValues res = null;
 
 		// Binary ops
 		// (just "and" for now - more to come later)
@@ -493,7 +492,7 @@ public class StateModelChecker
 		}
 		// Filter
 		else if (expr instanceof ExpressionFilter) {
-			throw new PrismException("Explicit engine does not yet handle filters");
+			res = checkExpressionFilter(model, (ExpressionFilter) expr);
 		}
 
 		// Anything else - just evaluate expression repeatedly
@@ -501,30 +500,21 @@ public class StateModelChecker
 			// Evaluate/replace any constants first
 			expr = (Expression) expr.replaceConstants(constantValues);
 			
+			int numStates = model.getNumStates();
+			res = new StateValues(expr.getType(), numStates);
+			List<State> statesList = model.getStatesList();
 			if (expr.getType() instanceof TypeBool) {
-				int numStates = model.getNumStates();
-				BitSet bs = new BitSet(numStates);
-				List<State> statesList = model.getStatesList();
 				for (int i = 0; i < numStates; i++) {
-					bs.set(i, expr.evaluateBoolean(statesList.get(i)));
+					res.setBooleanValue(i, expr.evaluateBoolean(statesList.get(i)));
 				}
-				res = bs;
 			} else if (expr.getType() instanceof TypeInt) {
-				int numStates = model.getNumStates();
-				StateValues sv = new StateValues(expr.getType(), numStates);
-				List<State> statesList = model.getStatesList();
 				for (int i = 0; i < numStates; i++) {
-					sv.setIntValue(i, expr.evaluateInt(statesList.get(i)));
+					res.setIntValue(i, expr.evaluateInt(statesList.get(i)));
 				}
-				res = sv;
 			} else if (expr.getType() instanceof TypeDouble) {
-				int numStates = model.getNumStates();
-				StateValues sv = new StateValues(expr.getType(), numStates);
-				List<State> statesList = model.getStatesList();
 				for (int i = 0; i < numStates; i++) {
-					sv.setDoubleValue(i, expr.evaluateDouble(statesList.get(i)));
+					res.setDoubleValue(i, expr.evaluateDouble(statesList.get(i)));
 				}
-				res = sv;
 			}
 		}
 		// Anything else - error
@@ -538,45 +528,30 @@ public class StateModelChecker
 	/**
 	 * Model check a binary operator.
 	 */
-	protected Object checkExpressionBinaryOp(Model model, ExpressionBinaryOp expr) throws PrismException
+	protected StateValues checkExpressionBinaryOp(Model model, ExpressionBinaryOp expr) throws PrismException
 	{
 		// (just "and" for now - more to come later)
-		BitSet res1bs = (BitSet) checkExpression(model, expr.getOperand1());
-		BitSet res2bs = (BitSet) checkExpression(model, expr.getOperand2());
-		res1bs.and(res2bs);
-		return res1bs;
+		StateValues res1 = checkExpression(model, expr.getOperand1());
+		StateValues res2 = checkExpression(model, expr.getOperand2());
+		res1.and(res2);
+		res2.clear();
+		return res1;
 	}
 
 	/**
 	 * Model check a literal.
 	 */
-	protected Object checkExpressionLiteral(Model model, ExpressionLiteral expr) throws PrismException
-	{
-		Type type;
-		Object res = null;
-		type = expr.getType();
-		if (type instanceof TypeBool) {
-			BitSet bs = new BitSet(model.getNumStates());
-			if (expr.evaluateBoolean()) {
-				bs.set(0, model.getNumStates());
-			}
-			res = bs;
-		} else if (type instanceof TypeInt || type instanceof TypeDouble) {
-			res = new StateValues(expr.getType(), model.getNumStates(), expr.evaluate());
-		} else {
-			throw new PrismException("Couldn't check literal " + expr);
-		}
-
-		return res;
+	protected StateValues checkExpressionLiteral(Model model, ExpressionLiteral expr) throws PrismException
+	{
+		return new StateValues(expr.getType(), model.getNumStates(), expr.evaluate());
 	}
 
 	/**
 	 * Model check a label.
 	 */
-	protected Object checkExpressionLabel(Model model, ExpressionLabel expr) throws PrismException
+	protected StateValues checkExpressionLabel(Model model, ExpressionLabel expr) throws PrismException
 	{
 		LabelList ll;
-		Map<String, BitSet> labels;
 		int i;
 
 		// treat special cases
@@ -586,14 +561,14 @@ public class StateModelChecker
 			for (i = 0; i < numStates; i++) {
 				bs.set(i, model.isFixedDeadlockState(i));
 			}
-			return bs;
+			return StateValues.createFromBitSet(bs, numStates);
 		} else if (expr.getName().equals("init")) {
 			int numStates = model.getNumStates();
 			BitSet bs = new BitSet(numStates);
 			for (i = 0; i < numStates; i++) {
 				bs.set(i, model.isInitialState(i));
 			}
-			return bs;
+			return StateValues.createFromBitSet(bs, numStates);
 		} else {
 			ll = propertiesFile.getCombinedLabelList();
 			i = ll.getLabelIndex(expr.getName());
@@ -601,17 +576,12 @@ public class StateModelChecker
 				throw new PrismException("Unknown label \"" + expr.getName() + "\" in property");
 			// check recursively
 			return checkExpression(model, ll.getLabel(i));
-
-			// TODO: remove this:
-			//labels = loadLabelsFile(getLabelsFilename());
-			// get expression associated with label
-			//return labels.get(expr.getName());
 		}
 	}
 
 	// Check property ref
 
-	protected Object checkExpressionProp(Model model, ExpressionProp expr) throws PrismException
+	protected StateValues checkExpressionProp(Model model, ExpressionProp expr) throws PrismException
 	{
 		// Look up property and check recursively
 		Property prop = propertiesFile.lookUpPropertyObjectByName(expr.getName());
@@ -623,6 +593,334 @@ public class StateModelChecker
 		}
 	}
 
+	// Check filter
+
+	protected StateValues checkExpressionFilter(Model model, ExpressionFilter expr) throws PrismException
+	{
+		throw new PrismException("Explicit engine does not yet handle filters");
+		
+		/*
+		// Filter info
+		Expression filter;
+		FilterOperator op;
+		String filterStatesString;
+		StateListMTBDD statesFilter;
+		boolean filterInit, filterInitSingle, filterTrue;
+		JDDNode ddFilter = null;
+		// Result info
+		StateValues vals = null, resVals = null;
+		JDDNode ddMatch = null, dd;
+		StateListMTBDD states;
+		double d = 0.0, d2 = 0.0;
+		boolean b = false;
+		String resultExpl = null;
+		Object resObj = null;
+
+		// Check operand recursively
+		vals = checkExpression(model, expr.getOperand());
+		// Translate filter
+		filter = expr.getFilter();
+		// Create default filter (true) if none given
+		if (filter == null)
+			filter = Expression.True();
+		// Remember whether filter is "true"
+		filterTrue = Expression.isTrue(filter);
+		// Store some more info
+		filterStatesString = filterTrue ? "all states" : "states satisfying filter";
+		ddFilter = checkExpressionDD(filter);
+		statesFilter = new StateListMTBDD(ddFilter, model);
+		// Check if filter state set is empty; we treat this as an error
+		if (ddFilter.equals(JDD.ZERO)) {
+			throw new PrismException("Filter satisfies no states");
+		}
+		// Remember whether filter is for the initial state and, if so, whether there's just one
+		filterInit = (filter instanceof ExpressionLabel && ((ExpressionLabel) filter).getName().equals("init"));
+		filterInitSingle = filterInit & model.getNumStartStates() == 1;
+		// Print out number of states satisfying filter
+		if (!filterInit)
+			mainLog.println("\nStates satisfying filter " + filter + ": " + statesFilter.sizeString());
+
+		// Compute result according to filter type
+		op = expr.getOperatorType();
+		switch (op) {
+		case PRINT:
+			// Format of print-out depends on type
+			if (expr.getType() instanceof TypeBool) {
+				// NB: 'usual' case for filter(print,...) on Booleans is to use no filter
+				mainLog.print("\nSatisfying states");
+				mainLog.println(filterTrue ? ":" : " that are also in filter " + filter + ":");
+				dd = vals.deepCopy().convertToStateValuesMTBDD().getJDDNode();
+				new StateListMTBDD(dd, model).print(mainLog);
+				JDD.Deref(dd);
+			} else {
+				// TODO: integer-typed case: either add to print method or store in StateValues
+				mainLog.println("\nResults (non-zero only) for filter " + filter + ":");
+				vals.printFiltered(mainLog, ddFilter);
+			}
+			// Result vector is unchanged; for ARGMIN, don't store a single value (in resObj)
+			// Also, don't bother with explanation string
+			resVals = vals;
+			// Set vals to null to stop it being cleared below
+			vals = null;
+			break;
+		case MIN:
+			// Compute min
+			d = vals.minOverBDD(ddFilter);
+			// Store as object/vector (note crazy Object cast to avoid Integer->int auto conversion)
+			resObj = (expr.getType() instanceof TypeInt) ? ((Object) new Integer((int) d)) : (new Double(d));
+			resVals = new StateValuesMTBDD(JDD.Constant(d), model);
+			// Create explanation of result and print some details to log
+			resultExpl = "Minimum value over " + filterStatesString;
+			mainLog.println("\n" + resultExpl + ": " + resObj);
+			// Also find states that (are close to) selected value for display to log
+			ddMatch = vals.getBDDFromCloseValue(d, prism.getTermCritParam(), prism.getTermCrit() == Prism.ABSOLUTE);
+			JDD.Ref(ddFilter);
+			ddMatch = JDD.And(ddMatch, ddFilter);
+			break;
+		case MAX:
+			// Compute max
+			d = vals.maxOverBDD(ddFilter);
+			// Store as object/vector (note crazy Object cast to avoid Integer->int auto conversion)
+			resObj = (expr.getType() instanceof TypeInt) ? ((Object) new Integer((int) d)) : (new Double(d));
+			resVals = new StateValuesMTBDD(JDD.Constant(d), model);
+			// Create explanation of result and print some details to log
+			resultExpl = "Maximum value over " + filterStatesString;
+			mainLog.println("\n" + resultExpl + ": " + resObj);
+			// Also find states that (are close to) selected value for display to log
+			ddMatch = vals.getBDDFromCloseValue(d, prism.getTermCritParam(), prism.getTermCrit() == Prism.ABSOLUTE);
+			JDD.Ref(ddFilter);
+			ddMatch = JDD.And(ddMatch, ddFilter);
+			break;
+		case ARGMIN:
+			// Compute/display min
+			d = vals.minOverBDD(ddFilter);
+			mainLog.print("\nMinimum value over " + filterStatesString + ": ");
+			mainLog.println((expr.getType() instanceof TypeInt) ? ((Object) new Integer((int) d)) : (new Double(d)));
+			// Find states that (are close to) selected value
+			ddMatch = vals.getBDDFromCloseValue(d, prism.getTermCritParam(), prism.getTermCrit() == Prism.ABSOLUTE);
+			JDD.Ref(ddFilter);
+			ddMatch = JDD.And(ddMatch, ddFilter);
+			// Store states in vector; for ARGMIN, don't store a single value (in resObj)
+			// Also, don't bother with explanation string
+			resVals = new StateValuesMTBDD(ddMatch, model);
+			// Print out number of matching states, but not the actual states
+			mainLog.println("\nNumber of states with minimum value: " + resVals.getNNZString());
+			ddMatch = null;
+			break;
+		case ARGMAX:
+			// Compute/display max
+			d = vals.maxOverBDD(ddFilter);
+			mainLog.print("\nMaximum value over " + filterStatesString + ": ");
+			mainLog.println((expr.getType() instanceof TypeInt) ? ((Object) new Integer((int) d)) : (new Double(d)));
+			// Find states that (are close to) selected value
+			ddMatch = vals.getBDDFromCloseValue(d, prism.getTermCritParam(), prism.getTermCrit() == Prism.ABSOLUTE);
+			JDD.Ref(ddFilter);
+			ddMatch = JDD.And(ddMatch, ddFilter);
+			// Store states in vector; for ARGMAX, don't store a single value (in resObj)
+			// Also, don't bother with explanation string
+			resVals = new StateValuesMTBDD(ddMatch, model);
+			// Print out number of matching states, but not the actual states
+			mainLog.println("\nNumber of states with maximum value: " + resVals.getNNZString());
+			ddMatch = null;
+			break;
+		case COUNT:
+			// Compute count
+			vals.filter(ddFilter);
+			d = vals.getNNZ();
+			// Store as object/vector
+			resObj = new Integer((int) d);
+			resVals = new StateValuesMTBDD(JDD.Constant(d), model);
+			// Create explanation of result and print some details to log
+			resultExpl = filterTrue ? "Count of satisfying states" : "Count of satisfying states also in filter";
+			mainLog.println("\n" + resultExpl + ": " + resObj);
+			break;
+		case SUM:
+			// Compute sum
+			d = vals.sumOverBDD(ddFilter);
+			// Store as object/vector (note crazy Object cast to avoid Integer->int auto conversion)
+			resObj = (expr.getType() instanceof TypeInt) ? ((Object) new Integer((int) d)) : (new Double(d));
+			resVals = new StateValuesMTBDD(JDD.Constant(d), model);
+			// Create explanation of result and print some details to log
+			resultExpl = "Sum over " + filterStatesString;
+			mainLog.println("\n" + resultExpl + ": " + resObj);
+			break;
+		case AVG:
+			// Compute average
+			d = vals.sumOverBDD(ddFilter) / JDD.GetNumMinterms(ddFilter, allDDRowVars.n());
+			// Store as object/vector
+			resObj = new Double(d);
+			resVals = new StateValuesMTBDD(JDD.Constant(d), model);
+			// Create explanation of result and print some details to log
+			resultExpl = "Average over " + filterStatesString;
+			mainLog.println("\n" + resultExpl + ": " + resObj);
+			break;
+		case FIRST:
+			// Find first value
+			d = vals.firstFromBDD(ddFilter);
+			// Store as object/vector
+			if (expr.getType() instanceof TypeInt) {
+				resObj = new Integer((int) d);
+			} else if (expr.getType() instanceof TypeDouble) {
+				resObj = new Double(d);
+			} else {
+				resObj = new Boolean(d > 0);
+			}
+			resVals = new StateValuesMTBDD(JDD.Constant(d), model);
+			// Create explanation of result and print some details to log
+			resultExpl = "Value in ";
+			if (filterInit) {
+				resultExpl += filterInitSingle ? "the initial state" : "first initial state";
+			} else {
+				resultExpl += filterTrue ? "the first state" : "first state satisfying filter";
+			}
+			mainLog.println("\n" + resultExpl + ": " + resObj);
+			break;
+		case RANGE:
+			// Find range of values
+			d = vals.minOverBDD(ddFilter);
+			d2 = vals.maxOverBDD(ddFilter);
+			// Store as object
+			if (expr.getOperand().getType() instanceof TypeInt) {
+				resObj = new prism.Interval((int) d, (int) d2);
+			} else {
+				resObj = new prism.Interval(d, d2);
+			}
+			// Leave result vector unchanged: for a range, result is only available from Result object
+			resVals = vals;
+			// Set vals to null to stop it being cleared below
+			vals = null;
+			// Create explanation of result and print some details to log
+			resultExpl = "Range of values over ";
+			resultExpl += filterInit ? "initial states" : filterStatesString;
+			mainLog.println("\n" + resultExpl + ": " + resObj);
+			break;
+		case FORALL:
+			// Get access to BDD for this
+			dd = vals.convertToStateValuesMTBDD().getJDDNode();
+			// Print some info to log
+			mainLog.print("\nNumber of states satisfying " + expr.getOperand() + ": ");
+			states = new StateListMTBDD(dd, model);
+			mainLog.print(states.sizeString());
+			mainLog.println(states.includesAll(reach) ? " (all in model)" : "");
+			// Check "for all" over filter, store result
+			JDD.Ref(ddFilter);
+			dd = JDD.And(dd, ddFilter);
+			states = new StateListMTBDD(dd, model);
+			b = dd.equals(ddFilter);
+			// Store as object/vector
+			resObj = new Boolean(b);
+			resVals = new StateValuesMTBDD(JDD.Constant(b ? 1.0 : 0.0), model);
+			// Set vals to null so that is not clear()-ed twice
+			vals = null;
+			// Create explanation of result and print some details to log
+			resultExpl = "Property " + (b ? "" : "not ") + "satisfied in ";
+			mainLog.print("\nProperty satisfied in " + states.sizeString());
+			if (filterInit) {
+				if (filterInitSingle) {
+					resultExpl += "the initial state";
+				} else {
+					resultExpl += "all initial states";
+				}
+				mainLog.println(" of " + model.getNumStartStatesString() + " initial states.");
+			} else {
+				if (filterTrue) {
+					resultExpl += "all states";
+					mainLog.println(" of all " + model.getNumStatesString() + " states.");
+				} else {
+					resultExpl += "all filter states";
+					mainLog.println(" of " + statesFilter.sizeString() + " filter states.");
+				}
+			}
+			// Derefs
+			JDD.Deref(dd);
+			break;
+		case EXISTS:
+			// Get access to BDD for this
+			dd = vals.convertToStateValuesMTBDD().getJDDNode();
+			// Check "there exists" over filter
+			JDD.Ref(ddFilter);
+			dd = JDD.And(dd, ddFilter);
+			b = !dd.equals(JDD.ZERO);
+			// Store as object/vector
+			resObj = new Boolean(b);
+			resVals = new StateValuesMTBDD(JDD.Constant(b ? 1.0 : 0.0), model);
+			// Set vals to null so that is not clear()-ed twice
+			vals = null;
+			// Create explanation of result and print some details to log
+			resultExpl = "Property satisfied in ";
+			if (filterTrue) {
+				resultExpl += b ? "at least one state" : "no states";
+			} else {
+				resultExpl += b ? "at least one filter state" : "no filter states";
+			}
+			mainLog.println("\n" + resultExpl);
+			// Derefs
+			JDD.Deref(dd);
+			break;
+		case STATE:
+			// Check filter satisfied by exactly one state
+			if (statesFilter.size() != 1) {
+				String s = "Filter should be satisfied in exactly 1 state";
+				s += " (but \"" + filter + "\" is true in " + statesFilter.size() + " states)";
+				throw new PrismException(s);
+			}
+			// Find first (only) value
+			d = vals.firstFromBDD(ddFilter);
+			// Store as object/vector
+			if (expr.getType() instanceof TypeInt) {
+				resObj = new Integer((int) d);
+			} else if (expr.getType() instanceof TypeDouble) {
+				resObj = new Double(d);
+			} else {
+				resObj = new Boolean(d > 0);
+			}
+			resVals = new StateValuesMTBDD(JDD.Constant(d), model);
+			// Create explanation of result and print some details to log
+			resultExpl = "Value in ";
+			if (filterInit) {
+				resultExpl += "the initial state";
+			} else {
+				resultExpl += "the filter state";
+			}
+			mainLog.println("\n" + resultExpl + ": " + resObj);
+			break;
+		default:
+			JDD.Deref(ddFilter);
+			throw new PrismException("Unrecognised filter type \"" + expr.getOperatorName() + "\"");
+		}
+
+		// For some operators, print out some matching states
+		if (ddMatch != null) {
+			states = new StateListMTBDD(ddMatch, model);
+			mainLog.print("\nThere are " + states.sizeString() + " states with ");
+			mainLog.print(expr.getType() instanceof TypeDouble ? "(approximately) " : "" + "this value");
+			if (!verbose && (states.size() == -1 || states.size() > 10)) {
+				mainLog.print(".\nThe first 10 states are displayed below. To view them all, enable verbose mode or use a print filter.\n");
+				states.print(mainLog, 10);
+			} else {
+				mainLog.print(":\n");
+				states.print(mainLog);
+			}
+			JDD.Deref(ddMatch);
+		}
+
+		// Store result
+		result.setResult(resObj);
+		// Set result explanation (if none or disabled, clear)
+		if (expr.getExplanationEnabled() && resultExpl != null) {
+			result.setExplanation(resultExpl.toLowerCase());
+		} else {
+			result.setExplanation(null);
+		}
+
+		// Derefs, clears
+		JDD.Deref(ddFilter);
+		if (vals != null)
+			vals.clear();
+
+		return resVals;*/
+	}
+	
 	/**
 	 * Loads labels from a PRISM labels file and stores them in BitSet objects.
 	 * (Actually, it returns a map from label name Strings to BitSets.)

prism/src/explicit/StateValues.java

@@ -29,9 +29,12 @@ package explicit;
 import java.util.BitSet;
 
 import parser.type.Type;
+import parser.type.TypeBool;
 import parser.type.TypeDouble;
 import parser.type.TypeInt;
 import prism.PrismException;
+import prism.PrismFileLog;
+import prism.PrismLangException;
 import prism.PrismLog;
 
 /**
@@ -39,13 +42,14 @@ import prism.PrismLog;
  */
 public class StateValues
 {
-	// Type (int or double)
+	// Type (int, double or boolean)
 	protected Type type;
 	// Size
 	protected int size;
 	// Vector (only one used, depending on type)
 	protected int[] valuesI;
 	protected double[] valuesD;
+	protected BitSet valuesB;
 
 	// CONSTRUCTORS, etc.
 
@@ -59,44 +63,56 @@ public class StateValues
 		size = 0;
 		valuesI = null;
 		valuesD = null;
+		valuesB = null;
 	}
 
 	/**
 	 * Construct a new state values vector of the given type and size.
 	 * All values are initially set to zero.
 	 */
-	public StateValues(Type type, int size)
+	public StateValues(Type type, int size) throws PrismLangException
 	{
-		// TODO: check this: ? probably always returns Double due to typing
-		this(type, size, type instanceof TypeInt ? new Integer(0) : new Double(0.0));
+		this(type, size, type.defaultValue());
 	}
 
 	/**
 	 * Construct a new state values vector of the given type and size,
-	 * initialising all values to 'init'.
-	 * @param type Value type (int/double)
+	 * initialising all values to {@code init}.
+	 * Throws an exception of {@code init} is of the wrong type.
+	 * @param type Value type
 	 * @param size Vector size
-	 * @param init Initial value for all states (as Integer or Double object)
+	 * @param init Initial value for all states (as an appropriate Object)
 	 */
-	public StateValues(Type type, int size, Object init)
+	public StateValues(Type type, int size, Object init) throws PrismLangException
 	{
-		int i, initI;
-		double initD;
+		super();
+		int i;
 		this.type = type;
 		this.size = size;
-		valuesI = null;
-		valuesD = null;
 		// Create/initialise array of appropriate type
 		if (type instanceof TypeInt) {
 			valuesI = new int[size];
-			initI = ((Integer) init).intValue();
+			Integer objI = (Integer) type.castValueTo(init);
+			int initI = objI.intValue();
 			for (i = 0; i < size; i++)
 				valuesI[i] = initI;
 		} else if (type instanceof TypeDouble) {
 			valuesD = new double[size];
-			initD = ((Double) init).doubleValue();
+			Double objD = (Double) type.castValueTo(init);
+			double initD = objD.doubleValue();
 			for (i = 0; i < size; i++)
 				valuesD[i] = initD;
+		} else if (type instanceof TypeBool) {
+			Boolean objB = (Boolean) type.castValueTo(init);
+			boolean initB = objB.booleanValue();
+			if (initB) {
+				valuesB = new BitSet(size);
+				valuesB.set(0, size);
+			} else {
+				valuesB = new BitSet();
+			}
+		} else {
+			throw new PrismLangException("Cannot create an vector of type " + type);
 		}
 	}
 
@@ -109,11 +125,23 @@ public class StateValues
 		StateValues sv = new StateValues();
 		sv.type = TypeDouble.getInstance();
 		sv.size = array.length;
-		sv.valuesI = null;
 		sv.valuesD = array;
 		return sv;
 	}
 
+	/**
+	 * Create a new (Boolean-valued) state values vector from an existing BitSet.
+	 * The BitSet is stored directly, not copied.
+	 */
+	public static StateValues createFromBitSet(BitSet bs, int size)
+	{
+		StateValues sv = new StateValues();
+		sv.type = TypeBool.getInstance();
+		sv.size = size;
+		sv.valuesB = bs;
+		return sv;
+	}
+
 	/**
 	 * Create a new (double-valued) state values vector from a BitSet,
 	 * where each entry is 1.0 if in the bitset, 0.0 otherwise.
@@ -206,6 +234,19 @@ public class StateValues
 		valuesD[i] = val;
 	}
 
+	public void setBooleanValue(int i, boolean val)
+	{
+		valuesB.set(i, val);
+	}
+
+	public void and(StateValues sv) throws PrismException
+	{
+		if (!(type instanceof TypeBool) || !(sv.type instanceof TypeBool)) {
+			throw new PrismException("Conjunction can only be applied to Boolean vectors");
+		}
+		valuesB.and(sv.valuesB);
+	}
+	
 	// ...
 
 	// clear (free memory)
@@ -218,6 +259,7 @@ public class StateValues
 	{
 		valuesI = null;
 		valuesD = null;
+		valuesB = null;
 	}
 
 	// METHODS TO ACCESS VECTOR DATA
@@ -231,11 +273,21 @@ public class StateValues
 			return valuesI[i];
 		} else if (type instanceof TypeDouble) {
 			return valuesD[i];
+		} else if (type instanceof TypeBool) {
+			return valuesB.get(i);
 		} else {
 			return null;
 		}
 	}
 
+	/**
+	 * For Boolean-valued vectors, get the BitSet storing the data.
+	 */
+	public BitSet getBitSet()
+	{
+		return valuesB;
+	}
+	
 	/*
 	// get num non zeros
 	
@@ -274,6 +326,6 @@ public class StateValues
 	public StateValues deepCopy() throws PrismException
 	{
 		// TODO
-		throw new PrismException("Not impleneted yet");
+		throw new PrismException("Not implemented yet");
 	}
 }

prism/src/parser/type/Type.java

@@ -30,8 +30,20 @@ import prism.PrismLangException;
 
 public abstract class Type 
 {
+	/**
+	 * Returns the string denoting this type, e.g. "int", "bool".
+	 */
 	public abstract String getTypeString();
 	
+	/**
+	 * Returns the default value for this type, assuming no initialisation specified.
+	 */
+	public Object defaultValue()
+	{
+		// Play safe: assume null
+		return null;
+	}
+	
 	/**
 	 * Returns true iff a variable of this type can be assigned a value that is of type {@code type}. 
 	 */

prism/src/parser/type/TypeBool.java

@@ -46,11 +46,18 @@ public class TypeBool extends Type
 		return (o instanceof TypeBool);
 	}
 	
+	@Override
 	public String getTypeString()
 	{
 		return "bool";
 	}
 	
+	@Override
+	public Object defaultValue()
+	{
+		return new Boolean(false);
+	}
+	
 	public static TypeBool getInstance()
 	{
 		return singleton;

prism/src/parser/type/TypeClock.java

@@ -46,11 +46,18 @@ public class TypeClock extends Type
 		return (o instanceof TypeClock);
 	}
 	
+	@Override
 	public String getTypeString()
 	{
 		return "clock";
 	}
 	
+	@Override
+	public Object defaultValue()
+	{
+		return new Double(0.0);
+	}
+	
 	public static TypeClock getInstance()
 	{
 		return singleton;

prism/src/parser/type/TypeDouble.java

@@ -46,11 +46,18 @@ public class TypeDouble extends Type
 		return (o instanceof TypeDouble);
 	}
 	
+	@Override
 	public String getTypeString()
 	{
 		return "double";
 	}
 	
+	@Override
+	public Object defaultValue()
+	{
+		return new Double(0.0);
+	}
+	
 	public static TypeDouble getInstance()
 	{
 		return singleton;

prism/src/parser/type/TypeInt.java

@@ -46,11 +46,18 @@ public class TypeInt extends Type
 		return (o instanceof TypeInt);
 	}
 	
+	@Override
 	public String getTypeString()
 	{
 		return "int";
 	}
 	
+	@Override
+	public Object defaultValue()
+	{
+		return new Integer(0);
+	}
+	
 	public static TypeInt getInstance()
 	{
 		return singleton;