From eda58763258577fd45ed2550eb417d3d7fe53e81 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 7 Dec 2015 10:33:10 +0000 Subject: [PATCH] Minor refactoring, ahead of upcoming patches. [from Steffen Marcker] git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11007 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/StateModelChecker.java | 40 +++++++++-------------- prism/src/param/ParamModelChecker.java | 2 +- prism/src/prism/StateModelChecker.java | 40 +++++++++-------------- 3 files changed, 32 insertions(+), 50 deletions(-) diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index f4944946..d406f393 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -806,44 +806,29 @@ public class StateModelChecker extends PrismComponent protected StateValues checkExpressionFilter(Model model, ExpressionFilter expr, BitSet statesOfInterest) throws PrismException { - // Filter info - Expression filter; - FilterOperator op; - String filterStatesString; - boolean filterInit, filterInitSingle, filterTrue; - BitSet bsFilter = null; - // Result info - StateValues vals = null, resVals = null; - BitSet bsMatch = null, bs; - StateValues states; - boolean b = false; - int count = 0; - String resultExpl = null; - Object resObj = null; - // Translate filter - filter = expr.getFilter(); + Expression filter = expr.getFilter(); // Create default filter (true) if none given if (filter == null) filter = Expression.True(); // Remember whether filter is "true" - filterTrue = Expression.isTrue(filter); + boolean filterTrue = Expression.isTrue(filter); // Store some more info - filterStatesString = filterTrue ? "all states" : "states satisfying filter"; + String filterStatesString = filterTrue ? "all states" : "states satisfying filter"; // get the BitSet of states matching the filter, without taking statesOfInterest into account - bsFilter = checkExpression(model, filter, null).getBitSet(); + BitSet bsFilter = checkExpression(model, filter, null).getBitSet(); // Check if filter state set is empty; we treat this as an error if (bsFilter.isEmpty()) { throw new PrismException("Filter satisfies no states"); } // Remember whether filter is for the initial state and, if so, whether there's just one - filterInit = (filter instanceof ExpressionLabel && ((ExpressionLabel) filter).getName().equals("init")); - filterInitSingle = filterInit & model.getNumInitialStates() == 1; + boolean filterInit = (filter instanceof ExpressionLabel && ((ExpressionLabel) filter).getName().equals("init")); + boolean filterInitSingle = filterInit & model.getNumInitialStates() == 1; // For some types of filter, store info that may be used to optimise model checking - op = expr.getOperatorType(); + FilterOperator op = expr.getOperatorType(); if (op == FilterOperator.STATE) { currentFilter = new Filter(Filter.FilterOperator.STATE, bsFilter.nextSetBit(0)); } else if (op == FilterOperator.FORALL && filterInit && filterInitSingle) { @@ -855,13 +840,18 @@ public class StateModelChecker extends PrismComponent } // Check operand recursively, using bsFilter as statesOfInterest - vals = checkExpression(model, expr.getOperand(), bsFilter); + 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; + boolean b = false; + String resultExpl = null; + Object resObj = null; switch (op) { case PRINT: case PRINTALL: @@ -944,7 +934,7 @@ public class StateModelChecker extends PrismComponent break; case COUNT: // Compute count - count = vals.countOverBitSet(bsFilter); + int count = vals.countOverBitSet(bsFilter); // Store as object/vector resObj = new Integer(count); resVals = new StateValues(expr.getType(), resObj, model); @@ -1070,7 +1060,7 @@ public class StateModelChecker extends PrismComponent // For some operators, print out some matching states if (bsMatch != null) { - states = StateValues.createFromBitSet(bsMatch, model); + StateValues states = StateValues.createFromBitSet(bsMatch, model); mainLog.print("\nThere are " + bsMatch.cardinality() + " states with "); mainLog.print((expr.getType() instanceof TypeDouble ? "(approximately) " : "") + "this value"); boolean verbose = verbosity > 0; // TODO diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index 90e09ee8..15963185 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/prism/src/param/ParamModelChecker.java @@ -491,7 +491,6 @@ final public class ParamModelChecker extends PrismComponent protected RegionValues checkExpressionFilter(ParamModel model, ExpressionFilter expr, BitSet needStates) throws PrismException { - RegionValues resVals = null; Expression filter = expr.getFilter(); if (filter == null) { filter = Expression.True(); @@ -521,6 +520,7 @@ final public class ParamModelChecker extends PrismComponent // Compute result according to filter type FilterOperator op = expr.getOperatorType(); + RegionValues resVals = null; switch (op) { case PRINT: // Format of print-out depends on type diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index 77dfa913..64f3ac65 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -1011,43 +1011,27 @@ public class StateModelChecker implements ModelChecker protected StateValues checkExpressionFilter(ExpressionFilter expr) throws PrismException { - // Filter info - Expression filter; - FilterOperator op; - String filterStatesString; - StateListMTBDD statesFilter; - boolean filterInit, filterInitSingle, filterTrue; - JDDNode ddFilter = null; - // Result info - StateValues vals = null, resVals = null; - JDDNode ddMatch = null, dd; - StateListMTBDD states; - double d = 0.0, d2 = 0.0; - boolean b = false; - String resultExpl = null; - Object resObj = null; - // Translate filter - filter = expr.getFilter(); + Expression filter = expr.getFilter(); // Create default filter (true) if none given if (filter == null) filter = Expression.True(); // Remember whether filter is "true" - filterTrue = Expression.isTrue(filter); + boolean filterTrue = Expression.isTrue(filter); // Store some more info - filterStatesString = filterTrue ? "all states" : "states satisfying filter"; - ddFilter = checkExpressionDD(filter); - statesFilter = new StateListMTBDD(ddFilter, model); + String filterStatesString = filterTrue ? "all states" : "states satisfying filter"; + JDDNode ddFilter = checkExpressionDD(filter); + StateListMTBDD statesFilter = new StateListMTBDD(ddFilter, model); // Check if filter state set is empty; we treat this as an error if (ddFilter.equals(JDD.ZERO)) { throw new PrismException("Filter satisfies no states"); } // Remember whether filter is for the initial state and, if so, whether there's just one - filterInit = (filter instanceof ExpressionLabel && ((ExpressionLabel) filter).getName().equals("init")); - filterInitSingle = filterInit & model.getNumStartStates() == 1; + boolean filterInit = (filter instanceof ExpressionLabel && ((ExpressionLabel) filter).getName().equals("init")); + boolean filterInitSingle = filterInit & model.getNumStartStates() == 1; // For some types of filter, store info that may be used to optimise model checking - op = expr.getOperatorType(); + FilterOperator 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) { @@ -1058,6 +1042,7 @@ public class StateModelChecker implements ModelChecker currentFilter = null; } + StateValues vals = null; try { // Check operand recursively vals = checkExpression(expr.getOperand()); @@ -1072,6 +1057,13 @@ public class StateModelChecker implements ModelChecker // Compute result according to filter type op = expr.getOperatorType(); + StateValues resVals = null; + JDDNode ddMatch = null, dd = null; + StateListMTBDD states; + double d = 0.0, d2 = 0.0; + boolean b = false; + String resultExpl = null; + Object resObj = null; switch (op) { case PRINT: case PRINTALL: