diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 40724ee2..045e441f 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/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; } diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index cd67107f..db5e7c65 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/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; }