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

Refactor explicit-files model import, splitting into two phases to allow addition of import for explicit engine later. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4694 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 15 years ago
parent
8cdac825ce
commit
0b2f9a078f
4 changed files with 524 additions and 387 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 268
      prism/src/parser/ExplicitFiles2ModulesFile.java
  2. 31
      prism/src/parser/VarList.java
  3. 589
      prism/src/prism/ExplicitFiles2MTBDD.java
  4. 23
      prism/src/prism/Prism.java

268
prism/src/parser/ExplicitFiles2ModulesFile.java
View File

@ -0,0 +1,268 @@
//==============================================================================
//
// Copyright (c) 2002-
// Authors:
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
//
//------------------------------------------------------------------------------
//
// This file is part of PRISM.
//
// PRISM is free software; you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
//
// PRISM is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with PRISM; if not, write to the Free Software Foundation,
// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
//
//==============================================================================
package parser;
import java.io.BufferedReader;
import java.io.File;
import java.io.FileReader;
import java.io.IOException;
import parser.ast.Declaration;
import parser.ast.DeclarationBool;
import parser.ast.DeclarationInt;
import parser.ast.DeclarationType;
import parser.ast.Expression;
import parser.ast.Module;
import parser.ast.ModulesFile;
import parser.type.Type;
import parser.type.TypeBool;
import parser.type.TypeInt;
import prism.ModelType;
import prism.Prism;
import prism.PrismException;
import prism.PrismLog;
/**
* Class to build a (partial) ModulesFile corresponding to imported explicit-state file storage of a model.
* Basically, the ModulesFile just stores the model type and variable info.
* The number of states in the model is also extracted.
*/
public class ExplicitFiles2ModulesFile
{
// Prism stuff
private Prism prism;
private PrismLog mainLog;
// Num states
private int numStates = 0;
public ExplicitFiles2ModulesFile(Prism prism)
{
this.prism = prism;
mainLog = prism.getMainLog();
}
/**
* Get the number of states
* (determined from either states file or transitions file).
*/
public int getNumStates()
{
return numStates;
}
/**
* Build a ModulesFile corresponding to the passed in states/transitions files.
* If {@code typeOverride} is null, we assume model is an MDP.
*/
public ModulesFile buildModulesFile(File statesFile, File transFile, ModelType typeOverride) throws PrismException
{
ModulesFile modulesFile;
ModelType modelType;
// Generate ModulesFile from states or transitions file, depending what is available
if (statesFile != null) {
modulesFile = createVarInfoFromStatesFile(statesFile);
} else {
modulesFile = createVarInfoFromTransFile(transFile);
}
// Set model type: if no preference stated, assume default of MDP
modelType = (typeOverride == null) ? ModelType.MDP : typeOverride;
modulesFile.setModelType(modelType);
return modulesFile;
}
/**
* Build a ModulesFile corresponding to a states file.
*/
private ModulesFile createVarInfoFromStatesFile(File statesFile) throws PrismException
{
BufferedReader in;
String s, ss[];
int i, j, lineNum = 0;
Module m;
Declaration d;
DeclarationType dt;
// Var info
int numVars;
String varNames[];
int varMins[];
int varMaxs[];
int varRanges[];
Type varTypes[];
ModulesFile modulesFile;
try {
// open file for reading
in = new BufferedReader(new FileReader(statesFile));
// read first line and extract var names
s = in.readLine();
lineNum = 1;
if (s == null)
throw new PrismException("empty states file");
s = s.trim();
if (s.charAt(0) != '(' || s.charAt(s.length() - 1) != ')')
throw new PrismException("badly formatted state");
s = s.substring(1, s.length() - 1);
varNames = s.split(",");
numVars = varNames.length;
// create arrays to store info about vars
varMins = new int[numVars];
varMaxs = new int[numVars];
varRanges = new int[numVars];
varTypes = new Type[numVars];
// read remaining lines
s = in.readLine();
lineNum++;
numStates = 0;
while (s != null) {
// skip blank lines
s = s.trim();
if (s.length() > 0) {
// increment state count
numStates++;
// split string
s = s.substring(s.indexOf('(') + 1, s.indexOf(')'));
ss = s.split(",");
if (ss.length != numVars)
throw new PrismException("wrong number of variables");
// for each variable...
for (i = 0; i < numVars; i++) {
// if this is the first state, establish variable type
if (numStates == 1) {
if (ss[i].equals("true") || ss[i].equals("false"))
varTypes[i] = TypeBool.getInstance();
else
varTypes[i] = TypeInt.getInstance();
}
// check for new min/max values (ints only)
if (varTypes[i] instanceof TypeInt) {
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;
}
}
}
}
// read next line
s = in.readLine();
lineNum++;
}
// compute variable ranges
for (i = 0; i < numVars; i++) {
if (varTypes[i] instanceof TypeInt) {
varRanges[i] = varMaxs[i] - varMins[i];
// if range = 0, increment maximum - we don't allow zero-range variables
if (varRanges[i] == 0)
varMaxs[i]++;
}
}
// 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 + "\"");
} catch (PrismException e) {
throw new PrismException("Error detected (" + e.getMessage() + ") at line " + lineNum + " of states file \"" + statesFile + "\"");
}
// create modules file
modulesFile = new ModulesFile();
m = new Module("M");
for (i = 0; i < numVars; i++) {
if (varTypes[i] instanceof TypeInt) {
dt = new DeclarationInt(Expression.Int(varMins[i]), Expression.Int(varMaxs[i]));
d = new Declaration(varNames[i], dt);
d.setStart(Expression.Int(varMins[i]));
} else {
dt = new DeclarationBool();
d = new Declaration(varNames[i], dt);
d.setStart(Expression.False());
}
m.addDeclaration(d);
}
modulesFile.addModule(m);
modulesFile.tidyUp();
return modulesFile;
}
/**
* Build a ModulesFile corresponding to a transitions file.
*/
private ModulesFile createVarInfoFromTransFile(File transFile) throws PrismException
{
BufferedReader in;
String s, ss[];
int lineNum = 0;
Module m;
Declaration d;
DeclarationType dt;
ModulesFile modulesFile;
try {
// open file for reading
in = new BufferedReader(new FileReader(transFile));
// read first line and extract num states
s = in.readLine();
lineNum = 1;
if (s == null)
throw new PrismException("empty transitions file");
s = s.trim();
ss = s.split(" ");
if (ss.length < 2)
throw new PrismException("");
numStates = Integer.parseInt(ss[0]);
// close file
in.close();
} catch (IOException e) {
throw new PrismException("File I/O error reading from \"" + transFile + "\"");
} catch (NumberFormatException e) {
throw new PrismException("Error detected at line " + lineNum + " of transition matrix file \"" + transFile + "\"");
} catch (PrismException e) {
throw new PrismException("Error detected (" + e.getMessage() + ") at line " + lineNum + " of transition matrix file \"" + transFile + "\"");
}
// create modules file
modulesFile = new ModulesFile();
m = new Module("M");
dt = new DeclarationInt(Expression.Int(0), Expression.Int(numStates - 1));
d = new Declaration("x", dt);
d.setStart(Expression.Int(0));
m.addDeclaration(d);
modulesFile.addModule(m);
modulesFile.tidyUp();
return modulesFile;
}
}

