From de50d8d145fd497265a9e48ed7b38a45258f2325 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 7 Dec 2015 11:44:04 +0000 Subject: [PATCH] Small update to previous commit: display filter size *before* possibly optimising it. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11011 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/StateModelChecker.java | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 2e1eeefe..5b017e4f 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -826,9 +826,17 @@ public class StateModelChecker extends PrismComponent // Remember whether filter is for the initial state and, if so, whether there's just one boolean filterInit = (filter instanceof ExpressionLabel && ((ExpressionLabel) filter).getName().equals("init")); boolean filterInitSingle = filterInit & model.getNumInitialStates() == 1; + // Print out number of states satisfying filter + if (!filterInit) { + mainLog.println("\nStates satisfying filter " + filter + ": " + bsFilter.cardinality()); + } + // Possibly optimise filter + FilterOperator op = expr.getOperatorType(); + if (op == FilterOperator.FIRST) { + bsFilter.clear(bsFilter.nextSetBit(0) + 1, bsFilter.length()); + } // 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) { @@ -844,18 +852,9 @@ 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); - // Print out number of states satisfying filter - if (!filterInit) - mainLog.println("\nStates satisfying filter " + filter + ": " + bsFilter.cardinality()); - // Compute result according to filter type StateValues resVals = null; BitSet bsMatch = null, bs = null;