From 8b45a02257e55f165759c2456f0a7a561ee5e15f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 4 Dec 2007 11:16:59 +0000 Subject: [PATCH] Sparse version of MDP instantaneous reward operator (and commented-out code for printing all values - sparse/mtbdd). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@542 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/include/PrismMTBDD.h | 4 +- prism/include/PrismSparse.h | 8 + prism/src/mtbdd/PM_NondetInstReward.cc | 11 +- prism/src/mtbdd/PrismMTBDD.java | 6 +- prism/src/prism/NondetModelChecker.java | 6 +- prism/src/sparse/PS_NondetInstReward.cc | 210 ++++++++++++++++++++++++ prism/src/sparse/PrismSparse.java | 9 + 7 files changed, 247 insertions(+), 7 deletions(-) create mode 100644 prism/src/sparse/PS_NondetInstReward.cc diff --git a/prism/include/PrismMTBDD.h b/prism/include/PrismMTBDD.h index fd38d5ec..c976bdbd 100644 --- a/prism/include/PrismMTBDD.h +++ b/prism/include/PrismMTBDD.h @@ -210,10 +210,10 @@ JNIEXPORT jlong JNICALL Java_mtbdd_PrismMTBDD_PM_1NondetUntil /* * Class: mtbdd_PrismMTBDD * Method: PM_NondetInstReward - * Signature: (JJJJJIJIJIIZ)J + * Signature: (JJJJJIJIJIIZJ)J */ JNIEXPORT jlong JNICALL Java_mtbdd_PrismMTBDD_PM_1NondetInstReward - (JNIEnv *, jclass, jlong, jlong, jlong, jlong, jlong, jint, jlong, jint, jlong, jint, jint, jboolean); + (JNIEnv *, jclass, jlong, jlong, jlong, jlong, jlong, jint, jlong, jint, jlong, jint, jint, jboolean, jlong); /* * Class: mtbdd_PrismMTBDD diff --git a/prism/include/PrismSparse.h b/prism/include/PrismSparse.h index 7bd63493..33de26dd 100644 --- a/prism/include/PrismSparse.h +++ b/prism/include/PrismSparse.h @@ -151,6 +151,14 @@ JNIEXPORT jlong JNICALL Java_sparse_PrismSparse_PS_1NondetBoundedUntil JNIEXPORT jlong JNICALL Java_sparse_PrismSparse_PS_1NondetUntil (JNIEnv *, jclass, jlong, jlong, jlong, jint, jlong, jint, jlong, jint, jlong, jlong, jboolean); +/* + * Class: sparse_PrismSparse + * Method: PS_NondetInstReward + * Signature: (JJJJIJIJIIZJ)J + */ +JNIEXPORT jlong JNICALL Java_sparse_PrismSparse_PS_1NondetInstReward + (JNIEnv *, jclass, jlong, jlong, jlong, jlong, jint, jlong, jint, jlong, jint, jint, jboolean, jlong); + /* * Class: sparse_PrismSparse * Method: PS_NondetReachReward diff --git a/prism/src/mtbdd/PM_NondetInstReward.cc b/prism/src/mtbdd/PM_NondetInstReward.cc index 39ed8c23..a8da6b10 100644 --- a/prism/src/mtbdd/PM_NondetInstReward.cc +++ b/prism/src/mtbdd/PM_NondetInstReward.cc @@ -51,7 +51,8 @@ jint num_cvars, jlong __pointer ndv, // nondet vars jint num_ndvars, jint bound, // time bound -jboolean min // min or max probabilities (true = min, false = max) +jboolean min, // min or max probabilities (true = min, false = max) +jlong __pointer in ) { // cast function parameters @@ -62,6 +63,7 @@ jboolean min // min or max probabilities (true = min, false = max) 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 *init = jlong_to_DdNode(in); // mtbdds DdNode *new_mask, *sol, *tmp; @@ -120,6 +122,13 @@ jboolean min // min or max probabilities (true = min, false = max) Cudd_RecursiveDeref(ddman, sol); sol = tmp; +// Cudd_Ref(sol); +// Cudd_Ref(init); +// tmp = DD_Apply(ddman, APPLY_TIMES, sol, init); +// tmp = DD_SumAbstract(ddman, tmp, rvars, num_rvars); +// PM_PrintToMainLog(env, "%i: %f (%0.f, %0d)\n", iters, Cudd_V(tmp), DD_GetNumMinterms(ddman, sol, num_rvars), DD_GetNumNodes(ddman, sol)); +// Cudd_RecursiveDeref(ddman, tmp); + // PM_PrintToMainLog(env, "%.2f %.2f sec\n", ((double)(util_cpu_time() - start3)/1000), ((double)(util_cpu_time() - start2)/1000)/iters); } diff --git a/prism/src/mtbdd/PrismMTBDD.java b/prism/src/mtbdd/PrismMTBDD.java index 4c3a0d21..9d90b225 100644 --- a/prism/src/mtbdd/PrismMTBDD.java +++ b/prism/src/mtbdd/PrismMTBDD.java @@ -312,10 +312,10 @@ public class PrismMTBDD } // pctl inst reward (nondeterministic/mdp) - private static native long PM_NondetInstReward(long trans, long sr, long odd, long mask, long rv, int nrv, long cv, int ncv, long ndv, int nndv, int time, boolean minmax); - public static JDDNode NondetInstReward(JDDNode trans, JDDNode sr, ODDNode odd, JDDNode nondetMask, JDDVars rows, JDDVars cols, JDDVars nondet, int time, boolean minmax) throws PrismException + private static native long PM_NondetInstReward(long trans, long sr, long odd, long mask, long rv, int nrv, long cv, int ncv, long ndv, int nndv, int time, boolean minmax, long init); + public static JDDNode NondetInstReward(JDDNode trans, JDDNode sr, ODDNode odd, JDDNode nondetMask, JDDVars rows, JDDVars cols, JDDVars nondet, int time, boolean minmax, JDDNode init) throws PrismException { - long ptr = PM_NondetInstReward(trans.ptr(), sr.ptr(), odd.ptr(), nondetMask.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), time, minmax); + long ptr = PM_NondetInstReward(trans.ptr(), sr.ptr(), odd.ptr(), nondetMask.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), time, minmax, init.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 7dc80dde..59f5474f 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -1513,9 +1513,13 @@ public class NondetModelChecker implements ModelChecker try { switch (engine) { case Prism.MTBDD: - rewardsMTBDD = PrismMTBDD.NondetInstReward(tr, sr, odd, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars, time, min); + 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); + rewards = new StateProbsDV(rewardsDV, model); + break; default: throw new PrismException("Engine does not support this numerical method"); } } diff --git a/prism/src/sparse/PS_NondetInstReward.cc b/prism/src/sparse/PS_NondetInstReward.cc new file mode 100644 index 00000000..ec2cceb7 --- /dev/null +++ b/prism/src/sparse/PS_NondetInstReward.cc @@ -0,0 +1,210 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Birmingham) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +// includes +#include "PrismSparse.h" +#include +#include +#include +#include +#include +#include +#include "sparse.h" +#include "PrismSparseGlob.h" +#include "jnipointer.h" + +//------------------------------------------------------------------------------ + +JNIEXPORT jlong __pointer JNICALL Java_sparse_PrismSparse_PS_1NondetInstReward +( +JNIEnv *env, +jclass cls, +jlong __pointer t, // trans matrix +jlong __pointer sr, // state rewards +jlong __pointer od, // odd +jlong __pointer rv, // row vars +jint num_rvars, +jlong __pointer cv, // col vars +jint num_cvars, +jlong __pointer ndv, // nondet vars +jint num_ndvars, +jint bound, // time bound +jboolean min, // min or max probabilities (true = min, false = max) +jlong __pointer in +) +{ + // cast function parameters + DdNode *trans = jlong_to_DdNode(t); // trans matrix + DdNode *state_rewards = jlong_to_DdNode(sr); // state rewards + ODDNode *odd = jlong_to_ODDNode(od); // 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 *init = jlong_to_DdNode(in); + + // mtbdds + DdNode *tmp; + // model stats + int n, nc; + long nnz; + // sparse matrix + NDSparseMatrix *ndsm; + // vectors + double *sr_vec, *soln, *soln2, *tmpsoln; + // timing stuff + long start1, start2, start3, stop; + double time_taken, time_for_setup, time_for_iters; + // misc + int i, j, k, l1, h1, l2, h2, iters; + double d1, d2, kb, kbt; + bool first; + + // start clocks + start1 = start2 = util_cpu_time(); + + // get number of states + n = odd->eoff + odd->toff; + + // build sparse matrix (probs) + PS_PrintToMainLog(env, "\nBuilding sparse matrix (transitions)... "); + ndsm = build_nd_sparse_matrix(ddman, trans, rvars, cvars, num_rvars, ndvars, num_ndvars, odd); + // get number of transitions/choices + nnz = ndsm->nnz; + nc = ndsm->nc; + // print out info + PS_PrintToMainLog(env, "[n=%d, nc=%d, nnz=%d, k=%d] ", n, nc, nnz, ndsm->k); + kb = (nnz*12.0+nc*4.0+n*4.0)/1024.0; + kbt = kb; + PS_PrintToMainLog(env, "[%.1f KB]\n", kb); + + // get vector for state rewards + PS_PrintToMainLog(env, "Creating vector for state rewards... "); + sr_vec = mtbdd_to_double_vector(ddman, state_rewards, rvars, num_rvars, odd); + kb = n*8.0/1024.0; + kbt += kb; + PS_PrintToMainLog(env, "[%.1f KB]\n", kb); + + // create solution/iteration vectors + PS_PrintToMainLog(env, "Allocating iteration vectors... "); + soln = new double[n]; + soln2 = new double[n]; + kb = n*8.0/1024.0; + kbt += 2*kb; + PS_PrintToMainLog(env, "[2 x %.1f KB]\n", kb); + + // print total memory usage + PS_PrintToMainLog(env, "TOTAL: [%.1f KB]\n", kbt); + + // initial solution is the state rewards + for (i = 0; i < n; i++) { + soln[i] = sr_vec[i]; + } + + // get setup time + stop = util_cpu_time(); + time_for_setup = (double)(stop - start2)/1000; + start2 = stop; + + // start iterations + PS_PrintToMainLog(env, "\nStarting iterations...\n"); + + // note that we ignore max_iters as we know how any iterations _should_ be performed + for (iters = 0; iters < bound; iters++) { + +// PS_PrintToMainLog(env, "iter %d\n", iters); +// start3 = util_cpu_time(); + + // store local copies of stuff + double *non_zeros = ndsm->non_zeros; + unsigned char *row_counts = ndsm->row_counts; + int *row_starts = (int *)ndsm->row_counts; + unsigned char *choice_counts = ndsm->choice_counts; + int *choice_starts = (int *)ndsm->choice_counts; + bool use_counts = ndsm->use_counts; + unsigned int *cols = ndsm->cols; + + // do matrix multiplication and min/max + h1 = h2 = 0; + // loop through states + for (i = 0; i < n; i++) { + d1 = 0.0; + first = true; + // get pointers to nondeterministic choices for state i + if (!use_counts) { l1 = row_starts[i]; h1 = row_starts[i+1]; } + else { l1 = h1; h1 += row_counts[i]; } + // loop through those choices + for (j = l1; j < h1; j++) { + // compute the reward value for state i for this iteration + // start with state reward for this state + d2 = 0.0; + // get pointers to transitions + if (!use_counts) { l2 = choice_starts[j]; h2 = choice_starts[j+1]; } + else { l2 = h2; h2 += choice_counts[j]; } + // loop through transitions + for (k = l2; k < h2; k++) { + // add prob * corresponding reward from previous iteration + d2 += non_zeros[k] * soln[cols[k]]; + } + // see if this value is the min/max so far + if (min) { + if (first | d2 < d1) d1 = d2; + } else { + if (first | d2 > d1) d1 = d2; + } + first = false; + } + // set vector element + // (if there were no choices from this state, reward is zero) + soln2[i] = (h1 > l1) ? d1 : 0; + } + + // prepare for next iteration + tmpsoln = soln; + soln = soln2; + soln2 = tmpsoln; + +// PS_PrintToMainLog(env, "%i: %f\n", iters, get_first_from_bdd(ddman, soln, init, rvars, num_rvars, odd)); + +// PS_PrintToMainLog(env, "%.2f %.2f sec\n", ((double)(util_cpu_time() - start3)/1000), ((double)(util_cpu_time() - start2)/1000)/iters); + } + + // stop clocks + stop = util_cpu_time(); + time_for_iters = (double)(stop - start2)/1000; + time_taken = (double)(stop - start1)/1000; + + // print iterations/timing info + PS_PrintToMainLog(env, "\nIterative method: %d iterations in %.2f seconds (average %.6f, setup %.2f)\n", iters, time_taken, time_for_iters/iters, time_for_setup); + + // free memory + free_nd_sparse_matrix(ndsm); + delete sr_vec; + delete soln2; + + return ptr_to_jlong(soln); +} + +//------------------------------------------------------------------------------ diff --git a/prism/src/sparse/PrismSparse.java b/prism/src/sparse/PrismSparse.java index 6a1700e4..dbbe8121 100644 --- a/prism/src/sparse/PrismSparse.java +++ b/prism/src/sparse/PrismSparse.java @@ -245,6 +245,15 @@ public class PrismSparse return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff())); } + // pctl inst reward (nondeterministic/mdp) + private static native long PS_NondetInstReward(long trans, long sr, long odd, long rv, int nrv, long cv, int ncv, long ndv, int nndv, int time, boolean minmax, long init); + public static DoubleVector NondetInstReward(JDDNode trans, JDDNode sr, ODDNode odd, JDDVars rows, JDDVars cols, JDDVars nondet, int time, boolean minmax, JDDNode init) throws PrismException + { + long ptr = PS_NondetInstReward(trans.ptr(), sr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), time, minmax, init.ptr()); + if (ptr == 0) throw new PrismException(getErrorMessage()); + return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff())); + } + // pctl reach reward (nondeterministic/mdp) private static native long PS_NondetReachReward(long trans, long sr, long trr, long odd, long rv, int nrv, long cv, int ncv, long ndv, int nndv, long goal, long inf, long maybe, boolean minmax); public static DoubleVector NondetReachReward(JDDNode trans, JDDNode sr, JDDNode trr, ODDNode odd, JDDVars rows, JDDVars cols, JDDVars nondet, JDDNode goal, JDDNode inf, JDDNode maybe, boolean minmax) throws PrismException