From 39974b5e7e6a2fa9733e834497ba56a9fb916981 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 11 Apr 2008 18:49:24 +0000 Subject: [PATCH] Removal of Expression2MTBDD class. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@748 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/Expression2MTBDD.java | 488 ------------------------- prism/src/prism/Modules2MTBDD.java | 12 +- prism/src/prism/Prism.java | 7 +- prism/src/prism/StateModelChecker.java | 24 +- 4 files changed, 32 insertions(+), 499 deletions(-) delete mode 100644 prism/src/prism/Expression2MTBDD.java diff --git a/prism/src/prism/Expression2MTBDD.java b/prism/src/prism/Expression2MTBDD.java deleted file mode 100644 index 48af350d..00000000 --- a/prism/src/prism/Expression2MTBDD.java +++ /dev/null @@ -1,488 +0,0 @@ -//============================================================================== -// -// Copyright (c) 2002- -// Authors: -// * Dave Parker (University of Oxford, formerly University of Birmingham) -// -//------------------------------------------------------------------------------ -// -// This file is part of PRISM. -// -// PRISM is free software; you can redistribute it and/or modify -// it under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 2 of the License, or -// (at your option) any later version. -// -// PRISM is distributed in the hope that it will be useful, -// but WITHOUT ANY WARRANTY; without even the implied warranty of -// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -// GNU General Public License for more details. -// -// You should have received a copy of the GNU General Public License -// along with PRISM; if not, write to the Free Software Foundation, -// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA -// -//============================================================================== - -package prism; - -import jdd.*; -import parser.*; -import parser.ast.*; - -// class to translate an expression into an MTBDD - -public class Expression2MTBDD -{ - // logs - private PrismLog mainLog; // main log - private PrismLog techLog; // tech log - - // info needed about model - private VarList varList; - private JDDVars[] varDDVars; - private Values constantValues; - - // filter to use at each recursive translate - // (e.g. 'reach' when model checking) - private JDDNode filter = null; - - // constructor - - public Expression2MTBDD(PrismLog log1, PrismLog log2, VarList vl, JDDVars[] vddv, Values cv) - { - mainLog = log1; - techLog = log2; - varList = vl; - varDDVars = vddv; - constantValues = cv; - } - - // set filter - - public void setFilter(JDDNode f) - { - filter = f; - } - - // Translate an expression - - public JDDNode translateExpression(Expression expr) throws PrismException - { - JDDNode res; - - // if-then-else - if (expr instanceof ExpressionITE) { - res = translateExpressionITE((ExpressionITE)expr); - } - // binary ops - else if (expr instanceof ExpressionBinaryOp) { - res = translateExpressionBinaryOp((ExpressionBinaryOp)expr); - } - // unary ops - else if (expr instanceof ExpressionUnaryOp) { - res = translateExpressionUnaryOp((ExpressionUnaryOp)expr); - } - // function - else if (expr instanceof ExpressionFunc) { - res = translateExpressionFunc((ExpressionFunc)expr); - } - // ident - else if (expr instanceof ExpressionIdent) { - // Should never happen - throw new PrismException("Unknown identifier \"" + ((ExpressionIdent)expr).getName() + "\""); - } - // literal - else if (expr instanceof ExpressionLiteral) { - res = translateExpressionLiteral((ExpressionLiteral)expr); - } - // constant - else if (expr instanceof ExpressionConstant) { - res = translateExpressionConstant((ExpressionConstant)expr); - } - // formula - else if (expr instanceof ExpressionFormula) { - // Should never happen - throw new PrismException("Unexpanded formula \"" + ((ExpressionFormula)expr).getName() + "\""); - } - // var - else if (expr instanceof ExpressionVar) { - res = translateExpressionVar((ExpressionVar)expr); - } - else { - throw new PrismException("Couldn't translate " + expr.getClass()); - } - - // apply filter if present - if (filter != null) { - JDD.Ref(filter); - res = JDD.Apply(JDD.TIMES, res, filter); - } - - return res; - } - - // Translate an 'if-then-else' - - private JDDNode translateExpressionITE(ExpressionITE expr) throws PrismException - { - JDDNode dd1, dd2, dd3; - - dd1 = translateExpression(expr.getOperand1()); - dd2 = translateExpression(expr.getOperand2()); - dd3 = translateExpression(expr.getOperand3()); - - return JDD.ITE(dd1, dd2, dd3); - } - - // Translate a binary operator - - private JDDNode translateExpressionBinaryOp(ExpressionBinaryOp expr) throws PrismException - { - JDDNode dd, tmp1, tmp2; - int op = expr.getOperator(); - - // Optimisations are possible for relational operators - // (note dubious use of knowledge that op IDs are consecutive) - if (op >= ExpressionBinaryOp.EQ && op <= ExpressionBinaryOp.LE) { - return translateExpressionRelOp(op, expr.getOperand1(), expr.getOperand2()); - } - - // Translate operands - tmp1 = translateExpression(expr.getOperand1()); - try { - tmp2 = translateExpression(expr.getOperand2()); - } - catch (PrismException e) { - JDD.Deref(tmp1); - throw e; - } - - // Apply operation - switch (op) { - case ExpressionBinaryOp.IMPLIES: dd = JDD.Or(JDD.Not(tmp1), tmp2); break; - case ExpressionBinaryOp.OR: dd = JDD.Or(tmp1, tmp2); break; - case ExpressionBinaryOp.AND: dd = JDD.And(tmp1, tmp2); break; - case ExpressionBinaryOp.PLUS: dd = JDD.Apply(JDD.PLUS, tmp1, tmp2); break; - case ExpressionBinaryOp.MINUS: dd = JDD.Apply(JDD.MINUS, tmp1, tmp2); break; - case ExpressionBinaryOp.TIMES: dd = JDD.Apply(JDD.TIMES, tmp1, tmp2); break; - case ExpressionBinaryOp.DIVIDE: dd = JDD.Apply(JDD.DIVIDE, tmp1, tmp2); break; - default: throw new PrismException("Unknown binary operator"); - } - - return dd; - } - - // Translate a relational operator (=, !=, >, >=, < <=) - - private JDDNode translateExpressionRelOp(int op, Expression expr1, Expression expr2) throws PrismException - { - JDDNode dd, tmp1, tmp2; - String s; - - // check for some easy (and common) special cases before resorting to the general case - - // var relop int - if (expr1 instanceof ExpressionVar && expr2.isConstant() && expr2.getType()==Expression.INT) { - ExpressionVar e1; - Expression e2; - int i, j, l, h, v; - e1 = (ExpressionVar)expr1; - e2 = expr2; - // get var's index - s = e1.getName(); - v = varList.getIndex(s); - if (v == -1) { - throw new PrismException("Unknown variable \"" + s + "\""); - } - // get some info on the variable - l = varList.getLow(v); - h = varList.getHigh(v); - // create dd - dd = JDD.Constant(0); - i = e2.evaluateInt(constantValues, null); - switch (op) { - case ExpressionBinaryOp.EQ: - if (i>=l && i <= h) dd = JDD.SetVectorElement(dd, varDDVars[v], i-l, 1); - break; - case ExpressionBinaryOp.NE: - if (i>=l && i <= h) dd = JDD.SetVectorElement(dd, varDDVars[v], i-l, 1); - dd = JDD.Not(dd); - break; - case ExpressionBinaryOp.GT: - for (j = i+1; j <= h; j++) dd = JDD.SetVectorElement(dd, varDDVars[v], j-l, 1); - break; - case ExpressionBinaryOp.GE: - for (j = i; j <= h; j++) dd = JDD.SetVectorElement(dd, varDDVars[v], j-l, 1); - break; - case ExpressionBinaryOp.LT: - for (j = i-1; j >= l; j--) dd = JDD.SetVectorElement(dd, varDDVars[v], j-l, 1); - break; - case ExpressionBinaryOp.LE: - for (j = i; j >= l; j--) dd = JDD.SetVectorElement(dd, varDDVars[v], j-l, 1); - break; - default: throw new PrismException("Unknown relational operator"); - } - return dd; - } - // int relop var - else if (expr1.isConstant() && expr1.getType()==Expression.INT && expr2 instanceof ExpressionVar) { - Expression e1; - ExpressionVar e2; - int i, j, l, h, v; - e1 = expr1; - e2 = (ExpressionVar)expr2; - // get var's index - s = e2.getName(); - v = varList.getIndex(s); - if (v == -1) { - throw new PrismException("Unknown variable \"" + s + "\""); - } - // get some info on the variable - l = varList.getLow(v); - h = varList.getHigh(v); - // create dd - dd = JDD.Constant(0); - i = e1.evaluateInt(constantValues, null); - switch (op) { - case ExpressionBinaryOp.EQ: - if (i>=l && i <= h) dd = JDD.SetVectorElement(dd, varDDVars[v], i-l, 1); - break; - case ExpressionBinaryOp.NE: - if (i>=l && i <= h) dd = JDD.SetVectorElement(dd, varDDVars[v], i-l, 1); - dd = JDD.Not(dd); - break; - case ExpressionBinaryOp.GT: - for (j = i-1; j >= l; j--) dd = JDD.SetVectorElement(dd, varDDVars[v], j-l, 1); - break; - case ExpressionBinaryOp.GE: - for (j = i; j >= l; j--) dd = JDD.SetVectorElement(dd, varDDVars[v], j-l, 1); - break; - case ExpressionBinaryOp.LT: - for (j = i+1; j <= h; j++) dd = JDD.SetVectorElement(dd, varDDVars[v], j-l, 1); - break; - case ExpressionBinaryOp.LE: - for (j = i; j <= h; j++) dd = JDD.SetVectorElement(dd, varDDVars[v], j-l, 1); - break; - default: throw new PrismException("Unknown relational operator"); - } - return dd; - } - - // general case - tmp1 = translateExpression(expr1); - tmp2 = translateExpression(expr2); - switch (op) { - case ExpressionBinaryOp.EQ: - dd = JDD.Apply(JDD.EQUALS, tmp1, tmp2); - break; - case ExpressionBinaryOp.NE: - dd = JDD.Apply(JDD.NOTEQUALS, tmp1, tmp2); - break; - case ExpressionBinaryOp.GT: - dd = JDD.Apply(JDD.GREATERTHAN, tmp1, tmp2); - break; - case ExpressionBinaryOp.GE: - dd = JDD.Apply(JDD.GREATERTHANEQUALS, tmp1, tmp2); - break; - case ExpressionBinaryOp.LT: - dd = JDD.Apply(JDD.LESSTHAN, tmp1, tmp2); - break; - case ExpressionBinaryOp.LE: - dd = JDD.Apply(JDD.LESSTHANEQUALS, tmp1, tmp2); - break; - default: throw new PrismException("Unknown relational operator"); - } - - return dd; - } - - // Translate a unary operator - - private JDDNode translateExpressionUnaryOp(ExpressionUnaryOp expr) throws PrismException - { - JDDNode dd, tmp; - int op = expr.getOperator(); - - // Translate operand - tmp = translateExpression(expr.getOperand()); - - // Apply operation - switch (op) { - case ExpressionUnaryOp.NOT: dd = JDD.Not(tmp); break; - case ExpressionUnaryOp.MINUS: dd = JDD.Apply(JDD.MINUS, JDD.Constant(0), tmp); break; - case ExpressionUnaryOp.PARENTH: dd = tmp; break; - default: throw new PrismException("Unknown unary operator"); - } - - return dd; - } - - // Translate a 'function' - - private JDDNode translateExpressionFunc(ExpressionFunc expr) throws PrismException - { - switch (expr.getNameCode()) { - case ExpressionFunc.MIN: return translateExpressionFuncMin(expr); - case ExpressionFunc.MAX: return translateExpressionFuncMax(expr); - case ExpressionFunc.FLOOR: return translateExpressionFuncFloor(expr); - case ExpressionFunc.CEIL: return translateExpressionFuncCeil(expr); - case ExpressionFunc.POW: return translateExpressionFuncPow(expr); - case ExpressionFunc.MOD: return translateExpressionFuncMod(expr); - case ExpressionFunc.LOG: return translateExpressionFuncLog(expr); - default: throw new PrismException("Unrecognised function \"" + expr.getName() + "\""); - } - } - - private JDDNode translateExpressionFuncMin(ExpressionFunc expr) throws PrismException - { - int i, n; - JDDNode dd, tmp; - - dd = translateExpression(expr.getOperand(0)); - n = expr.getNumOperands(); - for (i = 1; i < n; i++) { - try { - tmp = translateExpression(expr.getOperand(i)); - dd = JDD.Apply(JDD.MIN, dd, tmp); - } - catch (PrismException e) { - JDD.Deref(dd); - throw e; - } - } - - return dd; - } - - private JDDNode translateExpressionFuncMax(ExpressionFunc expr) throws PrismException - { - int i, n; - JDDNode dd, tmp; - - dd = translateExpression(expr.getOperand(0)); - n = expr.getNumOperands(); - for (i = 1; i < n; i++) { - try { - tmp = translateExpression(expr.getOperand(i)); - dd = JDD.Apply(JDD.MAX, dd, tmp); - } - catch (PrismException e) { - JDD.Deref(dd); - throw e; - } - } - - return dd; - } - - private JDDNode translateExpressionFuncFloor(ExpressionFunc expr) throws PrismException - { - JDDNode dd; - - dd = translateExpression(expr.getOperand(0)); - dd = JDD.MonadicApply(JDD.FLOOR, dd); - - return dd; - } - - private JDDNode translateExpressionFuncCeil(ExpressionFunc expr) throws PrismException - { - JDDNode dd; - - dd = translateExpression(expr.getOperand(0)); - dd = JDD.MonadicApply(JDD.CEIL, dd); - - return dd; - } - - private JDDNode translateExpressionFuncPow(ExpressionFunc expr) throws PrismException - { - JDDNode dd1, dd2, dd; - - dd1 = translateExpression(expr.getOperand(0)); - dd2 = translateExpression(expr.getOperand(1)); - dd = JDD.Apply(JDD.POW, dd1, dd2); - - return dd; - } - - private JDDNode translateExpressionFuncMod(ExpressionFunc expr) throws PrismException - { - JDDNode dd1, dd2, dd; - - dd1 = translateExpression(expr.getOperand(0)); - dd2 = translateExpression(expr.getOperand(1)); - dd = JDD.Apply(JDD.MOD, dd1, dd2); - - return dd; - } - - private JDDNode translateExpressionFuncLog(ExpressionFunc expr) throws PrismException - { - JDDNode dd1, dd2, dd; - - dd1 = translateExpression(expr.getOperand(0)); - dd2 = translateExpression(expr.getOperand(1)); - dd = JDD.Apply(JDD.LOGXY, dd1, dd2); - - return dd; - } - - // Translate a literal - - private JDDNode translateExpressionLiteral(ExpressionLiteral expr) throws PrismException - { - switch (expr.getType()) { - case Expression.BOOLEAN: return JDD.Constant(expr.evaluateBoolean(null, null) ? 1.0 : 0.0); - case Expression.INT: return JDD.Constant(expr.evaluateInt(null, null)); - case Expression.DOUBLE: return JDD.Constant(expr.evaluateDouble(null, null)); - default: throw new PrismException("Unknown literal type"); - } - } - - // Translate a constant - - private JDDNode translateExpressionConstant(ExpressionConstant expr) throws PrismException - { - int i; - Object o; - - i = constantValues.getIndexOf(expr.getName()); - if (i == -1) throw new PrismException("Couldn't evaluate constant \"" + expr.getName() + "\""); - switch (constantValues.getType(i)) { - case Expression.INT: return JDD.Constant(constantValues.getIntValue(i)); - case Expression.DOUBLE: return JDD.Constant(constantValues.getDoubleValue(i)); - case Expression.BOOLEAN: return JDD.Constant(constantValues.getBooleanValue(i) ? 1.0 : 0.0); - default: throw new PrismException("Unknown type for constant \"" + expr.getName() + "\""); - } - } - - // Translate a variable reference - - private JDDNode translateExpressionVar(ExpressionVar expr) throws PrismException - { - String s; - int v, l, h, i; - JDDNode dd, tmp; - - s = expr.getName(); - // get the variable's index - v = varList.getIndex(s); - if (v == -1) { - throw new PrismException("Unknown variable \"" + s + "\""); - } - // get some info on the variable - l = varList.getLow(v); - h = varList.getHigh(v); - // create dd - dd = JDD.Constant(0); - for (i = l; i <= h; i++) { - dd = JDD.SetVectorElement(dd, varDDVars[v], i-l, i); - } - - return dd; - } -} - -//------------------------------------------------------------------------------ diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index 1c216810..0227b8ae 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/prism/src/prism/Modules2MTBDD.java @@ -44,6 +44,9 @@ public class Modules2MTBDD // Prism object private Prism prism; + // StateModelChecker for expression -> MTBDD conversion + private StateModelChecker expr2mtbdd; + // logs private PrismLog mainLog; // main log private PrismLog techLog; // tech log @@ -51,9 +54,6 @@ public class Modules2MTBDD // ModulesFile object to store syntax tree from parser private ModulesFile modulesFile; - // Expression2MTBDD object for translating expressions - private Expression2MTBDD expr2mtbdd; - // model info // type @@ -178,8 +178,8 @@ public class Modules2MTBDD sortIdentities(); sortRanges(); - // create Expression2MTBDD object - expr2mtbdd = new Expression2MTBDD(mainLog, techLog, varList, varDDRowVars, constantValues); + // create stripped-down StateModelChecker for expression to MTBDD conversions + expr2mtbdd = new StateModelChecker(prism, varList, allDDRowVars, varDDRowVars, constantValues); // translate modules file into dd translateModules(); @@ -1846,7 +1846,7 @@ public class Modules2MTBDD private JDDNode translateExpression(Expression e) throws PrismException { // pass this work onto the Expression2MTBDD object - return expr2mtbdd.translateExpression(e); + return expr2mtbdd.checkExpressionDD(e); } // build state and transition rewards diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index eae37a3a..a64b11d7 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -1074,7 +1074,7 @@ public class Prism implements PrismSettingsListener LabelList ll; Expression expr; Values constantValues; - Expression2MTBDD expr2mtbdd = null; + StateModelChecker mc = null; JDDNode dd, labels[]; String labelNames[]; @@ -1096,15 +1096,14 @@ public class Prism implements PrismSettingsListener constantValues = new Values(); constantValues.addValues(model.getConstantValues()); if (propertiesFile != null) constantValues.addValues(propertiesFile.getConstantValues()); - expr2mtbdd = new Expression2MTBDD(mainLog, techLog, model.getVarList(), model.getVarDDRowVars(), constantValues); - expr2mtbdd.setFilter(model.getReach()); + mc = new StateModelChecker(this, model, null); } labels = new JDDNode[n+2]; labels[0] = model.getStart(); labels[1] = model.getFixedDeadlocks(); for (i = 0; i < n; i++) { expr = ll.getLabel(i); - dd = expr2mtbdd.translateExpression(expr); + dd = mc.checkExpressionDD(expr); labels[i+2] = dd; } // put names for labels in an array diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index 3229ef91..a8b87a1e 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -26,6 +26,8 @@ package prism; +import java.util.Vector; + import dv.DoubleVector; import jdd.*; import odd.*; @@ -98,6 +100,25 @@ public class StateModelChecker implements ModelChecker termCritParam = prism.getTermCritParam(); verbose = prism.getVerbose(); } + + /** + * Additional constructor for creating stripped down StateModelChecker for + * expression to MTBDD conversions. + */ + public StateModelChecker(Prism prism, VarList varList, JDDVars allDDRowVars, JDDVars[] varDDRowVars, Values constantValues) throws PrismException + { + // Initialise + this.prism = prism; + mainLog = prism.getMainLog(); + techLog = prism.getTechLog(); + this.varList = varList; + this.varDDRowVars = varDDRowVars; + this.constantValues = constantValues; + // Create dummy model + reach = null; + model = new ProbModel(JDD.Constant(0), JDD.Constant(0), new JDDNode[] {}, null, null, allDDRowVars, null, + null, 0, null, null, null, 0, varList, varDDRowVars, null, constantValues); + } // ----------------------------------------------------------------------------------- // Check a property, i.e. an expression @@ -313,7 +334,8 @@ public class StateModelChecker implements ModelChecker // Filter out non-reachable states from solution // (only necessary for symbolically stored vectors) - if (res instanceof StateProbsMTBDD) + // (skip if reach is null, e.g. if just being used to convert arbitrary expressions) + if (res instanceof StateProbsMTBDD && reach != null) res.filter(reach); return res;