From 031a14e778c5fb5a8b737dca92ecd3c955fc175b Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 7 Dec 2015 10:39:13 +0000 Subject: [PATCH] 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 | 4 ++++ prism/src/param/ParamModelChecker.java | 4 ++++ 2 files changed, 8 insertions(+) diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index f760cf57..2e1eeefe 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/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); diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index aff8ca34..dddd10e1 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/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