Added command-line option to import initial distribution for transient analysis.

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

prism/src/prism/Prism.java

@@ -1461,15 +1461,16 @@ public class Prism implements PrismSettingsListener
 	 */
 	public void doTransient(Model model, double time) throws PrismException
 	{
-		doTransient(model, time, EXPORT_PLAIN, null);
+		doTransient(model, time, EXPORT_PLAIN, null, null);
 	}
 	
 	/**
 	 * Compute transient probabilities (for DTMC or CTMC).
 	 * Output probability distribution to a file (or, if file is null, to log). 
 	 * The exportType should be EXPORT_PLAIN or EXPORT_MATLAB.
+	 * Optionally (if non-null), read in the initial probability distribution from a file.
 	 */
-	public void doTransient(Model model, double time, int exportType, File file) throws PrismException
+	public void doTransient(Model model, double time, int exportType, File fileOut, File fileIn) throws PrismException
 	{
 		long l = 0; // timer
 		StateProbs probs = null;
@@ -1477,7 +1478,7 @@ public class Prism implements PrismSettingsListener
 		
 		if (time < 0) throw new PrismException("Cannot compute transient probabilities for negative time value");
 		
-		if (file != null && getEngine() == MTBDD)
+		if (fileOut != null && getEngine() == MTBDD)
 			throw new PrismException("Transient probability export only supported for sparse/hybrid engines");
 		
 		// no specific states format for MRMC
@@ -1498,7 +1499,7 @@ public class Prism implements PrismSettingsListener
 		else if (model.getModelType() == ModelType.CTMC) {
 			mainLog.println("\nComputing transient probabilities (time = " + time + ")...");
 			mc = new StochModelChecker(this, model, null);
-			probs = ((StochModelChecker)mc).doTransient(time);
+			probs = ((StochModelChecker)mc).doTransient(time, fileIn);
 		}
 		else {
 			throw new PrismException("Transient probabilities only computed for DTMCs/CTMCs");
@@ -1512,27 +1513,27 @@ public class Prism implements PrismSettingsListener
 		case EXPORT_PLAIN: mainLog.print("in plain text format "); break;
 		case EXPORT_MATLAB: mainLog.print("in Matlab format "); break;
 		}
-		if (file != null) mainLog.println("to file \"" + file + "\"..."); else mainLog.println("below:");
+		if (fileOut != null) mainLog.println("to file \"" + fileOut + "\"..."); else mainLog.println("below:");
 		
 		// create new file log or use main log
-		if (file != null) {
-			tmpLog = new PrismFileLog(file.getPath());
+		if (fileOut != null) {
+			tmpLog = new PrismFileLog(fileOut.getPath());
 			if (!tmpLog.ready()) {
-				throw new PrismException("Could not open file \"" + file + "\" for output");
+				throw new PrismException("Could not open file \"" + fileOut + "\" for output");
 			}
 		} else {
 			tmpLog = mainLog;
 		}
 		
 		// print out or export probabilities
-		probs.print(tmpLog, file == null, exportType == EXPORT_MATLAB, file == null);
+		probs.print(tmpLog, fileOut == null, exportType == EXPORT_MATLAB, fileOut == null);
 		
 		// print out model checking time
 		mainLog.println("\nTime for transient probability computation: " + l/1000.0 + " seconds.");
 
 		// tidy up
 		probs.clear();
-		if (file != null) tmpLog.close();
+		if (fileOut != null) tmpLog.close();
 	}
 	
 	// clear up and close down

prism/src/prism/PrismCL.java

@@ -43,6 +43,7 @@ public class PrismCL
 	private boolean importtrans = false;
 	private boolean importstates = false;
 	private boolean importlabels = false;
+	private boolean importinitdist = false;
 	private boolean steadystate = false;
 	private boolean dotransient = false;
 	private boolean exporttrans = false;
@@ -80,6 +81,7 @@ public class PrismCL
 	private String modelFilename = null;
 	private String importStatesFilename = null;
 	private String importLabelsFilename = null;
+	private String importInitDistFilename = null;
 	private String propertiesFilename = null;
 	private String exportTransFilename = null;
 	private String exportStateRewardsFilename = null;
@@ -790,7 +792,7 @@ public class PrismCL
 			catch (NumberFormatException e) {
 				throw new PrismException("Invalid value \""+transientTime+"\" for transient probability computation");
 			}
-			prism.doTransient(model, d, exportType, exportTransientFile);
+			prism.doTransient(model, d, exportType, exportTransientFile, importinitdist ? new File(importInitDistFilename) : null);
 		}
 		else if (model.getModelType() == ModelType.DTMC) {
 			try {
@@ -799,7 +801,7 @@ public class PrismCL
 			catch (NumberFormatException e) {
 				throw new PrismException("Invalid value \""+transientTime+"\" for transient probability computation");
 			}
-			prism.doTransient(model, i, exportType, exportTransientFile);
+			prism.doTransient(model, i, exportType, exportTransientFile, importinitdist ? new File(importInitDistFilename) : null);
 		}
 		else {
 			mainLog.println("\nWarning: Transient probabilities only computed for DTMCs/CTMCs.");
@@ -1089,6 +1091,16 @@ public class PrismCL
 						errorAndExit("No file specified for -"+sw+" switch");
 					}
 				}
