From 66ea7475a742ba84851822901a4bc71519b6dc45 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 7 Dec 2015 10:35:08 +0000 Subject: [PATCH] Optimisation when dealing with filters: perform cardinality check for "state" filters earlier. [from Steffen Marcker] git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11008 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/StateModelChecker.java | 12 ++++++------ prism/src/param/ParamModelChecker.java | 14 +++++++------- prism/src/prism/StateModelChecker.java | 12 ++++++------ 3 files changed, 19 insertions(+), 19 deletions(-) diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index d406f393..f760cf57 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -830,6 +830,12 @@ public class StateModelChecker extends PrismComponent // For some types of filter, store info that may be used to optimise model checking FilterOperator op = expr.getOperatorType(); if (op == FilterOperator.STATE) { + // Check filter satisfied by exactly one state + if (bsFilter.cardinality() != 1) { + String s = "Filter should be satisfied in exactly 1 state"; + s += " (but \"" + filter + "\" is true in " + bsFilter.cardinality() + " states)"; + throw new PrismException(s); + } 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)); @@ -1035,12 +1041,6 @@ public class StateModelChecker extends PrismComponent mainLog.println("\n" + resultExpl); break; case STATE: - // Check filter satisfied by exactly one state - if (bsFilter.cardinality() != 1) { - String s = "Filter should be satisfied in exactly 1 state"; - s += " (but \"" + filter + "\" is true in " + bsFilter.cardinality() + " states)"; - throw new PrismException(s); - } // Find first (only) value // Store as object/vector resObj = vals.firstFromBitSet(bsFilter); diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index 15963185..aff8ca34 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/prism/src/param/ParamModelChecker.java @@ -504,6 +504,13 @@ final public class ParamModelChecker extends PrismComponent throw new PrismException("currently, parameter-dependent filters are not supported"); } BitSet bsFilter = rvFilter.getStateValues().toBitSet(); + // Check filter satisfied by exactly one state + FilterOperator op = expr.getOperatorType(); + if (op == FilterOperator.STATE && bsFilter.cardinality() != 1) { + String s = "Filter should be satisfied in exactly 1 state"; + s += " (but \"" + filter + "\" is true in " + bsFilter.cardinality() + " states)"; + throw new PrismException(s); + } RegionValues vals = checkExpression(model, expr.getOperand(), bsFilter); // Check if filter state set is empty; we treat this as an error @@ -519,7 +526,6 @@ final public class ParamModelChecker extends PrismComponent } // Compute result according to filter type - FilterOperator op = expr.getOperatorType(); RegionValues resVals = null; switch (op) { case PRINT: @@ -564,12 +570,6 @@ final public class ParamModelChecker extends PrismComponent resVals = vals.op(Region.EXISTS, bsFilter); break; case STATE: - // Check filter satisfied by exactly one state - if (bsFilter.cardinality() != 1) { - String s = "Filter should be satisfied in exactly 1 state"; - s += " (but \"" + filter + "\" is true in " + bsFilter.cardinality() + " states)"; - throw new PrismException(s); - } resVals = vals.op(Region.FIRST, bsFilter); break; default: diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index 64f3ac65..53b9092f 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -1033,6 +1033,12 @@ public class StateModelChecker implements ModelChecker // For some types of filter, store info that may be used to optimise model checking FilterOperator op = expr.getOperatorType(); if (op == FilterOperator.STATE) { + // Check filter satisfied by exactly one state + if (statesFilter.size() != 1) { + String s = "Filter should be satisfied in exactly 1 state"; + s += " (but \"" + filter + "\" is true in " + statesFilter.size() + " states)"; + throw new PrismException(s); + } 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)); @@ -1288,12 +1294,6 @@ public class StateModelChecker implements ModelChecker JDD.Deref(dd); break; case STATE: - // Check filter satisfied by exactly one state - if (statesFilter.size() != 1) { - String s = "Filter should be satisfied in exactly 1 state"; - s += " (but \"" + filter + "\" is true in " + statesFilter.size() + " states)"; - throw new PrismException(s); - } // Results of type void are handled differently if (expr.getType() instanceof TypeVoid) { // Extract result from StateValuesVoid object