Add support for computing ranges of transient probabilities (e.g. -tr 0.1:0.01:0.2) to command-line. Transient probability computation is done incrementally, using each computed distribution.

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

prism/src/explicit/CTMCModelChecker.java

@@ -168,16 +168,7 @@ public class CTMCModelChecker extends DTMCModelChecker
 	 */
 	public StateValues doTransient(CTMC ctmc, double t, File initDistFile) throws PrismException
 	{
-		StateValues initDist = null;
-
-		if (initDistFile != null) {
-			mainLog.println("\nImporting initial probability distribution from file \"" + initDistFile + "\"...");
-			// Build an empty vector 
-			initDist = new StateValues(TypeDouble.getInstance(), ctmc);
-			// Populate vector from file
-			initDist.readFromFile(initDistFile);
-		}
-
+		StateValues initDist = readDistributionFromFile(initDistFile, ctmc);
 		return doTransient(ctmc, t, initDist);
 	}
 

prism/src/explicit/DTMCModelChecker.java

@@ -26,12 +26,14 @@
 
 package explicit;
 
+import java.io.File;
 import java.util.*;
 
 import prism.*;
 import explicit.StateValues;
 import explicit.rewards.*;
 import parser.ast.*;
+import parser.type.TypeDouble;
 
 /**
  * Explicit-state model checker for discrete-time Markov chains (DTMCs).
@@ -248,6 +250,25 @@ public class DTMCModelChecker extends ProbModelChecker
 		throw new PrismException("Not implemented yet");
 	}
 	
+	/**
+	 * Generate a probability distribution, stored as a StateValues object, from a file.
+	 * If {@code distFile} is null, so is the return value.
+	 */
+	public StateValues readDistributionFromFile(File distFile, Model model) throws PrismException
+	{
+		StateValues dist = null;
+
+		if (distFile != null) {
+			mainLog.println("\nImporting probability distribution from file \"" + distFile + "\"...");
+			// Build an empty vector 
+			dist = new StateValues(TypeDouble.getInstance(), model);
+			// Populate vector from file
+			dist.readFromFile(distFile);
+		}
+
+		return dist;
+	}
+
 	// Numerical computation functions
 
 	/**

prism/src/prism/Prism.java

@@ -150,9 +150,9 @@ public class Prism implements PrismSettingsListener
 	// Round-off threshold for places where doubles are summed and compared to integers
 	// (e.g. checking that probabilities sum to 1 in an update).
 	private double sumRoundOff = 1e-5;
-	
+
 	// Method to use for (symbolic) state-space reachability
-	private int reachMethod = REACH_BFS; 
+	private int reachMethod = REACH_BFS;
 
 	//------------------------------------------------------------------------------
 	// Logs
@@ -494,7 +494,7 @@ public class Prism implements PrismSettingsListener
 
 	public static int REACH_BFS = 1;
 	public static int REACH_FRONTIER = 2;
-	
+
 	public void setReachMethod(int reachMethod)
 	{
 		this.reachMethod = reachMethod;
@@ -754,7 +754,7 @@ public class Prism implements PrismSettingsListener
 	{
 		return reachMethod;
 	}
-	
+
 	public void addModelListener(PrismModelListener listener)
 	{
 		modelListeners.add(listener);
@@ -2588,8 +2588,9 @@ public class Prism implements PrismSettingsListener
 	}
 
 	/**
-	 * Compute transient probabilities for the current model (DTMCs/CTMCs only).
-	 * Output probability distribution to log. 
+	 * Compute transient probabilities (forwards) for the current model (DTMCs/CTMCs only).
+	 * Output probability distribution to log.
+	 * For a discrete-time model, {@code time} will be cast to an integer.
 	 */
 	public void doTransient(double time) throws PrismException
 	{
@@ -2597,8 +2598,9 @@ public class Prism implements PrismSettingsListener
 	}
 
 	/**
-	 * Compute transient probabilities for the current model (DTMCs/CTMCs only).
+	 * Compute transient probabilities (forwards) for the current model (DTMCs/CTMCs only).
 	 * Output probability distribution to a file (or, if file is null, to log). 
+	 * For a discrete-time model, {@code time} will be cast to an integer.
 	 * The exportType should be EXPORT_PLAIN or EXPORT_MATLAB.
 	 * Optionally (if non-null), read in the initial probability distribution from a file.
 	 */
@@ -2687,6 +2689,125 @@ public class Prism implements PrismSettingsListener
 			tmpLog.close();
 	}
 
