|
|
@ -134,14 +134,16 @@ public class StateValuesMTBDD implements StateValues |
|
|
values = JDD.ITE(dd, JDD.Constant(d), values); |
|
|
values = JDD.ITE(dd, JDD.Constant(d), values); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
// read from file |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
/** |
|
|
|
|
|
* Set the elements of this vector by reading them in from a file. |
|
|
|
|
|
*/ |
|
|
public void readFromFile(File file) throws PrismException |
|
|
public void readFromFile(File file) throws PrismException |
|
|
{ |
|
|
{ |
|
|
BufferedReader in; |
|
|
BufferedReader in; |
|
|
String s; |
|
|
String s; |
|
|
int lineNum = 0, count = 0; |
|
|
int lineNum = 0, count = 0; |
|
|
double d; |
|
|
double d; |
|
|
|
|
|
long size = model.getNumStates(); |
|
|
|
|
|
|
|
|
try { |
|
|
try { |
|
|
// open file for reading |
|
|
// open file for reading |
|
|
@ -151,8 +153,8 @@ public class StateValuesMTBDD implements StateValues |
|
|
while (s != null) { |
|
|
while (s != null) { |
|
|
s = s.trim(); |
|
|
s = s.trim(); |
|
|
if (!("".equals(s))) { |
|
|
if (!("".equals(s))) { |
|
|
if (count + 1> model.getNumStates()) |
|
|
|
|
|
throw new PrismException("Too many values in initial distribution (" + (count + 1) + ", not " + model.getNumStates() + ")"); |
|
|
|
|
|
|
|
|
if (count + 1 > size) |
|
|
|
|
|
throw new PrismException("Too many values in file \"" + file + "\" (more than " + size + ")"); |
|
|
d = Double.parseDouble(s); |
|
|
d = Double.parseDouble(s); |
|
|
setElement(count, d); |
|
|
setElement(count, d); |
|
|
count++; |
|
|
count++; |
|
|
@ -162,8 +164,8 @@ public class StateValuesMTBDD implements StateValues |
|
|
// close file |
|
|
// close file |
|
|
in.close(); |
|
|
in.close(); |
|
|
// check size |
|
|
// check size |
|
|
if (count < model.getNumStates()) |
|
|
|
|
|
throw new PrismException("Too few values in initial distribution (" + count + ", not " + model.getNumStates() + ")"); |
|
|
|
|
|
|
|
|
if (count < size) |
|
|
|
|
|
throw new PrismException("Too few values in file \"" + file + "\" (" + count + ", not " + size + ")"); |
|
|
} |
|
|
} |
|
|
catch (IOException e) { |
|
|
catch (IOException e) { |
|
|
throw new PrismException("File I/O error reading from \"" + file + "\""); |
|
|
throw new PrismException("File I/O error reading from \"" + file + "\""); |
|
|
|