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

Removal of Expression2MTBDD class. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@748 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 18 years ago
parent
d9c38a0763
commit
39974b5e7e
4 changed files with 32 additions and 499 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. 488
      prism/src/prism/Expression2MTBDD.java
  2. 12
      prism/src/prism/Modules2MTBDD.java
  3. 7
      prism/src/prism/Prism.java
  4. 24
      prism/src/prism/StateModelChecker.java

488
prism/src/prism/Expression2MTBDD.java
View File

@ -1,488 +0,0 @@
//==============================================================================
//
// Copyright (c) 2002-
// Authors:
// * Dave Parker <david.parker@comlab.ox.ac.uk> (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;
}
}
//------------------------------------------------------------------------------

12
prism/src/prism/Modules2MTBDD.java
View File

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

7
prism/src/prism/Prism.java
View File

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

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

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

Write Preview
Loading…
Cancel
Save