diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index cc2c894b..7d70cfdd 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -55,17 +55,17 @@ public class Prism implements PrismSettingsListener // prism version suffix //private static String versionSuffix = ""; private static String versionSuffix = ".dev"; //".rXXXX"; - + //------------------------------------------------------------------------------ // Constants //------------------------------------------------------------------------------ - + // underlying computation engine public static final int MTBDD = 1; public static final int SPARSE = 2; public static final int HYBRID = 3; private static String[] engineStrings = { "?", "MTBDD", "Sparse", "Hybrid" }; - + // methods for solving linear equation systems public static final int POWER = 1; public static final int JACOBI = 2; @@ -78,18 +78,18 @@ public class Prism implements PrismSettingsListener public static final int BSOR = 9; public static final int PSOR = 10; public static final int BPSOR = 11; - + // methods for solving MDPs public static final int MDP_VALITER = 1; public static final int MDP_GAUSSSEIDEL = 2; public static final int MDP_POLITER = 3; public static final int MDP_MODPOLITER = 4; public static final int MDP_LP = 5; - + // termination criterion for iterative methods public static final int ABSOLUTE = 1; public static final int RELATIVE = 2; - + // options for model matrix export public static final int EXPORT_PLAIN = 1; public static final int EXPORT_MATLAB = 2; @@ -97,24 +97,24 @@ public class Prism implements PrismSettingsListener public static final int EXPORT_MRMC = 4; public static final int EXPORT_ROWS = 5; public static final int EXPORT_DOT_STATES = 6; - + // options for adversary export public static final int EXPORT_ADV_NONE = 1; public static final int EXPORT_ADV_DTMC = 2; public static final int EXPORT_ADV_MDP = 3; - + // methods for SCC decomposition public static final int XIEBEEREL = 1; public static final int LOCKSTEP = 2; public static final int SCCFIND = 3; - + //------------------------------------------------------------------------------ // Settings / flags / options //------------------------------------------------------------------------------ - + // Main PRISM settings private PrismSettings settings; - + // Some additional settings (here because not available from main options panel in GUI) // Export target state info? protected boolean exportTarget; @@ -124,14 +124,14 @@ public class Prism implements PrismSettingsListener protected String exportProductTransFilename; protected boolean exportProductStates; protected String exportProductStatesFilename; - + // A few miscellaneous options (i.e. defunct/hidden/undocumented/etc.) // See constructor below for default values - - private boolean doReach; // do reachability? (sometimes might want to skip it) - private boolean bsccComp; // do bscc computation before steady-state? + + private boolean doReach; // do reachability? (sometimes might want to skip it) + private boolean bsccComp; // do bscc computation before steady-state? private boolean checkZeroLoops; - + // MTBDD construction method (NOW DEFUNCT) // 1 - use with ordering 1: nondet vars form a tree at the top // 3 - use with ordering 2: zero for nonexistant bits @@ -142,42 +142,43 @@ public class Prism implements PrismSettingsListener // 1 - (s ... s) (l ... l) (r c ... r c) // 2 - (s l ... l r c ... r c) (s l ... l r c ... r c) ... private int ordering; - + // 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; - + //------------------------------------------------------------------------------ // Logs //------------------------------------------------------------------------------ - + private PrismLog mainLog; // one log for most output private PrismLog techLog; // another one for technical/diagnostic output - + //------------------------------------------------------------------------------ // Parsers/translators/model checkers/simulators/etc. //------------------------------------------------------------------------------ - + private static PrismParser thePrismParser = null; private static boolean prismParserInUse = false; - private Modules2MTBDD mod2mtbdd = null; private ExplicitFiles2MTBDD expf2mtbdd = null; private ExplicitModel2MTBDD expm2mtbdd = null; private SimulatorEngine theSimulator = null; - + //------------------------------------------------------------------------------ // State //------------------------------------------------------------------------------ - + // Info about currently loaded model, if any - private ModulesFile modulesFileCurrent = null; + private ModulesFile currentModulesFile = null; + private ModelType currentModelType = null; + private Model currentModel = null; // Has the CUDD library been initialised yet? private boolean cuddStarted = false; //------------------------------------------------------------------------------ // Constructors + options methods //------------------------------------------------------------------------------ - + /** * Construct a new Prism object. * @param mainLog PrismLog where messages and model checking output will be sent. @@ -188,27 +189,23 @@ public class Prism implements PrismSettingsListener // set up logs this.mainLog = mainLog; this.techLog = techLog; - + // set up some default options settings = new PrismSettings(); // load user's default settings try { settings.loadSettingsFile(); - } - catch(PrismException e) { + } catch (PrismException e) { // if there were no user defaults to load, create them - try - { + try { settings.saveSettingsFile(); - } - catch(PrismException ex) - { + } catch (PrismException ex) { mainLog.printWarning("Failed to create new PRISM settings file."); } } // add this Prism object as a listener settings.addSettingsListener(this); - + // default values for miscellaneous options exportTarget = false; exportTargetFilename = null; @@ -223,9 +220,9 @@ public class Prism implements PrismSettingsListener ordering = 1; sumRoundOff = 1e-5; } - + // Set methods - + /** * Set the PrismLog where messages and model checking output will be sent. */ @@ -238,7 +235,7 @@ public class Prism implements PrismSettingsListener PrismSparse.setMainLog(mainLog); PrismHybrid.setMainLog(mainLog); } - + /** * Set the PrismLog for output of detailed technical info (not really used). */ @@ -252,213 +249,219 @@ public class Prism implements PrismSettingsListener PrismSparse.setTechLog(techLog); PrismHybrid.setTechLog(techLog); } - + // Set methods for main prism settings // (provided for convenience and for compatibility with old code) - + public void setEngine(int e) throws PrismException { - settings.set(PrismSettings.PRISM_ENGINE, e-1); // note index offset correction + settings.set(PrismSettings.PRISM_ENGINE, e - 1); // note index offset correction } - + public void setVerbose(boolean b) throws PrismException { settings.set(PrismSettings.PRISM_VERBOSE, b); } - + public void setFairness(boolean b) throws PrismException { settings.set(PrismSettings.PRISM_FAIRNESS, b); } - + public void setPrecomp(boolean b) throws PrismException { settings.set(PrismSettings.PRISM_PRECOMPUTATION, b); } - + public void setProb0(boolean b) throws PrismException { settings.set(PrismSettings.PRISM_PROB0, b); } - + public void setProb1(boolean b) throws PrismException { settings.set(PrismSettings.PRISM_PROB1, b); } - + public void setDoProbChecks(boolean b) throws PrismException { settings.set(PrismSettings.PRISM_DO_PROB_CHECKS, b); - } - + } + public void setCompact(boolean b) throws PrismException { settings.set(PrismSettings.PRISM_COMPACT, b); } - + public void setLinEqMethod(int i) throws PrismException { - settings.set(PrismSettings.PRISM_LIN_EQ_METHOD, i-1); // note index offset correction + settings.set(PrismSettings.PRISM_LIN_EQ_METHOD, i - 1); // note index offset correction } - + public void setLinEqMethodParam(double d) throws PrismException { - settings.set(PrismSettings.PRISM_LIN_EQ_METHOD_PARAM, d); + settings.set(PrismSettings.PRISM_LIN_EQ_METHOD_PARAM, d); } - + public void setMDPSolnMethod(int i) throws PrismException { - settings.set(PrismSettings.PRISM_MDP_SOLN_METHOD, i-1); // note index offset correction + settings.set(PrismSettings.PRISM_MDP_SOLN_METHOD, i - 1); // note index offset correction } - + public void setTermCrit(int i) throws PrismException { - settings.set(PrismSettings.PRISM_TERM_CRIT, i-1); // note index offset correction + settings.set(PrismSettings.PRISM_TERM_CRIT, i - 1); // note index offset correction } - + public void setTermCritParam(double d) throws PrismException { settings.set(PrismSettings.PRISM_TERM_CRIT_PARAM, d); } - + public void setMaxIters(int i) throws PrismException { settings.set(PrismSettings.PRISM_MAX_ITERS, i); } - + public void setCUDDMaxMem(int i) throws PrismException { settings.set(PrismSettings.PRISM_CUDD_MAX_MEM, i); } - + public void setCUDDEpsilon(double d) throws PrismException { settings.set(PrismSettings.PRISM_CUDD_EPSILON, d); } - + public void setNumSBLevels(int i) throws PrismException { settings.set(PrismSettings.PRISM_NUM_SB_LEVELS, i); } - + public void setSBMaxMem(int i) throws PrismException { settings.set(PrismSettings.PRISM_SB_MAX_MEM, i); } - + public void setNumSORLevels(int i) throws PrismException { settings.set(PrismSettings.PRISM_NUM_SOR_LEVELS, i); } - + public void setSORMaxMem(int i) throws PrismException { settings.set(PrismSettings.PRISM_SOR_MAX_MEM, i); } - + public void setDoSSDetect(boolean b) throws PrismException { settings.set(PrismSettings.PRISM_DO_SS_DETECTION, b); } - + public void setExtraDDInfo(boolean b) throws PrismException { settings.set(PrismSettings.PRISM_EXTRA_DD_INFO, b); } - + public void setExtraReachInfo(boolean b) throws PrismException { settings.set(PrismSettings.PRISM_EXTRA_REACH_INFO, b); } - + public void setSCCMethod(int i) throws PrismException { - settings.set(PrismSettings.PRISM_SCC_METHOD, i-1); // note index offset correction + settings.set(PrismSettings.PRISM_SCC_METHOD, i - 1); // note index offset correction } - + public void setExportAdv(int i) throws PrismException { - settings.set(PrismSettings.PRISM_EXPORT_ADV, i-1); // note index offset correction + settings.set(PrismSettings.PRISM_EXPORT_ADV, i - 1); // note index offset correction } public void setExportAdvFilename(String s) throws PrismException { settings.set(PrismSettings.PRISM_EXPORT_ADV_FILENAME, s); } - + // Set methods for miscellaneous options - + public void setExportTarget(boolean b) throws PrismException { exportTarget = b; } - + public void setExportTargetFilename(String s) throws PrismException { exportTargetFilename = s; } - + public void setExportProductTrans(boolean b) throws PrismException { exportProductTrans = b; } - + public void setExportProductTransFilename(String s) throws PrismException { exportProductTransFilename = s; } - + public void setExportProductStates(boolean b) throws PrismException { exportProductStates = b; } - + public void setExportProductStatesFilename(String s) throws PrismException { exportProductStatesFilename = s; } - + public void setDoReach(boolean b) throws PrismException { doReach = b; } - + public void setBSCCComp(boolean b) throws PrismException { bsccComp = b; } - + public void setCheckZeroLoops(boolean checkZeroLoops) { - this.checkZeroLoops = checkZeroLoops; + this.checkZeroLoops = checkZeroLoops; } public void setConstruction(int i) throws PrismException { construction = i; } - + public void setOrdering(int i) throws PrismException { ordering = i; } - + public void setSumRoundOff(double d) throws PrismException { sumRoundOff = d; } - + // Get methods - + public static String getVersion() - { return version + versionSuffix; } - + { + return version + versionSuffix; + } + public PrismLog getMainLog() - { return mainLog; } - + { + return mainLog; + } + public PrismLog getTechLog() - { return techLog; } - + { + return techLog; + } + public PrismSettings getSettings() { return settings; @@ -466,135 +469,212 @@ public class Prism implements PrismSettingsListener // Get methods for main prism settings // (as above, provided for convenience and for compatibility with old code) - + public int getEngine() - { return settings.getInteger(PrismSettings.PRISM_ENGINE)+1; } //note the correction - + { + return settings.getInteger(PrismSettings.PRISM_ENGINE) + 1; + } //note the correction + public boolean getDoProbChecks() - { return settings.getBoolean(PrismSettings.PRISM_DO_PROB_CHECKS); } - + { + return settings.getBoolean(PrismSettings.PRISM_DO_PROB_CHECKS); + } + public int getLinEqMethod() - { return settings.getInteger(PrismSettings.PRISM_LIN_EQ_METHOD)+1; } //NOTE THE CORRECTION for the ChoiceSetting index - + { + return settings.getInteger(PrismSettings.PRISM_LIN_EQ_METHOD) + 1; + } //NOTE THE CORRECTION for the ChoiceSetting index + public double getLinEqMethodParam() - { return settings.getDouble(PrismSettings.PRISM_LIN_EQ_METHOD_PARAM); } - + { + return settings.getDouble(PrismSettings.PRISM_LIN_EQ_METHOD_PARAM); + } + public int getMDPSolnMethod() - { return settings.getInteger(PrismSettings.PRISM_MDP_SOLN_METHOD)+1; } //NOTE THE CORRECTION for the ChoiceSetting index - + { + return settings.getInteger(PrismSettings.PRISM_MDP_SOLN_METHOD) + 1; + } //NOTE THE CORRECTION for the ChoiceSetting index + public int getTermCrit() - { return settings.getInteger(PrismSettings.PRISM_TERM_CRIT)+1; } //NOTE THE CORRECTION for the ChoiceSetting index - + { + return settings.getInteger(PrismSettings.PRISM_TERM_CRIT) + 1; + } //NOTE THE CORRECTION for the ChoiceSetting index + public double getTermCritParam() - { return settings.getDouble(PrismSettings.PRISM_TERM_CRIT_PARAM); } - + { + return settings.getDouble(PrismSettings.PRISM_TERM_CRIT_PARAM); + } + public int getMaxIters() - { return settings.getInteger(PrismSettings.PRISM_MAX_ITERS); } - + { + return settings.getInteger(PrismSettings.PRISM_MAX_ITERS); + } + public boolean getVerbose() - { return settings.getBoolean(PrismSettings.PRISM_VERBOSE); } - + { + return settings.getBoolean(PrismSettings.PRISM_VERBOSE); + } + public boolean getPrecomp() - { return settings.getBoolean(PrismSettings.PRISM_PRECOMPUTATION); } - + { + return settings.getBoolean(PrismSettings.PRISM_PRECOMPUTATION); + } + public boolean getProb0() - { return settings.getBoolean(PrismSettings.PRISM_PROB0); } - + { + return settings.getBoolean(PrismSettings.PRISM_PROB0); + } + public boolean getProb1() - { return settings.getBoolean(PrismSettings.PRISM_PROB1); } - + { + return settings.getBoolean(PrismSettings.PRISM_PROB1); + } + public boolean getFairness() - { return settings.getBoolean(PrismSettings.PRISM_FAIRNESS); } - + { + return settings.getBoolean(PrismSettings.PRISM_FAIRNESS); + } + public int getSBMaxMem() - { return settings.getInteger(PrismSettings.PRISM_SB_MAX_MEM); } - + { + return settings.getInteger(PrismSettings.PRISM_SB_MAX_MEM); + } + public int getNumSBLevels() - { return settings.getInteger(PrismSettings.PRISM_NUM_SB_LEVELS); } - + { + return settings.getInteger(PrismSettings.PRISM_NUM_SB_LEVELS); + } + public int getSORMaxMem() - { return settings.getInteger(PrismSettings.PRISM_SOR_MAX_MEM); } - + { + return settings.getInteger(PrismSettings.PRISM_SOR_MAX_MEM); + } + public boolean getDoSSDetect() - { return settings.getBoolean(PrismSettings.PRISM_DO_SS_DETECTION); } - + { + return settings.getBoolean(PrismSettings.PRISM_DO_SS_DETECTION); + } + public boolean getExtraDDInfo() - { return settings.getBoolean(PrismSettings.PRISM_EXTRA_DD_INFO); } - + { + return settings.getBoolean(PrismSettings.PRISM_EXTRA_DD_INFO); + } + public boolean getExtraReachInfo() - { return settings.getBoolean(PrismSettings.PRISM_EXTRA_REACH_INFO); } - + { + return settings.getBoolean(PrismSettings.PRISM_EXTRA_REACH_INFO); + } + public int getNumSORLevels() - { return settings.getInteger(PrismSettings.PRISM_NUM_SOR_LEVELS); } - + { + return settings.getInteger(PrismSettings.PRISM_NUM_SOR_LEVELS); + } + public boolean getCompact() - { return settings.getBoolean(PrismSettings.PRISM_COMPACT); } - + { + return settings.getBoolean(PrismSettings.PRISM_COMPACT); + } + public long getCUDDMaxMem() - { return settings.getInteger(PrismSettings.PRISM_CUDD_MAX_MEM); } - + { + return settings.getInteger(PrismSettings.PRISM_CUDD_MAX_MEM); + } + public double getCUDDEpsilon() - { return settings.getDouble(PrismSettings.PRISM_CUDD_EPSILON); } - + { + return settings.getDouble(PrismSettings.PRISM_CUDD_EPSILON); + } + public int getSCCMethod() - { return settings.getInteger(PrismSettings.PRISM_SCC_METHOD)+1; } //NOTE THE CORRECTION for the ChoiceSetting index - + { + return settings.getInteger(PrismSettings.PRISM_SCC_METHOD) + 1; + } //NOTE THE CORRECTION for the ChoiceSetting index + public int getExportAdv() - { return settings.getInteger(PrismSettings.PRISM_EXPORT_ADV)+1; } //NOTE THE CORRECTION for the ChoiceSetting index - + { + return settings.getInteger(PrismSettings.PRISM_EXPORT_ADV) + 1; + } //NOTE THE CORRECTION for the ChoiceSetting index + public String getExportAdvFilename() - { return settings.getString(PrismSettings.PRISM_EXPORT_ADV_FILENAME); } - + { + return settings.getString(PrismSettings.PRISM_EXPORT_ADV_FILENAME); + } + // Get methods for miscellaneous options - + public boolean getExportTarget() - { return exportTarget; } - + { + return exportTarget; + } + public String getExportTargetFilename() - { return exportTargetFilename; } - + { + return exportTargetFilename; + } + public boolean getExportProductTrans() - { return exportProductTrans; } - + { + return exportProductTrans; + } + public String getExportProductTransFilename() - { return exportProductTransFilename; } - + { + return exportProductTransFilename; + } + public boolean getExportProductStates() - { return exportProductStates; } - + { + return exportProductStates; + } + public String getExportProductStatesFilename() - { return exportProductStatesFilename; } - + { + return exportProductStatesFilename; + } + public boolean getDoReach() - { return doReach; } - + { + return doReach; + } + public boolean getBSCCComp() - { return bsccComp; } - + { + return bsccComp; + } + public boolean getCheckZeroLoops() - { return this.checkZeroLoops; } - + { + return this.checkZeroLoops; + } + public int getConstruction() - { return construction; } - + { + return construction; + } + public int getOrdering() - { return ordering; } - + { + return ordering; + } + public double getSumRoundOff() - { return sumRoundOff; } - + { + return sumRoundOff; + } + // String methods for options - + public static String getEngineString(int engine) - { return engineStrings[engine]; } - + { + return engineStrings[engine]; + } + /** * Let PrismSettings object notify us things have changed */ public void notifySettings(PrismSettings settings) { - if (cuddStarted) - { + if (cuddStarted) { JDD.SetCUDDEpsilon(settings.getDouble(PrismSettings.PRISM_CUDD_EPSILON)); JDD.SetCUDDMaxMem(settings.getInteger(PrismSettings.PRISM_CUDD_MAX_MEM)); } @@ -603,40 +683,43 @@ public class Prism implements PrismSettingsListener //------------------------------------------------------------------------------ // Access to parser, simulator, etc. //------------------------------------------------------------------------------ - + /** * Get (exclusive) access to the PRISM parser. */ public static PrismParser getPrismParser() throws InterruptedException { // Note: this mutex mechanism is based on public domain code by Doug Lea - if (Thread.interrupted()) throw new InterruptedException(); + if (Thread.interrupted()) + throw new InterruptedException(); // this code is synchronized on the whole Prism class // (because this is a static method) synchronized (Prism.class) { try { // wait until parser is free - while (prismParserInUse) { Prism.class.wait(); } + while (prismParserInUse) { + Prism.class.wait(); + } // lock parser prismParserInUse = true; // return parser, creating anew if necessary - if (thePrismParser == null) thePrismParser = new PrismParser(); + if (thePrismParser == null) + thePrismParser = new PrismParser(); return thePrismParser; - } - catch (InterruptedException e) { + } catch (InterruptedException e) { Prism.class.notify(); throw e; } } } - + /** * Release (exclusive) access to the PRISM parser. */ public static synchronized void releasePrismParser() { prismParserInUse = false; - Prism.class.notify(); + Prism.class.notify(); } /** @@ -647,9 +730,9 @@ public class Prism implements PrismSettingsListener if (theSimulator == null) { theSimulator = new SimulatorEngine(this); } - return theSimulator; + return theSimulator; } - + /** * Get an SCCComputer object. * Type (i.e. algorithm) depends on SCCMethod PRISM option. @@ -658,7 +741,7 @@ public class Prism implements PrismSettingsListener { return getSCCComputer(model.getReach(), model.getTrans01(), model.getAllDDRowVars(), model.getAllDDColVars()); } - + /** * Get an SCCComputer object. * Type (i.e. algorithm) depends on SCCMethod PRISM option. @@ -681,11 +764,11 @@ public class Prism implements PrismSettingsListener } return sccComputer; } - + //------------------------------------------------------------------------------ // Utility methods //------------------------------------------------------------------------------ - + /** * Compare two version numbers of PRISM (strings). * Example ordering: { "1", "2.0", "2.1.alpha", "2.1.alpha.r5555", "2.1.alpha.r5557", "2.1.beta", "2.1.beta4", "2.1", "2.1.dev", "2.1.dev.r6666", "2.1.dev1", "2.1.dev2", "2.1.2", "2.9", "3", "3.4"}; @@ -697,9 +780,10 @@ public class Prism implements PrismSettingsListener int i, n, x; double s1 = 0, s2 = 0; boolean s1num, s2num; - + // Exactly equal - if (v1.equals(v2)) return 0; + if (v1.equals(v2)) + return 0; // Otherwise split into sections ss1 = v1.split("\\."); ss2 = v2.split("\\."); @@ -707,14 +791,18 @@ public class Prism implements PrismSettingsListener n = Math.max(ss1.length, ss2.length); if (ss1.length < n) { tmp = new String[n]; - for (i = 0; i < ss1.length; i++) tmp[i] = ss1[i]; - for (i = ss1.length; i < n; i++) tmp[i] = ""; + for (i = 0; i < ss1.length; i++) + tmp[i] = ss1[i]; + for (i = ss1.length; i < n; i++) + tmp[i] = ""; ss1 = tmp; } if (ss2.length < n) { tmp = new String[n]; - for (i = 0; i < ss2.length; i++) tmp[i] = ss2[i]; - for (i = ss2.length; i < n; i++) tmp[i] = ""; + for (i = 0; i < ss2.length; i++) + tmp[i] = ss2[i]; + for (i = ss2.length; i < n; i++) + tmp[i] = ""; ss2 = tmp; } // Loop through sections of string @@ -723,58 +811,123 @@ public class Prism implements PrismSettingsListener // 2.1.alpha < 2.1.alpha2 < 2.1.alpha3, etc. // so replace alphax with -10000+x if (ss1[i].matches("alpha.*")) { - try { if (ss1[i].length() == 5) x = 0; else x = Integer.parseInt(ss1[i].substring(5)); } catch (NumberFormatException e) { x = 0; } + try { + if (ss1[i].length() == 5) + x = 0; + else + x = Integer.parseInt(ss1[i].substring(5)); + } catch (NumberFormatException e) { + x = 0; + } ss1[i] = "" + (-10000 + x); } if (ss2[i].matches("alpha.*")) { - try { if (ss2[i].length() == 5) x = 0; else x = Integer.parseInt(ss2[i].substring(5)); } catch (NumberFormatException e) { x = 0; } + try { + if (ss2[i].length() == 5) + x = 0; + else + x = Integer.parseInt(ss2[i].substring(5)); + } catch (NumberFormatException e) { + x = 0; + } ss2[i] = "" + (-10000 + x); } // 2.1.beta < 2.1, etc. // 2.1.beta < 2.1.beta2 < 2.1.beta3, etc. // so replace betax with -100+x if (ss1[i].matches("beta.*")) { - try { if (ss1[i].length() == 4) x = 0; else x = Integer.parseInt(ss1[i].substring(4)); } catch (NumberFormatException e) { x = 0; } + try { + if (ss1[i].length() == 4) + x = 0; + else + x = Integer.parseInt(ss1[i].substring(4)); + } catch (NumberFormatException e) { + x = 0; + } ss1[i] = "" + (-100 + x); } if (ss2[i].matches("beta.*")) { - try { if (ss2[i].length() == 4) x = 0; else x = Integer.parseInt(ss2[i].substring(4)); } catch (NumberFormatException e) { x = 0; } + try { + if (ss2[i].length() == 4) + x = 0; + else + x = Integer.parseInt(ss2[i].substring(4)); + } catch (NumberFormatException e) { + x = 0; + } ss2[i] = "" + (-100 + x); } // 2 < 2.1, etc. // so treat 2 as 2.0 - if (ss1[i].equals("")) ss1[i] = "0"; - if (ss2[i].equals("")) ss2[i] = "0"; + if (ss1[i].equals("")) + ss1[i] = "0"; + if (ss2[i].equals("")) + ss2[i] = "0"; // 2.1 < 2.1.dev, etc. // 2.1.dev < 2.1.dev2 < 2.1.dev3, etc. // so replace devx with 0.5+x/1000 if (ss1[i].matches("dev.*")) { - try { if (ss1[i].length() == 3) x = 0; else x = Integer.parseInt(ss1[i].substring(3)); } catch (NumberFormatException e) { x = 0; } + try { + if (ss1[i].length() == 3) + x = 0; + else + x = Integer.parseInt(ss1[i].substring(3)); + } catch (NumberFormatException e) { + x = 0; + } ss1[i] = "" + (0.5 + x / 1000.0); } if (ss2[i].matches("dev.*")) { - try { if (ss2[i].length() == 3) x = 0; else x = Integer.parseInt(ss2[i].substring(3)); } catch (NumberFormatException e) { x = 0; } + try { + if (ss2[i].length() == 3) + x = 0; + else + x = Integer.parseInt(ss2[i].substring(3)); + } catch (NumberFormatException e) { + x = 0; + } ss2[i] = "" + (0.5 + x / 1000.0); } // replace rx (e.g. as in 4.0.alpha.r5555) with x if (ss1[i].matches("r.*")) { - try { x = Integer.parseInt(ss1[i].substring(1)); } catch (NumberFormatException e) { x = 0; } + try { + x = Integer.parseInt(ss1[i].substring(1)); + } catch (NumberFormatException e) { + x = 0; + } ss1[i] = "" + x; } if (ss2[i].matches("r.*")) { - try { x = Integer.parseInt(ss2[i].substring(1)); } catch (NumberFormatException e) { x = 0; } + try { + x = Integer.parseInt(ss2[i].substring(1)); + } catch (NumberFormatException e) { + x = 0; + } ss2[i] = "" + x; } // See if strings are integers - try { s1num = true; s1 = Double.parseDouble(ss1[i]); } catch (NumberFormatException e) { s1num = false; } - try { s2num = true; s2 = Double.parseDouble(ss2[i]); } catch (NumberFormatException e) { s2num = false; } + try { + s1num = true; + s1 = Double.parseDouble(ss1[i]); + } catch (NumberFormatException e) { + s1num = false; + } + try { + s2num = true; + s2 = Double.parseDouble(ss2[i]); + } catch (NumberFormatException e) { + s2num = false; + } if (s1num && s2num) { - if (s1 < s2) return -1; - if (s1 > s2) return 1; - if (s1 == s2) continue; + if (s1 < s2) + return -1; + if (s1 > s2) + return 1; + if (s1 == s2) + continue; } } - + return 0; } @@ -793,8 +946,8 @@ public class Prism implements PrismSettingsListener System.out.println(); } }*/ - - /** + + /** * Get access to the list of all PRISM language keywords. */ public static List getListOfKeyords() @@ -804,21 +957,19 @@ public class Prism implements PrismSettingsListener // (don't forget to release it afterwards) try { return getPrismParser().getListOfKeywords(); - } - finally { + } finally { // release prism parser releasePrismParser(); } - } - catch(InterruptedException ie) { + } catch (InterruptedException ie) { return null; } } - + //------------------------------------------------------------------------------ - // Main "API" methods + // Main API methods //------------------------------------------------------------------------------ - + /** * Initialise PRISM. */ @@ -832,23 +983,24 @@ public class Prism implements PrismSettingsListener try { String h = java.net.InetAddress.getLocalHost().getHostName(); mainLog.print("Hostname: " + h + "\n"); - } catch (java.net.UnknownHostException e) {} - + } catch (java.net.UnknownHostException e) { + } + // initialise cudd/jdd JDD.InitialiseCUDD(getCUDDMaxMem(), getCUDDEpsilon()); cuddStarted = true; JDD.SetOutputStream(techLog.getFilePointer()); - + // initialise all three engines PrismMTBDD.initialise(mainLog, techLog); PrismSparse.initialise(mainLog, techLog); PrismHybrid.initialise(mainLog, techLog); - + // set cudd manager in other packages DoubleVector.setCUDDManager(); ODDUtils.setCUDDManager(); } - + /** * Parse a PRISM model from a file. * @param file File to read in @@ -866,12 +1018,12 @@ public class Prism implements PrismSettingsListener public ModulesFile parseModelFile(File file, ModelType typeOverride) throws FileNotFoundException, PrismLangException { FileInputStream strModel; - PrismParser prismParser; + PrismParser prismParser; ModulesFile modulesFile = null; - + // open file strModel = new FileInputStream(file); - + try { // obtain exclusive access to the prism parser // (don't forget to release it afterwards) @@ -879,18 +1031,16 @@ public class Prism implements PrismSettingsListener try { // parse file modulesFile = prismParser.parseModulesFile(strModel, typeOverride); - } - finally { + } finally { // release prism parser releasePrismParser(); } - } - catch(InterruptedException ie) { + } catch (InterruptedException ie) { throw new PrismLangException("Concurrency error in parser"); } - + modulesFile.tidyUp(); - + return modulesFile; } @@ -902,7 +1052,7 @@ public class Prism implements PrismSettingsListener { return parseModelString(s, null); } - + /** * Parse a PRISM model from a string. * @param s String containing model @@ -910,9 +1060,9 @@ public class Prism implements PrismSettingsListener */ public ModulesFile parseModelString(String s, ModelType typeOverride) throws PrismLangException { - PrismParser prismParser; + PrismParser prismParser; ModulesFile modulesFile = null; - + try { // obtain exclusive access to the prism parser // (don't forget to release it afterwards) @@ -920,18 +1070,16 @@ public class Prism implements PrismSettingsListener try { // parse string modulesFile = prismParser.parseModulesFile(new ByteArrayInputStream(s.getBytes()), typeOverride); - } - finally { + } finally { // release prism parser releasePrismParser(); } - } - catch(InterruptedException ie) { + } catch (InterruptedException ie) { throw new PrismLangException("Concurrency error in parser"); } - + modulesFile.tidyUp(); - + return modulesFile; } @@ -942,19 +1090,18 @@ public class Prism implements PrismSettingsListener public ModulesFile importPepaFile(File file) throws PrismException, PrismLangException { String modelString; - + // compile pepa file to string try { modelString = pepa.compiler.Main.compile("" + file); - } - catch (pepa.compiler.InternalError e) { + } catch (pepa.compiler.InternalError e) { throw new PrismException("Could not import PEPA file:\n" + e.getMessage()); } - + // parse string as prism model and return return parseModelString(modelString); } - + /** * Import a PRISM model from a PEPA model in a string * @param s String containing model @@ -963,30 +1110,28 @@ public class Prism implements PrismSettingsListener { File pepaFile = null; String modelString; - + // create temporary file containing pepa model - try - { + try { pepaFile = File.createTempFile("tempPepa" + System.currentTimeMillis(), ".pepa"); FileWriter write = new FileWriter(pepaFile); write.write(s); write.close(); - } - catch(IOException e) - { - if(pepaFile != null) pepaFile.delete(); + } catch (IOException e) { + if (pepaFile != null) + pepaFile.delete(); throw new PrismException("Couldn't create temporary file for PEPA conversion"); } - + // compile pepa file to string try { modelString = pepa.compiler.Main.compile("" + pepaFile); - } - catch (pepa.compiler.InternalError e) { - if(pepaFile != null) pepaFile.delete(); + } catch (pepa.compiler.InternalError e) { + if (pepaFile != null) + pepaFile.delete(); throw new PrismException("Could not import PEPA file:\n" + e.getMessage()); } - + // parse string as prism model and return return parseModelString(modelString); } @@ -999,7 +1144,7 @@ public class Prism implements PrismSettingsListener public ModulesFile importPrismPreprocFile(File file, String params[]) throws PrismException { String modelString; - + // Compile preprocessor file to a string Preprocessor pp = new Preprocessor(this, file); pp.setParameters(params); @@ -1007,11 +1152,11 @@ public class Prism implements PrismSettingsListener if (modelString == null) { throw new PrismException("No preprocessing information"); } - + // Parse string as PRISM model and return return parseModelString(modelString); } - + /** * Parse a PRISM properties file. Typically, you need to pass in the corresponding PRISM model * (for access to constants, etc.) but if left null, a blank one is created automatically. @@ -1022,7 +1167,7 @@ public class Prism implements PrismSettingsListener { return parsePropertiesFile(mf, file, true); } - + /** * Parse a PRISM properties file. Typically, you need to pass in the corresponding PRISM model * (for access to constants, etc.) but if left null, a blank one is created automatically. @@ -1035,19 +1180,19 @@ public class Prism implements PrismSettingsListener public PropertiesFile parsePropertiesFile(ModulesFile mf, File file, boolean tidy) throws FileNotFoundException, PrismLangException { FileInputStream strProperties; - PrismParser prismParser; + PrismParser prismParser; PropertiesFile propertiesFile = null; - + // open file strProperties = new FileInputStream(file); - + // if null modules file passed, create a blank one if (mf == null) { mf = new ModulesFile(); mf.setFormulaList(new FormulaList()); mf.setConstantList(new ConstantList()); } - + try { // obtain exclusive access to the prism parser // (don't forget to release it afterwards) @@ -1055,18 +1200,17 @@ public class Prism implements PrismSettingsListener try { // parse file propertiesFile = prismParser.parsePropertiesFile(mf, strProperties); - } - finally { + } finally { // release prism parser releasePrismParser(); } - } - catch(InterruptedException ie) { + } catch (InterruptedException ie) { throw new PrismLangException("Concurrency error in parser"); } - - if (tidy) propertiesFile.tidyUp(); - + + if (tidy) + propertiesFile.tidyUp(); + return propertiesFile; } @@ -1078,16 +1222,16 @@ public class Prism implements PrismSettingsListener */ public PropertiesFile parsePropertiesString(ModulesFile mf, String s) throws PrismLangException { - PrismParser prismParser; + PrismParser prismParser; PropertiesFile propertiesFile = null; - + // if null modules file passed, create a blank one if (mf == null) { mf = new ModulesFile(); mf.setFormulaList(new FormulaList()); mf.setConstantList(new ConstantList()); } - + try { // obtain exclusive access to the prism parser // (don't forget to release it afterwards) @@ -1095,18 +1239,16 @@ public class Prism implements PrismSettingsListener try { // parse string propertiesFile = prismParser.parsePropertiesFile(mf, new ByteArrayInputStream(s.getBytes())); - } - finally { + } finally { // release prism parser releasePrismParser(); } - } - catch(InterruptedException ie) { + } catch (InterruptedException ie) { throw new PrismLangException("Concurrency error in parser"); } - + propertiesFile.tidyUp(); - + return propertiesFile; } @@ -1116,9 +1258,9 @@ public class Prism implements PrismSettingsListener */ public Expression parseSingleExpressionString(String s) throws PrismLangException { - PrismParser prismParser; + PrismParser prismParser; Expression expr; - + try { // obtain exclusive access to the prism parser // (don't forget to release it afterwards) @@ -1126,16 +1268,14 @@ public class Prism implements PrismSettingsListener try { // parse expression expr = prismParser.parseSingleExpression(new ByteArrayInputStream(s.getBytes())); - } - finally { + } finally { // release prism parser releasePrismParser(); } - } - catch(InterruptedException ie) { + } catch (InterruptedException ie) { throw new PrismLangException("Concurrency error in parser"); } - + return expr; } @@ -1145,9 +1285,9 @@ public class Prism implements PrismSettingsListener */ public ForLoop parseForLoopString(String s) throws PrismLangException { - PrismParser prismParser; + PrismParser prismParser; ForLoop fl; - + try { // obtain exclusive access to the prism parser // (don't forget to release it afterwards) @@ -1155,49 +1295,118 @@ public class Prism implements PrismSettingsListener try { // parse for loop fl = prismParser.parseForLoop(new ByteArrayInputStream(s.getBytes())); - } - finally { + } finally { // release prism parser releasePrismParser(); } - } - catch(InterruptedException ie) { + } catch (InterruptedException ie) { throw new PrismLangException("Concurrency error in parser"); } - + return fl; } /** - * Build a model from a PRISM modelling language description, storing it symbolically, - * as MTBDDs) via (MT)BDD-based reachability and model construction. - * It is assumed that all constants in the model file have been defined by now. - * @param modulesFile Model to build + * Load a (parsed) PRISM model, which will be stored and used for subsequent model checking etc. + * Some model constants can still be undefined at this stage. + * Pass in null to clear storage of the current PRISM model. + * @param modulesFile The PRISM model */ - public Model buildModel(ModulesFile modulesFile) throws PrismException + public void loadPRISMModel(ModulesFile modulesFile) + { + // Store PRISM model + currentModulesFile = modulesFile; + // Reset dependent info + currentModelType = currentModulesFile.getModelType(); + currentModel = null; + } + + /** + * Set any undefined constants for the currently loaded PRISM model. + * @param modulesFile The PRISM model + */ + public void setPRISMModelConstants(Values definedMFConstants) throws PrismLangException + { + // If non-null/non-empty, print new model constants to log + if (definedMFConstants != null && definedMFConstants.getNumValues() > 0) + mainLog.println("\nModel constants: " + definedMFConstants); + + // Set constant values in stored ModulesFile + currentModulesFile.setUndefinedConstants(definedMFConstants); + + // Reset dependent info + currentModel = null; + } + + /** + * Load a (built) model, with an accompanying (parsed) PRISM model. + * These will be stored and used for subsequent model checking etc. + * Pass in nulls to clear storage of the current model. + * @param modulesFile The PRISM model + */ + public void loadPRISMModelAndBuiltModel(ModulesFile modulesFile, Model model) + { + // Store model info + currentModulesFile = modulesFile; + currentModel = model; + // Reset dependent info + currentModelType = currentModulesFile.getModelType(); + } + + /** + * Load a (built) model, without an accompanying (parsed) PRISM model. + * The model will be stored and used for subsequent model checking etc. + * Pass in null to clear storage of the current model. + * @param modulesFile The PRISM model + */ + public void loadBuiltModel(Model model) + { + // Store model info + currentModulesFile = null; + currentModel = model; + // Reset dependent info + currentModelType = currentModel.getModelType(); + } + + /** + * Get the currently stored built model. + * @return + */ + public Model getBuiltModel() + { + return currentModel; + } + + /** + * Build the currently loaded PRISM model and store for later use. + * The build model can be accessed subsequently via {@link #getBuiltModel()}. + * Reachability and model construction are done symbolically, i.e. using (MT)BDDs. + */ + public void buildModel() throws PrismException { long l; // timer - Model model; - - if (modulesFile.getModelType() == ModelType.PTA) { + Modules2MTBDD mod2mtbdd = null; + + if (currentModulesFile == null) + throw new PrismException("There is no currently loaded PRISM model to build"); + + if (currentModelType == ModelType.PTA) { throw new PrismException("You cannot build a PTA model explicitly, only perform model checking"); } - + mainLog.print("\nBuilding model...\n"); - + // create translator - mod2mtbdd = new Modules2MTBDD(this, modulesFile); - + mod2mtbdd = new Modules2MTBDD(this, currentModulesFile); + // build model l = System.currentTimeMillis(); - model = mod2mtbdd.translate(); + currentModel = mod2mtbdd.translate(); l = System.currentTimeMillis() - l; - - mainLog.println("\nTime for model construction: " + l/1000.0 + " seconds."); - - return model; + + mainLog.println("\nTime for model construction: " + l / 1000.0 + " seconds."); } - + /** * Builds a ModulesFile from files containing an explicit list of transitions/etc. * This is step 1 of the process; {@link #buildExplicitModel} should be called subsequently. @@ -1211,11 +1420,11 @@ public class Prism implements PrismSettingsListener { // create ExplicitFiles2MTBDD object expf2mtbdd = new ExplicitFiles2MTBDD(this, statesFile, transFile, labelsFile, typeOverride); - + // build state space return expf2mtbdd.buildStates(); } - + /** * Builds a model from files containing an explicit list of transitions/etc. * This is step 2 of the process; {@link #parseExplicitModel} should have been called first. @@ -1224,22 +1433,23 @@ public class Prism implements PrismSettingsListener { long l; // timer Model model; - + // check ExplicitFiles2MTBDD object created - if (expf2mtbdd == null) throw new PrismException("ExplicitFiles2MTBDD object never created"); - + if (expf2mtbdd == null) + throw new PrismException("ExplicitFiles2MTBDD object never created"); + mainLog.print("\nBuilding model...\n"); - + // build model l = System.currentTimeMillis(); model = expf2mtbdd.buildModel(); l = System.currentTimeMillis() - l; - - mainLog.println("\nTime for model construction: " + l/1000.0 + " seconds."); - + + mainLog.println("\nTime for model construction: " + l / 1000.0 + " seconds."); + return model; } - + /** * Build a model from a PRISM modelling language description, storing it symbolically, * as MTBDDs) via explicit-state reachability and model construction. @@ -1253,132 +1463,147 @@ public class Prism implements PrismSettingsListener explicit.Model modelExpl; Model model; List statesList; - + if (modulesFile.getModelType() == ModelType.PTA) { throw new PrismException("You cannot build a PTA model explicitly, only perform model checking"); } - + mainLog.print("\nBuilding model...\n"); - + constructModel = new ConstructModel(getSimulator(), mainLog); modelExpl = constructModel.constructModel(modulesFile); statesList = constructModel.getStatesList(); - + // create Explicit2MTBDD object expm2mtbdd = new ExplicitModel2MTBDD(this); - + // build model l = System.currentTimeMillis(); model = expm2mtbdd.buildModel(modelExpl, statesList, modulesFile, false); l = System.currentTimeMillis() - l; - - mainLog.println("\nTime for model construction: " + l/1000.0 + " seconds."); - + + mainLog.println("\nTime for model construction: " + l / 1000.0 + " seconds."); + return model; } - - // export trans to a spy file - - public void exportToSpyFile(Model model, File file) throws FileNotFoundException + + /** + * Export the currently loaded model's transition matrix to a Spy file. + * @param file File to export to + */ + public void exportToSpyFile(File file) throws FileNotFoundException, PrismException { int depth; JDDNode tmp; - + + // Build model, if necessary + if (currentModel == null) + buildModel(currentModulesFile); + mainLog.println("\nExporting to spy file \"" + file + "\"..."); - + // choose depth - depth = model.getAllDDRowVars().n(); - if (depth > 9) depth = 9; - + depth = currentModel.getAllDDRowVars().n(); + if (depth > 9) + depth = 9; + // get rid of non det vars if necessary - tmp = model.getTrans(); + tmp = currentModel.getTrans(); JDD.Ref(tmp); - if (model.getModelType() == ModelType.MDP) - { - tmp = JDD.MaxAbstract(tmp, ((NondetModel)model).getAllDDNondetVars()); + if (currentModelType == ModelType.MDP) { + tmp = JDD.MaxAbstract(tmp, ((NondetModel) currentModel).getAllDDNondetVars()); } - + // export to spy file - JDD.ExportMatrixToSpyFile(tmp, model.getAllDDRowVars(), model.getAllDDColVars(), depth, file.getPath()); + JDD.ExportMatrixToSpyFile(tmp, currentModel.getAllDDRowVars(), currentModel.getAllDDColVars(), depth, file.getPath()); JDD.Deref(tmp); } - + /** - * Export the MTBDD for a model's transition matrix to a Dot file. + * Export the MTBDD for the currently loaded model's transition matrix to a Dot file. + * @param file File to export to */ - public void exportToDotFile(Model model, File file) throws FileNotFoundException + public void exportToDotFile(File file) throws FileNotFoundException, PrismException { + // Build model, if necessary + if (currentModel == null) + buildModel(currentModulesFile); + mainLog.println("\nExporting to dot file \"" + file + "\"..."); - + // export to dot file - JDD.ExportDDToDotFileLabelled(model.getTrans(), file.getPath(), model.getDDVarNames()); + JDD.ExportDDToDotFileLabelled(currentModel.getTrans(), file.getPath(), currentModel.getDDVarNames()); } - - /** - * Export a model's transition matrix to a file - * @param model The model - * @param ordered Ensure that (source) states are in ascending order? - * @param exportType Type of export; one of: - * @param file File to export to - */ - public void exportToFile(Model model, boolean ordered, int exportType, File file) throws FileNotFoundException, PrismException - { exportTransToFile(model, ordered, exportType, file); } - + /** - * Export a model's transition matrix to a file (or to the log) - * @param model The model + * Export the currently loaded model's transition matrix to a file (or to the log) * @param ordered Ensure that (source) states are in ascending order? * @param exportType Type of export; one of: * @param file File to export to (if null, print to the log instead) */ - public void exportTransToFile(Model model, boolean ordered, int exportType, File file) throws FileNotFoundException, PrismException + public void exportTransToFile(boolean ordered, int exportType, File file) throws FileNotFoundException, PrismException { // can only do ordered version of export for MDPs - if (model.getModelType() == ModelType.MDP) { - if (!ordered) mainLog.printWarning("Cannot export unordered transition matrix for MDPs; using ordered."); + if (currentModelType == ModelType.MDP) { + if (!ordered) + mainLog.printWarning("Cannot export unordered transition matrix for MDPs; using ordered."); ordered = true; } // can only do ordered version of export for MRMC if (exportType == EXPORT_MRMC) { - if (!ordered) mainLog.printWarning("Cannot export unordered transition matrix in MRMC format; using ordered."); + if (!ordered) + mainLog.printWarning("Cannot export unordered transition matrix in MRMC format; using ordered."); ordered = true; } // can only do ordered version of export for rows format if (exportType == EXPORT_ROWS) { - if (!ordered) mainLog.printWarning("Cannot export unordered transition matrix in rows format; using ordered."); + if (!ordered) + mainLog.printWarning("Cannot export unordered transition matrix in rows format; using ordered."); ordered = true; } - + + // Build model, if necessary + if (currentModel == null) + buildModel(currentModulesFile); + // print message mainLog.print("\nExporting transition matrix "); switch (exportType) { - case EXPORT_PLAIN: mainLog.print("in plain text format "); break; - case EXPORT_MATLAB: mainLog.print("in Matlab format "); break; - case EXPORT_DOT: mainLog.print("in Dot format "); break; - case EXPORT_MRMC: mainLog.print("in MRMC format "); break; - case EXPORT_ROWS: mainLog.print("in rows format "); break; - case EXPORT_DOT_STATES: mainLog.print("in Dot format (with states) "); break; + case EXPORT_PLAIN: + mainLog.print("in plain text format "); + break; + case EXPORT_MATLAB: + mainLog.print("in Matlab format "); + break; + case EXPORT_DOT: + mainLog.print("in Dot format "); + break; + case EXPORT_MRMC: + mainLog.print("in MRMC format "); + break; + case EXPORT_ROWS: + mainLog.print("in rows format "); + break; + case EXPORT_DOT_STATES: + mainLog.print("in Dot format (with states) "); + break; } - if (file != null) mainLog.println("to file \"" + file + "\"..."); else mainLog.println("below:"); - + if (file != null) + mainLog.println("to file \"" + file + "\"..."); + else + mainLog.println("below:"); + // do export - model.exportToFile(exportType, ordered, file); - - // for export to dotm with states, need to do a bit more + currentModel.exportToFile(exportType, ordered, file); + + // for export to dot with states, need to do a bit more if (exportType == EXPORT_DOT_STATES) { // open (appending to) existing new file log or use main log PrismLog tmpLog; @@ -1391,78 +1616,134 @@ public class Prism implements PrismSettingsListener tmpLog = mainLog; } // insert states info into dot file - model.getReachableStates().printDot(tmpLog); + currentModel.getReachableStates().printDot(tmpLog); // print footer tmpLog.println("}"); // tidy up - if (file != null) tmpLog.close(); + if (file != null) + tmpLog.close(); } } - // export state rewards to a file (plain, matlab, ...) - - public void exportStateRewardsToFile(Model model, int exportType, File file) throws FileNotFoundException, PrismException + /** + * Export the currently loaded model's state rewards to a file + * @param exportType Type of export; one of: + * @param file File to export to (if null, print to the log instead) + */ + public void exportStateRewardsToFile(int exportType, File file) throws FileNotFoundException, PrismException { String s; - + // rows format does not apply to vectors - if (exportType == EXPORT_ROWS) exportType = EXPORT_PLAIN; - + if (exportType == EXPORT_ROWS) + exportType = EXPORT_PLAIN; + + // Build model, if necessary + if (currentModel == null) + buildModel(currentModulesFile); + // print message mainLog.print("\nExporting state rewards vector "); switch (exportType) { - case EXPORT_PLAIN: mainLog.print("in plain text format "); break; - case EXPORT_MATLAB: mainLog.print("in Matlab format "); break; - case EXPORT_MRMC: mainLog.print("in MRMC format "); break; + case EXPORT_PLAIN: + mainLog.print("in plain text format "); + break; + case EXPORT_MATLAB: + mainLog.print("in Matlab format "); + break; + case EXPORT_MRMC: + mainLog.print("in MRMC format "); + break; } - if (file != null) mainLog.println("to file \"" + file + "\"..."); else mainLog.println("below:"); - + if (file != null) + mainLog.println("to file \"" + file + "\"..."); + else + mainLog.println("below:"); + // do export - s = model.exportStateRewardsToFile(exportType, file); - if (s != null) mainLog.println("Rewards exported to files: "+s); + s = currentModel.exportStateRewardsToFile(exportType, file); + if (s != null) + mainLog.println("Rewards exported to files: " + s); } - // export transition rewards to a file (plain, matlab, ...) - - public void exportTransRewardsToFile(Model model, boolean ordered, int exportType, File file) throws FileNotFoundException, PrismException + /** + * Export the currently loaded model's transition rewards to a file + * @param ordered Ensure that (source) states are in ascending order? + * @param exportType Type of export; one of: + * @param file File to export to (if null, print to the log instead) + */ + public void exportTransRewardsToFile(boolean ordered, int exportType, File file) throws FileNotFoundException, PrismException { String s; - + // can only do ordered version of export for MDPs - if (model.getModelType() == ModelType.MDP) { - if (!ordered) mainLog.printWarning("Cannot export unordered transition reward matrix for MDPs; using ordered."); + if (currentModelType == ModelType.MDP) { + if (!ordered) + mainLog.printWarning("Cannot export unordered transition reward matrix for MDPs; using ordered."); ordered = true; } // can only do ordered version of export for MRMC if (exportType == EXPORT_MRMC) { - if (!ordered) mainLog.printWarning("Cannot export unordered transition reward matrix in MRMC format; using ordered."); + if (!ordered) + mainLog.printWarning("Cannot export unordered transition reward matrix in MRMC format; using ordered."); ordered = true; } // can only do ordered version of export for rows format if (exportType == EXPORT_ROWS) { - if (!ordered) mainLog.printWarning("Cannot export unordered transition matrix in rows format; using ordered."); + if (!ordered) + mainLog.printWarning("Cannot export unordered transition matrix in rows format; using ordered."); ordered = true; } - + + // Build model, if necessary + if (currentModel == null) + buildModel(currentModulesFile); + // print message mainLog.print("\nExporting transition rewards matrix "); switch (exportType) { - case EXPORT_PLAIN: mainLog.print("in plain text format "); break; - case EXPORT_MATLAB: mainLog.print("in Matlab format "); break; - case EXPORT_MRMC: mainLog.print("in MRMC format "); break; - case EXPORT_ROWS: mainLog.print("in rows format "); break; + case EXPORT_PLAIN: + mainLog.print("in plain text format "); + break; + case EXPORT_MATLAB: + mainLog.print("in Matlab format "); + break; + case EXPORT_MRMC: + mainLog.print("in MRMC format "); + break; + case EXPORT_ROWS: + mainLog.print("in rows format "); + break; } - if (file != null) mainLog.println("to file \"" + file + "\"..."); else mainLog.println("below:"); - + if (file != null) + mainLog.println("to file \"" + file + "\"..."); + else + mainLog.println("below:"); + // do export - s = model.exportTransRewardsToFile(exportType, ordered, file); - if (s != null) mainLog.println("Rewards exported to files: "+s); + s = currentModel.exportTransRewardsToFile(exportType, ordered, file); + if (s != null) + mainLog.println("Rewards exported to files: " + s); } - // export states list to a file (plain, matlab, ...) - // file == null mean export to log - - public void exportBSCCsToFile(Model model, int exportType, File file) throws FileNotFoundException + /** + * Export the currently loaded model's bottom strongly connected components (BSCCs) to a file + * @param exportType Type of export; one of: + * @param file File to export to (if null, print to the log instead) + */ + public void exportBSCCsToFile(int exportType, File file) throws FileNotFoundException, PrismException { int i, n; long l; // timer @@ -1470,30 +1751,43 @@ public class Prism implements PrismSettingsListener SCCComputer sccComputer; Vector bsccs; JDDNode not, bscc; - + // no specific states format for MRMC - if (exportType == EXPORT_MRMC) exportType = EXPORT_PLAIN; + if (exportType == EXPORT_MRMC) + exportType = EXPORT_PLAIN; // rows format does not apply to states output - if (exportType == EXPORT_ROWS) exportType = EXPORT_PLAIN; - + if (exportType == EXPORT_ROWS) + exportType = EXPORT_PLAIN; + + // Build model, if necessary + if (currentModel == null) + buildModel(currentModulesFile); + // Compute BSCCs mainLog.println("\nComputing BSCCs..."); - sccComputer = getSCCComputer(model); + sccComputer = getSCCComputer(currentModel); l = System.currentTimeMillis(); sccComputer.computeBSCCs(); l = System.currentTimeMillis() - l; bsccs = sccComputer.getVectBSCCs(); not = sccComputer.getNotInBSCCs(); - mainLog.println("\nTime for BSCC computation: " + l/1000.0 + " seconds."); - + mainLog.println("\nTime for BSCC computation: " + l / 1000.0 + " seconds."); + // print message mainLog.print("\nExporting BSCCs "); switch (exportType) { - case EXPORT_PLAIN: mainLog.print("in plain text format "); break; - case EXPORT_MATLAB: mainLog.print("in Matlab format "); break; + 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 (file != null) + mainLog.println("to file \"" + file + "\"..."); + else + mainLog.println("below:"); + // create new file log or use main log if (file != null) { tmpLog = new PrismFileLog(file.getPath()); @@ -1503,42 +1797,55 @@ public class Prism implements PrismSettingsListener } else { tmpLog = mainLog; } - + // print header: list of model vars - if (exportType == EXPORT_MATLAB) tmpLog.print("% "); + if (exportType == EXPORT_MATLAB) + tmpLog.print("% "); tmpLog.print("Variables: ("); - for (i = 0; i < model.getNumVars(); i++) { - tmpLog.print(model.getVarName(i)); - if (i < model.getNumVars()-1) tmpLog.print(","); + for (i = 0; i < currentModel.getNumVars(); i++) { + tmpLog.print(currentModel.getVarName(i)); + if (i < currentModel.getNumVars() - 1) + tmpLog.print(","); } tmpLog.println(")"); - + // print states for each bscc n = bsccs.size(); for (i = 0; i < n; i++) { tmpLog.println(); - if (exportType == EXPORT_MATLAB) tmpLog.print("% "); - tmpLog.println("BSCC "+(i+1)+"/"+n+":"); - if (exportType == EXPORT_MATLAB) tmpLog.println("bscc"+(i+1)+"=["); + if (exportType == EXPORT_MATLAB) + tmpLog.print("% "); + tmpLog.println("BSCC " + (i + 1) + "/" + n + ":"); + if (exportType == EXPORT_MATLAB) + tmpLog.println("bscc" + (i + 1) + "=["); bscc = bsccs.get(i); if (exportType != EXPORT_MATLAB) - new StateListMTBDD(bscc, model).print(tmpLog); + new StateListMTBDD(bscc, currentModel).print(tmpLog); else - new StateListMTBDD(bscc, model).printMatlab(tmpLog); - if (exportType == EXPORT_MATLAB) tmpLog.println("];"); + new StateListMTBDD(bscc, currentModel).printMatlab(tmpLog); + if (exportType == EXPORT_MATLAB) + tmpLog.println("];"); JDD.Deref(bscc); } - + JDD.Deref(not); - + // tidy up - if (file != null) tmpLog.close(); + if (file != null) + tmpLog.close(); } - // export labels and satisfying states to a file - // file == null mean export to log - - public void exportLabelsToFile(Model model, ModulesFile modulesFile, PropertiesFile propertiesFile, int exportType, File file) throws FileNotFoundException, PrismException + /** + * Export the states satisfying labels from the currently loaded model and a properties file to a file. + * The PropertiesFile should correspond to the currently loaded model. + * @param propertiesFile The properties file (for further labels) + * @param exportType Type of export; one of:
    + *
  • {@link #EXPORT_PLAIN} + *
  • {@link #EXPORT_MATLAB} + *
+ * @param file File to export to (if null, print to the log instead) + */ + public void exportLabelsToFile(PropertiesFile propertiesFile, int exportType, File file) throws FileNotFoundException, PrismException { int i, n; LabelList ll; @@ -1546,67 +1853,96 @@ public class Prism implements PrismSettingsListener StateModelChecker mc = null; JDDNode dd, labels[]; String labelNames[]; - + // get label list and size if (propertiesFile == null) { - ll = modulesFile.getLabelList(); + ll = currentModulesFile.getLabelList(); n = ll.size(); } else { ll = propertiesFile.getCombinedLabelList(); n = ll.size(); } - + + // Build model, if necessary + if (currentModel == null) + buildModel(currentModulesFile); + // print message mainLog.print("\nExporting labels and satisfying states "); - if (file != null) mainLog.println("to file \"" + file + "\"..."); else mainLog.println("below:"); - + if (file != null) + mainLog.println("to file \"" + file + "\"..."); + else + mainLog.println("below:"); + // convert labels to bdds if (n > 0) { - mc = new StateModelChecker(this, model, propertiesFile); + mc = new StateModelChecker(this, currentModel, propertiesFile); } - labels = new JDDNode[n+2]; - labels[0] = model.getStart(); - labels[1] = model.getFixedDeadlocks(); + labels = new JDDNode[n + 2]; + labels[0] = currentModel.getStart(); + labels[1] = currentModel.getFixedDeadlocks(); for (i = 0; i < n; i++) { expr = ll.getLabel(i); dd = mc.checkExpressionDD(expr); - labels[i+2] = dd; + labels[i + 2] = dd; } // put names for labels in an array - labelNames = new String[n+2]; + labelNames = new String[n + 2]; labelNames[0] = "init"; labelNames[1] = "deadlock"; for (i = 0; i < n; i++) { - labelNames[i+2] = ll.getLabelName(i); + labelNames[i + 2] = ll.getLabelName(i); } - + // export them to a file - PrismMTBDD.ExportLabels(labels, labelNames, "l", model.getAllDDRowVars(), model.getODD(), exportType, (file != null)?file.getPath():null); - + PrismMTBDD.ExportLabels(labels, labelNames, "l", currentModel.getAllDDRowVars(), currentModel.getODD(), exportType, (file != null) ? file.getPath() + : null); + // deref dds for (i = 0; i < n; i++) { - JDD.Deref(labels[i+2]); + JDD.Deref(labels[i + 2]); } } - public void exportStatesToFile(Model model, int exportType, File file) throws FileNotFoundException + /** + * Export the currently loaded model's states to a file + * @param exportType Type of export; one of:
    + *
  • {@link #EXPORT_PLAIN} + *
  • {@link #EXPORT_MATLAB} + *
+ * @param file File to export to (if null, print to the log instead) + */ + public void exportStatesToFile(int exportType, File file) throws FileNotFoundException, PrismException { int i; PrismLog tmpLog; - + // no specific states format for MRMC - if (exportType == EXPORT_MRMC) exportType = EXPORT_PLAIN; + if (exportType == EXPORT_MRMC) + exportType = EXPORT_PLAIN; // rows format does not apply to states output - if (exportType == EXPORT_ROWS) exportType = EXPORT_PLAIN; - + if (exportType == EXPORT_ROWS) + exportType = EXPORT_PLAIN; + + // Build model, if necessary + if (currentModel == null) + buildModel(currentModulesFile); + // print message mainLog.print("\nExporting list of reachable states "); switch (exportType) { - case EXPORT_PLAIN: mainLog.print("in plain text format "); break; - case EXPORT_MATLAB: mainLog.print("in Matlab format "); break; + 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 (file != null) + mainLog.println("to file \"" + file + "\"..."); + else + mainLog.println("below:"); + // create new file log or use main log if (file != null) { tmpLog = new PrismFileLog(file.getPath()); @@ -1616,65 +1952,74 @@ public class Prism implements PrismSettingsListener } else { tmpLog = mainLog; } - + // print header: list of model vars - if (exportType == EXPORT_MATLAB) tmpLog.print("% "); + if (exportType == EXPORT_MATLAB) + tmpLog.print("% "); tmpLog.print("("); - for (i = 0; i < model.getNumVars(); i++) { - tmpLog.print(model.getVarName(i)); - if (i < model.getNumVars()-1) tmpLog.print(","); + for (i = 0; i < currentModel.getNumVars(); i++) { + tmpLog.print(currentModel.getVarName(i)); + if (i < currentModel.getNumVars() - 1) + tmpLog.print(","); } tmpLog.println(")"); - if (exportType == EXPORT_MATLAB) tmpLog.println("states=["); - + if (exportType == EXPORT_MATLAB) + tmpLog.println("states=["); + // print states if (exportType != EXPORT_MATLAB) - model.getReachableStates().print(tmpLog); + currentModel.getReachableStates().print(tmpLog); else - model.getReachableStates().printMatlab(tmpLog); - + currentModel.getReachableStates().printMatlab(tmpLog); + // print footer - if (exportType == EXPORT_MATLAB) tmpLog.println("];"); - + if (exportType == EXPORT_MATLAB) + tmpLog.println("];"); + // tidy up - if (file != null) tmpLog.close(); + if (file != null) + tmpLog.close(); } - + /** - * Perform model checking of a property on a model and return result. - * @param model The model (DTMC, CTMC or MDP) + * Perform model checking of a property on the currently loaded model and return result. * @param propertiesFile Parent property file of property (for labels/constants/...) - * @param expr The property + * @param expr The property to check */ - public Result modelCheck(Model model, PropertiesFile propertiesFile, Expression expr) throws PrismException, PrismLangException + public Result modelCheck(PropertiesFile propertiesFile, Expression expr) throws PrismException, PrismLangException { ModelChecker mc = null; Result res; - - // Check that property is valid for this model type - // and create new model checker object - expr.checkValid(model.getModelType()); - switch (model.getModelType()) { + + // Check that property is valid for the current model type + expr.checkValid(currentModelType); + + // Build model, if necessary + if (currentModel == null) + buildModel(currentModulesFile); + + // Create new model checker object + switch (currentModelType) { case DTMC: - mc = new ProbModelChecker(this, model, propertiesFile); + mc = new ProbModelChecker(this, currentModel, propertiesFile); break; case MDP: - mc = new NondetModelChecker(this, model, propertiesFile); + mc = new NondetModelChecker(this, currentModel, propertiesFile); break; case CTMC: - mc = new StochModelChecker(this, model, propertiesFile); + mc = new StochModelChecker(this, currentModel, propertiesFile); break; default: - throw new PrismException("Unknown model type"+model.getModelType()); + throw new PrismException("Unknown model type " + currentModelType); } - + // Do model checking res = mc.check(expr); - + // Return result return res; } - + /** * Perform model checking of a property on a PTA model and return result. * @param modulesFile The PTA model (language-level) @@ -1685,17 +2030,17 @@ public class Prism implements PrismSettingsListener { PTAModelChecker mcPta; Result res; - + // Check that property is valid for this model type // and create new model checker object expr.checkValid(modulesFile.getModelType()); mcPta = new PTAModelChecker(this, modulesFile, propertiesFile); // Do model checking res = mcPta.check(expr); - + return res; } - + /** * Check if a property is suitable for analysis with the simulator. * If not, an explanatory exception is thrown. @@ -1705,7 +2050,7 @@ public class Prism implements PrismSettingsListener { getSimulator().checkPropertyForSimulation(expr); } - + /** * Perform approximate model checking of a property on a model, using the simulator. * Sampling starts from the initial state provided or, if null, the default @@ -1719,19 +2064,20 @@ public class Prism implements PrismSettingsListener * @param maxPathLength The maximum path length for sampling * @param simMethod Object specifying details of method to use for simulation */ - public Result modelCheckSimulator(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression expr, State initialState, int maxPathLength, SimulationMethod simMethod) throws PrismException + public Result modelCheckSimulator(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression expr, State initialState, int maxPathLength, + SimulationMethod simMethod) throws PrismException { Object res = null; - + // Check that property is valid for this model type expr.checkValid(modulesFile.getModelType()); - + // Do model checking res = getSimulator().modelCheckSingleProperty(modulesFile, propertiesFile, expr, initialState, maxPathLength, simMethod); - + return new Result(res); } - + /** * Perform approximate model checking of several properties (simultaneously) on a model, using the simulator. * Sampling starts from the initial state provided or, if null, the default @@ -1746,22 +2092,24 @@ public class Prism implements PrismSettingsListener * @param maxPathLength The maximum path length for sampling * @param simMethod Object specifying details of method to use for simulation */ - public Result[] modelCheckSimulatorSimultaneously(ModulesFile modulesFile, PropertiesFile propertiesFile, List exprs, State initialState, int maxPathLength, SimulationMethod simMethod) throws PrismException + public Result[] modelCheckSimulatorSimultaneously(ModulesFile modulesFile, PropertiesFile propertiesFile, List exprs, State initialState, + int maxPathLength, SimulationMethod simMethod) throws PrismException { Object[] res = null; - + // Check that properties are valid for this model type for (Expression expr : exprs) expr.checkValid(modulesFile.getModelType()); - + // Do model checking res = getSimulator().modelCheckMultipleProperties(modulesFile, propertiesFile, exprs, initialState, maxPathLength, simMethod); - + Result[] resArray = new Result[res.length]; - for (int i = 0; i < res.length; i++) resArray[i] = new Result(res[i]); + for (int i = 0; i < res.length; i++) + resArray[i] = new Result(res[i]); return resArray; } - + /** * Perform an approximate model checking experiment on a model, using the simulator. * Perform an approximate model checking experiment on a model, using the simulator @@ -1783,11 +2131,13 @@ public class Prism implements PrismSettingsListener * @throws PrismException if something goes wrong with the sampling algorithm * @throws InterruptedException if the thread is interrupted */ - public void modelCheckSimulatorExperiment(ModulesFile modulesFile, PropertiesFile propertiesFile, UndefinedConstants undefinedConstants, ResultsCollection results, Expression propertyToCheck, State initialState, int pathLength, SimulationMethod simMethod) throws PrismException, InterruptedException + public void modelCheckSimulatorExperiment(ModulesFile modulesFile, PropertiesFile propertiesFile, UndefinedConstants undefinedConstants, + ResultsCollection results, Expression propertyToCheck, State initialState, int pathLength, SimulationMethod simMethod) throws PrismException, + InterruptedException { getSimulator().modelCheckExperiment(modulesFile, propertiesFile, undefinedConstants, results, propertyToCheck, initialState, pathLength, simMethod); } - + /** * Generate a random path through the model using the simulator. * @param modulesFile The model @@ -1800,61 +2150,75 @@ public class Prism implements PrismSettingsListener GenerateSimulationPath genPath = new GenerateSimulationPath(getSimulator(), mainLog); genPath.generateSimulationPath(modulesFile, null, details, maxPathLength, file); } - + /** - * Compute steady-state probabilities (for a DTMC or CTMC). + * Compute steady-state probabilities for the current model (DTMCs/CTMCs only). * Output probability distribution to log. */ - public void doSteadyState(Model model) throws PrismException + public void doSteadyState() throws PrismException { - doSteadyState(model, EXPORT_PLAIN, null); + doSteadyState(EXPORT_PLAIN, null); } - + /** - * Compute steady-state probabilities (for a DTMC or CTMC). + * Compute steady-state probabilities for the current model (DTMCs/CTMCs only). * Output probability distribution to a file (or, if file is null, to log). * The exportType should be EXPORT_PLAIN or EXPORT_MATLAB. */ - public void doSteadyState(Model model, int exportType, File fileOut) throws PrismException + public void doSteadyState(int exportType, File fileOut) throws PrismException { long l = 0; // timer ModelChecker mc = null; StateValues probs = null; PrismLog tmpLog; - + + if (!(currentModelType == ModelType.CTMC || currentModelType == ModelType.DTMC)) + throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs"); + if (fileOut != null && getEngine() == MTBDD) throw new PrismException("Steady-state probability export only supported for sparse/hybrid engines"); - + + // Build model, if necessary + if (currentModel == null) + buildModel(currentModulesFile); + // no specific states format for MRMC - if (exportType == EXPORT_MRMC) exportType = EXPORT_PLAIN; + if (exportType == EXPORT_MRMC) + exportType = EXPORT_PLAIN; // rows format does not apply to states output - if (exportType == EXPORT_ROWS) exportType = EXPORT_PLAIN; - + if (exportType == EXPORT_ROWS) + exportType = EXPORT_PLAIN; + mainLog.println("\nComputing steady-state probabilities..."); l = System.currentTimeMillis(); - if (model.getModelType() == ModelType.DTMC) { - mc = new ProbModelChecker(this, model, null); - probs = ((ProbModelChecker)mc).doSteadyState(); - } - else if (model.getModelType() == ModelType.CTMC) { - mc = new StochModelChecker(this, model, null); - probs = ((StochModelChecker)mc).doSteadyState(); - } - else { + if (currentModel.getModelType() == ModelType.DTMC) { + mc = new ProbModelChecker(this, currentModel, null); + probs = ((ProbModelChecker) mc).doSteadyState(); + } else if (currentModel.getModelType() == ModelType.CTMC) { + mc = new StochModelChecker(this, currentModel, null); + probs = ((StochModelChecker) mc).doSteadyState(); + } else { throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs"); } - + l = System.currentTimeMillis() - l; - + // print message mainLog.print("\nPrinting steady-state probabilities "); switch (exportType) { - case EXPORT_PLAIN: mainLog.print("in plain text format "); break; - case EXPORT_MATLAB: mainLog.print("in Matlab format "); break; + case EXPORT_PLAIN: + mainLog.print("in plain text format "); + break; + case EXPORT_MATLAB: + mainLog.print("in Matlab format "); + break; } - if (fileOut != null) mainLog.println("to file \"" + fileOut + "\"..."); 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 (fileOut != null) { tmpLog = new PrismFileLog(fileOut.getPath()); @@ -1864,76 +2228,90 @@ public class Prism implements PrismSettingsListener } else { tmpLog = mainLog; } - + // print out or export probabilities probs.print(tmpLog, fileOut == null, exportType == EXPORT_MATLAB, fileOut == null); - + // print out computation time - mainLog.println("\nTime for steady-state probability computation: " + l/1000.0 + " seconds."); - + mainLog.println("\nTime for steady-state probability computation: " + l / 1000.0 + " seconds."); + // tidy up probs.clear(); - if (fileOut != null) tmpLog.close(); + if (fileOut != null) + tmpLog.close(); } - + /** - * Compute transient probabilities (for a DTMC or CTMC). + * Compute transient probabilities for the current model (DTMCs/CTMCs only). * Output probability distribution to log. */ - public void doTransient(Model model, double time) throws PrismException + public void doTransient(double time) throws PrismException { - doTransient(model, time, EXPORT_PLAIN, null, null); + doTransient(time, EXPORT_PLAIN, null, null); } - + /** - * Compute transient probabilities (for a DTMC or CTMC). + * Compute transient probabilities for the current model (DTMCs/CTMCs only). * 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 fileOut, File fileIn) throws PrismException + public void doTransient(double time, int exportType, File fileOut, File fileIn) throws PrismException { long l = 0; // timer ModelChecker mc = null; StateValues probs = null; PrismLog tmpLog; - - if (time < 0) throw new PrismException("Cannot compute transient probabilities for negative time value"); - + + if (!(currentModelType == ModelType.CTMC || currentModelType == ModelType.DTMC)) + throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs"); + + if (time < 0) + throw new PrismException("Cannot compute transient probabilities for negative time value"); + if (fileOut != null && getEngine() == MTBDD) throw new PrismException("Transient probability export only supported for sparse/hybrid engines"); - + + // Build model, if necessary + if (currentModel == null) + buildModel(currentModulesFile); + // no specific states format for MRMC - if (exportType == EXPORT_MRMC) exportType = EXPORT_PLAIN; + if (exportType == EXPORT_MRMC) + exportType = EXPORT_PLAIN; // rows format does not apply to states output - if (exportType == EXPORT_ROWS) exportType = EXPORT_PLAIN; - + if (exportType == EXPORT_ROWS) + exportType = EXPORT_PLAIN; + l = System.currentTimeMillis(); - 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, fileIn); - } - else if (model.getModelType() == ModelType.CTMC) { + if (currentModelType == ModelType.DTMC) { + mainLog.println("\nComputing transient probabilities (time = " + (int) time + ")..."); + mc = new ProbModelChecker(this, currentModel, null); + probs = ((ProbModelChecker) mc).doTransient((int) time, fileIn); + } else { mainLog.println("\nComputing transient probabilities (time = " + time + ")..."); - mc = new StochModelChecker(this, model, null); - probs = ((StochModelChecker)mc).doTransient(time, fileIn); - } - else { - throw new PrismException("Transient probabilities only computed for DTMCs/CTMCs"); + mc = new StochModelChecker(this, currentModel, null); + probs = ((StochModelChecker) mc).doTransient(time, fileIn); } - + l = System.currentTimeMillis() - l; - + // print message mainLog.print("\nPrinting transient probabilities "); switch (exportType) { - case EXPORT_PLAIN: mainLog.print("in plain text format "); break; - case EXPORT_MATLAB: mainLog.print("in Matlab format "); break; + case EXPORT_PLAIN: + mainLog.print("in plain text format "); + break; + case EXPORT_MATLAB: + mainLog.print("in Matlab format "); + break; } - if (fileOut != null) mainLog.println("to file \"" + fileOut + "\"..."); 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 (fileOut != null) { tmpLog = new PrismFileLog(fileOut.getPath()); @@ -1943,36 +2321,273 @@ public class Prism implements PrismSettingsListener } else { tmpLog = mainLog; } - + // print out or export probabilities probs.print(tmpLog, fileOut == null, exportType == EXPORT_MATLAB, fileOut == null); - + // print out computation time - mainLog.println("\nTime for transient probability computation: " + l/1000.0 + " seconds."); + mainLog.println("\nTime for transient probability computation: " + l / 1000.0 + " seconds."); // tidy up probs.clear(); - if (fileOut != null) tmpLog.close(); + if (fileOut != null) + tmpLog.close(); } - - // clear up and close down - + + /** + * Clear up and close down. + */ public void closeDown() - { closeDown(true); } + { + closeDown(true); + } + + /** + * Clear up and close down. + * @param check Whether to perform checks on CUDD status when shutting it down. + */ public void closeDown(boolean check) { - // close down engines + // Close down engines PrismMTBDD.closeDown(); PrismSparse.closeDown(); PrismHybrid.closeDown(); - // close down jdd/cudd - if (cuddStarted) - { + // Close down CUDD/JDD + if (cuddStarted) { JDD.CloseDownCUDD(check); if (jdd.DebugJDD.debugEnabled) DebugJDD.endLifeCycle(); } } + + //------------------------------------------------------------------------------ + // Old API methods, supported via new one + //------------------------------------------------------------------------------ + + /** + * Old API: + * Load a PRISM model, build it, store for later use and return. + * Reachability and model construction are done symbolically, i.e. using (MT)BDDs. + * It is assumed that all constants in the PRISM model file have been defined by now. + * @param modulesFile Model to build + */ + public Model buildModel(ModulesFile modulesFile) throws PrismException + { + loadPRISMModel(modulesFile); + buildModel(); + return getBuiltModel(); + } + + /** + * Old API: + * Load a (built) model and export its transition matrix to a Spy file. + * @param model The model + * @param file File to export to + */ + public void exportToSpyFile(Model model, File file) throws FileNotFoundException, PrismException + { + loadBuiltModel(model); + exportToSpyFile(file); + } + + /** + * Old API: + * Load a (built) model and export the MTBDD for its transition matrix to a Dot file. + * @param model The model + * @param file File to export to + */ + public void exportToDotFile(Model model, File file) throws FileNotFoundException, PrismException + { + loadBuiltModel(model); + exportToDotFile(file); + } + + /** + * Old API: + * Load a (built) model and export its transition matrix to a file + * @param model The model + * @param ordered Ensure that (source) states are in ascending order? + * @param exportType Type of export; one of:
    + *
  • {@link #EXPORT_PLAIN} + *
  • {@link #EXPORT_MATLAB} + *
  • {@link #EXPORT_DOT} + *
  • {@link #EXPORT_MRMC} + *
  • {@link #EXPORT_ROWS} + *
  • {@link #EXPORT_DOT_STATES} + *
+ * @param file File to export to (if null, print to the log instead) + */ + public void exportToFile(Model model, boolean ordered, int exportType, File file) throws FileNotFoundException, PrismException + { + exportTransToFile(model, ordered, exportType, file); + } + + /** + * Old API: + * Load a (built) model and export its transition matrix to a file (or to the log) + * @param model The model + * @param ordered Ensure that (source) states are in ascending order? + * @param exportType Type of export; one of:
    + *
  • {@link #EXPORT_PLAIN} + *
  • {@link #EXPORT_MATLAB} + *
  • {@link #EXPORT_DOT} + *
  • {@link #EXPORT_MRMC} + *
  • {@link #EXPORT_ROWS} + *
  • {@link #EXPORT_DOT_STATES} + *
+ * @param file File to export to (if null, print to the log instead) + */ + public void exportTransToFile(Model model, boolean ordered, int exportType, File file) throws FileNotFoundException, PrismException + { + loadBuiltModel(model); + exportTransToFile(ordered, exportType, file); + } + + /** + * Old API: + * Load a (built) model and export its state rewards to a file + * @param model The model + * @param exportType Type of export; one of:
    + *
  • {@link #EXPORT_PLAIN} + *
  • {@link #EXPORT_MATLAB} + *
  • {@link #EXPORT_MRMC} + *
+ * @param file File to export to (if null, print to the log instead) + */ + public void exportStateRewardsToFile(Model model, int exportType, File file) throws FileNotFoundException, PrismException + { + loadBuiltModel(model); + exportStateRewardsToFile(exportType, file); + } + + /** + * Old API: + * Load a (built) model and export its transition rewards to a file + * @param model The model + * @param ordered Ensure that (source) states are in ascending order? + * @param exportType Type of export; one of:
    + *
  • {@link #EXPORT_PLAIN} + *
  • {@link #EXPORT_MATLAB} + *
  • {@link #EXPORT_MRMC} + *
  • {@link #EXPORT_ROWS} + *
+ * @param file File to export to (if null, print to the log instead) + */ + public void exportTransRewardsToFile(Model model, boolean ordered, int exportType, File file) throws FileNotFoundException, PrismException + { + loadBuiltModel(model); + exportTransRewardsToFile(ordered, exportType, file); + } + + /** + * Old API: + * Load a (built) model and export its bottom strongly connected components (BSCCs) to a file + * @param model The model + * @param exportType Type of export; one of:
    + *
  • {@link #EXPORT_PLAIN} + *
  • {@link #EXPORT_MATLAB} + *
+ * @param file File to export to (if null, print to the log instead) + */ + public void exportBSCCsToFile(Model model, int exportType, File file) throws FileNotFoundException, PrismException + { + loadBuiltModel(model); + exportBSCCsToFile(exportType, file); + } + + /** + * Old API: + * Load a (built) model and export the states satisfying labels from it and a properties file to a file + * The PropertiesFile should correspond to the model. + * @param model The model + * @param modulesFile The corresponding (parsed) PRISM model (for the labels) + * @param propertiesFile The properties file (for further labels) + * @param exportType Type of export; one of:
    + *
  • {@link #EXPORT_PLAIN} + *
  • {@link #EXPORT_MATLAB} + *
+ * @param file File to export to (if null, print to the log instead) + */ + public void exportLabelsToFile(Model model, ModulesFile modulesFile, PropertiesFile propertiesFile, int exportType, File file) + throws FileNotFoundException, PrismException + { + loadPRISMModelAndBuiltModel(modulesFile, model); + exportLabelsToFile(propertiesFile, exportType, file); + } + + /** + * Old API: + * Load a (built) model and export its states to a file + * @param model The model + * @param exportType Type of export; one of:
    + *
  • {@link #EXPORT_PLAIN} + *
  • {@link #EXPORT_MATLAB} + *
+ * @param file File to export to (if null, print to the log instead) + */ + public void exportStatesToFile(Model model, int exportType, File file) throws FileNotFoundException, PrismException + { + loadBuiltModel(model); + exportStateRewardsToFile(exportType, file); + } + + /** + * Old API: + * Load a (built) model, perform model checking of a property on it and return result. + * @param model The model to check + * @param propertiesFile Parent property file of property (for labels/constants/...) + * @param expr The property to check + */ + public Result modelCheck(Model model, PropertiesFile propertiesFile, Expression expr) throws PrismException, PrismLangException + { + loadBuiltModel(model); + return modelCheck(propertiesFile, expr); + } + + /** + * Old API: + * Load (built) model and compute steady-state probabilities (DTMCs/CTMCs only). + * Output probability distribution to log. + */ + public void doSteadyState(Model model) throws PrismException + { + doSteadyState(model, EXPORT_PLAIN, null); + } + + /** + * Old API: + * Load (built) model and compute steady-state probabilities (DTMCs/CTMCs only). + * Output probability distribution to a file (or, if file is null, to log). + * The exportType should be EXPORT_PLAIN or EXPORT_MATLAB. + */ + public void doSteadyState(Model model, int exportType, File fileOut) throws PrismException + { + loadBuiltModel(model); + doSteadyState(exportType, fileOut); + } + + /** + * Old API: + * Load (built) model and compute transient probabilities (DTMCs/CTMCs only). + * Output probability distribution to log. + */ + public void doTransient(Model model, double time) throws PrismException + { + doTransient(model, time, EXPORT_PLAIN, null, null); + } + + /** + * Old API: + * Load (built) model and compute transient probabilities (DTMCs/CTMCs only). + * 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 fileOut, File fileIn) throws PrismException + { + loadBuiltModel(model); + doTransient(time, exportType, fileOut, fileIn); + } } //------------------------------------------------------------------------------