+	/**
+	 * Compute transient probabilities (forwards) for the current model (DTMCs/CTMCs only)
+	 * for a range of time points. Each distribution is computed incrementally.
+	 * Output probability distribution to a file (or, if file is null, to log).
+	 * Time points are specified using an UndefinedConstants with a single ranging variable  
+	 * (of the appropriate type (int/double) and with arbitrary name).
+	 * 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(UndefinedConstants times, int exportType, File file, File fileIn) throws PrismException
+	{
+		int i, timeInt = 0, initTimeInt = 0;
+		double timeDouble = 0, initTimeDouble = 0;
+		Object time;
+		long l = 0; // timer
+		StateValues probs = null, initDist = null;
+		explicit.StateValues probsExpl = null, initDistExpl = null;
+		PrismLog tmpLog = null;
+
+		if (!(currentModelType == ModelType.CTMC || currentModelType == ModelType.DTMC))
+			throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs");
+
+		if (file != null && getEngine() == MTBDD)
+			throw new PrismException("Transient probability export only supported for sparse/hybrid engines");
+
+		// no specific states format for MRMC
+		if (exportType == EXPORT_MRMC)
+			exportType = EXPORT_PLAIN;
+		// rows format does not apply to states output
+		if (exportType == EXPORT_ROWS)
+			exportType = EXPORT_PLAIN;
+
+		// Step through required time points
+		for (i = 0; i < times.getNumPropertyIterations(); i++) {
+			
+			// Get time, check non-negative
+			time = times.getPFConstantValues().getValue(0);
+			if (currentModelType.continuousTime())
+				timeDouble = ((Double) time).doubleValue();
+			else
+				timeInt = ((Integer) time).intValue();
+			if (currentModelType.continuousTime() ? (((Double) time).doubleValue() < 0) : (((Integer) time).intValue() < 0))
+				throw new PrismException("Cannot compute transient probabilities for negative time value");
+
+			mainLog.printSeparator();
+			mainLog.println("\nComputing transient probabilities (time = " + time + ")...");
+			
+			// Build model, if necessary
+			buildModelIfRequired();
+
+			l = System.currentTimeMillis();
+
+			if (!getExplicit()) {
+				if (currentModelType.continuousTime()) {
+					StochModelChecker mc = new StochModelChecker(this, currentModel, null);
+					if (i == 0) {
+						initDist = mc.readDistributionFromFile(fileIn);
+						initTimeDouble = 0;
+					}
+					probs = ((StochModelChecker) mc).doTransient(timeDouble - initTimeDouble, initDist);
+				} else {
+					ProbModelChecker mc = new ProbModelChecker(this, currentModel, null);
+					if (i == 0) {
+						initDist = mc.readDistributionFromFile(fileIn);
+						initTimeInt = 0;
+					}
+					probs = ((ProbModelChecker) mc).doTransient(timeInt - initTimeInt, initDist);
+				}
+			} else {
+				if (currentModelType.continuousTime()) {
+					CTMCModelChecker mc = new CTMCModelChecker();
+					mc.setLog(mainLog);
+					mc.setSettings(settings);
+					if (i == 0) {
+						initDistExpl = mc.readDistributionFromFile(fileIn, currentModelExpl);
+						initTimeDouble = 0;
+					}
+					probsExpl = mc.doTransient((CTMC) currentModelExpl, timeDouble - initTimeDouble, initDistExpl);
+				} else {
+					throw new PrismException("Not implemented yet");
+				}
+			}
+
+			l = System.currentTimeMillis() - l;
+
+			// print message
+			mainLog.print("\nPrinting transient probabilities ");
+			mainLog.print(getStringForExportType(exportType) + " ");
+			mainLog.println(getDestinationStringForFile(file));
+
+			// create new file log or use main log
+			tmpLog = getPrismLogForFile(file);
+
+			// print out or export probabilities
+			if (!getExplicit())
+				probs.print(tmpLog, file == null, exportType == EXPORT_MATLAB, file == null);
+			else
+				probsExpl.print(tmpLog, file == null, exportType == EXPORT_MATLAB, file == null, true);
+
+			// print out computation time
+			mainLog.println("\nTime for transient probability computation: " + l / 1000.0 + " seconds.");
+
+			// Prepare for next iteration
+			initDist = probs;
+			initDistExpl = probsExpl;
+			initTimeInt = timeInt;
+			initTimeDouble = timeDouble;
+			times.iterateProperty();
+		}
+
+		// tidy up
+		if (!getExplicit())
+			probs.clear();
+		else
+			probsExpl.clear();
+		if (file != null)
+			tmpLog.close();
+	}
+
 	public void explicitBuildTest() throws PrismException
 	{
 		/* old code...
@@ -2721,7 +2842,7 @@ public class Prism implements PrismSettingsListener
 			throw new PrismException("Could not create temporary file \"" + tmpFile + "\"");
 		}*/
 	}
-	
+
 	/**
 	 * Clear the built model if needed (free/deallocate memory etc)
 	 */

prism/src/prism/PrismCL.java

