Small optimisation when model checking filters: Reduce set of filter states to the first state if filter is "first". [from Steffen Marcker]

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

prism/src/explicit/StateModelChecker.java

@@ -844,6 +844,10 @@ public class StateModelChecker extends PrismComponent
 		} else {
 			currentFilter = null;
 		}
+		if (op == FilterOperator.FIRST) {
+			// only first state is of interest
+			bsFilter.clear(bsFilter.nextSetBit(0) + 1, bsFilter.length());
+		}
 
 		// Check operand recursively, using bsFilter as statesOfInterest
 		StateValues vals = checkExpression(model, expr.getOperand(), bsFilter);

prism/src/param/ParamModelChecker.java

@@ -511,6 +511,10 @@ final public class ParamModelChecker extends PrismComponent
 			s += " (but \"" + filter + "\" is true in " + bsFilter.cardinality() + " states)";
 			throw new PrismException(s);
 		}
+		if (op == FilterOperator.FIRST) {
+			// only first state is of interest
+			bsFilter.clear(bsFilter.nextSetBit(0) + 1, bsFilter.length());
+		}
 		RegionValues vals = checkExpression(model, expr.getOperand(), bsFilter);
 
 		// Check if filter state set is empty; we treat this as an error