Precomputation algorithm tidy-up.

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

prism/include/PrismMTBDD.h

@@ -106,10 +106,10 @@ JNIEXPORT jlong JNICALL Java_mtbdd_PrismMTBDD_PM_1Reachability
 /*
  * Class:     mtbdd_PrismMTBDD
  * Method:    PM_Prob1
- * Signature: (JJIJIJJ)J
+ * Signature: (JJJIJIJJJ)J
  */
 JNIEXPORT jlong JNICALL Java_mtbdd_PrismMTBDD_PM_1Prob1
-  (JNIEnv *, jclass, jlong, jlong, jint, jlong, jint, jlong, jlong);
+  (JNIEnv *, jclass, jlong, jlong, jlong, jint, jlong, jint, jlong, jlong, jlong);
 
 /*
  * Class:     mtbdd_PrismMTBDD
@@ -122,10 +122,10 @@ JNIEXPORT jlong JNICALL Java_mtbdd_PrismMTBDD_PM_1Prob0
 /*
  * Class:     mtbdd_PrismMTBDD
  * Method:    PM_Prob1E
- * Signature: (JJIJIJIJJ)J
+ * Signature: (JJJIJIJIJJJ)J
  */
 JNIEXPORT jlong JNICALL Java_mtbdd_PrismMTBDD_PM_1Prob1E
