From 56091fb8ac31a802df3191174b4abe18ac6d85f7 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 20 Nov 2009 23:06:25 +0000 Subject: [PATCH] Import initial distributiion option for DTMCs too. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1575 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/hybrid/PH_ProbTransient.cc | 8 +- prism/src/hybrid/PrismHybrid.java | 4 +- prism/src/mtbdd/PM_ProbTransient.cc | 6 +- prism/src/prism/Prism.java | 2 +- prism/src/prism/ProbModelChecker.java | 115 +++++++++++++++++++------- prism/src/sparse/PS_ProbTransient.cc | 8 +- prism/src/sparse/PrismSparse.java | 4 +- 7 files changed, 103 insertions(+), 44 deletions(-) diff --git a/prism/src/hybrid/PH_ProbTransient.cc b/prism/src/hybrid/PH_ProbTransient.cc index 035f7c75..a58d9f30 100644 --- a/prism/src/hybrid/PH_ProbTransient.cc +++ b/prism/src/hybrid/PH_ProbTransient.cc @@ -61,7 +61,7 @@ JNIEnv *env, jclass cls, jlong __jlongpointer tr, // trans matrix jlong __jlongpointer od, // odd -jlong __jlongpointer in, // initial distribution +jlong __jlongpointer in, // initial distribution (note: this will be deleted afterwards) jlong __jlongpointer rv, // row vars jint num_rvars, jlong __jlongpointer cv, // col vars @@ -72,7 +72,7 @@ jint time // time // cast function parameters DdNode *trans = jlong_to_DdNode(tr); // trans matrix ODDNode *odd = jlong_to_ODDNode(od); // odd - DdNode *init = jlong_to_DdNode(in); // initial distribution + double *init = jlong_to_double(in); // initial distribution DdNode **rvars = jlong_to_DdNode_array(rv); // row vars DdNode **cvars = jlong_to_DdNode_array(cv); // col vars @@ -127,7 +127,9 @@ jint time // time // create solution/iteration vectors PH_PrintToMainLog(env, "Allocating iteration vectors... "); - soln = mtbdd_to_double_vector(ddman, init, rvars, num_rvars, odd); + // for soln, we just use init (since we are free to modify/delete this vector) + // we also report the memory usage of this vector here, even though it has already been created + soln = init; soln2 = new double[n]; sum = new double[n]; kb = n*8.0/1024.0; diff --git a/prism/src/hybrid/PrismHybrid.java b/prism/src/hybrid/PrismHybrid.java index b3152b8b..b4edebe8 100644 --- a/prism/src/hybrid/PrismHybrid.java +++ b/prism/src/hybrid/PrismHybrid.java @@ -274,9 +274,9 @@ public class PrismHybrid // transient (probabilistic/dtmc) private static native long PH_ProbTransient(long trans, long odd, long init, long rv, int nrv, long cv, int ncv, int time); - public static DoubleVector ProbTransient(JDDNode trans, ODDNode odd, JDDNode init, JDDVars rows, JDDVars cols, int time) throws PrismException + public static DoubleVector ProbTransient(JDDNode trans, ODDNode odd, DoubleVector init, JDDVars rows, JDDVars cols, int time) throws PrismException { - long ptr = PH_ProbTransient(trans.ptr(), odd.ptr(), init.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), time); + long ptr = PH_ProbTransient(trans.ptr(), odd.ptr(), init.getPtr(), rows.array(), rows.n(), cols.array(), cols.n(), time); if (ptr == 0) throw new PrismException(getErrorMessage()); return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff())); } diff --git a/prism/src/mtbdd/PM_ProbTransient.cc b/prism/src/mtbdd/PM_ProbTransient.cc index 9b58c2f5..9108e06b 100644 --- a/prism/src/mtbdd/PM_ProbTransient.cc +++ b/prism/src/mtbdd/PM_ProbTransient.cc @@ -43,7 +43,7 @@ JNIEnv *env, jclass cls, jlong __jlongpointer tr, // rate matrix jlong __jlongpointer od, // odd -jlong __jlongpointer in, // initial distribution +jlong __jlongpointer in, // initial distribution (note: this will be derefed afterwards) jlong __jlongpointer rv, // row vars jint num_rvars, jlong __jlongpointer cv, // col vars @@ -130,6 +130,10 @@ jint time // time if (done) PM_PrintToMainLog(env, "\nSteady state detected at iteration %d\n", iters); PM_PrintToMainLog(env, "\nIterative method: %d iterations in %.2f seconds (average %.6f, setup %.2f)\n", iters, time_taken, time_for_iters/iters, time_for_setup); + // derefs + // nb: we deref init, even though it is passed in as a param + Cudd_RecursiveDeref(ddman, init); + return ptr_to_jlong(sol); } diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 1f7f65a2..003eeb6f 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -1494,7 +1494,7 @@ public class Prism implements PrismSettingsListener if (model.getModelType() == ModelType.DTMC) { mainLog.println("\nComputing transient probabilities (time = " + (int)time + ")..."); mc = new ProbModelChecker(this, model, null); - probs = ((ProbModelChecker)mc).doTransient((int)time); + probs = ((ProbModelChecker)mc).doTransient((int)time, fileIn); } else if (model.getModelType() == ModelType.CTMC) { mainLog.println("\nComputing transient probabilities (time = " + time + ")..."); diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 7ef0b730..77fd7f95 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -26,6 +26,7 @@ package prism; +import java.io.File; import java.util.Vector; import jdd.*; @@ -1217,39 +1218,76 @@ public class ProbModelChecker extends NonProbModelChecker // do transient computation // ----------------------------------------------------------------------------------- - // transient computation (from initial states) - + /** + * Compute transient probability distribution (forwards). + * Start from initial state (or uniform distribution over multiple initial states). + */ public StateProbs doTransient(int time) throws PrismException { - // mtbdd stuff - JDDNode start, init; - // other stuff - StateProbs probs = null; - - // get initial states of model - start = model.getStart(); - - // and hence compute initial probability distribution (equiprobable over - // all start states) - JDD.Ref(start); - init = JDD.Apply(JDD.DIVIDE, start, JDD.Constant(JDD.GetNumMinterms(start, allDDRowVars.n()))); + return doTransient(time, (StateProbs) null); + } + + /** + * Compute transient probability distribution (forwards). + * Optionally, use the passed in file initDistFile to give the initial probability distribution (time 0). + * If null, start from initial state (or uniform distribution over multiple initial states). + */ + public StateProbs doTransient(int time, File initDistFile) throws PrismException + { + StateProbs initDist = null; - // compute transient probabilities - try { - // special case: time = 0 - if (time == 0) { - JDD.Ref(init); - probs = new StateProbsMTBDD(init, model); + if (initDistFile != null) { + mainLog.println("\nImporting initial probability distribution from file \"" + initDistFile + "\"..."); + // Build an empty vector of the appropriate type + if (engine == Prism.MTBDD) { + initDist = new StateProbsMTBDD(JDD.Constant(0), model); } else { - probs = computeTransientProbs(trans, init, time); + initDist = new StateProbsDV(new DoubleVector((int) model.getNumStates()), model); } - } catch (PrismException e) { - JDD.Deref(init); - throw e; + // Populate vector from file + initDist.readFromFile(initDistFile); } + + return doTransient(time, initDist); + } - // derefs - JDD.Deref(init); + /** + * Compute transient probability distribution (forwards). + * Optionally, use the passed in vector initDist as the initial probability distribution (time 0). + * If null, start from initial state (or uniform distribution over multiple initial states). + * For reasons of efficiency, when a vector is passed in, it will be trampled over and + * then deleted afterwards, so if you wanted it, take a copy. + */ + public StateProbs doTransient(int time, StateProbs initDist) throws PrismException + { + // mtbdd stuff + JDDNode start, init; + // other stuff + StateProbs initDistNew = null, probs = null; + + // build initial distribution (if not specified) + if (initDist == null) { + // first construct as MTBDD + // get initial states of model + start = model.getStart(); + // compute initial probability distribution (equiprobable over all start states) + JDD.Ref(start); + init = JDD.Apply(JDD.DIVIDE, start, JDD.Constant(JDD.GetNumMinterms(start, allDDRowVars.n()))); + // if using MTBDD engine, distribution needs to be an MTBDD + if (engine == Prism.MTBDD) { + initDistNew = new StateProbsMTBDD(init, model); + } + // for sparse/hybrid engines, distribution needs to be a double vector + else { + initDistNew = new StateProbsDV(init, model); + JDD.Deref(init); + } + } else { + initDistNew = initDist; + } + + // compute transient probabilities + probs = computeTransientProbs(trans, initDistNew, time); return probs; } @@ -1765,26 +1803,39 @@ public class ProbModelChecker extends NonProbModelChecker return probs; } - // compute transient probabilities - - protected StateProbs computeTransientProbs(JDDNode tr, JDDNode init, int time) throws PrismException + /** + * Compute transient probability distribution (forwards). + * Use the passed in vector initDist as the initial probability distribution (time 0). + * The type of this should match the current engine + * (i.e. StateProbsMTBDD for MTBDD, StateProbsDV for sparse/hybrid). + * For reasons of efficiency, this vector will be trampled over and + * then deleted afterwards, so if you wanted it, take a copy. + */ + protected StateProbs computeTransientProbs(JDDNode tr, StateProbs initDist, int time) throws PrismException { JDDNode probsMTBDD; DoubleVector probsDV; StateProbs probs = null; + // special case: time = 0 + if (time == 0) { + // we are allowed to keep the init vector, so no need to clone + return initDist; + } + + // general case try { switch (engine) { case Prism.MTBDD: - probsMTBDD = PrismMTBDD.ProbTransient(tr, odd, init, allDDRowVars, allDDColVars, time); + probsMTBDD = PrismMTBDD.ProbTransient(tr, odd, ((StateProbsMTBDD) initDist).getJDDNode(), allDDRowVars, allDDColVars, time); probs = new StateProbsMTBDD(probsMTBDD, model); break; case Prism.SPARSE: - probsDV = PrismSparse.ProbTransient(tr, odd, init, allDDRowVars, allDDColVars, time); + probsDV = PrismSparse.ProbTransient(tr, odd, ((StateProbsDV) initDist).getDoubleVector(), allDDRowVars, allDDColVars, time); probs = new StateProbsDV(probsDV, model); break; case Prism.HYBRID: - probsDV = PrismHybrid.ProbTransient(tr, odd, init, allDDRowVars, allDDColVars, time); + probsDV = PrismHybrid.ProbTransient(tr, odd, ((StateProbsDV) initDist).getDoubleVector(), allDDRowVars, allDDColVars, time); probs = new StateProbsDV(probsDV, model); break; default: diff --git a/prism/src/sparse/PS_ProbTransient.cc b/prism/src/sparse/PS_ProbTransient.cc index 0c50d568..0b78e6f9 100644 --- a/prism/src/sparse/PS_ProbTransient.cc +++ b/prism/src/sparse/PS_ProbTransient.cc @@ -46,7 +46,7 @@ JNIEnv *env, jclass cls, jlong __jlongpointer tr, // trans matrix jlong __jlongpointer od, // odd -jlong __jlongpointer in, // initial distribution +jlong __jlongpointer in, // initial distribution (note: this will be deleted afterwards) jlong __jlongpointer rv, // row vars jint num_rvars, jlong __jlongpointer cv, // col vars @@ -57,7 +57,7 @@ jint time // time // cast function parameters DdNode *trans = jlong_to_DdNode(tr); // trans matrix ODDNode *odd = jlong_to_ODDNode(od); // odd - DdNode *init = jlong_to_DdNode(in); // initial distribution + double *init = jlong_to_double(in); // initial distribution DdNode **rvars = jlong_to_DdNode_array(rv); // row vars DdNode **cvars = jlong_to_DdNode_array(cv); // col vars @@ -112,7 +112,9 @@ jint time // time // create solution/iteration vectors PS_PrintToMainLog(env, "Allocating iteration vectors... "); - soln = mtbdd_to_double_vector(ddman, init, rvars, num_rvars, odd); + // for soln, we just use init (since we are free to modify/delete this vector) + // we also report the memory usage of this vector here, even though it has already been created + soln = init; soln2 = new double[n]; kb = n*8.0/1024.0; kbt += 2*kb; diff --git a/prism/src/sparse/PrismSparse.java b/prism/src/sparse/PrismSparse.java index b14b0bf1..a13f8785 100644 --- a/prism/src/sparse/PrismSparse.java +++ b/prism/src/sparse/PrismSparse.java @@ -235,9 +235,9 @@ public class PrismSparse // transient (probabilistic/dtmc) private static native long PS_ProbTransient(long trans, long odd, long init, long rv, int nrv, long cv, int ncv, int time); - public static DoubleVector ProbTransient(JDDNode trans, ODDNode odd, JDDNode init, JDDVars rows, JDDVars cols, int time) throws PrismException + public static DoubleVector ProbTransient(JDDNode trans, ODDNode odd, DoubleVector init, JDDVars rows, JDDVars cols, int time) throws PrismException { - long ptr = PS_ProbTransient(trans.ptr(), odd.ptr(), init.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), time); + long ptr = PS_ProbTransient(trans.ptr(), odd.ptr(), init.getPtr(), rows.array(), rows.n(), cols.array(), cols.n(), time); if (ptr == 0) throw new PrismException(getErrorMessage()); return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff())); }