diff --git a/prism/src/prism/ExplicitFiles2MTBDD.java b/prism/src/prism/ExplicitFiles2MTBDD.java index fb5a7ed6..50a54bdd 100644 --- a/prism/src/prism/ExplicitFiles2MTBDD.java +++ b/prism/src/prism/ExplicitFiles2MTBDD.java @@ -57,6 +57,7 @@ public class ExplicitFiles2MTBDD private File statesFile; private File transFile; private File labelsFile; + private File stateRewardsFile; // Model info private ModulesFile modulesFile; @@ -118,11 +119,12 @@ public class ExplicitFiles2MTBDD * Variable info and model type is taken from {@code modulesFile}. * The number of states should also be passed in as {@code numStates}. */ - public Model build(File statesFile, File transFile, File labelsFile, ModulesFile modulesFile, int numStates) throws PrismException + public Model build(File statesFile, File transFile, File labelsFile, File stateRewardsFile, ModulesFile modulesFile, int numStates) throws PrismException { this.statesFile = statesFile; this.transFile = transFile; this.labelsFile = labelsFile; + this.stateRewardsFile = stateRewardsFile; this.modulesFile = modulesFile; modelType = modulesFile.getModelType(); varList = modulesFile.createVarList(); @@ -737,7 +739,7 @@ public class ExplicitFiles2MTBDD } } - /** Read info about state rewards from states file */ + /** Read info about state rewards from a .srew file */ private void computeStateRewards() throws PrismException { String s, ss[]; @@ -748,11 +750,11 @@ public class ExplicitFiles2MTBDD // initialise mtbdd stateRewards = JDD.Constant(0); - if (statesFile == null) + if (stateRewardsFile == null) return; // open file for reading, automatic close when done - try (BufferedReader in = new BufferedReader(new FileReader(statesFile))) { + try (BufferedReader in = new BufferedReader(new FileReader(stateRewardsFile))) { // skip first line in.readLine(); lineNum = 1; @@ -763,39 +765,39 @@ public class ExplicitFiles2MTBDD // skip blank lines s = s.trim(); if (s.length() > 0) { - // split into two/three parts - ss = s.split(":"); - // determine which state this line describes + // split into two parts + ss = s.split(" "); + if (ss.length != 2) + throw new PrismException(""); + // determine which state this line refers to i = Integer.parseInt(ss[0]); - // if there is a state reward... - ss = ss[1].split("="); - if (ss.length == 2) { - // determine value - d = Double.parseDouble(ss[1]); - // construct element of vector mtbdd - // case where we don't have a state list... - if (statesFile == null) { - tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[0], i, 1.0); - } - // case where we do have a state list... - 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], 1)); - } + // determine reward value + d = Double.parseDouble(ss[1]); + // construct element of vector mtbdd + // case where we don't have a state list... + if (statesFile == null) { + tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[0], i, 1.0); + } + // case where we do have a state list... + 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], 1)); } - // add it into mtbdd for state rewards - stateRewards = JDD.Apply(JDD.PLUS, stateRewards, JDD.Apply(JDD.TIMES, JDD.Constant(d), tmp)); } + // add it into mtbdd for state rewards + stateRewards = JDD.Apply(JDD.PLUS, stateRewards, JDD.Apply(JDD.TIMES, JDD.Constant(d), tmp)); } // read next line s = in.readLine(); lineNum++; } } catch (IOException e) { - throw new PrismException("File I/O error reading from \"" + statesFile + "\": " + e.getMessage()); + throw new PrismException("File I/O error reading from \"" + stateRewardsFile + "\": " + e.getMessage()); } catch (NumberFormatException e) { - throw new PrismException("Error detected at line " + lineNum + " of states file \"" + statesFile + "\""); + throw new PrismException("Error detected at line " + lineNum + " of state rewards file \"" + stateRewardsFile + "\""); + } catch (PrismException e) { + throw new PrismException("Error detected " + e.getMessage() + "at line " + lineNum + " of state rewards file \"" + stateRewardsFile + "\""); } } } diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 00aeebea..92e04a8e 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -267,6 +267,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener private File explicitFilesStatesFile = null; private File explicitFilesTransFile = null; private File explicitFilesLabelsFile = null; + private File explicitFilesStateRewardsFile = null; private int explicitFilesNumStates = -1; // Has the CUDD library been initialised yet? @@ -1825,9 +1826,10 @@ public class Prism extends PrismComponent implements PrismSettingsListener * @param statesFile File containing a list of states (optional, can be null) * @param transFile File containing the list of transitions (required) * @param labelsFile File containing label definitions (optional, can be null) + * @param stateRewardsFile File containing state reward definitions (optional, can be null) * @param typeOverride Type of model to be built (optional, use null if not required) */ - public ModulesFile loadModelFromExplicitFiles(File statesFile, File transFile, File labelsFile, ModelType typeOverride) throws PrismException + public ModulesFile loadModelFromExplicitFiles(File statesFile, File transFile, File labelsFile, File stateRewardsFile, ModelType typeOverride) throws PrismException { currentModelSource = ModelSource.EXPLICIT_FILES; // Clear any existing built model(s) @@ -1839,6 +1841,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener explicitFilesStatesFile = statesFile; explicitFilesTransFile = transFile; explicitFilesLabelsFile = labelsFile; + explicitFilesStateRewardsFile = stateRewardsFile; explicitFilesNumStates = ef2mf.getNumStates(); // Reset dependent info currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType(); @@ -1985,8 +1988,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener case EXPLICIT_FILES: if (!getExplicit()) { expf2mtbdd = new ExplicitFiles2MTBDD(this); - currentModel = expf2mtbdd.build(explicitFilesStatesFile, explicitFilesTransFile, explicitFilesLabelsFile, currentModulesFile, - explicitFilesNumStates); + currentModel = expf2mtbdd.build(explicitFilesStatesFile, explicitFilesTransFile, explicitFilesLabelsFile, explicitFilesStateRewardsFile, + currentModulesFile, explicitFilesNumStates); } else { currentModelExpl = new ExplicitFiles2Model(this).build(explicitFilesStatesFile, explicitFilesTransFile, explicitFilesLabelsFile, currentModulesFile, explicitFilesNumStates); } diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index a1fe642b..e0d2bafc 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -65,6 +65,7 @@ public class PrismCL implements PrismModelListener private boolean importtrans = false; private boolean importstates = false; private boolean importlabels = false; + private boolean importstaterewards = false; private boolean importinitdist = false; private boolean steadystate = false; private boolean dotransient = false; @@ -122,6 +123,7 @@ public class PrismCL implements PrismModelListener private String modelFilename = null; private String importStatesFilename = null; private String importLabelsFilename = null; + private String importStateRewardsFilename = null; private String importInitDistFilename = null; private String propertiesFilename = null; private String exportTransFilename = null; @@ -548,7 +550,7 @@ public class PrismCL implements PrismModelListener private void doParsing() { int i; - File sf = null, lf = null; + File sf = null, lf = null, srf = null; // parse model @@ -572,8 +574,12 @@ public class PrismCL implements PrismModelListener mainLog.print(", \"" + importLabelsFilename + "\""); lf = new File(importLabelsFilename); } + if (importstaterewards) { + mainLog.print(", \"" + importStateRewardsFilename + "\""); + srf = new File(importStateRewardsFilename); + } mainLog.println("..."); - modulesFile = prism.loadModelFromExplicitFiles(sf, new File(modelFilename), lf, typeOverride); + modulesFile = prism.loadModelFromExplicitFiles(sf, new File(modelFilename), lf, srf, typeOverride); } else { mainLog.print("\nParsing model file \"" + modelFilename + "\"...\n"); modulesFile = prism.parseModelFile(new File(modelFilename), typeOverride); @@ -1247,6 +1253,15 @@ public class PrismCL implements PrismModelListener errorAndExit("No file specified for -" + sw + " switch"); } } + // import state rewards for explicit model import + else if (sw.equals("importstaterewards")) { + if (i < args.length - 1) { + importstaterewards = true; + importStateRewardsFilename = args[++i]; + } else { + errorAndExit("No file specified for -" + sw + " switch"); + } + } // import initial distribution e.g. for transient probability distribution else if (sw.equals("importinitdist")) { if (i < args.length - 1) { @@ -1807,6 +1822,10 @@ public class PrismCL implements PrismModelListener importStatesFilename = basename + ".sta"; importlabels = true; importLabelsFilename = basename + ".lab"; + if (new File(basename + ".srew").exists()) { + importstaterewards = true; + importStateRewardsFilename = basename + ".srew"; + } } else if (ext.equals("tra")) { importtrans = true; modelFilename = basename + ".tra"; @@ -1819,6 +1838,9 @@ public class PrismCL implements PrismModelListener } else if (ext.equals("lab")) { importlabels = true; importLabelsFilename = basename + ".lab"; + } else if (ext.equals("srew")) { + importstaterewards = true; + importStateRewardsFilename = basename + ".srew"; } // Unknown extension else { @@ -2291,6 +2313,7 @@ public class PrismCL implements PrismModelListener 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("-importstaterewards ...... Import the state rewards directly from a text file"); mainLog.println("-importinitdist .......... Specify the initial probability distribution for transient analysis"); mainLog.println("-dtmc .......................... Force imported/built model to be a DTMC"); mainLog.println("-ctmc .......................... Force imported/built model to be a CTMC"); @@ -2375,7 +2398,7 @@ public class PrismCL implements PrismModelListener mainLog.println("Import the model directly from text file(s)."); mainLog.println("Use a list of file extensions to indicate which files should be read, e.g.:"); mainLog.println("\n -importmodel in.tra,sta\n"); - mainLog.println("Possible extensions are: .tra, .sta, .lab"); + mainLog.println("Possible extensions are: .tra, .sta, .lab, .srew"); mainLog.println("Use extension .all to import all, e.g.:"); mainLog.println("\n -importmodel in.all\n"); }