From 36ef85cf07f0ccb216cbf4aa7a1897b0d11723c5 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 3 Jul 2008 15:00:49 +0000 Subject: [PATCH] Initial states for explicit model import can (should) be specified with importlabels. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@799 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/Explicit2MTBDD.java | 89 ++++++++++++++++++++++++++--- prism/src/prism/Prism.java | 17 +++++- prism/src/prism/PrismCL.java | 28 +++++++-- 3 files changed, 120 insertions(+), 14 deletions(-) diff --git a/prism/src/prism/Explicit2MTBDD.java b/prism/src/prism/Explicit2MTBDD.java index d96b7aee..aa8677fb 100644 --- a/prism/src/prism/Explicit2MTBDD.java +++ b/prism/src/prism/Explicit2MTBDD.java @@ -48,6 +48,7 @@ public class Explicit2MTBDD // files to read in from private File statesFile; private File transFile; + private File labelsFile; // initial state info private String initString; @@ -108,13 +109,14 @@ public class Explicit2MTBDD // constructor - public Explicit2MTBDD(Prism prism, File sf, File tf, int t, String is) + public Explicit2MTBDD(Prism prism, File sf, File tf, File lf, int t, String is) { this.prism = prism; mainLog = prism.getMainLog(); techLog = prism.getTechLog(); statesFile = sf; transFile = tf; + labelsFile = lf; // set type at this point // if no preference stated, assume default of mdp switch (t) { @@ -437,11 +439,7 @@ public class Explicit2MTBDD // JDD.Deref(tmp); // calculate dd for initial state - start = JDD.Constant(1); - for (i = 0; i < numVars; i++) { - tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], varList.getStart(i)-varList.getLow(i), 1); - start = JDD.And(start, tmp); - } + buildInit(); // compute state rewards computeStateRewards(); @@ -822,7 +820,84 @@ public class Explicit2MTBDD throw new PrismException("Error detected " + e.getMessage() + "at line " + lineNum + " of transition matrix file \"" + transFile + "\""); } } - + + // calculate dd for initial state + + private void buildInit() throws PrismException + { + BufferedReader in; + String s, s1, s2, ss[]; + int i, r, lineNum = 0, count = 0; + JDDNode tmp; + + // If no labels file provided, just use state 0 (i.e. min value for each var) + if (labelsFile == null) { + start = JDD.Constant(1); + for (i = 0; i < numVars; i++) { + tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], 0, 1); + start = JDD.And(start, tmp); + } + } + // Otherwise, construct from labels file + else { + start = JDD.Constant(0); + try { + // open file for reading + in = new BufferedReader(new FileReader(labelsFile)); + // read first line (label names) and ignore + in.readLine(); lineNum = 1; + // read remaining lines + s = in.readLine(); lineNum++; + numStates = 0; + while (s != null) { + // split string + s = s.trim(); + ss = s.split(":"); + s1 = ss[0].trim(); + s2 = ss[1].trim(); + // search right hand part for 0 (which is index of "init" label) + ss = s2.split(" "); + for (i = 0; i < ss.length; i++) { + if (ss[i].trim().equals("0")) { + count++; + r = Integer.parseInt(s1); + System.out.println("XXX" + r); + // set element in init states bdd + // case where we don't have a state list... + if (statesFile == null) { + tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[0], r, 1); + } + // case where we do have a state list... + else { + tmp = JDD.Constant(1); + for (i = 0; i < numVars; i++) { + tmp = JDD.Apply(JDD.TIMES, tmp, JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], statesArray[r][i], 1)); + } + } + // add it into bdd + JDD.Ref(tmp); + start = JDD.Or(start, tmp); + JDD.Deref(tmp); + } + } + // read next line + s = in.readLine(); lineNum++; + } + // close file + in.close(); + } + catch (IOException e) { + throw new PrismException("File I/O error reading from \"" + statesFile + "\""); + } + catch (NumberFormatException e) { + throw new PrismException("Error detected at line " + lineNum + " of states file \"" + statesFile + "\""); + } + if (count < 1) { + throw new PrismException("No initial states found in labels file"); + } + } + } + // read info about state rewards from states file public void computeStateRewards() throws PrismException diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index a4a49760..3328e6ab 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -859,15 +859,28 @@ public class Prism implements PrismSettingsListener return model; } - public ModulesFile parseExplicitModel(File statesFile, File transFile, int typeOverride, String initString) throws PrismException + /** + * Builds a model from files containing an explicit list of transitions/etc. + * This is step 1 of the process; buildExplicitModel(...) should be called subsequently. + * @param statesFile File containing the list of states (optional, can be null) + * @param transFile File containing the list of transitions (required) + * @param typeOverride Type of model to be built (see ModulesFile) (optional, use 0 if not required) + * @param initString Specification of initial state (optional, can be null) + * @throws PrismException + */ + public ModulesFile parseExplicitModel(File statesFile, File transFile, File labelsFile, int typeOverride, String initString) throws PrismException { // create Explicit2MTBDD object - exp2mtbdd = new Explicit2MTBDD(this, statesFile, transFile, typeOverride, initString); + exp2mtbdd = new Explicit2MTBDD(this, statesFile, transFile, labelsFile, typeOverride, initString); // build state space return exp2mtbdd.buildStates(); } + /** + * Builds a model from files containing an explicit list of transitions/etc. + * This is step 2 of the process; parseExplicitModel(...) should have been called first. + */ public Model buildExplicitModel() throws PrismException { long l; // timer diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 6b580c72..3206f125 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -41,6 +41,7 @@ public class PrismCL private boolean importpepa = false; private boolean importtrans = false; private boolean importstates = false; + private boolean importlabels = false; private boolean steadystate = false; private boolean dotransient = false; private boolean exporttrans = false; @@ -77,6 +78,7 @@ public class PrismCL private String techLogFilename = "stdout"; private String modelFilename = null; private String importStatesFilename = null; + private String importLabelsFilename = null; private String propertiesFilename = null; private String exportTransFilename = null; private String exportStateRewardsFilename = null; @@ -415,6 +417,7 @@ public class PrismCL private void doParsing() throws PrismException { int i; + File sf = null, lf = null; // parse model @@ -431,13 +434,17 @@ public class PrismCL case ModulesFile.STOCHASTIC: mainLog.print("CTMC"); break; default: mainLog.print("MDP"); break; } + mainLog.print(") from \"" + modelFilename + "\""); if (importstates) { - mainLog.print(") from files \"" + importStatesFilename + "\" and \"" + modelFilename + "\"...\n"); - modulesFile = prism.parseExplicitModel(new File(importStatesFilename), new File(modelFilename), typeOverride, importInitString); - } else { - mainLog.print(") from file \"" + modelFilename + "\"...\n"); - modulesFile = prism.parseExplicitModel(null, new File(modelFilename), typeOverride, importInitString); + mainLog.print(", \"" + importStatesFilename + "\""); + sf = new File(importStatesFilename); } + if (importlabels) { + mainLog.print(", \"" + importLabelsFilename + "\""); + lf = new File(importLabelsFilename); + } + mainLog.println("..."); + modulesFile = prism.parseExplicitModel(sf, new File(modelFilename), lf, typeOverride, importInitString); } else { mainLog.print("\nParsing model file \"" + modelFilename + "\"...\n"); @@ -937,6 +944,16 @@ public class PrismCL errorAndExit("No file specified for -"+sw+" switch"); } } + // import labels for explicit model import + else if (sw.equals("importlabels")) { + if (i < args.length-1) { + importlabels = true; + importLabelsFilename = args[++i]; + } + else { + errorAndExit("No file specified for -"+sw+" switch"); + } + } // import initial states info for explicit model import else if (sw.equals("importinit")) { if (i < args.length-1) { @@ -1475,6 +1492,7 @@ public class PrismCL mainLog.println("-importpepa .................... Model description is in PEPA, not the PRISM language"); mainLog.println("-importtrans ............ Import the transition matrix directly from a text file"); 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("-dtmc .......................... Force imported/built model to be a DTMC"); mainLog.println("-ctmc .......................... Force imported/built model to be a CTMC");