@@ -732,8 +732,6 @@ public class PrismCL implements PrismModelListener
 	private void doTransient()
 	{
 		ModelType modelType;
-		double d;
-		int i;
 		File exportTransientFile = null;
 
 		if (dotransient) {
@@ -747,24 +745,20 @@ public class PrismCL implements PrismModelListener
 				// Determine model type
 				modelType = prism.getModelType();
 
-				// Compute transient probabilities
-				if (modelType == ModelType.CTMC) {
-					try {
-						d = Double.parseDouble(transientTime);
-					} catch (NumberFormatException e) {
-						throw new PrismException("Invalid value \"" + transientTime + "\" for transient probability computation");
-					}
-					prism.doTransient(d, exportType, exportTransientFile, importinitdist ? new File(importInitDistFilename) : null);
-				} else if (modelType == ModelType.DTMC) {
-					try {
-						i = Integer.parseInt(transientTime);
-					} catch (NumberFormatException e) {
-						throw new PrismException("Invalid value \"" + transientTime + "\" for transient probability computation");
-					}
-					prism.doTransient(i, exportType, exportTransientFile, importinitdist ? new File(importInitDistFilename) : null);
-				} else {
-					mainLog.printWarning("Transient probabilities only computed for DTMCs/CTMCs.");
+				// Parse time specification, store as UndefinedConstant for constant T
+				String timeType = modelType.continuousTime() ? "double" : "int";
+				UndefinedConstants ucTransient = new UndefinedConstants(null, prism.parsePropertiesString(null, "const " + timeType + " T; T;"));
+				try {
+					ucTransient.defineUsingConstSwitch("T=" + transientTime);
+				} catch (PrismException e) {
+					if (transientTime.contains(":"))
+						errorAndExit("\"" + transientTime + "\" is not a valid time range for a " + modelType);
+					else
+						errorAndExit("\"" + transientTime + "\" is not a valid time for a " + modelType);
 				}
+				
+				// Compute transient probabilities
+				prism.doTransient(ucTransient, exportType, exportTransientFile, importinitdist ? new File(importInitDistFilename) : null);
 			}
 			// In case of error, report it and proceed
 			catch (PrismException e) {
@@ -814,7 +808,6 @@ public class PrismCL implements PrismModelListener
 	private void parseArguments(String[] args) throws PrismException
 	{
 		int i, j;
-		double d;
 		String sw, s;
 		PrismLog log;
 
@@ -886,16 +879,8 @@ public class PrismCL implements PrismModelListener
 				// do transient probability computation
 				else if (sw.equals("transient") || sw.equals("tr")) {
 					if (i < args.length - 1) {
-						try {
-							dotransient = true;
-							transientTime = args[++i];
-							// Make sure transient time parses as a +ve double
-							d = Double.parseDouble(transientTime);
-							if (d < 0)
-								throw new NumberFormatException("");
-						} catch (NumberFormatException e) {
-							errorAndExit("Invalid value for -" + sw + " switch");
-						}
+						dotransient = true;
+						transientTime = args[++i];
 					} else {
 						errorAndExit("No value specified for -" + sw + " switch");
 					}
@@ -1418,8 +1403,7 @@ public class PrismCL implements PrismModelListener
 				// reachability options (hidden options)
 				else if (sw.equals("frontier")) {
 					prism.setReachMethod(Prism.REACH_FRONTIER);
-				}
-				else if (sw.equals("bfs")) {
+				} else if (sw.equals("bfs")) {
 					prism.setReachMethod(Prism.REACH_BFS);
 				}
 

prism/src/prism/ProbModelChecker.java

@@ -1225,20 +1225,7 @@ public class ProbModelChecker extends NonProbModelChecker
 	 */
 	public StateValues doTransient(int time, File initDistFile) throws PrismException
 	{
-		StateValues 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 StateValuesMTBDD(JDD.Constant(0), model);
-			} else {
-				initDist = new StateValuesDV(new DoubleVector((int) model.getNumStates()), model);
-			}
-			// Populate vector from file
-			initDist.readFromFile(initDistFile);
-		}
-
+		StateValues initDist = readDistributionFromFile(initDistFile);
 		return doTransient(time, initDist);
 	}
 
@@ -1283,6 +1270,30 @@ public class ProbModelChecker extends NonProbModelChecker
 		return probs;
 	}
 
+	/**
+	 * Generate a probability distribution, stored as a StateValues object, from a file.
+	 * The type of storage (MTBDD or double vector) matches the current engine.
+	 * If {@code distFile} is null, so is the return value.
+	 */
+	public StateValues readDistributionFromFile(File distFile) throws PrismException
+	{
+		StateValues dist = null;
+
+		if (distFile != null) {
+			mainLog.println("\nImporting probability distribution from file \"" + distFile + "\"...");
+			// Build an empty vector of the appropriate type 
+			if (engine == Prism.MTBDD) {
+				dist = new StateValuesMTBDD(JDD.Constant(0), model);
+			} else {
+				dist = new StateValuesDV(new DoubleVector((int) model.getNumStates()), model);
+			}
+			// Populate vector from file
+			dist.readFromFile(distFile);
+		}
+		
+		return dist;
+	}
+
 	// -----------------------------------------------------------------------------------
 	// probability computation methods
 	// -----------------------------------------------------------------------------------