s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Add support for a state rewards file when doing explicit model import (not the explicit engine). 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11745 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 9 years ago
parent
81451753d1
commit
a6eb2bd327
3 changed files with 61 additions and 33 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 56
      prism/src/prism/ExplicitFiles2MTBDD.java
  2. 9
      prism/src/prism/Prism.java
  3. 29
      prism/src/prism/PrismCL.java

56
prism/src/prism/ExplicitFiles2MTBDD.java
View File

@ -57,6 +57,7 @@ public class ExplicitFiles2MTBDD
private File statesFile; private File statesFile;
private File transFile; private File transFile;
private File labelsFile; private File labelsFile;
private File stateRewardsFile;
// Model info // Model info
private ModulesFile modulesFile; private ModulesFile modulesFile;
@ -118,11 +119,12 @@ public class ExplicitFiles2MTBDD
* Variable info and model type is taken from {@code modulesFile}. * Variable info and model type is taken from {@code modulesFile}.
* The number of states should also be passed in as {@code numStates}. * 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.statesFile = statesFile;
this.transFile = transFile; this.transFile = transFile;
this.labelsFile = labelsFile; this.labelsFile = labelsFile;
this.stateRewardsFile = stateRewardsFile;
this.modulesFile = modulesFile; this.modulesFile = modulesFile;
modelType = modulesFile.getModelType(); modelType = modulesFile.getModelType();
varList = modulesFile.createVarList(); 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 private void computeStateRewards() throws PrismException
{ {
String s, ss[]; String s, ss[];
@ -748,11 +750,11 @@ public class ExplicitFiles2MTBDD
// initialise mtbdd // initialise mtbdd
stateRewards = JDD.Constant(0); stateRewards = JDD.Constant(0);
if (statesFile == null)
if (stateRewardsFile == null)
return; return;
// open file for reading, automatic close when done // 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 // skip first line
in.readLine(); in.readLine();
lineNum = 1; lineNum = 1;
@ -763,39 +765,39 @@ public class ExplicitFiles2MTBDD
// skip blank lines // skip blank lines
s = s.trim(); s = s.trim();
if (s.length() > 0) { 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]); 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 // read next line
s = in.readLine(); s = in.readLine();
lineNum++; lineNum++;
} }
} catch (IOException e) { } 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) { } 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 + "\"");
} }
} }
} }

9
prism/src/prism/Prism.java
View File

@ -267,6 +267,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
private File explicitFilesStatesFile = null; private File explicitFilesStatesFile = null;
private File explicitFilesTransFile = null; private File explicitFilesTransFile = null;
private File explicitFilesLabelsFile = null; private File explicitFilesLabelsFile = null;
private File explicitFilesStateRewardsFile = null;
private int explicitFilesNumStates = -1; private int explicitFilesNumStates = -1;
// Has the CUDD library been initialised yet? // 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 statesFile File containing a list of states (optional, can be null)
* @param transFile File containing the list of transitions (required) * @param transFile File containing the list of transitions (required)
* @param labelsFile File containing label definitions (optional, can be null) * @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) * @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; currentModelSource = ModelSource.EXPLICIT_FILES;
// Clear any existing built model(s) // Clear any existing built model(s)
@ -1839,6 +1841,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
explicitFilesStatesFile = statesFile; explicitFilesStatesFile = statesFile;
explicitFilesTransFile = transFile; explicitFilesTransFile = transFile;
explicitFilesLabelsFile = labelsFile; explicitFilesLabelsFile = labelsFile;
explicitFilesStateRewardsFile = stateRewardsFile;
explicitFilesNumStates = ef2mf.getNumStates(); explicitFilesNumStates = ef2mf.getNumStates();
// Reset dependent info // Reset dependent info
currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType(); currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType();
@ -1985,8 +1988,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener
case EXPLICIT_FILES: case EXPLICIT_FILES:
if (!getExplicit()) { if (!getExplicit()) {
expf2mtbdd = new ExplicitFiles2MTBDD(this); expf2mtbdd = new ExplicitFiles2MTBDD(this);
currentModel = expf2mtbdd.build(explicitFilesStatesFile, explicitFilesTransFile, explicitFilesLabelsFile, currentModulesFile,
explicitFilesNumStates);
currentModel = expf2mtbdd.build(explicitFilesStatesFile, explicitFilesTransFile, explicitFilesLabelsFile, explicitFilesStateRewardsFile,
currentModulesFile, explicitFilesNumStates);
} else { } else {
currentModelExpl = new ExplicitFiles2Model(this).build(explicitFilesStatesFile, explicitFilesTransFile, explicitFilesLabelsFile, currentModulesFile, explicitFilesNumStates); currentModelExpl = new ExplicitFiles2Model(this).build(explicitFilesStatesFile, explicitFilesTransFile, explicitFilesLabelsFile, currentModulesFile, explicitFilesNumStates);
} }

29
prism/src/prism/PrismCL.java
View File