-  (JNIEnv *, jclass, jlong, jlong, jint, jlong, jint, jlong, jint, jlong, jlong);
+  (JNIEnv *, jclass, jlong, jlong, jlong, jint, jlong, jint, jlong, jint, jlong, jlong, jlong);
 
 /*
  * Class:     mtbdd_PrismMTBDD

prism/src/mtbdd/PM_Prob0.cc

@@ -41,24 +41,24 @@ JNIEXPORT jlong __jlongpointer JNICALL Java_mtbdd_PrismMTBDD_PM_1Prob0
 (
 JNIEnv *env,
 jclass cls,
-jlong __jlongpointer t01, 		// 0-1 trans matrix
-jlong __jlongpointer a,		// all reachable states
-jlong __jlongpointer rv,		// row vars
+jlong __jlongpointer t01, 	// 0-1 trans matrix
+jlong __jlongpointer r,		// all reachable states
+jlong __jlongpointer rv,	// row vars
 jint num_rvars,
-jlong __jlongpointer cv,		// col vars
+jlong __jlongpointer cv,	// col vars
 jint num_cvars,
-jlong __jlongpointer phi,		// phi(b1)
-jlong __jlongpointer psi		// psi(b2)
+jlong __jlongpointer phi,	// phi(b1)
+jlong __jlongpointer psi	// psi(b2)
 )
 {
 	DdNode *trans01 = jlong_to_DdNode(t01);		// 0-1 trans matrix
-	DdNode *b1 = jlong_to_DdNode(phi);		// b1
-	DdNode *b2 = jlong_to_DdNode(psi);		// b2
-	DdNode *all = jlong_to_DdNode(a);		// all reachable states
+	DdNode *reach = jlong_to_DdNode(r);			// all reachable states
+	DdNode *b1 = jlong_to_DdNode(phi);			// b1
+	DdNode *b2 = jlong_to_DdNode(psi);			// b2
 	DdNode **rvars = jlong_to_DdNode_array(rv);	// row vars
-	DdNode **cvars = jlong_to_DdNode_array(cv);	// col vars	
+	DdNode **cvars = jlong_to_DdNode_array(cv);	// col vars
 	
-	DdNode *reach, *sol, *tmp;
+	DdNode *sol, *tmp;
 	bool done;
 	int iters;
 
@@ -71,15 +71,15 @@ jlong __jlongpointer psi		// psi(b2)
 	
 	// reachability fixpoint loop
 	Cudd_Ref(b2);
-	reach = b2;
+	sol = b2;
 	done = false;
 	iters = 0;
 	while (!done) {
 	
 		iters++;
 		
-		Cudd_Ref(reach);
-		tmp = DD_PermuteVariables(ddman, reach, rvars, cvars, num_cvars);
+		Cudd_Ref(sol);
+		tmp = DD_PermuteVariables(ddman, sol, rvars, cvars, num_cvars);
 		Cudd_Ref(trans01);
 		tmp = DD_And(ddman, tmp, trans01);
 		tmp = DD_ThereExists(ddman, tmp, cvars, num_cvars);
@@ -89,17 +89,17 @@ jlong __jlongpointer psi		// psi(b2)
 		Cudd_Ref(b2);
 		tmp = DD_Or(ddman, b2, tmp);
 		
-		if (tmp == reach) {
+		if (tmp == sol) {
 			done = true;
 		}
-		Cudd_RecursiveDeref(ddman, reach);
-		reach = tmp;
+		Cudd_RecursiveDeref(ddman, sol);
+		sol = tmp;
 	}
-	reach = DD_PermuteVariables(ddman, reach, cvars, rvars, num_cvars);
+	sol = DD_PermuteVariables(ddman, sol, cvars, rvars, num_cvars);
 	
 	// actual answer is states NOT reachable
-	Cudd_Ref(all);
-	sol = DD_And(ddman, all, DD_Not(ddman, reach));
+	Cudd_Ref(reach);
+	sol = DD_And(ddman, reach, DD_Not(ddman, sol));
 
 	// stop clock
 	time_taken = (double)(util_cpu_time() - start1)/1000;

prism/src/mtbdd/PM_Prob0A.cc

@@ -57,14 +57,14 @@ jlong __jlongpointer psi	// psi(b2)
 )
 {
 	DdNode *trans01 = jlong_to_DdNode(t01);		// 0-1 trans matrix
-	DdNode *all = jlong_to_DdNode(r);		// reachable states
+	DdNode *reach = jlong_to_DdNode(r);		// reachable states
 	DdNode **rvars = jlong_to_DdNode_array(rv);	// row vars
 	DdNode **cvars = jlong_to_DdNode_array(cv);	// col vars
 	DdNode **ndvars = jlong_to_DdNode_array(ndv);	// nondet vars
 	DdNode *b1 = jlong_to_DdNode(phi);		// b1
 	DdNode *b2 = jlong_to_DdNode(psi);		// b2
 	
-	DdNode *reach, *sol, *tmp;
+	DdNode *sol, *tmp;
 	bool done;
 	int iters;
 
@@ -77,15 +77,15 @@ jlong __jlongpointer psi	// psi(b2)
 	
 	// reachability fixpoint loop
 	Cudd_Ref(b2);
-	reach = b2;
+	sol = b2;
 	done = false;
 	iters = 0;
 	while (!done) {
 	
 		iters++;
 		
-		Cudd_Ref(reach);
-		tmp = DD_PermuteVariables(ddman, reach, rvars, cvars, num_cvars);
+		Cudd_Ref(sol);
+		tmp = DD_PermuteVariables(ddman, sol, rvars, cvars, num_cvars);
 		Cudd_Ref(trans01);
 		tmp = DD_And(ddman, tmp, trans01);
 		tmp = DD_ThereExists(ddman, tmp, cvars, num_cvars);
@@ -97,17 +97,17 @@ jlong __jlongpointer psi	// psi(b2)
 		Cudd_Ref(b2);
 		tmp = DD_Or(ddman, b2, tmp);
 		
-		if (tmp == reach) {
+		if (tmp == sol) {
 			done = true;
 		}
-		Cudd_RecursiveDeref(ddman, reach);
-		reach = tmp;
+		Cudd_RecursiveDeref(ddman, sol);
+		sol = tmp;
 	}
-	reach = DD_PermuteVariables(ddman, reach, cvars, rvars, num_cvars);
+	sol = DD_PermuteVariables(ddman, sol, cvars, rvars, num_cvars);
 	
 	// actual answer is states NOT reachable
-	Cudd_Ref(all);
-	sol = DD_And(ddman, all, DD_Not(ddman, reach));
+	Cudd_Ref(reach);
+	sol = DD_And(ddman, reach, DD_Not(ddman, sol));
 
 	// stop clock
 	time_taken = (double)(util_cpu_time() - start1)/1000;

prism/src/mtbdd/PM_Prob0E.cc

@@ -58,7 +58,7 @@ jlong __jlongpointer psi	// psi(b2)
 )
 {
 	DdNode *trans01 = jlong_to_DdNode(t01);		// 0-1 trans matrix
-	DdNode *all = jlong_to_DdNode(r);		// reachable states
+	DdNode *reach = jlong_to_DdNode(r);		// reachable states
 	DdNode *mask = jlong_to_DdNode(ndm);		// nondeterminism mask
 	DdNode **rvars = jlong_to_DdNode_array(rv);	// row vars
 	DdNode **cvars = jlong_to_DdNode_array(cv);	// col vars	
@@ -66,7 +66,7 @@ jlong __jlongpointer psi	// psi(b2)
 	DdNode *b1 = jlong_to_DdNode(phi);		// b1
 	DdNode *b2 = jlong_to_DdNode(psi);		// b2
 	
-	DdNode *reach, *sol, *tmp;
+	DdNode *sol, *tmp;
 	bool done;
 	int iters;
 
@@ -79,15 +79,15 @@ jlong __jlongpointer psi	// psi(b2)
 	
 	// reachability fixpoint loop
 	Cudd_Ref(b2);
-	reach = b2;
+	sol = b2;
 	done = false;
 	iters = 0;
 	while (!done) {
 	
 		iters++;
 		
-		Cudd_Ref(reach);
-		tmp = DD_PermuteVariables(ddman, reach, rvars, cvars, num_cvars);
+		Cudd_Ref(sol);
+		tmp = DD_PermuteVariables(ddman, sol, rvars, cvars, num_cvars);
 		Cudd_Ref(trans01);
 		tmp = DD_And(ddman, tmp, trans01);
 		tmp = DD_ThereExists(ddman, tmp, cvars, num_cvars);
@@ -101,17 +101,17 @@ jlong __jlongpointer psi	// psi(b2)
 		Cudd_Ref(b2);
 		tmp = DD_Or(ddman, b2, tmp);
 		
-		if (tmp == reach) {
+		if (tmp == sol) {
 			done = true;
 		}
-		Cudd_RecursiveDeref(ddman, reach);
-		reach = tmp;
+		Cudd_RecursiveDeref(ddman, sol);
+		sol = tmp;
 	}
-	reach = DD_PermuteVariables(ddman, reach, cvars, rvars, num_cvars);
+	sol = DD_PermuteVariables(ddman, sol, cvars, rvars, num_cvars);
 	
 	// actual answer is states NOT reachable
-	Cudd_Ref(all);
-	sol = DD_And(ddman, all, DD_Not(ddman, reach));
+	Cudd_Ref(reach);
+	sol = DD_And(ddman, reach, DD_Not(ddman, sol));
 
 	// stop clock
 	time_taken = (double)(util_cpu_time() - start1)/1000;

prism/src/mtbdd/PM_Prob1.cc

@@ -42,22 +42,26 @@ JNIEXPORT jlong __jlongpointer JNICALL Java_mtbdd_PrismMTBDD_PM_1Prob1
 JNIEnv *env,
 jclass cls,
 jlong __jlongpointer t01, 	// 0-1 trans matrix
+jlong __jlongpointer r,		// all reachable states
 jlong __jlongpointer rv,	// row vars
 jint num_rvars,
 jlong __jlongpointer cv,	// col vars
 jint num_cvars,
 jlong __jlongpointer phi,	// phi(b1)
-jlong __jlongpointer psi	// psi(b2)
+jlong __jlongpointer psi,	// psi(b2)
+jlong __jlongpointer _no	// no
 )
 {
 	DdNode *trans01 = jlong_to_DdNode(t01);		// 0-1 trans matrix
-	DdNode *b1 = jlong_to_DdNode(phi);		// b1
-	DdNode *b2 = jlong_to_DdNode(psi);		// b2
+	DdNode *reach = jlong_to_DdNode(r);			// all reachable states
+	DdNode *b1 = jlong_to_DdNode(phi);			// b1
+	DdNode *b2 = jlong_to_DdNode(psi);			// b2
+	DdNode *no = jlong_to_DdNode(_no);			// no
 	DdNode **rvars = jlong_to_DdNode_array(rv);	// row vars
 	DdNode **cvars = jlong_to_DdNode_array(cv);	// col vars
 	
-	DdNode *u, *v, *tmp, *tmp2;
-	bool u_done, v_done;
+	DdNode *sol, *tmp;
+	bool done;
 	int iters;
 
 	// timing stuff
@@ -67,51 +71,40 @@ jlong __jlongpointer psi	// psi(b2)
 	// start clock
 	start1 = util_cpu_time();
 	
-	// greatest fixed point - start from true
-	u = DD_Constant(ddman, 1);
-	u_done = false;
+	// reachability fixpoint loop
+	Cudd_Ref(no);
+	sol = no;
+	done = false;
 	iters = 0;
+	while (!done) {
 	
-	while (!u_done) {
-	
-		// least fixed point - start from false
-		v = DD_Constant(ddman, 0);
-		v_done = false;
+		iters++;
 		
-		while (!v_done) {
-				
-			iters++;
-				
-			Cudd_Ref(u);
-			tmp = DD_SwapVariables(ddman, u, rvars, cvars, num_rvars);
-			Cudd_Ref(trans01);
-			tmp = DD_ForAll(ddman, DD_Implies(ddman, trans01, tmp), cvars, num_cvars);
-
-			Cudd_Ref(v);
-			tmp2 = DD_SwapVariables(ddman, v, rvars, cvars, num_rvars);
-			Cudd_Ref(trans01);
-			tmp2 = DD_ThereExists(ddman, DD_And(ddman, tmp2, trans01), cvars, num_cvars);
-
-			tmp = DD_And(ddman, tmp, tmp2);
-
-			Cudd_Ref(b1);
-			tmp = DD_And(ddman, b1, tmp);		
-			Cudd_Ref(b2);
-			tmp = DD_Or(ddman, b2, tmp);
-			
-			if (tmp == v) {
-				v_done = true;
-			}
-			Cudd_RecursiveDeref(ddman, v);
-			v = tmp;
-		}
-		if (v == u) {
-			u_done = true;
+		Cudd_Ref(sol);
+		tmp = DD_PermuteVariables(ddman, sol, rvars, cvars, num_cvars);
+		Cudd_Ref(trans01);
+		tmp = DD_And(ddman, tmp, trans01);
+		tmp = DD_ThereExists(ddman, tmp, cvars, num_cvars);
+		
+		Cudd_Ref(b1);
+		tmp = DD_And(ddman, b1, tmp);		
+		Cudd_Ref(b2);
+		tmp = DD_And(ddman, DD_Not(ddman, b2), tmp);
+		Cudd_Ref(no);
+		tmp = DD_Or(ddman, no, tmp);
+		
+		if (tmp == sol) {
+			done = true;
 		}
-		Cudd_RecursiveDeref(ddman, u);
-		u = v;
+		Cudd_RecursiveDeref(ddman, sol);
+		sol = tmp;
 	}
+	sol = DD_PermuteVariables(ddman, sol, cvars, rvars, num_cvars);
 	
+	// actual answer is states NOT reachable
+	Cudd_Ref(reach);
+	sol = DD_And(ddman, reach, DD_Not(ddman, sol));
+
 	// stop clock
 	time_taken = (double)(util_cpu_time() - start1)/1000;
 	time_for_setup = 0;
@@ -120,7 +113,7 @@ jlong __jlongpointer psi	// psi(b2)
 	// print iterations/timing info
 	PM_PrintToMainLog(env, "\nProb1: %d iterations in %.2f seconds (average %.6f, setup %.2f)\n", iters, time_taken, time_for_iters/iters, time_for_setup);
 
-	return ptr_to_jlong(u);
+	return ptr_to_jlong(sol);
 }
 
 //------------------------------------------------------------------------------

prism/src/mtbdd/PM_Prob1A.cc

@@ -58,7 +58,7 @@ jlong __jlongpointer psi	// psi(b2)
 )
 {
 	DdNode *trans01 = jlong_to_DdNode(t01);		// 0-1 trans matrix
-	DdNode *all = jlong_to_DdNode(r);		// reachable states
+	DdNode *reach = jlong_to_DdNode(r);		// reachable states
 	DdNode *mask = jlong_to_DdNode(ndm);		// nondeterminism mask
 	DdNode *no = jlong_to_DdNode(n);		// no
 	DdNode *b2 = jlong_to_DdNode(psi);		// b2
@@ -66,7 +66,7 @@ jlong __jlongpointer psi	// psi(b2)
 	DdNode **cvars = jlong_to_DdNode_array(cv);	// col vars
 	DdNode **ndvars = jlong_to_DdNode_array(ndv);	// nondet vars
 	
-	DdNode  *reach,*sol, *tmp, *notno;
+	DdNode  *sol, *tmp, *notno;
 	bool done;
 	int iters;
 	
@@ -78,9 +78,9 @@ jlong __jlongpointer psi	// psi(b2)
 	start = util_cpu_time();
 	
 	// negate set "no" ("there exists an adversary with prob=0") to get set "for all adversaries prob>0"
-	Cudd_Ref(all);
+	Cudd_Ref(reach);
 	Cudd_Ref(no);
-	notno = DD_And(ddman, all, DD_Not(ddman, no));
+	notno = DD_And(ddman, reach, DD_Not(ddman, no));
 	
 	// greatest fixed point loop
 	Cudd_Ref(b2);

prism/src/mtbdd/PM_Prob1E.cc

@@ -44,6 +44,7 @@ JNIEXPORT jlong __jlongpointer JNICALL Java_mtbdd_PrismMTBDD_PM_1Prob1E
 JNIEnv *env,
 jclass cls,
 jlong __jlongpointer t01, 	// 0-1 trans matrix
+jlong __jlongpointer r,	// reachable states
 jlong __jlongpointer rv,	// row vars
 jint num_rvars,
 jlong __jlongpointer cv,	// col vars
@@ -51,15 +52,18 @@ jint num_cvars,
 jlong __jlongpointer ndv,	// nondet vars
 jint num_ndvars,
 jlong __jlongpointer phi,	// phi(b1)
-jlong __jlongpointer psi	// psi(b2)
+jlong __jlongpointer psi,	// psi(b2)
+jlong __jlongpointer _no	// no
 )
 {
 	DdNode *trans01 = jlong_to_DdNode(t01);		// 0-1 trans matrix
+	DdNode *reach = jlong_to_DdNode(r);		// reachable states
 	DdNode **rvars = jlong_to_DdNode_array(rv);	// row vars
 	DdNode **cvars = jlong_to_DdNode_array(cv);	// col vars
 	DdNode **ndvars = jlong_to_DdNode_array(ndv);	// nondet vars
 	DdNode *b1 = jlong_to_DdNode(phi);		// b1
 	DdNode *b2 = jlong_to_DdNode(psi);		// b2
+	DdNode *no = jlong_to_DdNode(_no);			// no
 	
 	DdNode *u, *v, *tmp, *tmp2;
 	bool u_done, v_done;
@@ -72,8 +76,13 @@ jlong __jlongpointer psi	// psi(b2)
 	// start clock
 	start1 = util_cpu_time();
 	
-	// greatest fixed point - start from true
-	u = DD_Constant(ddman, 1);
+	// greatest fixed point so should start from true,
+	// but for efficiency we use the passed in "no", which will
+	// be the result of the first (outer) iteration
+	Cudd_Ref(reach);
+	Cudd_Ref(no);
+	u = DD_And(ddman, reach, DD_Not(ddman, no));
+	//u = DD_Constant(ddman, 1);
 	u_done = false;
 	iters = 0;
 	

prism/src/mtbdd/PrismMTBDD.java

@@ -188,10 +188,10 @@ public class PrismMTBDD
 	}
 	
 	// pctl until probability 1 precomputation (probabilistic/dtmc)
-	private static native long PM_Prob1(long trans01, long rv, int nrv, long cv, int ncv, long b1, long b2);
-	public static JDDNode Prob1(JDDNode trans01, JDDVars rows, JDDVars cols, JDDNode b1, JDDNode b2)// throws PrismException
+	private static native long PM_Prob1(long trans01, long reach, long rv, int nrv, long cv, int ncv, long b1, long b2, long no);
+	public static JDDNode Prob1(JDDNode trans01, JDDNode reach,JDDVars rows, JDDVars cols, JDDNode b1, JDDNode b2, JDDNode no)// throws PrismException
 	{
-		long ptr = PM_Prob1(trans01.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), b1.ptr(), b2.ptr());
+		long ptr = PM_Prob1(trans01.ptr(), reach.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), b1.ptr(), b2.ptr(), no.ptr());
 		//if (ptr == 0) throw new PrismException(getErrorMessage());
 		return new JDDNode(ptr);
 	}
@@ -206,10 +206,10 @@ public class PrismMTBDD
 	}
 	
 	// pctl until probability 1 precomputation - there exists (nondeterministic/mdp)
-	private static native long PM_Prob1E(long trans01, long rv, int nrv, long cv, int ncv, long ndv, int nndv, long b1, long b2);
-	public static JDDNode Prob1E(JDDNode trans01, JDDVars rows, JDDVars cols, JDDVars nd, JDDNode b1, JDDNode b2)// throws PrismException
+	private static native long PM_Prob1E(long trans01, long reach, long rv, int nrv, long cv, int ncv, long ndv, int nndv, long b1, long b2, long no);
+	public static JDDNode Prob1E(JDDNode trans01, JDDNode reach, JDDVars rows, JDDVars cols, JDDVars nd, JDDNode b1, JDDNode b2, JDDNode no)// throws PrismException
 	{
-		long ptr = PM_Prob1E(trans01.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nd.array(), nd.n(), b1.ptr(), b2.ptr());
+		long ptr = PM_Prob1E(trans01.ptr(), reach.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nd.array(), nd.n(), b1.ptr(), b2.ptr(), no.ptr());
 		//if (ptr == 0) throw new PrismException(getErrorMessage());
 		return new JDDNode(ptr);
 	}

prism/src/prism/NondetModelChecker.java

@@ -154,13 +154,11 @@ public class NondetModelChecker extends StateModelChecker
 		// Check for trivial (i.e. stupid) cases
 		if (pb != null) {
 			if ((p == 0 && relOp.equals(">=")) || (p == 1 && relOp.equals("<="))) {
-				mainLog.print("\nWarning: checking for probability " + relOp + " " + p
-						+ " - formula trivially satisfies all states\n");
+				mainLog.print("\nWarning: checking for probability " + relOp + " " + p + " - formula trivially satisfies all states\n");
 				JDD.Ref(reach);
 				return new StateProbsMTBDD(reach, model);
 			} else if ((p == 0 && relOp.equals("<")) || (p == 1 && relOp.equals(">"))) {
-				mainLog.print("\nWarning: checking for probability " + relOp + " " + p
-						+ " - formula trivially satisfies no states\n");
+				mainLog.print("\nWarning: checking for probability " + relOp + " " + p + " - formula trivially satisfies no states\n");
 				return new StateProbsMTBDD(JDD.Constant(0), model);
 			}
 		}
@@ -248,13 +246,11 @@ public class NondetModelChecker extends StateModelChecker
 		// check for trivial (i.e. stupid) cases
 		if (rb != null) {
 			if (r == 0 && relOp.equals(">=")) {
-				mainLog.print("\nWarning: checking for reward " + relOp + " " + r
-						+ " - formula trivially satisfies all states\n");
+				mainLog.print("\nWarning: checking for reward " + relOp + " " + r + " - formula trivially satisfies all states\n");
 				JDD.Ref(reach);
 				return new StateProbsMTBDD(reach, model);
 			} else if (r == 0 && relOp.equals("<")) {
-				mainLog.print("\nWarning: checking for reward " + relOp + " " + r
-						+ " - formula trivially satisfies no states\n");
+				mainLog.print("\nWarning: checking for reward " + relOp + " " + r + " - formula trivially satisfies no states\n");
 				return new StateProbsMTBDD(JDD.Constant(0), model);
 			}
 		}
@@ -312,7 +308,7 @@ public class NondetModelChecker extends StateModelChecker
 	protected StateProbs checkProbPathFormula(Expression expr, boolean qual, boolean min) throws PrismException
 	{
 		// Test whether this is a simple path formula (i.e. PCTL)
-		// and then pass control to appropriate method. 
+		// and then pass control to appropriate method.
 		if (expr.isSimplePathFormula()) {
 			return checkProbPathFormulaSimple(expr, qual, min);
 		} else {
@@ -336,7 +332,7 @@ public class NondetModelChecker extends StateModelChecker
 			}
 			// Negation
 			else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) {
-				// Flip min/max, then subtract from 1 
+				// Flip min/max, then subtract from 1
 				probs = checkProbPathFormulaSimple(exprUnary.getOperand(), qual, !min);
 				probs.subtractFromOne();
 			}
@@ -383,41 +379,42 @@ public class NondetModelChecker extends StateModelChecker
 		JDDVars draDDRowVars;
 		int i;
 		long l;
-		
+
 		// Can't do LTL with time-bounded variants of the temporal operators
 		try {
 			expr.accept(new ASTTraverse()
 			{
 				public void visitPre(ExpressionTemporal e) throws PrismLangException
 				{
-					if (e.getLowerBound() != null) throw new PrismLangException(e.getOperatorSymbol());
-					if (e.getUpperBound() != null) throw new PrismLangException(e.getOperatorSymbol());
+					if (e.getLowerBound() != null)
+						throw new PrismLangException(e.getOperatorSymbol());
+					if (e.getUpperBound() != null)
+						throw new PrismLangException(e.getOperatorSymbol());
 				}
 			});
 		} catch (PrismLangException e) {
-			String s = "Temporal operators (like "+e.getMessage()+")";
+			String s = "Temporal operators (like " + e.getMessage() + ")";
 			s += " cannot have time bounds for LTL properties";
 			throw new PrismException(s);
 		}
-		
-		// For LTL model checking routines 
+
+		// For LTL model checking routines
 		mcLtl = new LTLModelChecker(prism, this);
-		
+
 		// Model check maximal state formulas
 		labelDDs = new Vector<JDDNode>();
 		ltl = mcLtl.checkMaximalStateFormulas(model, expr.deepCopy(), labelDDs);
-		
+
 		// Convert LTL formula to deterministic Rabin automaton (DRA)
-		mainLog.println("\nBuilding deterministic Rabin automaton (for "+(min&&!fairness?"!":"")+ltl+")...");
+		mainLog.println("\nBuilding deterministic Rabin automaton (for " + (min && !fairness ? "!" : "") + ltl + ")...");
 		l = System.currentTimeMillis();
 		if (min && !fairness) {
 			dra = LTL2Rabin.ltl2rabin(ltl.convertForJltl2ba().negate());
-		}
-		else {
+		} else {
 			dra = LTL2Rabin.ltl2rabin(ltl.convertForJltl2ba());
 		}
 		mainLog.println("\nDRA has " + dra.size() + " states.");
-		//dra.print(System.out);
+		// dra.print(System.out);
 		l = System.currentTimeMillis() - l;
 		mainLog.println("\nTime for Rabin translation: " + l / 1000.0 + " seconds.");
 
@@ -426,21 +423,21 @@ public class NondetModelChecker extends StateModelChecker
 		modelProduct = mcLtl.constructProductModel(dra, model, labelDDs);
 		mainLog.println();
 		modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo());
-		//prism.exportStatesToFile(modelProduct, Prism.EXPORT_PLAIN, null);
-		//prism.exportTransToFile(modelProduct, true, Prism.EXPORT_PLAIN, null);
-		
+		// prism.exportStatesToFile(modelProduct, Prism.EXPORT_PLAIN, null);
+		// prism.exportTransToFile(modelProduct, true, Prism.EXPORT_PLAIN, null);
+
 		mainLog.println("\nFinding accepting end components...");
 		JDDNode acc = mcLtl.findAcceptingStates(dra, modelProduct, fairness);
-		
+
 		mainLog.println("\nComputing reachability probabilities...");
 		mcProduct = new NondetModelChecker(prism, modelProduct, null);
 		probsProduct = mcProduct.checkProbUntil(modelProduct.getReach(), acc, qual, min && fairness);
-		
+
 		// subtract from 1 if we're model checking a negated formula for regular Pmin
 		if (min && !fairness) {
 			probsProduct.subtractFromOne();
 		}
-		
+
 		// Convert probability vector to original model
 		// First, filter over DRA start states
 		startMask = mcLtl.buildStartMask(dra, labelDDs);
@@ -451,7 +448,7 @@ public class NondetModelChecker extends StateModelChecker
 		draDDRowVars.addVars(modelProduct.getAllDDRowVars());
 		draDDRowVars.removeVars(allDDRowVars);
 		probs = probsProduct.sumOverDDVars(draDDRowVars, model);
-		
+
 		// Deref, clean up
 		probsProduct.clear();
 		modelProduct.clear();
@@ -459,7 +456,7 @@ public class NondetModelChecker extends StateModelChecker
 			JDD.Deref(labelDDs.get(i));
 		}
 		JDD.Deref(acc);
-		
+
 		return probs;
 	}
 
@@ -540,8 +537,8 @@ public class NondetModelChecker extends StateModelChecker
 	}
 
 	// until (unbounded)
-	
-	// this method is split into two steps so that the LTL model checker can use the second part directly 
+
+	// this method is split into two steps so that the LTL model checker can use the second part directly
 
 	protected StateProbs checkProbUntil(ExpressionTemporal expr, boolean qual, boolean min) throws PrismException
 	{
@@ -562,25 +559,24 @@ public class NondetModelChecker extends StateModelChecker
 		// allDDRowVars.n()));
 		// mainLog.print(" states, b2 = " + JDD.GetNumMintermsString(b2,
 		// allDDRowVars.n()) + " states\n");
-		
+
 		try {
 			probs = checkProbUntil(b1, b2, qual, min);
-		}
-		catch (PrismException e) {
+		} catch (PrismException e) {
 			JDD.Deref(b1);
 			JDD.Deref(b2);
 			throw e;
 		}
-		
+
 		// derefs
 		JDD.Deref(b1);
 		JDD.Deref(b2);
 
 		return probs;
 	}
-	
+
 	// until (unbounded): b1/b2 are bdds for until operands
-	
+
 	protected StateProbs checkProbUntil(JDDNode b1, JDDNode b2, boolean qual, boolean min) throws PrismException
 	{
 		JDDNode splus, newb1, newb2;
@@ -615,19 +611,17 @@ public class NondetModelChecker extends StateModelChecker
 			mainLog.print("\nTime for fairness conversion: " + l / 1000.0 + " seconds.\n");
 			// mainLog.print("\nb1 = " + JDD.GetNumMintermsString(newb1, allDDRowVars.n()));
 			// mainLog.print(" states, b2 = " + JDD.GetNumMintermsString(newb2, allDDRowVars.n()) + " states\n");
-		}
-		else {
+		} else {
 			JDD.Ref(b1);
-			newb1 = b1; 
+			newb1 = b1;
 			JDD.Ref(b2);
-			newb2 = b2; 
+			newb2 = b2;
 		}
 
 		// if requested (i.e. when prob bound is 0 or 1 and precomputation algorithms are enabled),
 		// compute probabilities qualitatively
 		if (qual) {
-			mainLog.print("\nWarning: probability bound in formula is"
-					+ " 0/1 so exact probabilities may not be computed\n");
+			mainLog.print("\nWarning: probability bound in formula is" + " 0/1 so exact probabilities may not be computed\n");
 			// for fairness, we compute max here
 			probs = computeUntilProbsQual(trans01, newb1, newb2, min && !fairness);
 		}
@@ -636,8 +630,7 @@ public class NondetModelChecker extends StateModelChecker
 			// for fairness, we compute max here
 			try {
 				probs = computeUntilProbs(trans, trans01, newb1, newb2, min && !fairness);
-			}
-			catch (PrismException e) {
+			} catch (PrismException e) {
 				JDD.Deref(newb1);
 				JDD.Deref(newb2);
 				throw e;
@@ -650,18 +643,18 @@ public class NondetModelChecker extends StateModelChecker
 		if (min && fairness) {
 			probs.subtractFromOne();
 		}
-		
+
 		// Derefs
 		JDD.Deref(newb1);
 		JDD.Deref(newb2);
-		
+
 		return probs;
 	}
 
 	// inst reward
 
-	protected StateProbs checkRewardInst(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards,
-			boolean min) throws PrismException
+	protected StateProbs checkRewardInst(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min)
+			throws PrismException
 	{
 		int time; // time bound
 		StateProbs rewards = null;
@@ -680,8 +673,8 @@ public class NondetModelChecker extends StateModelChecker
 
 	// reach reward
 
-	protected StateProbs checkRewardReach(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards,
-			boolean min) throws PrismException
+	protected StateProbs checkRewardReach(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min)
+			throws PrismException
 	{
 		JDDNode b;
 		StateProbs rewards = null;
@@ -744,8 +737,8 @@ public class NondetModelChecker extends StateModelChecker
 
 	// compute probabilities for bounded until
 
-	protected StateProbs computeBoundedUntilProbs(JDDNode tr, JDDNode tr01, JDDNode b1, JDDNode b2, int time,
-			boolean min) throws PrismException
+	protected StateProbs computeBoundedUntilProbs(JDDNode tr, JDDNode tr01, JDDNode b1, JDDNode b2, int time, boolean min)
+			throws PrismException
 	{
 		JDDNode yes, no, maybe;
 		JDDNode probsMTBDD;
@@ -775,8 +768,7 @@ public class NondetModelChecker extends StateModelChecker
 			} else if (precomp) {
 				if (min) {
 					// "min prob = 0" equates to "there exists a prob 0"
-					no = PrismMTBDD.Prob0E(tr01, reach, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars, b1,
-							yes);
+					no = PrismMTBDD.Prob0E(tr01, reach, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars, b1, yes);
 				} else {
 					// "max prob = 0" equates to "all probs 0"
 					no = PrismMTBDD.Prob0A(tr01, reach, allDDRowVars, allDDColVars, allDDNondetVars, b1, yes);
@@ -810,18 +802,16 @@ public class NondetModelChecker extends StateModelChecker
 			try {
 				switch (engine) {
 				case Prism.MTBDD:
-					probsMTBDD = PrismMTBDD.NondetBoundedUntil(tr, odd, nondetMask, allDDRowVars, allDDColVars,
-							allDDNondetVars, yes, maybe, time, min);
+					probsMTBDD = PrismMTBDD.NondetBoundedUntil(tr, odd, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars, yes,
+							maybe, time, min);
 					probs = new StateProbsMTBDD(probsMTBDD, model);
 					break;
 				case Prism.SPARSE:
-					probsDV = PrismSparse.NondetBoundedUntil(tr, odd, allDDRowVars, allDDColVars, allDDNondetVars, yes,
-							maybe, time, min);
+					probsDV = PrismSparse.NondetBoundedUntil(tr, odd, allDDRowVars, allDDColVars, allDDNondetVars, yes, maybe, time, min);
 					probs = new StateProbsDV(probsDV, model);
 					break;
 				case Prism.HYBRID:
-					probsDV = PrismHybrid.NondetBoundedUntil(tr, odd, allDDRowVars, allDDColVars, allDDNondetVars, yes,
-							maybe, time, min);
+					probsDV = PrismHybrid.NondetBoundedUntil(tr, odd, allDDRowVars, allDDColVars, allDDNondetVars, yes, maybe, time, min);
 					probs = new StateProbsDV(probsDV, model);
 					break;
 				default:
@@ -872,39 +862,17 @@ public class NondetModelChecker extends StateModelChecker
 		} else {
 			// min
 			if (min) {
-				// no: "min prob = 0" equates to "there exists an adversary prob
-				// equals 0"
+				// no: "min prob = 0" equates to "there exists an adversary prob equals 0"
 				no = PrismMTBDD.Prob0E(tr01, reach, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars, b1, b2);
-				// yes: "min prob = 1" equates to "for all adversaries prob
-				// equals 1"
-				if (no.equals(JDD.ZERO)) {
-					// if there are no "no" states, all states must have min
-					// prob 1
-					JDD.Ref(reach);
-					yes = reach;
-				} else {
-					// use precomp alg
-					// note that prob1a (unlike prob1e) requires no/b2, not
-					// b1/b2
-					yes = PrismMTBDD.Prob1A(tr01, reach, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars, no,
-							b2);
-				}
+				// yes: "min prob = 1" equates to "for all adversaries prob equals 1"
+				yes = PrismMTBDD.Prob1A(tr01, reach, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars, no, b2);
 			}
 			// max
 			else {
-				// yes: "max prob = 1" equates to "there exists an adversary
-				// prob equals 1"
-				yes = PrismMTBDD.Prob1E(tr01, allDDRowVars, allDDColVars, allDDNondetVars, b1, b2);
-				// no: "max prob = 0" equates to "for all adversaries prob
-				// equals 0"
-				if (yes.equals(reach)) {
-					// trivial case - because yes+no+maybe=all, so yes=all =>
-					// no,maybe=empty
-					no = JDD.Constant(0);
-				} else {
-					// use precomp alg
-					no = PrismMTBDD.Prob0A(tr01, reach, allDDRowVars, allDDColVars, allDDNondetVars, b1, yes);
-				}
+				// no: "max prob = 0" equates to "for all adversaries prob equals 0"
+				no = PrismMTBDD.Prob0A(tr01, reach, allDDRowVars, allDDColVars, allDDNondetVars, b1, b2);
+				// yes: "max prob = 1" equates to "there exists an adversary prob equals 1"
+				yes = PrismMTBDD.Prob1E(tr01, reach, allDDRowVars, allDDColVars, allDDNondetVars, b1, b2, no);
 			}
 			// maybe
 			JDD.Ref(reach);
@@ -951,8 +919,7 @@ public class NondetModelChecker extends StateModelChecker
 	// note: this function doesn't need to know anything about fairness
 	// it is just told whether to compute min or max probabilities
 
-	protected StateProbs computeUntilProbs(JDDNode tr, JDDNode tr01, JDDNode b1, JDDNode b2, boolean min)
-			throws PrismException
+	protected StateProbs computeUntilProbs(JDDNode tr, JDDNode tr01, JDDNode b1, JDDNode b2, boolean min) throws PrismException
 	{
 		JDDNode yes, no, maybe;
 		JDDNode probsMTBDD;
@@ -977,40 +944,17 @@ public class NondetModelChecker extends StateModelChecker
 			if (precomp) {
 				// min
 				if (min) {
-					// no: "min prob = 0" equates to "there exists an adversary
-					// prob equals 0"
-					no = PrismMTBDD
-							.Prob0E(tr01, reach, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars, b1, b2);
-					// yes: "min prob = 1" equates to "for all adversaries prob
-					// equals 1"
-					if (no.equals(JDD.ZERO)) {
-						// if there are no "no" states, all states must have min
-						// prob 1
-						JDD.Ref(reach);
-						yes = reach;
-					} else {
-						// use precomp alg
-						// note that prob1a (unlike prob1e) requires no/b2, not
-						// b1/b2
-						yes = PrismMTBDD.Prob1A(tr01, reach, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars,
-								no, b2);
-					}
+					// no: "min prob = 0" equates to "there exists an adversary prob equals 0"
+					no = PrismMTBDD.Prob0E(tr01, reach, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars, b1, b2);
+					// yes: "min prob = 1" equates to "for all adversaries prob equals 1"
+					yes = PrismMTBDD.Prob1A(tr01, reach, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars, no, b2);
 				}
 				// max
 				else {
-					// yes: "max prob = 1" equates to "there exists an adversary
-					// prob equals 1"
-					yes = PrismMTBDD.Prob1E(tr01, allDDRowVars, allDDColVars, allDDNondetVars, b1, b2);
-					// no: "max prob = 0" equates to "for all adversaries prob
-					// equals 0"
-					if (yes.equals(reach)) {
-						// trivial case - because yes+no+maybe=all, so yes=all
-						// => no,maybe=empty
-						no = JDD.Constant(0);
-					} else {
-						// use precomp alg
-						no = PrismMTBDD.Prob0A(tr01, reach, allDDRowVars, allDDColVars, allDDNondetVars, b1, yes);
-					}
+					// no: "max prob = 0" equates to "for all adversaries prob equals 0"
+					no = PrismMTBDD.Prob0A(tr01, reach, allDDRowVars, allDDColVars, allDDNondetVars, b1, b2);
+					// yes: "max prob = 1" equates to "there exists an adversary prob equals 1"
+					yes = PrismMTBDD.Prob1E(tr01, reach, allDDRowVars, allDDColVars, allDDNondetVars, b1, b2, no);
 				}
 			}
 			// if precomputation not enabled
@@ -1049,18 +993,15 @@ public class NondetModelChecker extends StateModelChecker
 			try {
 				switch (engine) {
 				case Prism.MTBDD:
-					probsMTBDD = PrismMTBDD.NondetUntil(tr, odd, nondetMask, allDDRowVars, allDDColVars,
-							allDDNondetVars, yes, maybe, min);
+					probsMTBDD = PrismMTBDD.NondetUntil(tr, odd, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars, yes, maybe, min);
 					probs = new StateProbsMTBDD(probsMTBDD, model);
 					break;
 				case Prism.SPARSE:
-					probsDV = PrismSparse.NondetUntil(tr, odd, allDDRowVars, allDDColVars, allDDNondetVars, yes, maybe,
-							min);
+					probsDV = PrismSparse.NondetUntil(tr, odd, allDDRowVars, allDDColVars, allDDNondetVars, yes, maybe, min);
 					probs = new StateProbsDV(probsDV, model);
 					break;
 				case Prism.HYBRID:
-					probsDV = PrismHybrid.NondetUntil(tr, odd, allDDRowVars, allDDColVars, allDDNondetVars, yes, maybe,
-							min);
+					probsDV = PrismHybrid.NondetUntil(tr, odd, allDDRowVars, allDDColVars, allDDNondetVars, yes, maybe, min);
 					probs = new StateProbsDV(probsDV, model);
 					break;
 				default:
@@ -1101,13 +1042,12 @@ public class NondetModelChecker extends StateModelChecker
 			try {
 				switch (engine) {
 				case Prism.MTBDD:
-					rewardsMTBDD = PrismMTBDD.NondetInstReward(tr, sr, odd, nondetMask, allDDRowVars, allDDColVars,
-							allDDNondetVars, time, min, start);
+					rewardsMTBDD = PrismMTBDD.NondetInstReward(tr, sr, odd, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars, time,
+							min, start);
 					rewards = new StateProbsMTBDD(rewardsMTBDD, model);
 					break;
 				case Prism.SPARSE:
-					rewardsDV = PrismSparse.NondetInstReward(tr, sr, odd, allDDRowVars, allDDColVars, allDDNondetVars,
-							time, min, start);
+					rewardsDV = PrismSparse.NondetInstReward(tr, sr, odd, allDDRowVars, allDDColVars, allDDNondetVars, time, min, start);
 					rewards = new StateProbsDV(rewardsDV, model);
 					break;
 				default:
@@ -1141,20 +1081,19 @@ public class NondetModelChecker extends StateModelChecker
 			maybe = JDD.Constant(0);
 		} else {
 			if (!min) {
-				// compute states for which some adversaries don't reach goal
-				// with probability 1
+				// compute states for which some adversaries don't reach goal with probability 1
 				// note that prob1a (unlike prob1e) requires no/b2, not b1/b2
 				// hence we have to call prob0e first
-				no = PrismMTBDD
-						.Prob0E(tr01, reach, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars, JDD.ONE, b);
+				no = PrismMTBDD.Prob0E(tr01, reach, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars, reach, b);
 				prob1 = PrismMTBDD.Prob1A(tr01, reach, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars, no, b);
 				JDD.Deref(no);
 				JDD.Ref(reach);
 				inf = JDD.And(reach, JDD.Not(prob1));
 			} else {
-				// compute states for which all adversaries don't reach goal
-				// with probability 1
-				prob1 = PrismMTBDD.Prob1E(tr01, allDDRowVars, allDDColVars, allDDNondetVars, reach, b);
+				// compute states for which all adversaries don't reach goal with probability 1
+				no = PrismMTBDD.Prob0A(tr01, reach, allDDRowVars, allDDColVars, allDDNondetVars, reach, b);
+				prob1 = PrismMTBDD.Prob1E(tr01, reach, allDDRowVars, allDDColVars, allDDNondetVars, reach, b, no);
+				JDD.Deref(no);
 				JDD.Ref(reach);
 				inf = JDD.And(reach, JDD.Not(prob1));
 			}
@@ -1186,13 +1125,13 @@ public class NondetModelChecker extends StateModelChecker
 			try {
 				switch (engine) {
 				case Prism.MTBDD:
-					rewardsMTBDD = PrismMTBDD.NondetReachReward(tr, sr, trr, odd, nondetMask, allDDRowVars,
-							allDDColVars, allDDNondetVars, b, inf, maybe, min);
+					rewardsMTBDD = PrismMTBDD.NondetReachReward(tr, sr, trr, odd, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars,
+							b, inf, maybe, min);
 					rewards = new StateProbsMTBDD(rewardsMTBDD, model);
 					break;
 				case Prism.SPARSE:
-					rewardsDV = PrismSparse.NondetReachReward(tr, sr, trr, odd, allDDRowVars, allDDColVars,
-							allDDNondetVars, b, inf, maybe, min);
+					rewardsDV = PrismSparse.NondetReachReward(tr, sr, trr, odd, allDDRowVars, allDDColVars, allDDNondetVars, b, inf, maybe,
+							min);
 					rewards = new StateProbsDV(rewardsDV, model);
 					break;
 				case Prism.HYBRID:

prism/src/prism/ProbModelChecker.java

@@ -1272,13 +1272,9 @@ public class ProbModelChecker extends NonProbModelChecker
 			no = JDD.And(reach, JDD.Not(b2));
 			maybe = JDD.Constant(0);
 		} else {
-			// yes
-			yes = PrismMTBDD.Prob1(tr01, allDDRowVars, allDDColVars, b1, b2);
-			if (yes.equals(reach)) {
-				no = JDD.Constant(0);
-			} else {
-				no = PrismMTBDD.Prob0(tr01, reach, allDDRowVars, allDDColVars, b1, yes);
-			}
+			// no/yes
+			no = PrismMTBDD.Prob0(tr01, reach, allDDRowVars, allDDColVars, b1, b2);
+			yes = PrismMTBDD.Prob1(tr01, reach, allDDRowVars, allDDColVars, b1, b2, no);
 			// maybe
 			JDD.Ref(reach);
 			JDD.Ref(yes);
@@ -1341,19 +1337,13 @@ public class ProbModelChecker extends NonProbModelChecker
 			no = JDD.And(reach, JDD.Not(b2));
 			maybe = JDD.Constant(0);
 		} else {
-			// yes
+			// no/yes
 			if (precomp) {
-				yes = PrismMTBDD.Prob1(tr01, allDDRowVars, allDDColVars, b1, b2);
+				no = PrismMTBDD.Prob0(tr01, reach, allDDRowVars, allDDColVars, b1, b2);
+				yes = PrismMTBDD.Prob1(tr01, reach, allDDRowVars, allDDColVars, b1, b2, no);
 			} else {
 				JDD.Ref(b2);
 				yes = b2;
-			}
-			// no
-			if (yes.equals(reach)) {
-				no = JDD.Constant(0);
-			} else if (precomp) {
-				no = PrismMTBDD.Prob0(tr01, reach, allDDRowVars, allDDColVars, b1, yes);
-			} else {
 				JDD.Ref(reach);
 				JDD.Ref(b1);
 				JDD.Ref(b2);
@@ -1518,7 +1508,9 @@ public class ProbModelChecker extends NonProbModelChecker
 			inf = JDD.Constant(0);
 			maybe = JDD.Constant(0);
 		} else {
-			JDDNode prob1 = PrismMTBDD.Prob1(tr01, allDDRowVars, allDDColVars, reach, b);
+			JDDNode no = PrismMTBDD.Prob0(tr01, reach, allDDRowVars, allDDColVars, reach, b);
+			JDDNode prob1 = PrismMTBDD.Prob1(tr01, reach, allDDRowVars, allDDColVars, reach, b, no);
+			JDD.Deref(no);
 			JDD.Ref(reach);
 			inf = JDD.And(reach, JDD.Not(prob1));
 			JDD.Ref(reach);