From 19ef6934e8b0bac9f5ea17885bf1febc36059227 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 21 Feb 2012 14:32:43 +0000 Subject: [PATCH] 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 | 4 ++++ prism/src/prism/StateModelChecker.java | 4 ++++ 2 files changed, 8 insertions(+) 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; }