From e9bcc66bd1cd113194a35cbf568e0393f366f257 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 8 Dec 2008 11:38:19 +0000 Subject: [PATCH] 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 | 8 +- prism/src/mtbdd/PM_Prob0.cc | 40 ++--- prism/src/mtbdd/PM_Prob0A.cc | 22 +-- prism/src/mtbdd/PM_Prob0E.cc | 22 +-- prism/src/mtbdd/PM_Prob1.cc | 83 ++++----- prism/src/mtbdd/PM_Prob1A.cc | 8 +- prism/src/mtbdd/PM_Prob1E.cc | 15 +- prism/src/mtbdd/PrismMTBDD.java | 12 +- prism/src/prism/NondetModelChecker.java | 229 +++++++++--------------- prism/src/prism/ProbModelChecker.java | 26 +-- 10 files changed, 199 insertions(+), 266 deletions(-) diff --git a/prism/include/PrismMTBDD.h b/prism/include/PrismMTBDD.h index 5d5e1791..3af33868 100644 --- a/prism/include/PrismMTBDD.h +++ b/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 diff --git a/prism/src/mtbdd/PM_Prob0.cc b/prism/src/mtbdd/PM_Prob0.cc index 7d77467f..5a0c250a 100644 --- a/prism/src/mtbdd/PM_Prob0.cc +++ b/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; diff --git a/prism/src/mtbdd/PM_Prob0A.cc b/prism/src/mtbdd/PM_Prob0A.cc index 2fd8b830..6ea78874 100644 --- a/prism/src/mtbdd/PM_Prob0A.cc +++ b/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; diff --git a/prism/src/mtbdd/PM_Prob0E.cc b/prism/src/mtbdd/PM_Prob0E.cc index babc4b95..73d6eb64 100644 --- a/prism/src/mtbdd/PM_Prob0E.cc +++ b/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; diff --git a/prism/src/mtbdd/PM_Prob1.cc b/prism/src/mtbdd/PM_Prob1.cc index 86676f30..da6312a3 100644 --- a/prism/src/mtbdd/PM_Prob1.cc +++ b/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); } //------------------------------------------------------------------------------ diff --git a/prism/src/mtbdd/PM_Prob1A.cc b/prism/src/mtbdd/PM_Prob1A.cc index 0e933b3d..16e1fdab 100644 --- a/prism/src/mtbdd/PM_Prob1A.cc +++ b/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); diff --git a/prism/src/mtbdd/PM_Prob1E.cc b/prism/src/mtbdd/PM_Prob1E.cc index 5978af64..1bb8b542 100644 --- a/prism/src/mtbdd/PM_Prob1E.cc +++ b/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; diff --git a/prism/src/mtbdd/PrismMTBDD.java b/prism/src/mtbdd/PrismMTBDD.java index 55e1dfeb..73b0001d 100644 --- a/prism/src/mtbdd/PrismMTBDD.java +++ b/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); } diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 4920ba0d..1a193eed 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/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(); 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: diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 876910ce..1ea7f89a 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/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);