+				// import initial distribution e.g. for transient probability distribution
+				else if (sw.equals("importinitdist")) {
+					if (i < args.length-1) {
+						importinitdist = true;
+						importInitDistFilename = args[++i];
+					}
+					else {
+						errorAndExit("No file specified for -"+sw+" switch");
+					}
+				}
 				// override model type to dtmc
 				else if (sw.equals("dtmc")) {
 					typeOverride = ModelType.DTMC;
@@ -1682,6 +1694,7 @@ public class PrismCL
 		mainLog.println("-importstates <file>............ Import the list of states directly from a text file");
 		mainLog.println("-importlabels <file>............ Import the list of labels directly from a text file");
 		mainLog.println("-importinit <expr>.............. Specify the initial state for explicitly imported models");
+		mainLog.println("-importinitdist <expr>.......... Specify the initial probability distribution for transient analysis");
 		mainLog.println("-dtmc .......................... Force imported/built model to be a DTMC");
 		mainLog.println("-ctmc .......................... Force imported/built model to be a CTMC");
 		mainLog.println("-mdp ........................... Force imported/built model to be an MDP");
@@ -1701,7 +1714,7 @@ public class PrismCL
 		mainLog.println("-exporttransdotstates <file> ... Export the transition matrix graph to a dot file, with state info");
 		mainLog.println("-exportdot <file> .............. Export the transition matrix MTBDD to a dot file");
 		mainLog.println("-exportbsccs <file> ............ Compute and export all BSCCs of the model");
-		mainLog.println("-exporttransient <file> ......... Export transient probabilities to a file");
+		mainLog.println("-exporttransient <file> ........ Export transient probabilities to a file");
 		mainLog.println("-exportprism <file> ............ Export final PRISM model to a file");
 		mainLog.println();
 		mainLog.println("-mtbdd (or -m) ................. Use the MTBDD engine");

prism/src/prism/StateProbs.java

@@ -26,6 +26,8 @@
 
 package prism;
 
+import java.io.File;
+
 import jdd.JDDNode;
 import jdd.JDDVars;
 
@@ -35,6 +37,7 @@ public interface StateProbs
 {
 	StateProbsDV convertToStateProbsDV();
 	StateProbsMTBDD convertToStateProbsMTBDD();
+	void readFromFile(File file) throws PrismException;
 	void roundOff(int places);
 	void subtractFromOne();
 	void add(StateProbs sp);

prism/src/prism/StateProbsDV.java

@@ -26,6 +26,8 @@
 
 package prism;
 
+import java.io.*;
+
 import dv.*;
 import jdd.*;
 import odd.*;
@@ -34,10 +36,6 @@ import parser.type.*;;
 
 // state probability vector (double vector)
 
-/**
- * @author dxp
- *
- */
 public class StateProbsDV implements StateProbs
 {
 	// prob vector
@@ -115,6 +113,53 @@ public class StateProbsDV implements StateProbs
 	
 	// METHODS TO MODIFY VECTOR
 	
+	/**
+	 * Set element i of this vector to value d. 
+	 */
+	private void setElement(int i, double d)
+	{
+		probs.setElement(i, d);
+	}
+	
+	// read from file
+	
+	public void readFromFile(File file) throws PrismException
+	{
+		BufferedReader in;
+		String s;
+		int lineNum = 0, count = 0;
+		double d;
+		
+		try {
+			// open file for reading
+			in = new BufferedReader(new FileReader(file));
+			// read remaining lines
+			s = in.readLine(); lineNum++;
+			while (s != null) {
+				s = s.trim();
+				if (!("".equals(s))) {
+					if (count + 1 > probs.getSize())
+						throw new PrismException("Too many values in initial distribution (" + (count + 1) + ", not " + probs.getSize() + ")");
+					d = Double.parseDouble(s);
+					setElement(count, d);
+					count++;
+				}
+				s = in.readLine(); lineNum++;
+			}
+			// close file
+			in.close();
+			// check size
+			if (count < probs.getSize())
+				throw new PrismException("Too few values in initial distribution (" + count + ", not " + probs.getSize() + ")");
+		}
+		catch (IOException e) {
+			throw new PrismException("File I/O error reading from \"" + file + "\"");
+		}
+		catch (NumberFormatException e) {
+			throw new PrismException("Error detected at line " + lineNum + " of file \"" + file + "\"");
+		}
+	}
+	
 	// round
 	
 	public void roundOff(int places)

prism/src/prism/StateProbsMTBDD.java

@@ -26,6 +26,11 @@
 
 package prism;
 
+import java.io.BufferedReader;
+import java.io.File;
+import java.io.FileReader;
+import java.io.IOException;
+
 import jdd.*;
 import odd.*;
 import parser.VarList;
@@ -100,6 +105,74 @@ public class StateProbsMTBDD implements StateProbs
 	
 	// METHODS TO MODIFY VECTOR
 	
+	/**
+	 * Set element i of this vector to value d. 
+	 */
+	public void setElement(int i, double d)
+	{
+		ODDNode ptr;
+		JDDNode dd;
+		int j, k;
+		
+		// Use ODD to build BDD for state index i
+		dd = JDD.Constant(1);
+		ptr = odd;
+		j = i;
+		for (k = 0; k < numVars; k++) {
+			JDD.Ref(vars.getVar(k));
+			if (j >= ptr.getEOff()) {
+				j -= ptr.getEOff();
+				dd = JDD.And(dd, vars.getVar(k));
+				ptr = ptr.getThen();
+			} else {
+				dd = JDD.And(dd, JDD.Not(vars.getVar(k)));
+				ptr = ptr.getElse();
+			}
+		}
+		
+		// Add element to vector MTBDD
+		probs = JDD.ITE(dd, JDD.Constant(d), probs);
+	}
+	
+	// read from file
+	
+	public void readFromFile(File file) throws PrismException
+	{
+		BufferedReader in;
+		String s;
+		int lineNum = 0, count = 0;
+		double d;
+		
+		try {
+			// open file for reading
+			in = new BufferedReader(new FileReader(file));
+			// read remaining lines
+			s = in.readLine(); lineNum++;
+			while (s != null) {
+				s = s.trim();
+				if (!("".equals(s))) {
+					if (count + 1> model.getNumStates())
+						throw new PrismException("Too many values in initial distribution (" + (count + 1) + ", not " + model.getNumStates() + ")");
+					d = Double.parseDouble(s);
+					setElement(count, d);
+					count++;
+				}
+				s = in.readLine(); lineNum++;
+			}
+			// close file
+			in.close();
+			// check size
+			if (count < model.getNumStates())
+				throw new PrismException("Too few values in initial distribution (" + count + ", not " + model.getNumStates() + ")");
+		}
+		catch (IOException e) {
+			throw new PrismException("File I/O error reading from \"" + file + "\"");
+		}
+		catch (NumberFormatException e) {
+			throw new PrismException("Error detected at line " + lineNum + " of file \"" + file + "\"");
+		}
+	}
+	
 	// round
 	
 	public void roundOff(int places)

prism/src/prism/StochModelChecker.java

@@ -26,6 +26,8 @@
 
 package prism;
 
+import java.io.*;
+
 import jdd.*;
 import dv.*;
 import mtbdd.*;
@@ -318,9 +320,33 @@ public class StochModelChecker extends ProbModelChecker
 	 */
 	public StateProbs doTransient(double time) throws PrismException
 	{
-		return doTransient(time, null);
+		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(double time, File initDistFile) throws PrismException
+	{
+		StateProbs initDist = null;
+
+		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 {
+				initDist = new StateProbsDV(new DoubleVector((int) model.getNumStates()), model);
+			}
+			// Populate vector from file
+			initDist.readFromFile(initDistFile);
+		}
+		
+		return doTransient(time, initDist);
+	}
+
 	/**
 	 * Compute transient probability distribution (forwards).
 	 * Optionally, use the passed in vector initDist as the initial probability distribution (time 0).