@ -65,6 +65,7 @@ public class PrismCL implements PrismModelListener
private boolean importtrans = false; private boolean importtrans = false;
private boolean importstates = false; private boolean importstates = false;
private boolean importlabels = false; private boolean importlabels = false;
private boolean importstaterewards = false;
private boolean importinitdist = false; private boolean importinitdist = false;
private boolean steadystate = false; private boolean steadystate = false;
private boolean dotransient = false; private boolean dotransient = false;
@ -122,6 +123,7 @@ public class PrismCL implements PrismModelListener
private String modelFilename = null; private String modelFilename = null;
private String importStatesFilename = null; private String importStatesFilename = null;
private String importLabelsFilename = null; private String importLabelsFilename = null;
private String importStateRewardsFilename = null;
private String importInitDistFilename = null; private String importInitDistFilename = null;
private String propertiesFilename = null; private String propertiesFilename = null;
private String exportTransFilename = null; private String exportTransFilename = null;
@ -548,7 +550,7 @@ public class PrismCL implements PrismModelListener
private void doParsing() private void doParsing()
{ {
int i; int i;
File sf = null, lf = null;
File sf = null, lf = null, srf = null;
// parse model // parse model
@ -572,8 +574,12 @@ public class PrismCL implements PrismModelListener
mainLog.print(", \"" + importLabelsFilename + "\""); mainLog.print(", \"" + importLabelsFilename + "\"");
lf = new File(importLabelsFilename); lf = new File(importLabelsFilename);
} }
if (importstaterewards) {
mainLog.print(", \"" + importStateRewardsFilename + "\"");
srf = new File(importStateRewardsFilename);
}
mainLog.println("..."); mainLog.println("...");
modulesFile = prism.loadModelFromExplicitFiles(sf, new File(modelFilename), lf, typeOverride);
modulesFile = prism.loadModelFromExplicitFiles(sf, new File(modelFilename), lf, srf, typeOverride);
} else { } else {
mainLog.print("\nParsing model file \"" + modelFilename + "\"...\n"); mainLog.print("\nParsing model file \"" + modelFilename + "\"...\n");
modulesFile = prism.parseModelFile(new File(modelFilename), typeOverride); modulesFile = prism.parseModelFile(new File(modelFilename), typeOverride);
@ -1247,6 +1253,15 @@ public class PrismCL implements PrismModelListener
errorAndExit("No file specified for -" + sw + " switch"); 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 // import initial distribution e.g. for transient probability distribution
else if (sw.equals("importinitdist")) { else if (sw.equals("importinitdist")) {
if (i < args.length - 1) { if (i < args.length - 1) {
@ -1807,6 +1822,10 @@ public class PrismCL implements PrismModelListener
importStatesFilename = basename + ".sta"; importStatesFilename = basename + ".sta";
importlabels = true; importlabels = true;
importLabelsFilename = basename + ".lab"; importLabelsFilename = basename + ".lab";
if (new File(basename + ".srew").exists()) {
importstaterewards = true;
importStateRewardsFilename = basename + ".srew";
}
} else if (ext.equals("tra")) { } else if (ext.equals("tra")) {
importtrans = true; importtrans = true;
modelFilename = basename + ".tra"; modelFilename = basename + ".tra";
@ -1819,6 +1838,9 @@ public class PrismCL implements PrismModelListener
} else if (ext.equals("lab")) { } else if (ext.equals("lab")) {
importlabels = true; importlabels = true;
importLabelsFilename = basename + ".lab"; importLabelsFilename = basename + ".lab";
} else if (ext.equals("srew")) {
importstaterewards = true;
importStateRewardsFilename = basename + ".srew";
} }
// Unknown extension // Unknown extension
else { else {
@ -2291,6 +2313,7 @@ public class PrismCL implements PrismModelListener
mainLog.println("-importtrans <file> ............ Import the transition matrix directly from a text file"); mainLog.println("-importtrans <file> ............ Import the transition matrix directly from a text file");
mainLog.println("-importstates <file>............ Import the list of states directly from a text file"); mainLog.println("-importstates <file>............ Import the list of states directly from a text file");
mainLog.println("-importlabels <file>............ Import the list of labels directly from a text file"); mainLog.println("-importlabels <file>............ Import the list of labels directly from a text file");
mainLog.println("-importstaterewards <file>...... Import the state rewards directly from a text file");
mainLog.println("-importinitdist <file>.......... Specify the initial probability distribution for transient analysis"); mainLog.println("-importinitdist <file>.......... Specify the initial probability distribution for transient analysis");
mainLog.println("-dtmc .......................... Force imported/built model to be a DTMC"); mainLog.println("-dtmc .......................... Force imported/built model to be a DTMC");
mainLog.println("-ctmc .......................... Force imported/built model to be a CTMC"); 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("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("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("\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("Use extension .all to import all, e.g.:");
mainLog.println("\n -importmodel in.all\n"); mainLog.println("\n -importmodel in.all\n");
} }

Write Preview
Loading…
Cancel
Save