First version of explicit expression evaluation stuff (all but functions).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@722 bbc10eb1-c90d-0410-af57-cb519fbb1720

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

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)
+		)
+	);
+}
+
+//------------------------------------------------------------------------------

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)
 	{

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);
 	}
 }
 

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

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

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