31
prism/src/parser/VarList.java
View File

@ -334,6 +334,37 @@ public class VarList
}
}
/**
* Get the integer encoding of a value for a variable, specified as a string.
*/
public int encodeToIntFromString(int var, String s) throws PrismLangException
{
Type type = getType(var);
// Integer type
if (type instanceof TypeInt) {
try {
int i = Integer.parseInt(s);
return i - getLow(var);
} catch (NumberFormatException e) {
throw new PrismLangException("\"" + s + "\" is not a valid integer value");
}
}
// Boolean type
else if (type instanceof TypeBool) {
if (s.equals("true"))
return 1;
else if (s.equals("false"))
return 0;
else
throw new PrismLangException("\"" + s + "\" is not a valid Boolean value");
}
// Anything else
else {
throw new PrismLangException("Unknown type " + type + " for variable " + getName(var));
}
}
/**
* Get a list of all possible values for a subset of the variables in this list.
* @param vars The subset of variables

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

@ -26,291 +26,130 @@
package prism;
import java.io.*;
import java.io.BufferedReader;
import java.io.File;
import java.io.FileReader;
import java.io.IOException;
import java.util.Vector;
import jdd.*;
import parser.*;
import parser.ast.*;
import parser.type.*;
import jdd.JDD;
import jdd.JDDNode;
import jdd.JDDVars;
import parser.Values;
import parser.VarList;
import parser.ast.ModulesFile;
/**
* Class to convert explicit-state file storage of a model to symbolic representation.
*/
public class ExplicitFiles2MTBDD
{
// prism
// Prism stuff
private Prism prism;
// logs
private PrismLog mainLog; // main log
private PrismLog techLog; // tech log
private PrismLog mainLog;
// files to read in from
// Files to read in from
private File statesFile;
private File transFile;
private File labelsFile;
// ModulesFile object, essentially just to store variable info
// Model info
private ModulesFile modulesFile;
private ModelType modelType;
private VarList varList;
private int numVars;
private int numStates;
// model info
// type
private ModelType modelType; // model type (dtmc/mdp/ctmc.)
// vars info
private int numVars; // total number of variables
private String varNames[]; // names of vars
private int varMins[]; // min values of vars
private int varMaxs[]; // max values of vars
private int varRanges[]; // ranges of vars
private Type varTypes[]; // types of vars
private VarList varList; // VarList object to store all var info
// explicit storage of states
private int numStates = 0;
// Explicit storage of states
private int statesArray[][] = null;
// mtbdd stuff
// dds/dd vars - whole system
private JDDNode trans; // transition matrix dd
private JDDNode range; // dd giving range for system
private JDDNode start; // dd for start state
private JDDNode stateRewards; // dd of state rewards
private JDDNode transRewards; // dd of transition rewards
private JDDVars allDDRowVars; // all dd vars (rows)
private JDDVars allDDColVars; // all dd vars (cols)
private JDDVars allDDSynchVars; // all dd vars (synchronising actions)
private JDDVars allDDSchedVars; // all dd vars (scheduling)
private JDDVars allDDChoiceVars; // all dd vars (internal non-det.)
private JDDVars allDDNondetVars; // all dd vars (all non-det.)
private JDDNode trans; // transition matrix dd
private JDDNode range; // dd giving range for system
private JDDNode start; // dd for start state
private JDDNode stateRewards; // dd of state rewards
private JDDNode transRewards; // dd of transition rewards
private JDDVars allDDRowVars; // all dd vars (rows)
private JDDVars allDDColVars; // all dd vars (cols)
private JDDVars allDDSynchVars; // all dd vars (synchronising actions)
private JDDVars allDDSchedVars; // all dd vars (scheduling)
private JDDVars allDDChoiceVars; // all dd vars (internal non-det.)
private JDDVars allDDNondetVars; // all dd vars (all non-det.)
// dds/dd vars - modules
private JDDVars[] moduleDDRowVars; // dd vars for each module (rows)
private JDDVars[] moduleDDColVars; // dd vars for each module (cols)
private JDDNode[] moduleRangeDDs; // dd giving range for each module
private JDDNode[] moduleIdentities; // identity matrix for each module
private JDDVars[] moduleDDRowVars; // dd vars for each module (rows)
private JDDVars[] moduleDDColVars; // dd vars for each module (cols)
private JDDNode[] moduleRangeDDs; // dd giving range for each module
private JDDNode[] moduleIdentities; // identity matrix for each module
// dds/dd vars - variables
private JDDVars[] varDDRowVars; // dd vars (row/col) for each module variable
private JDDVars[] varDDRowVars; // dd vars (row/col) for each module variable
private JDDVars[] varDDColVars;
private JDDNode[] varRangeDDs; // dd giving range for each module variable
private JDDNode[] varColRangeDDs; // dd giving range for each module variable (in col vars)
private JDDNode[] varIdentities; // identity matrix for each module variable
private JDDNode[] varRangeDDs; // dd giving range for each module variable
private JDDNode[] varColRangeDDs; // dd giving range for each module variable (in col vars)
private JDDNode[] varIdentities; // identity matrix for each module variable
// dds/dd vars - nondeterminism
private JDDNode[] ddSynchVars; // individual dd vars for synchronising actions
private JDDNode[] ddSchedVars; // individual dd vars for scheduling non-det.
private JDDNode[] ddChoiceVars; // individual dd vars for local non-det.
private JDDNode[] ddSynchVars; // individual dd vars for synchronising actions
private JDDNode[] ddSchedVars; // individual dd vars for scheduling non-det.
private JDDNode[] ddChoiceVars; // individual dd vars for local non-det.
// names for all dd vars used
private Vector<String> ddVarNames;
// action info
private Vector<String> synchs; // list of action names
private JDDNode transActions; // dd for transition action labels (MDPs)
private Vector<JDDNode> transPerAction; // dds for transition action labels (D/CTMCs)
private Vector<String> synchs; // list of action names
private JDDNode transActions; // dd for transition action labels (MDPs)
private Vector<JDDNode> transPerAction; // dds for transition action labels (D/CTMCs)
private int maxNumChoices = 0;
// constructor
public ExplicitFiles2MTBDD(Prism prism, File sf, File tf, File lf, ModelType t)
public ExplicitFiles2MTBDD(Prism prism)
{
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
modelType = (t == null) ? ModelType.MDP : t;
}
// build state space
public ModulesFile buildStates() throws PrismException
/**
* Build a Model corresponding to the passed in states/transitions/labels files.
* 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
{
// generate info about variables...
// ...either reading from state list file
this.statesFile = statesFile;
this.transFile = transFile;
this.labelsFile = labelsFile;
this.modulesFile = modulesFile;
modelType = modulesFile.getModelType();
varList = modulesFile.createVarList();
numVars = varList.getNumVars();
this.numStates = numStates;
// Build states list, if info is available
if (statesFile != null) {
createVarInfoFromStatesFile();
// in this case, also create explicit table of states
readStatesFromFile();
}
// ...or just creating it from scratch in the trivial case (need transitions file)
else {
createVarInfoFromTransFile();
}
modulesFile.setModelType(modelType);
return modulesFile;
}
// create info about vars from states file and put into ModulesFile object
public void createVarInfoFromStatesFile() throws PrismException
{
BufferedReader in;
String s, ss[];
int i, j, lineNum = 0;
Module m;
Declaration d;
DeclarationType dt;
try {
// open file for reading
in = new BufferedReader(new FileReader(statesFile));
// read first line and extract var names
s = in.readLine(); lineNum = 1;
if (s == null)
throw new PrismException("empty states file");
s = s.trim();
if (s.charAt(0) != '(' || s.charAt(s.length()-1) != ')') throw new PrismException("badly formatted state");
s = s.substring(1, s.length()-1);
varNames = s.split(",");
numVars = varNames.length;
// create arrays to store info about vars
varMins = new int[numVars];
varMaxs = new int[numVars];
varRanges = new int[numVars];
varTypes = new Type[numVars];
// read remaining lines
s = in.readLine(); lineNum++;
numStates = 0;
while (s != null) {
// skip blank lines
s = s.trim();
if (s.length() > 0) {
// increment state count
numStates++;
// split string
s = s.substring(s.indexOf('(')+1, s.indexOf(')'));
ss = s.split(",");
if (ss.length != numVars) throw new PrismException("wrong number of variables");
// for each variable...
for (i = 0; i < numVars; i++) {
// if this is the first state, establish variable type
if (numStates == 1) {
if (ss[i].equals("true") || ss[i].equals("false")) varTypes[i] = TypeBool.getInstance();
else varTypes[i] = TypeInt.getInstance();
}
// check for new min/max values (ints only)
if (varTypes[i] instanceof TypeInt) {
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;
}
}
}
}
// read next line
s = in.readLine(); lineNum++;
}
// compute variable ranges
for (i = 0; i < numVars; i++) {
if (varTypes[i] instanceof TypeInt) {
varRanges[i] = varMaxs[i] - varMins[i];
// if range = 0, increment maximum - we don't allow zero-range variables
if (varRanges[i] == 0) varMaxs[i]++;
}
}
// 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 + "\"");
}
catch (PrismException e) {
throw new PrismException("Error detected (" + e.getMessage() + ") at line " + lineNum + " of states file \"" + statesFile + "\"");
}
// create modules file
modulesFile = new ModulesFile();
m = new Module("M");
for (i = 0; i < numVars; i++) {
if (varTypes[i] instanceof TypeInt) {
dt = new DeclarationInt(Expression.Int(varMins[i]), Expression.Int(varMaxs[i]));
d = new Declaration(varNames[i], dt);
d.setStart(Expression.Int(varMins[i]));
}
else {
dt = new DeclarationBool();
d = new Declaration(varNames[i], dt);
d.setStart(Expression.False());
}
m.addDeclaration(d);
}
modulesFile.addModule(m);
modulesFile.tidyUp();
}
// create info about vars from trans file and put into ModulesFile object
public void createVarInfoFromTransFile() throws PrismException
{
BufferedReader in;
String s, ss[];
int lineNum = 0;
Module m;
Declaration d;
DeclarationType dt;
try {
// open file for reading
in = new BufferedReader(new FileReader(transFile));
// read first line and extract num states
s = in.readLine(); lineNum = 1;
if (s == null)
throw new PrismException("empty transitions file");
s = s.trim();
ss = s.split(" ");
if (ss.length < 2) throw new PrismException("");
numStates = Integer.parseInt(ss[0]);
// close file
in.close();
}
catch (IOException e) {
throw new PrismException("File I/O error reading from \"" + transFile + "\"");
}
catch (NumberFormatException e) {
throw new PrismException("Error detected at line " + lineNum + " of transition matrix file \"" + transFile + "\"");
}
catch (PrismException e) {
throw new PrismException("Error detected (" + e.getMessage() + ") at line " + lineNum + " of transition matrix file \"" + transFile + "\"");
}
// create modules file
modulesFile = new ModulesFile();
m = new Module("M");
dt = new DeclarationInt(Expression.Int(0), Expression.Int(numStates-1));
d = new Declaration("x", dt);
d.setStart(Expression.Int(0));
m.addDeclaration(d);
modulesFile.addModule(m);
modulesFile.tidyUp();
return buildModel();
}
// read info about reachable state space from file and store explicitly
public void readStatesFromFile() throws PrismException
private void readStatesFromFile() throws PrismException
{
BufferedReader in;
String s, ss[];
int i, j, k, lineNum = 0;
int i, j, lineNum = 0;
// create arrays for explicit state storage
statesArray = new int[numStates][];
try {
// open file for reading
in = new BufferedReader(new FileReader(statesFile));
// skip first line
in.readLine(); lineNum = 1;
in.readLine();
lineNum = 1;
// read remaining lines
s = in.readLine(); lineNum++;
s = in.readLine();
lineNum++;
while (s != null) {
// skip blank lines
s = s.trim();
@ -320,64 +159,51 @@ public class ExplicitFiles2MTBDD
// determine which state this line describes
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("(wrong number of variable values) ");
if (statesArray[i] != null) throw new PrismException("(duplicated state) ");
ss = ss[1].substring(ss[1].indexOf('(') + 1, ss[1].indexOf(')')).split(",");
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++) {
if (varTypes[j] instanceof TypeInt) {
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]+"\") ");
}
statesArray[i][j] = varList.encodeToIntFromString(j, ss[j]);
}
}
// read next line
s = in.readLine(); lineNum++;
s = in.readLine();
lineNum++;
}
// close file
in.close();
}
catch (IOException e) {
} 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 + "\"");
}
catch (PrismException e) {
} catch (PrismException e) {
throw new PrismException("Error detected " + e.getMessage() + "at line " + lineNum + " of states file \"" + statesFile + "\"");
}
}
// build model
public Model buildModel() throws PrismException
private Model buildModel() throws PrismException
{
Model model = null;
JDDNode tmp, tmp2;
JDDVars ddv;
int i;
// get variable info from ModulesFile
varList = modulesFile.createVarList();
numVars = varList.getNumVars();
// for an mdp, compute the max number of choices in a state
if (modelType == ModelType.MDP) computeMaxChoicesFromFile();
if (modelType == ModelType.MDP)
computeMaxChoicesFromFile();
// allocate dd variables
allocateDDVars();
sortDDVars();
sortIdentities();
sortRanges();
// construct transition matrix from file
buildTrans();
// get rid of any nondet dd variables not needed
if (modelType == ModelType.MDP) {
tmp = JDD.GetSupport(trans);
@ -393,81 +219,78 @@ public class ExplicitFiles2MTBDD
allDDNondetVars.derefAll();
allDDNondetVars = ddv;
}
// // print dd variables actually used (support of trans)
// mainLog.print("\nMTBDD variables used (" + allDDRowVars.n() + "r, " + allDDRowVars.n() + "c");
// if (modelType == ModelType.MDP) mainLog.print(", " + allDDNondetVars.n() + "nd");
// mainLog.print("):");
// tmp = JDD.GetSupport(trans);
// tmp2 = tmp;
// while (!tmp2.isConstant()) {
// //mainLog.print(" " + tmp2.getIndex() + ":" + ddVarNames.elementAt(tmp2.getIndex()));
// mainLog.print(" " + ddVarNames.elementAt(tmp2.getIndex()));
// tmp2 = tmp2.getThen();
// }
// mainLog.println();
// JDD.Deref(tmp);
// // print dd variables actually used (support of trans)
// mainLog.print("\nMTBDD variables used (" + allDDRowVars.n() + "r, " + allDDRowVars.n() + "c");
// if (modelType == ModelType.MDP) mainLog.print(", " + allDDNondetVars.n() + "nd");
// mainLog.print("):");
// tmp = JDD.GetSupport(trans);
// tmp2 = tmp;
// while (!tmp2.isConstant()) {
// //mainLog.print(" " + tmp2.getIndex() + ":" + ddVarNames.elementAt(tmp2.getIndex()));
// mainLog.print(" " + ddVarNames.elementAt(tmp2.getIndex()));
// tmp2 = tmp2.getThen();
// }
// mainLog.println();
// JDD.Deref(tmp);
// calculate dd for initial state
buildInit();
// compute state rewards
computeStateRewards();
int numModules = 1; // just one module
String moduleNames[] = modulesFile.getModuleNames(); // whose name is stored here
Values constantValues = new Values(); // no constants
JDDNode stateRewardsArray[] = new JDDNode[1]; stateRewardsArray[0] = stateRewards;
JDDNode transRewardsArray[] = new JDDNode[1]; transRewardsArray[0] = transRewards;
String rewardStructNames[] = new String[1]; rewardStructNames[0] = "";
JDDNode stateRewardsArray[] = new JDDNode[1];
stateRewardsArray[0] = stateRewards;
JDDNode transRewardsArray[] = new JDDNode[1];
transRewardsArray[0] = transRewards;
String rewardStructNames[] = new String[1];
rewardStructNames[0] = "";
// create new Model object to be returned
if (modelType == ModelType.DTMC) {
model = new ProbModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames,
numModules, moduleNames, moduleDDRowVars, moduleDDColVars,
numVars, varList, varDDRowVars, varDDColVars, constantValues);
}
else if (modelType == ModelType.MDP) {
model = new NondetModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars,
allDDSynchVars, allDDSchedVars, allDDChoiceVars, allDDNondetVars, ddVarNames,
numModules, moduleNames, moduleDDRowVars, moduleDDColVars,
numVars, varList, varDDRowVars, varDDColVars, constantValues);
}
else if (modelType == ModelType.CTMC) {
model = new StochModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames,
numModules, moduleNames, moduleDDRowVars, moduleDDColVars,
numVars, varList, varDDRowVars, varDDColVars, constantValues);
model = new ProbModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames, numModules,
moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, varDDRowVars, varDDColVars, constantValues);
} else if (modelType == ModelType.MDP) {
model = new NondetModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, allDDSynchVars,
allDDSchedVars, allDDChoiceVars, allDDNondetVars, ddVarNames, numModules, moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList,
varDDRowVars, varDDColVars, constantValues);
} else if (modelType == ModelType.CTMC) {
model = new StochModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames, numModules,
moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, varDDRowVars, varDDColVars, constantValues);
}
// set action info
// TODO: disable if not required?
model.setSynchs(synchs);
if (modelType != ModelType.MDP) {
model.setTransPerAction((JDDNode[])transPerAction.toArray(new JDDNode[0]));
model.setTransPerAction((JDDNode[]) transPerAction.toArray(new JDDNode[0]));
} else {
model.setTransActions(transActions);
}
// do reachability (or not)
if (prism.getDoReach()) {
mainLog.print("\nComputing reachable states...\n");
model.doReachability();
model.filterReachableStates();
}
else {
} else {
mainLog.print("\nSkipping reachable state computation.\n");
model.skipReachability();
model.filterReachableStates();
}
// Print some info (if extraddinfo flag on)
if (prism.getExtraDDInfo()) {
mainLog.print("Reach: " + JDD.GetNumNodes(model.getReach()) + " nodes\n");
}
// find any deadlocks
model.findDeadlocks(prism.getFixDeadlocks());
// deref spare dds
JDD.Deref(moduleIdentities[0]);
JDD.Deref(moduleRangeDDs[0]);
@ -488,62 +311,64 @@ public class ExplicitFiles2MTBDD
JDD.Deref(ddChoiceVars[i]);
}
}
return model;
}
// for an mdp, compute max number of choices in a state (from transitions file)
public void computeMaxChoicesFromFile() throws PrismException
private void computeMaxChoicesFromFile() throws PrismException
{
BufferedReader in;
String s, ss[];
int j, lineNum = 0;
try {
// open file for reading
in = new BufferedReader(new FileReader(transFile));
// skip first line
in.readLine(); lineNum = 1;
in.readLine();
lineNum = 1;
// read remaining lines
s = in.readLine(); lineNum++;
s = in.readLine();
lineNum++;
maxNumChoices = 0;
while (s != null) {
s = s.trim();
if (s.length() > 0) {
ss = s.split(" ");
if (ss.length < 4 || ss.length > 5) throw new PrismException("");
if (ss.length < 4 || ss.length > 5)
throw new PrismException("");
j = Integer.parseInt(ss[1]);
if (j+1 > maxNumChoices) maxNumChoices = j+1;
if (j + 1 > maxNumChoices)
maxNumChoices = j + 1;
}
s = in.readLine(); lineNum++;
s = in.readLine();
lineNum++;
}
// close file
in.close();
}
catch (IOException e) {
} catch (IOException e) {
throw new PrismException("File I/O error reading from \"" + transFile + "\"");
}
catch (NumberFormatException e) {
} catch (NumberFormatException e) {
throw new PrismException("Error detected at line " + lineNum + " of transition matrix file \"" + transFile + "\"");
}
catch (PrismException e) {
} catch (PrismException e) {
throw new PrismException("Error detected " + e.getMessage() + "at line " + lineNum + " of transition matrix file \"" + transFile + "\"");
}
}
// allocate DD vars for system
// i.e. decide on variable ordering and request variables from CUDD
private void allocateDDVars()
{
JDDNode v, vr, vc;
int i, j, n;
int ddVarsUsed = 0;
ddVarNames = new Vector<String>();
// create arrays/etc. first
// nondeterministic variables
if (modelType == ModelType.MDP) {
ddSynchVars = new JDDNode[0];
@ -557,9 +382,9 @@ public class ExplicitFiles2MTBDD
varDDRowVars[i] = new JDDVars();
varDDColVars[i] = new JDDVars();
}
// now allocate variables
// allocate nondeterministic variables
if (modelType == ModelType.MDP) {
for (i = 0; i < maxNumChoices; i++) {
@ -568,7 +393,7 @@ public class ExplicitFiles2MTBDD
ddVarNames.add("l" + i);
}
}
// allocate dd variables for module variables (i.e. rows/cols)
// go through all vars in order (incl. global variables)
// so overall ordering can be specified by ordering in the input file
@ -590,14 +415,14 @@ public class ExplicitFiles2MTBDD
}
}
}
// sort out DD variables and the arrays they are stored in
// (more than one copy of most variables is stored)
private void sortDDVars()
{
int i;
// put refs for all vars in each module together
// create arrays
moduleDDRowVars = new JDDVars[1];
@ -611,7 +436,7 @@ public class ExplicitFiles2MTBDD
moduleDDRowVars[0].addVars(varDDRowVars[i]);
moduleDDColVars[0].addVars(varDDColVars[i]);
}
// put refs for all vars in whole system together
// create arrays
allDDRowVars = new JDDVars();
@ -640,14 +465,14 @@ public class ExplicitFiles2MTBDD
}
}
}
// sort DDs for identities
private void sortIdentities()
{
int i, j;
JDDNode id;
// variable identities
varIdentities = new JDDNode[numVars];
for (i = 0; i < numVars; i++) {
@ -672,14 +497,14 @@ public class ExplicitFiles2MTBDD
}
// Sort DDs for ranges
private void sortRanges()
{
int i;
// initialise raneg for whole system
range = JDD.Constant(1);
// variable ranges
varRangeDDs = new JDDNode[numVars];
varColRangeDDs = new JDDNode[numVars];
@ -702,7 +527,7 @@ public class ExplicitFiles2MTBDD
}
// construct transition matrix from file
private void buildTrans() throws PrismException
{
BufferedReader in;
@ -710,10 +535,10 @@ public class ExplicitFiles2MTBDD
int i, j, r, c, k = 0, lineNum = 0;
double d;
JDDNode elem, tmp;
// initailise action list
synchs = new Vector<String>();
synchs = new Vector<String>();
// initialise mtbdds
trans = JDD.Constant(0);
transRewards = JDD.Constant(0);
@ -723,14 +548,16 @@ public class ExplicitFiles2MTBDD
} else {
transActions = JDD.Constant(0);
}
try {
// open file for reading
in = new BufferedReader(new FileReader(transFile));
// skip first line
in.readLine(); lineNum = 1;
in.readLine();
lineNum = 1;
// read remaining lines
s = in.readLine(); lineNum++;
s = in.readLine();
lineNum++;
while (s != null) {
// skip blank lines
s = s.trim();
@ -740,7 +567,8 @@ public class ExplicitFiles2MTBDD
ss = s.split(" ");
// case for dtmcs/ctmcs...
if (modelType != ModelType.MDP) {
if (ss.length < 3 || ss.length > 4) throw new PrismException("");
if (ss.length < 3 || ss.length > 4)
throw new PrismException("");
r = Integer.parseInt(ss[0]);
c = Integer.parseInt(ss[1]);
d = Double.parseDouble(ss[2]);
@ -750,7 +578,8 @@ public class ExplicitFiles2MTBDD
}
// case for mdps...
else {
if (ss.length < 4 || ss.length > 5) throw new PrismException("");
if (ss.length < 4 || ss.length > 5)
throw new PrismException("");
r = Integer.parseInt(ss[0]);
k = Integer.parseInt(ss[1]);
c = Integer.parseInt(ss[2]);
@ -822,31 +651,29 @@ public class ExplicitFiles2MTBDD
JDD.Deref(elem);
}
// read next line
s = in.readLine(); lineNum++;
s = in.readLine();
lineNum++;
}
// close file
in.close();
}
catch (IOException e) {
} catch (IOException e) {
throw new PrismException("File I/O error reading from \"" + transFile + "\"");
}
catch (NumberFormatException e) {
} catch (NumberFormatException e) {
throw new PrismException("Error detected at line " + lineNum + " of transition matrix file \"" + transFile + "\"");
}
catch (PrismException e) {
} catch (PrismException e) {
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);
@ -862,10 +689,11 @@ public class ExplicitFiles2MTBDD
// open file for reading
in = new BufferedReader(new FileReader(labelsFile));
// read first line (label names) and ignore
in.readLine(); lineNum = 1;
in.readLine();
lineNum = 1;
// read remaining lines
s = in.readLine(); lineNum++;
numStates = 0;
s = in.readLine();
lineNum++;
while (s != null) {
// skip blank lines
s = s.trim();
@ -900,15 +728,14 @@ public class ExplicitFiles2MTBDD
}
}
// read next line
s = in.readLine(); lineNum++;
s = in.readLine();
lineNum++;
}
// close file
in.close();
}
catch (IOException e) {
} catch (IOException e) {
throw new PrismException("File I/O error reading from \"" + statesFile + "\"");
}
catch (NumberFormatException e) {
} catch (NumberFormatException e) {
throw new PrismException("Error detected at line " + lineNum + " of states file \"" + statesFile + "\"");
}
if (count < 1) {
@ -916,29 +743,32 @@ public class ExplicitFiles2MTBDD
}
}
}
// read info about state rewards from states file
public void computeStateRewards() throws PrismException
private void computeStateRewards() throws PrismException
{
BufferedReader in;
String s, ss[];
int i, j, lineNum = 0;
double d;
JDDNode tmp;
// initialise mtbdd
stateRewards = JDD.Constant(0);
if (statesFile == null) return;
if (statesFile == null)
return;
try {
// open file for reading
in = new BufferedReader(new FileReader(statesFile));
// skip first line
in.readLine(); lineNum = 1;
in.readLine();
lineNum = 1;
// read remaining lines
s = in.readLine(); lineNum++;
s = in.readLine();
lineNum++;
while (s != null) {
// skip blank lines
s = s.trim();
@ -969,15 +799,14 @@ public class ExplicitFiles2MTBDD
}
}
// read next line
s = in.readLine(); lineNum++;
s = in.readLine();
lineNum++;
}
// close file
in.close();
}
catch (IOException e) {
} catch (IOException e) {
throw new PrismException("File I/O error reading from \"" + statesFile + "\"");
}
catch (NumberFormatException e) {
} catch (NumberFormatException e) {
throw new PrismException("Error detected at line " + lineNum + " of states file \"" + statesFile + "\"");
}
}

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

@ -199,6 +199,12 @@ public class Prism implements PrismSettingsListener
private explicit.Model currentModelExpl = null;
// Are we doing digital clocks translation for PTAs?
boolean digital = false;
// Info for explicit files load
private File explicitFilesStatesFile = null;
private File explicitFilesTransFile = null;
private File explicitFilesLabelsFile = null;
private int explicitFilesNumStates = -1;
// Has the CUDD library been initialised yet?
private boolean cuddStarted = false;
@ -1528,9 +1534,14 @@ public class Prism implements PrismSettingsListener
currentModelSource = ModelSource.EXPLICIT_FILES;
// Clear any existing built model(s)
clearBuiltModel();
// Create ExplicitFiles2MTBDD object and build state space
expf2mtbdd = new ExplicitFiles2MTBDD(this, statesFile, transFile, labelsFile, typeOverride);
currentModulesFile = expf2mtbdd.buildStates();
// Construct ModulesFile
ExplicitFiles2ModulesFile ef2mf = new ExplicitFiles2ModulesFile(this);
currentModulesFile = ef2mf.buildModulesFile(statesFile, transFile, typeOverride);
// Store explicit files info for later
explicitFilesStatesFile = statesFile;
explicitFilesTransFile = transFile;
explicitFilesLabelsFile = labelsFile;
explicitFilesNumStates = ef2mf.getNumStates();
// Reset dependent info
currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType();
currentDefinedMFConstants = null;
@ -1660,10 +1671,8 @@ public class Prism implements PrismSettingsListener
break;
case EXPLICIT_FILES:
if (!getExplicit()) {
// check ExplicitFiles2MTBDD object created
if (expf2mtbdd == null)
throw new PrismException("ExplicitFiles2MTBDD object never created");
currentModel = expf2mtbdd.buildModel();
expf2mtbdd = new ExplicitFiles2MTBDD(this);
currentModel = expf2mtbdd.build(explicitFilesStatesFile, explicitFilesTransFile, explicitFilesLabelsFile, currentModulesFile, explicitFilesNumStates);
} else {
throw new PrismException("Explicit import not yet supported for explicit engine");
}

Write Preview
Loading…
Cancel
Save