diff --git a/prism/include/DoubleVector.h b/prism/include/DoubleVector.h index a10e1d9b..8790c6e7 100644 --- a/prism/include/DoubleVector.h +++ b/prism/include/DoubleVector.h @@ -39,6 +39,14 @@ JNIEXPORT jlong JNICALL Java_dv_DoubleVector_DV_1ConvertMTBDD JNIEXPORT jdouble JNICALL Java_dv_DoubleVector_DV_1GetElement (JNIEnv *, jobject, jlong, jint, jint); +/* + * Class: dv_DoubleVector + * Method: DV_SetElement + * Signature: (JIID)V + */ +JNIEXPORT void JNICALL Java_dv_DoubleVector_DV_1SetElement + (JNIEnv *, jobject, jlong, jint, jint, jdouble); + /* * Class: dv_DoubleVector * Method: DV_RoundOff @@ -175,6 +183,14 @@ JNIEXPORT jlong JNICALL Java_dv_DoubleVector_DV_1BDDLessThan JNIEXPORT jlong JNICALL Java_dv_DoubleVector_DV_1BDDInterval (JNIEnv *, jobject, jlong, jdouble, jdouble, jlong, jint, jlong); +/* + * Class: dv_DoubleVector + * Method: DV_ConvertToMTBDD + * Signature: (JJIJ)J + */ +JNIEXPORT jlong JNICALL Java_dv_DoubleVector_DV_1ConvertToMTBDD + (JNIEnv *, jobject, jlong, jlong, jint, jlong); + #ifdef __cplusplus } #endif diff --git a/prism/src/dv/DoubleVector.cc b/prism/src/dv/DoubleVector.cc index de05563a..b40802a5 100644 --- a/prism/src/dv/DoubleVector.cc +++ b/prism/src/dv/DoubleVector.cc @@ -110,6 +110,22 @@ jint i //------------------------------------------------------------------------------ +JNIEXPORT void JNICALL Java_dv_DoubleVector_DV_1SetElement +( +JNIEnv *env, +jobject obj, +jlong __pointer v, +jint n, +jint i, +jdouble d +) +{ + double *vector = jlong_to_double(v); + vector[i] = d; +} + +//------------------------------------------------------------------------------ + JNIEXPORT void JNICALL Java_dv_DoubleVector_DV_1RoundOff ( JNIEnv *env, @@ -482,3 +498,25 @@ jlong __pointer odd } //------------------------------------------------------------------------------ + +JNIEXPORT jlong __pointer JNICALL Java_dv_DoubleVector_DV_1ConvertToMTBDD +( +JNIEnv *env, +jobject obj, +jlong __pointer vector, +jlong __pointer vars, +jint num_vars, +jlong __pointer odd +) +{ + return ptr_to_jlong( + double_vector_to_mtbdd( + ddman, + jlong_to_double(vector), + jlong_to_DdNode_array(vars), num_vars, + jlong_to_ODDNode(odd) + ) + ); +} + +//------------------------------------------------------------------------------ diff --git a/prism/src/dv/DoubleVector.java b/prism/src/dv/DoubleVector.java index a11e7dfd..3bf9699d 100644 --- a/prism/src/dv/DoubleVector.java +++ b/prism/src/dv/DoubleVector.java @@ -110,6 +110,13 @@ public class DoubleVector return DV_GetElement(v, n, i); } + // set element + private native void DV_SetElement(long v, int n, int i, double d); + public void setElement(int i, double d) + { + DV_SetElement(v, n, i, d); + } + // round off private native void DV_RoundOff(long v, int n, int places); public void roundOff(int places) @@ -241,6 +248,18 @@ public class DoubleVector return sol; } + private native long DV_ConvertToMTBDD(long v, long vars, int num_vars, long odd); + public JDDNode convertToMTBDD(JDDVars vars, ODDNode odd) + { + JDDNode sol; + + sol = new JDDNode( + DV_ConvertToMTBDD(v, vars.array(), vars.n(), odd.ptr()) + ); + + return sol; + } + // print (all, including nonzeros) public void print(PrismLog log) { diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index 5a1f302d..42b6d78f 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -26,6 +26,7 @@ package prism; +import dv.DoubleVector; import jdd.*; import odd.*; import parser.*; @@ -328,22 +329,55 @@ public class StateModelChecker implements ModelChecker private StateProbs checkExpressionITE(ExpressionITE expr) throws PrismException { + StateProbs res1 = null, res2 = null, res3 = null; JDDNode dd, dd1, dd2, dd3; - - dd1 = checkExpressionDD(expr.getOperand1()); - dd2 = checkExpressionDD(expr.getOperand2()); - dd3 = checkExpressionDD(expr.getOperand3()); - dd = JDD.ITE(dd1, dd2, dd3); - - return new StateProbsMTBDD(dd, model); + DoubleVector dv2, dv3; + + // Check operands recursively + try { + res1 = checkExpression(expr.getOperand1()); + res2 = checkExpression(expr.getOperand2()); + res3 = checkExpression(expr.getOperand3()); + } + catch (PrismException e) { + if (res1 != null) res1.clear(); + if (res2 != null) res2.clear(); + if (res3 != null) res3.clear(); + throw e; + } + + // Operand 1 is boolean so should be symbolic + dd1 = res1.convertToStateProbsMTBDD().getJDDNode(); + + // If both operands 2/3 are symbolic, result will be symbolic + if (res2 instanceof StateProbsMTBDD && res3 instanceof StateProbsMTBDD) { + dd2 = ((StateProbsMTBDD)res2).getJDDNode(); + dd3 = ((StateProbsMTBDD)res3).getJDDNode(); + dd = JDD.ITE(dd1, dd2, dd3); + return new StateProbsMTBDD(dd, model); + } + // Otherwise result will be explicit + else { + dv2 = res2.convertToStateProbsDV().getDoubleVector(); + dv2.filter(dd1, allDDRowVars, odd); + dv3 = res3.convertToStateProbsDV().getDoubleVector(); + dd1 = JDD.Not(dd1); + dv3.filter(dd1, allDDRowVars, odd); + dv2.add(dv3); + dv3.clear(); + JDD.Deref(dd1); + return new StateProbsDV(dv2, model); + } } // Check a binary operator private StateProbs checkExpressionBinaryOp(ExpressionBinaryOp expr) throws PrismException { - JDDNode dd, tmp1, tmp2; - int op = expr.getOperator(); + StateProbs res1 = null, res2 = null; + JDDNode dd, dd1, dd2; + DoubleVector dv1, dv2; + int i, n, op = expr.getOperator(); // Optimisations are possible for relational operators // (note dubious use of knowledge that op IDs are consecutive) @@ -351,53 +385,92 @@ public class StateModelChecker implements ModelChecker return checkExpressionRelOp(op, expr.getOperand1(), expr.getOperand2()); } - // Check operands - tmp1 = checkExpressionDD(expr.getOperand1()); + // Check operands recursively try { - tmp2 = checkExpressionDD(expr.getOperand2()); - } catch (PrismException e) { - JDD.Deref(tmp1); + res1 = checkExpression(expr.getOperand1()); + res2 = checkExpression(expr.getOperand2()); + } + catch (PrismException e) { + if (res1 != null) res1.clear(); + if (res2 != null) res2.clear(); 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"); + // If both operands are symbolic, result will be symbolic + if (res1 instanceof StateProbsMTBDD && res2 instanceof StateProbsMTBDD) { + dd1 = ((StateProbsMTBDD)res1).getJDDNode(); + dd2 = ((StateProbsMTBDD)res2).getJDDNode(); + // Apply operation + switch (op) { + case ExpressionBinaryOp.IMPLIES: + dd = JDD.Or(JDD.Not(dd1), dd2); + break; + case ExpressionBinaryOp.OR: + dd = JDD.Or(dd1, dd2); + break; + case ExpressionBinaryOp.AND: + dd = JDD.And(dd1, dd2); + break; + case ExpressionBinaryOp.PLUS: + dd = JDD.Apply(JDD.PLUS, dd1, dd2); + break; + case ExpressionBinaryOp.MINUS: + dd = JDD.Apply(JDD.MINUS, dd1, dd2); + break; + case ExpressionBinaryOp.TIMES: + dd = JDD.Apply(JDD.TIMES, dd1, dd2); + break; + case ExpressionBinaryOp.DIVIDE: + dd = JDD.Apply(JDD.DIVIDE, dd1, dd2); + break; + default: + throw new PrismException("Unknown binary operator"); + } + return new StateProbsMTBDD(dd, model); + } + // Otherwise result will be explicit + else { + dv1 = res1.convertToStateProbsDV().getDoubleVector(); + dv2 = res2.convertToStateProbsDV().getDoubleVector(); + n = dv1.getSize(); + // Apply operation + switch (op) { + case ExpressionBinaryOp.IMPLIES: + case ExpressionBinaryOp.OR: + case ExpressionBinaryOp.AND: + throw new PrismException("Internal error: Explicit evaluation of Boolean"); + //for (i = 0; i < n; i++) dv1.setElement(i, (!(dv1.getElement(i)>0) || (dv2.getElement(i)>0)) ? 1.0 : 0.0); + //for (i = 0; i < n; i++) dv1.setElement(i, ((dv1.getElement(i)>0) || (dv2.getElement(i)>0)) ? 1.0 : 0.0); + //for (i = 0; i < n; i++) dv1.setElement(i, ((dv1.getElement(i)>0) && (dv2.getElement(i)>0)) ? 1.0 : 0.0); + case ExpressionBinaryOp.PLUS: + for (i = 0; i < n; i++) dv1.setElement(i, dv1.getElement(i) + dv2.getElement(i)); + break; + case ExpressionBinaryOp.MINUS: + for (i = 0; i < n; i++) dv1.setElement(i, dv1.getElement(i) - dv2.getElement(i)); + break; + case ExpressionBinaryOp.TIMES: + for (i = 0; i < n; i++) dv1.setElement(i, dv1.getElement(i) * dv2.getElement(i)); + break; + case ExpressionBinaryOp.DIVIDE: + for (i = 0; i < n; i++) dv1.setElement(i, dv1.getElement(i) / dv2.getElement(i)); + break; + default: + throw new PrismException("Unknown binary operator"); + } + dv2.clear(); + return new StateProbsDV(dv1, model); } - - return new StateProbsMTBDD(dd, model); } // Check a relational operator (=, !=, >, >=, < <=) private StateProbs checkExpressionRelOp(int op, Expression expr1, Expression expr2) throws PrismException { - JDDNode dd, tmp1, tmp2; + StateProbs res1 = null, res2 = null; + JDDNode dd, dd1, dd2; String s; - - // check for some easy (and common) special cases before resorting to + + // Check for some easy (and common) special cases before resorting to // the general case // var relop int @@ -501,32 +574,43 @@ public class StateModelChecker implements ModelChecker return new StateProbsMTBDD(dd, model); } - // general case - tmp1 = checkExpressionDD(expr1); - tmp2 = checkExpressionDD(expr2); + // General case. + // Since the result is a Boolean and thus returned as an MTBDD, we + // just convert both operands to MTBDDs first. Optimisations would be possible here. + // Check operands recursively + try { + res1 = checkExpression(expr1); + res2 = checkExpression(expr2); + } + catch (PrismException e) { + if (res1 != null) res1.clear(); + if (res2 != null) res2.clear(); + throw e; + } + dd1 = res1.convertToStateProbsMTBDD().getJDDNode(); + dd2 = res2.convertToStateProbsMTBDD().getJDDNode(); switch (op) { case ExpressionBinaryOp.EQ: - dd = JDD.Apply(JDD.EQUALS, tmp1, tmp2); + dd = JDD.Apply(JDD.EQUALS, dd1, dd2); break; case ExpressionBinaryOp.NE: - dd = JDD.Apply(JDD.NOTEQUALS, tmp1, tmp2); + dd = JDD.Apply(JDD.NOTEQUALS, dd1, dd2); break; case ExpressionBinaryOp.GT: - dd = JDD.Apply(JDD.GREATERTHAN, tmp1, tmp2); + dd = JDD.Apply(JDD.GREATERTHAN, dd1, dd2); break; case ExpressionBinaryOp.GE: - dd = JDD.Apply(JDD.GREATERTHANEQUALS, tmp1, tmp2); + dd = JDD.Apply(JDD.GREATERTHANEQUALS, dd1, dd2); break; case ExpressionBinaryOp.LT: - dd = JDD.Apply(JDD.LESSTHAN, tmp1, tmp2); + dd = JDD.Apply(JDD.LESSTHAN, dd1, dd2); break; case ExpressionBinaryOp.LE: - dd = JDD.Apply(JDD.LESSTHANEQUALS, tmp1, tmp2); + dd = JDD.Apply(JDD.LESSTHANEQUALS, dd1, dd2); break; default: throw new PrismException("Unknown relational operator"); } - return new StateProbsMTBDD(dd, model); } @@ -534,28 +618,56 @@ public class StateModelChecker implements ModelChecker private StateProbs checkExpressionUnaryOp(ExpressionUnaryOp expr) throws PrismException { - JDDNode dd, tmp; - int op = expr.getOperator(); - - // Check operand - tmp = checkExpressionDD(expr.getOperand()); + StateProbs res1 = null; + JDDNode dd, dd1; + DoubleVector dv1; + int i, n, op = expr.getOperator(); - // 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"); + // Check operand recursively + try { + res1 = checkExpression(expr.getOperand()); + } + catch (PrismException e) { + if (res1 != null) res1.clear(); + throw e; + } + + // Parentheses are easy - nothing to do: + if (op == ExpressionUnaryOp.PARENTH) return res1; + + // If operand is symbolic, result will be symbolic + if (res1 instanceof StateProbsMTBDD) { + dd1 = ((StateProbsMTBDD)res1).getJDDNode(); + // Apply operation + switch (op) { + case ExpressionUnaryOp.NOT: + dd = JDD.Not(dd1); + break; + case ExpressionUnaryOp.MINUS: + dd = JDD.Apply(JDD.MINUS, JDD.Constant(0), dd1); + break; + default: + throw new PrismException("Unknown unary operator"); + } + return new StateProbsMTBDD(dd, model); + } + // Otherwise result will be explicit + else { + dv1 = res1.convertToStateProbsDV().getDoubleVector(); + n = dv1.getSize(); + // Apply operation + switch (op) { + case ExpressionUnaryOp.NOT: + throw new PrismException("Internal error: Explicit evaluation of Boolean"); + //for (i = 0; i < n; i++) dv1.setElement(i, (dv1.getElement(i)>0) ? 0.0 : 1.0); + case ExpressionUnaryOp.MINUS: + for (i = 0; i < n; i++) dv1.setElement(i, -dv1.getElement(i)); + break; + default: + throw new PrismException("Unknown unary operator"); + } + return new StateProbsDV(dv1, model); } - - return new StateProbsMTBDD(dd, model); } // Check a 'function' @@ -761,9 +873,11 @@ public class StateModelChecker implements ModelChecker if (expr.getName().equals("deadlock")) { dd = model.getFixedDeadlocks(); JDD.Ref(dd); + return new StateProbsMTBDD(dd, model); } else if (expr.getName().equals("init")) { dd = start; JDD.Ref(dd); + return new StateProbsMTBDD(dd, model); } else { // get expression associated with label ll = propertiesFile.getCombinedLabelList(); @@ -771,10 +885,8 @@ public class StateModelChecker implements ModelChecker if (i == -1) throw new PrismException("Unknown label \"" + expr.getName() + "\" in property"); // check recursively - dd = checkExpressionDD(ll.getLabel(i)); + return checkExpression(ll.getLabel(i)); } - - return new StateProbsMTBDD(dd, model); } } diff --git a/prism/src/prism/StateProbs.java b/prism/src/prism/StateProbs.java index 33ac64ae..91701953 100644 --- a/prism/src/prism/StateProbs.java +++ b/prism/src/prism/StateProbs.java @@ -32,6 +32,8 @@ import jdd.JDDNode; public interface StateProbs { + StateProbsDV convertToStateProbsDV(); + StateProbsMTBDD convertToStateProbsMTBDD(); void roundOff(int places); void subtractFromOne(); void add(StateProbs sp); diff --git a/prism/src/prism/StateProbsDV.java b/prism/src/prism/StateProbsDV.java index 2091ace4..c5824b01 100644 --- a/prism/src/prism/StateProbsDV.java +++ b/prism/src/prism/StateProbsDV.java @@ -40,6 +40,7 @@ public class StateProbsDV implements StateProbs DoubleVector probs; // info from model + Model model; JDDVars vars; int numVars; ODDNode odd; @@ -57,7 +58,7 @@ public class StateProbsDV implements StateProbs // CONSTRUCTORS - public StateProbsDV(DoubleVector p, Model model) + public StateProbsDV(DoubleVector p, Model m) { int i; @@ -65,6 +66,7 @@ public class StateProbsDV implements StateProbs probs = p; // get info from model + model = m; vars = model.getAllDDRowVars(); numVars = vars.n(); odd = model.getODD(); @@ -83,7 +85,23 @@ public class StateProbsDV implements StateProbs // construct double vector from an mtbdd this(new DoubleVector(dd, model.getAllDDRowVars(), model.getODD()), model); } - + + // CONVERSION METHODS + + // convert to StateProbsDV (nothing to do) + public StateProbsDV convertToStateProbsDV() + { + return this; + } + + // convert to StateProbsMTBDD, destroy (clear) old vector + public StateProbsMTBDD convertToStateProbsMTBDD() + { + StateProbsMTBDD res = new StateProbsMTBDD(probs.convertToMTBDD(vars, odd), model); + clear(); + return res; + } + // METHODS TO MODIFY VECTOR // round diff --git a/prism/src/prism/StateProbsMTBDD.java b/prism/src/prism/StateProbsMTBDD.java index c91f23dc..04f3b580 100644 --- a/prism/src/prism/StateProbsMTBDD.java +++ b/prism/src/prism/StateProbsMTBDD.java @@ -39,6 +39,7 @@ public class StateProbsMTBDD implements StateProbs JDDNode probs; // info from model + Model model; JDDVars vars; JDDNode reach; int numDDRowVars; @@ -57,7 +58,7 @@ public class StateProbsMTBDD implements StateProbs // CONSTRUCTOR - public StateProbsMTBDD(JDDNode p, Model model) + public StateProbsMTBDD(JDDNode p, Model m) { int i; @@ -65,6 +66,7 @@ public class StateProbsMTBDD implements StateProbs probs = p; // get info from model + model = m; vars = model.getAllDDRowVars(); reach = model.getReach(); numDDRowVars = model.getNumDDRowVars(); @@ -80,6 +82,22 @@ public class StateProbsMTBDD implements StateProbs varValues = new int[varList.getNumVars()]; } + // CONVERSION METHODS + + // convert to StateProbsDV, destroy (clear) old vector + public StateProbsDV convertToStateProbsDV() + { + StateProbsDV res = new StateProbsDV(probs, model); + clear(); + return res; + } + + // convert to StateProbsMTBDD (nothing to do) + public StateProbsMTBDD convertToStateProbsMTBDD() + { + return this; + } + // METHODS TO MODIFY VECTOR // round