From a0176385c76dbeb342627980af628e83155b3eb4 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 3 Jul 2008 15:06:34 +0000 Subject: [PATCH] Initial state info for explicit import is now (only) via -importlabels. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@800 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/CHANGELOG.txt | 3 +- prism/src/prism/Explicit2MTBDD.java | 62 ++--------------------------- prism/src/prism/Prism.java | 5 +-- prism/src/prism/PrismCL.java | 14 +------ 4 files changed, 9 insertions(+), 75 deletions(-) diff --git a/prism/CHANGELOG.txt b/prism/CHANGELOG.txt index ff5f9244..56f281c4 100644 --- a/prism/CHANGELOG.txt +++ b/prism/CHANGELOG.txt @@ -10,7 +10,8 @@ Ongoing changes: * LTL model checking Latest changes (reverse chronological): - + +* Initial state info for explicit import is now via -importlabels * Transient probabilities computation for DTMCs * Sparse/hybrid versions of instantaneous reward properties (R=?[I=k]) for DTMCs * Added weak until (W) and release (R) to properties language diff --git a/prism/src/prism/Explicit2MTBDD.java b/prism/src/prism/Explicit2MTBDD.java index aa8677fb..226f33b9 100644 --- a/prism/src/prism/Explicit2MTBDD.java +++ b/prism/src/prism/Explicit2MTBDD.java @@ -28,7 +28,6 @@ package prism; import java.io.*; import java.util.Vector; -import java.util.HashMap; import jdd.*; import parser.*; @@ -50,10 +49,6 @@ public class Explicit2MTBDD private File transFile; private File labelsFile; - // initial state info - private String initString; - private HashMap initVals; - // ModulesFile object, essentially just to store variable info private ModulesFile modulesFile; @@ -109,7 +104,7 @@ public class Explicit2MTBDD // constructor - public Explicit2MTBDD(Prism prism, File sf, File tf, File lf, int t, String is) + public Explicit2MTBDD(Prism prism, File sf, File tf, File lf, int t) { this.prism = prism; mainLog = prism.getMainLog(); @@ -127,16 +122,12 @@ public class Explicit2MTBDD default: type = ModulesFile.NONDETERMINISTIC; break; } - initString = is; } // build state space public ModulesFile buildStates() throws PrismException { - // parse any info about initial state - parseInitString(); - // generate info about variables... // ...either reading from state list file @@ -153,36 +144,6 @@ public class Explicit2MTBDD return modulesFile; } - // parse info about initial state - - public void parseInitString() throws PrismException - { - String ss[], ss2[]; - int i, j; - - // create hash map to store var name -> var value mapping - initVals = new HashMap(); - // parse string - if (initString == null) return; - ss = initString.split(","); - for (i = 0; i < ss.length; i++) { - ss2 = ss[i].split("="); - if (ss2.length != 2) throw new PrismException("Badly formatted initial states string"); - if (!ss2[0].matches("[A-Za-z_][A-Za-z_0-9]*")) throw new PrismException("Badly formatted variable name in initial states string"); - if (ss2[1].equals("true")) initVals.put(ss2[0], new Boolean(true)); - else if (ss2[1].equals("false")) initVals.put(ss2[0], new Boolean(false)); - else { - try { - j = Integer.parseInt(ss2[1]); - initVals.put(ss2[0], new Integer(j)); - } - catch (NumberFormatException e) { - throw new PrismException("Badly formatted value in initial states string"); - } - } - } - } - // create info about vars from states file and put into ModulesFile object public void createVarInfoFromStatesFile() throws PrismException @@ -192,7 +153,6 @@ public class Explicit2MTBDD int i, j, lineNum = 0; Module m; Declaration d; - Object o; try { // open file for reading @@ -264,18 +224,10 @@ public class Explicit2MTBDD m = new Module("M"); for (i = 0; i < numVars; i++) { if (varTypes[i] == Expression.INT) { - o = initVals.get(varNames[i]); - if (o == null) - d = new Declaration(varNames[i], new ExpressionLiteral(Expression.INT, varMins[i]), new ExpressionLiteral(Expression.INT, varMaxs[i]), new ExpressionLiteral(Expression.INT, varMins[i])); - else - d = new Declaration(varNames[i], new ExpressionLiteral(Expression.INT, varMins[i]), new ExpressionLiteral(Expression.INT, varMaxs[i]), new ExpressionLiteral(Expression.INT, ((Integer)o).intValue())); + d = new Declaration(varNames[i], new ExpressionLiteral(Expression.INT, varMins[i]), new ExpressionLiteral(Expression.INT, varMaxs[i]), new ExpressionLiteral(Expression.INT, varMins[i])); } else { - o = initVals.get(varNames[i]); - if (o == null) - d = new Declaration(varNames[i], new ExpressionLiteral(Expression.BOOLEAN, false)); - else - d = new Declaration(varNames[i], new ExpressionLiteral(Expression.BOOLEAN, ((Boolean)o).booleanValue())); + d = new Declaration(varNames[i], new ExpressionLiteral(Expression.BOOLEAN, false)); } m.addDeclaration(d); } @@ -292,8 +244,6 @@ public class Explicit2MTBDD int lineNum = 0; Module m; Declaration d; - Expression init; - Object o; try { // open file for reading @@ -315,14 +265,10 @@ public class Explicit2MTBDD catch (PrismException e) { throw new PrismException("Error detected " + e.getMessage() + "at line " + lineNum + " of transition matrix file \"" + transFile + "\""); } - // determine initial value for variable - o = initVals.get("x"); - if (o == null) init = new ExpressionLiteral(Expression.INT, 0); - else init = new ExpressionLiteral(Expression.INT, ((Integer)o).intValue()); // create modules file modulesFile = new ModulesFile(); m = new Module("M"); - d = new Declaration("x", new ExpressionLiteral(Expression.INT, 0), new ExpressionLiteral(Expression.INT, numStates-1), init); + d = new Declaration("x", new ExpressionLiteral(Expression.INT, 0), new ExpressionLiteral(Expression.INT, numStates-1), new ExpressionLiteral(Expression.INT, 0)); m.addDeclaration(d); modulesFile.addModule(m); modulesFile.tidyUp(); diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 3328e6ab..c2a40790 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -865,13 +865,12 @@ public class Prism implements PrismSettingsListener * @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 + public ModulesFile parseExplicitModel(File statesFile, File transFile, File labelsFile, int typeOverride) throws PrismException { // create Explicit2MTBDD object - exp2mtbdd = new Explicit2MTBDD(this, statesFile, transFile, labelsFile, typeOverride, initString); + exp2mtbdd = new Explicit2MTBDD(this, statesFile, transFile, labelsFile, typeOverride); // build state space return exp2mtbdd.buildStates(); diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 3206f125..c7ebd128 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -70,9 +70,6 @@ public class PrismCL // argument to -simpath switch private String simpathDetails = null; - // import info - private String importInitString = null; - // files/filenames private String mainLogFilename = "stdout"; private String techLogFilename = "stdout"; @@ -444,7 +441,7 @@ public class PrismCL lf = new File(importLabelsFilename); } mainLog.println("..."); - modulesFile = prism.parseExplicitModel(sf, new File(modelFilename), lf, typeOverride, importInitString); + modulesFile = prism.parseExplicitModel(sf, new File(modelFilename), lf, typeOverride); } else { mainLog.print("\nParsing model file \"" + modelFilename + "\"...\n"); @@ -954,15 +951,6 @@ public class PrismCL 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) { - importInitString = args[++i]; - } - else { - errorAndExit("No file specified for -"+sw+" switch"); - } - } // override model type to dtmc else if (sw.equals("dtmc")) { typeOverride = ModulesFile.PROBABILISTIC;