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

Re-factoring - push the creation of default filters during model checking into a utility method in ExpressionFilter. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8394 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 12 years ago
parent
0c3219e175
commit
f85400152d
4 changed files with 69 additions and 131 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. 48
      prism/src/explicit/StateModelChecker.java
  2. 46
      prism/src/param/ParamModelChecker.java
  3. 58
      prism/src/parser/ast/ExpressionFilter.java
  4. 48
      prism/src/prism/StateModelChecker.java

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

@ -259,7 +259,6 @@ public class StateModelChecker extends PrismComponent
*/
public Result check(Model model, Expression expr) throws PrismException
{
ExpressionFilter exprFilter = null;
long timer = 0;
StateValues vals;
String resultString;
@ -269,49 +268,10 @@ public class StateModelChecker extends PrismComponent
// Remove any existing filter info
currentFilter = null;
// The final result of model checking will be a single value. If the expression to be checked does not
// already yield a single value (e.g. because a filter has not been explicitly included), we need to wrap
// a new (invisible) filter around it. Note that some filters (e.g. print/argmin/argmax) also do not
// return single values and have to be treated in this way.
if (!expr.returnsSingleValue()) {
// New filter depends on expression type and number of initial states.
// Boolean expressions...
if (expr.getType() instanceof TypeBool) {
// Result is true iff true for all initial states
exprFilter = new ExpressionFilter("forall", expr, new ExpressionLabel("init"));
}
// Non-Boolean (double or integer) expressions...
else {
// Result is for the initial state, if there is just one,
// or the range over all initial states, if multiple
if (model.getNumInitialStates() == 1) {
exprFilter = new ExpressionFilter("state", expr, new ExpressionLabel("init"));
} else {
exprFilter = new ExpressionFilter("range", expr, new ExpressionLabel("init"));
}
}
}
// Even, when the expression does already return a single value, if the the outermost operator
// of the expression is not a filter, we still need to wrap a new filter around it.
// e.g. 2*filter(...) or 1-P=?[...{...}]
// This because the final result of model checking is only stored when we process a filter.
else if (!(expr instanceof ExpressionFilter)) {
// We just pick the first value (they are all the same)
exprFilter = new ExpressionFilter("first", expr, new ExpressionLabel("init"));
// We stop any additional explanation being displayed to avoid confusion.
exprFilter.setExplanationEnabled(false);
}
// For any case where a new filter was created above...
if (exprFilter != null) {
// Make it invisible (not that it will be displayed)
exprFilter.setInvisible(true);
// Compute type of new filter expression (will be same as child)
exprFilter.typeCheck();
// Store as expression to be model checked
expr = exprFilter;
}
// Wrap a filter round the property, if needed
// (in order to extract the final result of model checking)
expr = ExpressionFilter.addDefaultFilterIfNeeded(expr, model.getNumInitialStates() == 1);
// If required, do bisimulation minimisation
if (doBisim) {

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

@ -222,7 +222,6 @@ final public class ParamModelChecker extends PrismComponent
model.getNumStates(), model.getFirstInitialState(), simplifyRegions, splitMethod);
valueComputer = new ValueComputer(paramModel, regionFactory, precision, eliminationOrder, bisimType);
ExpressionFilter exprFilter = null;
long timer = 0;
// Remove labels from property, using combined label list (on a copy of the expression)
@ -233,48 +232,9 @@ final public class ParamModelChecker extends PrismComponent
// Also evaluate/replace any constants
//expr = (Expression) expr.replaceConstants(constantValues);
// The final result of model checking will be a single value. If the expression to be checked does not
// already yield a single value (e.g. because a filter has not been explicitly included), we need to wrap
// a new (invisible) filter around it. Note that some filters (e.g. print/argmin/argmax) also do not
// return single values and have to be treated in this way.
if (!expr.returnsSingleValue()) {
// New filter depends on expression type and number of initial states.
// Boolean expressions...
if (expr.getType() instanceof TypeBool) {
// Result is true iff true for all initial states
exprFilter = new ExpressionFilter("forall", expr, new ExpressionLabel("init"));
}
// Non-Boolean (double or integer) expressions...
else {
// Result is for the initial state, if there is just one,
// or the range over all initial states, if multiple
if (model.getNumInitialStates() == 1) {
exprFilter = new ExpressionFilter("state", expr, new ExpressionLabel("init"));
} else {
exprFilter = new ExpressionFilter("range", expr, new ExpressionLabel("init"));
}
}
}
// Even, when the expression does already return a single value, if the the outermost operator
// of the expression is not a filter, we still need to wrap a new filter around it.
// e.g. 2*filter(...) or 1-P=?[...{...}]
// This because the final result of model checking is only stored when we process a filter.
else if (!(expr instanceof ExpressionFilter)) {
// We just pick the first value (they are all the same)
exprFilter = new ExpressionFilter("first", expr, new ExpressionLabel("init"));
// We stop any additional explanation being displayed to avoid confusion.
exprFilter.setExplanationEnabled(false);
}
// For any case where a new filter was created above...
if (exprFilter != null) {
// Make it invisible (not that it will be displayed)
exprFilter.setInvisible(true);
// Compute type of new filter expression (will be same as child)
exprFilter.typeCheck();
// Store as expression to be model checked
expr = exprFilter;
}
// Wrap a filter round the property, if needed
// (in order to extract the final result of model checking)
expr = ExpressionFilter.addDefaultFilterIfNeeded(expr, model.getNumInitialStates() == 1);
// Do model checking and store result vector
timer = System.currentTimeMillis();

58
prism/src/parser/ast/ExpressionFilter.java
View File

@ -27,6 +27,7 @@
package parser.ast;
import parser.*;
import parser.type.TypeBool;
import parser.visitor.*;
import prism.PrismLangException;
@ -246,6 +247,63 @@ public class ExpressionFilter extends Expression
return e;
}
/**
* Wrap a "default" ExpressionFilter around an Expression representing a property to be model checked,
* in order to pick out a single value (the final result of model checking) from a vector of values for all states.
* See the PRISM manual (or check the code below) to see the definition of the "default" filter.
* If the expression is already an ExpressionFilter (of the right kind), nothing is done.
* Note that we need to know whether the model has multiple initial states, because this affects the default filter.
* @param expr Expression to be model checked
* @param singleInit Does the model on which it is being checked have a single initial states?
*/
public static Expression addDefaultFilterIfNeeded(Expression expr, boolean singleInit) throws PrismLangException
{
ExpressionFilter exprFilter = null;
// The final result of model checking will be a single value. If the expression to be checked does not
// already yield a single value (e.g. because a filter has not been explicitly included), we need to wrap
// a new (invisible) filter around it. Note that some filters (e.g. print/argmin/argmax) also do not
// return single values and have to be treated in this way.
if (!expr.returnsSingleValue()) {
// New filter depends on expression type and number of initial states.
// Boolean expressions...
if (expr.getType() instanceof TypeBool) {
// Result is true iff true for all initial states
exprFilter = new ExpressionFilter("forall", expr, new ExpressionLabel("init"));
}
// Non-Boolean (double or integer) expressions...
else {
// Result is for the initial state, if there is just one,
// or the range over all initial states, if multiple
if (singleInit) {
exprFilter = new ExpressionFilter("state", expr, new ExpressionLabel("init"));
} else {
exprFilter = new ExpressionFilter("range", expr, new ExpressionLabel("init"));
}
}
}
// Even, when the expression does already return a single value, if the the outermost operator
// of the expression is not a filter, we still need to wrap a new filter around it.
// e.g. 2*filter(...) or 1-P=?[...{...}]
// This because the final result of model checking is only stored when we process a filter.
else if (!(expr instanceof ExpressionFilter)) {
// We just pick the first value (they are all the same)
exprFilter = new ExpressionFilter("first", expr, new ExpressionLabel("init"));
// We stop any additional explanation being displayed to avoid confusion.
exprFilter.setExplanationEnabled(false);
}
// Finalise filter (if created) and return
if (exprFilter != null) {
// Make it invisible (not that it will be displayed)
exprFilter.setInvisible(true);
// Compute type of new filter expression (will be same as child)
exprFilter.typeCheck();
return exprFilter;
} else {
return expr;
}
}
}
// ------------------------------------------------------------------------------

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

@ -167,7 +167,6 @@ public class StateModelChecker implements ModelChecker
*/
public Result check(Expression expr) throws PrismException
{
ExpressionFilter exprFilter = null;
long timer = 0;
StateValues vals;
String resultString;
@ -178,49 +177,10 @@ public class StateModelChecker implements ModelChecker
// Remove any existing filter info
currentFilter = null;
// The final result of model checking will be a single value. If the expression to be checked does not
// already yield a single value (e.g. because a filter has not been explicitly included), we need to wrap
// a new (invisible) filter around it. Note that some filters (e.g. print/argmin/argmax) also do not
// return single values and have to be treated in this way.
if (!expr.returnsSingleValue()) {
// New filter depends on expression type and number of initial states.
// Boolean expressions...
if (expr.getType() instanceof TypeBool) {
// Result is true iff true for all initial states
exprFilter = new ExpressionFilter("forall", expr, new ExpressionLabel("init"));
}
// Non-Boolean (double or integer) expressions...
else {
// Result is for the initial state, if there is just one,
// or the range over all initial states, if multiple
if (model.getNumStartStates() == 1) {
exprFilter = new ExpressionFilter("state", expr, new ExpressionLabel("init"));
} else {
exprFilter = new ExpressionFilter("range", expr, new ExpressionLabel("init"));
}
}
}
// Even, when the expression does already return a single value, if the the outermost operator
// of the expression is not a filter, we still need to wrap a new filter around it.
// e.g. 2*filter(...) or 1-P=?[...{...}]
// This because the final result of model checking is only stored when we process a filter.
else if (!(expr instanceof ExpressionFilter)) {
// We just pick the first value (they are all the same)
exprFilter = new ExpressionFilter("first", expr, new ExpressionLabel("init"));
// We stop any additional explanation being displayed to avoid confusion.
exprFilter.setExplanationEnabled(false);
}
// For any case where a new filter was created above...
if (exprFilter != null) {
// Make it invisible (not that it will be displayed)
exprFilter.setInvisible(true);
// Compute type of new filter expression (will be same as child)
exprFilter.typeCheck();
// Store as expression to be model checked
expr = exprFilter;
}
// Wrap a filter round the property, if needed
// (in order to extract the final result of model checking)
expr = ExpressionFilter.addDefaultFilterIfNeeded(expr, model.getNumStartStates() == 1);
// Do model checking and store result vector
timer = System.currentTimeMillis();
vals = checkExpression(expr);

Write Preview
Loading…
Cancel
Save