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

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

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

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

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 + ")...");

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:

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;

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