Bug fix in symbolic model checking of filters.

The statesOfInterest variables was wrongly not reset to 'reach'.
Not usually caught because the statesOfInterest optimisation is
currently used in very few places. The attached bugfix test shows
an example of where it does go wrong.

prism-tests/bugfixes/filters+statesOfInterest.prism

@@ -0,0 +1,23 @@
+dtmc
+
+module die
+
+	// local state
+	s : [0..7] init 0;
+	// value of the die
+	d : [0..6] init 0;
+	
+	[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2);
+	[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4);
+	[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6);
+	[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1);
+	[] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3);
+	[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5);
+	[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6);
+	[] s=7 -> (s'=7);
+	
+endmodule
+
+rewards "coin_flips"
+	[] s<7 : 1;
+endrewards

prism-tests/bugfixes/filters+statesOfInterest.prism.args

@@ -0,0 +1,4 @@
+-ex
+-m
+-s
+-h

prism-tests/bugfixes/filters+statesOfInterest.prism.props

@@ -0,0 +1,5 @@
+// Bug fix test case for filters; see commit for details
+// The "0.0+" is needed because of missing integer-valued vector export
+
+// RESULT: 13
+0.0 + filter(sum, filter(count, true, P>0[ X F s=7]), s=2);

prism-tests/bugfixes/filters+statesOfInterest.prism.props.args

@@ -0,0 +1 @@
+-exportvector filters+statesOfInterest.prism.props.txt

prism-tests/bugfixes/filters+statesOfInterest.prism.props.txt

@@ -0,0 +1,13 @@
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0

prism/src/prism/StateModelChecker.java

@@ -1140,7 +1140,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, statesOfInterest.copy());
+		JDDNode ddFilter = checkExpressionDD(filter,  model.getReach().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)) {