diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index dc63ed23..1f7f65a2 100644 --- a/prism/src/prism/Prism.java +++ b/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 diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 0e79d980..c293729e 100644 --- a/prism/src/prism/PrismCL.java +++ b/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 ............ Import the list of states directly from a text file"); mainLog.println("-importlabels ............ Import the list of labels directly from a text file"); mainLog.println("-importinit .............. Specify the initial state for explicitly imported models"); + mainLog.println("-importinitdist .......... 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 ... Export the transition matrix graph to a dot file, with state info"); mainLog.println("-exportdot .............. Export the transition matrix MTBDD to a dot file"); mainLog.println("-exportbsccs ............ Compute and export all BSCCs of the model"); - mainLog.println("-exporttransient ......... Export transient probabilities to a file"); + mainLog.println("-exporttransient ........ Export transient probabilities to a file"); mainLog.println("-exportprism ............ Export final PRISM model to a file"); mainLog.println(); mainLog.println("-mtbdd (or -m) ................. Use the MTBDD engine"); diff --git a/prism/src/prism/StateProbs.java b/prism/src/prism/StateProbs.java index 24567125..32bfd76d 100644 --- a/prism/src/prism/StateProbs.java +++ b/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); diff --git a/prism/src/prism/StateProbsDV.java b/prism/src/prism/StateProbsDV.java index 24ce7823..e44f3705 100644 --- a/prism/src/prism/StateProbsDV.java +++ b/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) diff --git a/prism/src/prism/StateProbsMTBDD.java b/prism/src/prism/StateProbsMTBDD.java index 97488103..189f9462 100644 --- a/prism/src/prism/StateProbsMTBDD.java +++ b/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) diff --git a/prism/src/prism/StochModelChecker.java b/prism/src/prism/StochModelChecker.java index b4e94f82..293433f4 100644 --- a/prism/src/prism/StochModelChecker.java +++ b/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).