s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

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
master
Dave Parker 10 years ago
parent
0f2bbbc7b6
commit
eda5876325
3 changed files with 32 additions and 50 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 40
      prism/src/explicit/StateModelChecker.java
  2. 2
      prism/src/param/ParamModelChecker.java
  3. 40
      prism/src/prism/StateModelChecker.java

40
prism/src/explicit/StateModelChecker.java
View File

@ -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

2
prism/src/param/ParamModelChecker.java
View File

@ -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

40
prism/src/prism/StateModelChecker.java
View File

@ -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:

Write Preview
Loading…
Cancel
Save