From e5f9542506f25d7e41b69234c601a9a7f8c28c41 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 22 Mar 2006 21:53:10 +0000 Subject: [PATCH] Improvements to explicit import functionality: * -importstates understands Boolean variables now * -importinit option added * Default module variable (x) indexed from 0, not 1 git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@30 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/Explicit2MTBDD.java | 109 ++++++++++++++++++++++++---- prism/src/prism/Prism.java | 4 +- prism/src/prism/PrismCL.java | 16 +++- 3 files changed, 109 insertions(+), 20 deletions(-) diff --git a/prism/src/prism/Explicit2MTBDD.java b/prism/src/prism/Explicit2MTBDD.java index 7a5fa789..3ff3d680 100644 --- a/prism/src/prism/Explicit2MTBDD.java +++ b/prism/src/prism/Explicit2MTBDD.java @@ -24,6 +24,7 @@ package prism; import java.io.*; import java.util.Vector; +import java.util.HashMap; import jdd.*; import mtbdd.*; @@ -44,6 +45,10 @@ public class Explicit2MTBDD private File statesFile; private File transFile; + // initial state info + private String initString; + private HashMap initVals; + // ModulesFile object, essentially just to store variable info private ModulesFile modulesFile; @@ -57,6 +62,7 @@ public class Explicit2MTBDD private int varMins[]; // min values of vars private int varMaxs[]; // max values of vars private int varRanges[]; // ranges of vars + private int varTypes[]; // types of vars private VarList varList; // VarList object to store all var info // explicit storage of states private int numStates = 0; @@ -103,7 +109,7 @@ public class Explicit2MTBDD // constructor - public Explicit2MTBDD(PrismLog log1, PrismLog log2, File sf, File tf, int t) + public Explicit2MTBDD(PrismLog log1, PrismLog log2, File sf, File tf, int t, String is) { mainLog = log1; techLog = log2; @@ -119,6 +125,7 @@ public class Explicit2MTBDD default: type = ModulesFile.NONDETERMINISTIC; break; } + initString = is; } // set options (generic) @@ -150,6 +157,9 @@ public class Explicit2MTBDD Module m; Declaration d; + // parse any info about initial state + parseInitString(); + // generate info about variables... // ...either reading from state list file @@ -166,6 +176,36 @@ 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 @@ -175,6 +215,7 @@ public class Explicit2MTBDD int i, j, lineNum = 0; Module m; Declaration d; + Object o; try { // open file for reading @@ -189,30 +230,40 @@ public class Explicit2MTBDD varMins = new int[numVars]; varMaxs = new int[numVars]; varRanges = new int[numVars]; + varTypes = new int[numVars]; // read remaining lines s = in.readLine(); lineNum++; numStates = 0; while (s != null) { // increment state count numStates++; - // check var vals for new min/max + // split string s = s.trim(); s = s.substring(s.indexOf('(')+1, s.indexOf(')')); ss = s.split(","); if (ss.length != numVars) throw new PrismException(""); + // for each variable... for (i = 0; i < numVars; i++) { - j = Integer.parseInt(ss[i]); + // if this is the first state, establish variable type if (numStates == 1) { - varMins[i] = varMaxs[i] = j; - } else { - if (j < varMins[i]) varMins[i] = j; - if (j > varMaxs[i]) varMaxs[i] = j; + if (ss[i].equals("true") || ss[i].equals("false")) varTypes[i] = Expression.BOOLEAN; + else varTypes[i] = Expression.INT; + } + // check for new min/max values (ints only) + if (varTypes[i] == Expression.INT) { + j = Integer.parseInt(ss[i]); + if (numStates == 1) { + varMins[i] = varMaxs[i] = j; + } else { + if (j < varMins[i]) varMins[i] = j; + if (j > varMaxs[i]) varMaxs[i] = j; + } } } s = in.readLine(); lineNum++; } for (i = 0; i < numVars; i++) { - varRanges[i] = varMaxs[i] - varMins[i]; + if (varTypes[i] == Expression.INT) varRanges[i] = varMaxs[i] - varMins[i]; } // close file in.close(); @@ -230,7 +281,20 @@ public class Explicit2MTBDD modulesFile = new ModulesFile(); m = new Module("M"); for (i = 0; i < numVars; i++) { - d = new Declaration(varNames[i], new ExpressionInt(varMins[i]), new ExpressionInt(varMaxs[i]), new ExpressionInt(varMins[i])); + if (varTypes[i] == Expression.INT) { + o = initVals.get(varNames[i]); + if (o == null) + d = new Declaration(varNames[i], new ExpressionInt(varMins[i]), new ExpressionInt(varMaxs[i]), new ExpressionInt(varMins[i])); + else + d = new Declaration(varNames[i], new ExpressionInt(varMins[i]), new ExpressionInt(varMaxs[i]), new ExpressionInt(((Integer)o).intValue())); + } + else { + o = initVals.get(varNames[i]); + if (o == null) + d = new Declaration(varNames[i], new ExpressionFalse()); + else + d = new Declaration(varNames[i], ((Boolean)o).booleanValue() ? new ExpressionTrue() : new ExpressionFalse()); + } m.addDeclaration(d); } modulesFile.addModule(m); @@ -246,6 +310,8 @@ public class Explicit2MTBDD int lineNum = 0; Module m; Declaration d; + Expression init; + Object o; try { // open file for reading @@ -267,10 +333,14 @@ 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 ExpressionInt(0); + else init = new ExpressionInt(((Integer)o).intValue()); // create modules file modulesFile = new ModulesFile(); m = new Module("M"); - d = new Declaration("x", new ExpressionInt(1), new ExpressionInt(numStates), new ExpressionInt(1)); + d = new Declaration("x", new ExpressionInt(0), new ExpressionInt(numStates-1), init); m.addDeclaration(d); modulesFile.addModule(m); modulesFile.tidyUp(); @@ -302,12 +372,19 @@ public class Explicit2MTBDD i = Integer.parseInt(ss[0]); // now split up middle bit and extract var info ss = ss[1].substring(ss[1].indexOf('(')+1, ss[1].indexOf(')')).split(","); - if (ss.length != numVars) throw new PrismException(""); + if (ss.length != numVars) throw new PrismException("(wrong number of variable values) "); if (statesArray[i] != null) throw new PrismException("(duplicated state) "); statesArray[i] = new int[numVars]; for (j = 0; j < numVars; j++) { - k = Integer.parseInt(ss[j]); - statesArray[i][j] = k - varMins[j]; + if (varTypes[j] == Expression.INT) { + k = Integer.parseInt(ss[j]); + statesArray[i][j] = k - varMins[j]; + } + else { + if (ss[j].equals("true")) statesArray[i][j] = 1; + else if (ss[j].equals("false")) statesArray[i][j] = 0; + else throw new PrismException("(invalid Boolean value \""+ss[j]+"\") "); + } } s = in.readLine(); lineNum++; } @@ -715,8 +792,8 @@ public class Explicit2MTBDD 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]-varMins[i], 1)); - tmp = JDD.Apply(JDD.TIMES, tmp, JDD.SetVectorElement(JDD.Constant(0), varDDColVars[i], statesArray[c][i]-varMins[i], 1)); + tmp = JDD.Apply(JDD.TIMES, tmp, JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], statesArray[r][i], 1)); + tmp = JDD.Apply(JDD.TIMES, tmp, JDD.SetVectorElement(JDD.Constant(0), varDDColVars[i], statesArray[c][i], 1)); } if (type == ModulesFile.NONDETERMINISTIC) { tmp = JDD.Apply(JDD.TIMES, tmp, JDD.SetVectorElement(JDD.Constant(0), allDDChoiceVars, k, 1)); @@ -789,7 +866,7 @@ public class Explicit2MTBDD else { tmp = JDD.Constant(1); for (j = 0; j < numVars; j++) { - tmp = JDD.Apply(JDD.TIMES, tmp, JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[j], statesArray[i][j]-varMins[j], 1)); + tmp = JDD.Apply(JDD.TIMES, tmp, JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[j], statesArray[i][j], 1)); } } // add it into mtbdd for state rewards diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 4602851b..b462fa41 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -739,10 +739,10 @@ public class Prism return model; } - public ModulesFile parseExplicitModel(File statesFile, File transFile, int typeOverride) throws PrismException + public ModulesFile parseExplicitModel(File statesFile, File transFile, int typeOverride, String initString) throws PrismException { // create Explicit2MTBDD object - exp2mtbdd = new Explicit2MTBDD(mainLog, techLog, statesFile, transFile, typeOverride); + exp2mtbdd = new Explicit2MTBDD(mainLog, techLog, statesFile, transFile, typeOverride, initString); exp2mtbdd.setOption("doreach", getDoReach()); // build state space diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 8af1d080..5dfcc143 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -66,6 +66,9 @@ public class PrismCL // argument to -const switch private String constSwitch = null; + // import info + private String importInitString = null; + // files/filenames private String mainLogFilename = "stdout"; private String techLogFilename = "stdout"; @@ -415,10 +418,10 @@ public class PrismCL } if (importstates) { mainLog.print(") from files \"" + importStatesFilename + "\" and \"" + modelFilename + "\"...\n"); - modulesFile = prism.parseExplicitModel(new File(importStatesFilename), new File(modelFilename), typeOverride); + 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); + modulesFile = prism.parseExplicitModel(null, new File(modelFilename), typeOverride, importInitString); } } else { @@ -895,6 +898,15 @@ 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;