More cases handled when cacheing filter info in (symbolic/explicit) model checkers.

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

prism/src/explicit/StateModelChecker.java

@@ -612,6 +612,10 @@ public class StateModelChecker
 		op = expr.getOperatorType();
 		if (op == FilterOperator.STATE) {
 			currentFilter = new Filter(Filter.FilterOperator.STATE, bsFilter.nextSetBit(0));
+		} else if (op == FilterOperator.FORALL && filterInit && filterInitSingle) {
+			currentFilter = new Filter(Filter.FilterOperator.STATE, bsFilter.nextSetBit(0));
+		} else if (op == FilterOperator.FIRST && filterInit && filterInitSingle) {
+			currentFilter = new Filter(Filter.FilterOperator.STATE, bsFilter.nextSetBit(0));
 		} else {
 			currentFilter = null;
 		}

prism/src/prism/StateModelChecker.java

@@ -1031,6 +1031,10 @@ public class StateModelChecker implements ModelChecker
 		op = expr.getOperatorType();
 		if (op == FilterOperator.STATE) {
 			currentFilter = new Filter(Filter.FilterOperator.STATE, ODDUtils.GetIndexOfFirstFromDD(ddFilter, odd, allDDRowVars));
+		} else if (op == FilterOperator.FORALL && filterInit && filterInitSingle) {
+			currentFilter = new Filter(Filter.FilterOperator.STATE, ODDUtils.GetIndexOfFirstFromDD(ddFilter, odd, allDDRowVars));
+		} else if (op == FilterOperator.FIRST && filterInit && filterInitSingle) {
+			currentFilter = new Filter(Filter.FilterOperator.STATE, ODDUtils.GetIndexOfFirstFromDD(ddFilter, odd, allDDRowVars));
 		} else {
 			currentFilter = null;
 		}