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

Use VarList decodeFromInt methods in a few places (and move/tidy them).

accumulation-v4.7
Dave Parker 7 years ago
parent
acee7edc5c
commit
19b66ffa2e
4 changed files with 76 additions and 84 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. 36
      prism/src/parser/VarList.java
  2. 10
      prism/src/prism/StateAndValuePrinter.java
  3. 19
      prism/src/prism/StateListMTBDD.java
  4. 95
      prism/src/prism/StateModelChecker.java

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

@ -315,60 +315,60 @@ public class VarList
}
/**
* Get the value (as an Object) of a variable, from the value encoded as an integer.
* Get the value (as an Object) for the ith variable, from its encoding as an integer.
*/
public Object decodeFromInt(int var, int val)
public Object decodeFromInt(int i, int val)
{
Type type = getType(var);
Type type = getType(i);
// Integer type
if (type instanceof TypeInt) {
return new Integer(val + getLow(var));
return val + getLow(i);
}
// Boolean type
else if (type instanceof TypeBool) {
return new Boolean(val != 0);
return val != 0;
}
// Anything else
return null;
}
/**
* Get the integer encoding of a value for a variable, specified as an Object.
* Get the integer encoding of a value for the ith variable, specified as an Object.
* The Object is assumed to be of correct type (e.g. Integer, Boolean).
* Throws an exception if Object is of the wrong type.
*/
public int encodeToInt(int var, Object val) throws PrismLangException
public int encodeToInt(int i, Object val) throws PrismLangException
{
Type type = getType(var);
Type type = getType(i);
try {
// Integer type
if (type instanceof TypeInt) {
return ((Integer) val).intValue() - getLow(var);
return ((TypeInt) type).castValueTo(val).intValue() - getLow(i);
}
// Boolean type
else if (type instanceof TypeBool) {
return ((Boolean) val).booleanValue() ? 1 : 0;
return ((TypeBool) type).castValueTo(val).booleanValue() ? 1 : 0;
}
// Anything else
else {
throw new PrismLangException("Unknown type " + type + " for variable " + getName(var));
throw new PrismLangException("Unknown type " + type + " for variable " + getName(i));
}
} catch (ClassCastException e) {
throw new PrismLangException("Value " + val + " is wrong type for variable " + getName(var));
throw new PrismLangException("Value " + val + " is wrong type for variable " + getName(i));
}
}
/**
* Get the integer encoding of a value for a variable, specified as a string.
* Get the integer encoding of a value for the ith variable, specified as a string.
*/
public int encodeToIntFromString(int var, String s) throws PrismLangException
public int encodeToIntFromString(int i, String s) throws PrismLangException
{
Type type = getType(var);
Type type = getType(i);
// Integer type
if (type instanceof TypeInt) {
try {
int i = Integer.parseInt(s);
return i - getLow(var);
int iVal = Integer.parseInt(s);
return iVal - getLow(i);
} catch (NumberFormatException e) {
throw new PrismLangException("\"" + s + "\" is not a valid integer value");
}
@ -385,7 +385,7 @@ public class VarList
}
// Anything else
else {
throw new PrismLangException("Unknown type " + type + " for variable " + getName(var));
throw new PrismLangException("Unknown type " + type + " for variable " + getName(i));
}
}

10
prism/src/prism/StateAndValuePrinter.java
View File

@ -105,15 +105,7 @@ class StateAndValuePrinter implements StateAndValueConsumer
for (int i = 0; i < n; i++) {
if (i > 0)
outputLog.print(",");
// integer variable
if (varList.getType(i) instanceof TypeInt) {
outputLog.print(varValues[i]);
}
// boolean variable
else {
outputLog.print(varValues[i] == 1);
}
outputLog.print(varList.decodeFromInt(i, varValues[i]).toString());
}
outputLog.print(")");
}

19
prism/src/prism/StateListMTBDD.java
View File

@ -33,7 +33,6 @@ import odd.*;
import parser.State;
import parser.Values;
import parser.VarList;
import parser.type.*;
/**
* Stores a list of states as a BDD (or as a 0-1 MTBDD).
@ -267,15 +266,10 @@ public class StateListMTBDD implements StateList
j = varList.getNumVars();
varsString = "";
for (i = 0; i < j; i++) {
// integer variable
if (varList.getType(i) instanceof TypeInt) {
varsString += varValues[i]+varList.getLow(i);
varsString += varList.decodeFromInt(i, varValues[i]).toString();
if (i < j-1) {
varsString += ",";
}
// boolean variable
else {
varsString += (varValues[i] == 1);
}
if (i < j-1) varsString += ",";
}
switch (outputFormat) {
case NORMAL: outputLog.println(varsString + ")"); break;
@ -376,12 +370,7 @@ public class StateListMTBDD implements StateList
}
level++;
}
v += varList.getLow(i);
if (varList.getType(i) instanceof TypeInt) {
o = new Integer(v);
} else {
o = new Boolean(v == 1);
}
o = varList.decodeFromInt(i, v);
values.addValue(varList.getName(i), o);
}

95
prism/src/prism/StateModelChecker.java
View File

@ -992,19 +992,13 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
*/
protected StateValues checkExpressionLiteral(ExpressionLiteral expr, JDDNode statesOfInterest) throws PrismException
{
JDDNode dd;
// it's more efficient to return the constant node
// instead of a MTBDD function for ITE(statesOfInterest, value, 0),
// so we ignore statesOfInterest
JDD.Deref(statesOfInterest);
try {
dd = JDD.Constant(expr.evaluateDouble());
} catch (PrismLangException e) {
throw new PrismException("Unknown literal type");
}
return new StateValuesMTBDD(dd, model);
double d = encodeToDouble(expr.getType(), expr.evaluate());
return new StateValuesMTBDD(JDD.Constant(d), model);
}
/**
@ -1014,24 +1008,13 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
*/
protected StateValues checkExpressionConstant(ExpressionConstant expr, JDDNode statesOfInterest) throws PrismException
{
int i;
JDDNode dd;
// it's more efficient to return the constant node
// instead of a MTBDD function for ITE(statesOfInterest, value, 0),
// so we ignore statesOfInterest
JDD.Deref(statesOfInterest);
i = constantValues.getIndexOf(expr.getName());
if (i == -1)
throw new PrismException("Couldn't evaluate constant \"" + expr.getName() + "\"");
try {
dd = JDD.Constant(constantValues.getDoubleValue(i));
} catch (PrismLangException e) {
throw new PrismException("Unknown type for constant \"" + expr.getName() + "\"");
}
return new StateValuesMTBDD(dd, model);
double d = encodeToDouble(expr.getType(), expr.evaluate(constantValues));
return new StateValuesMTBDD(JDD.Constant(d), model);
}
/**
@ -1234,7 +1217,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
// Compute min
d = vals.minOverBDD(ddFilter);
// Store as object/vector (note crazy Object cast to avoid Integer->int auto conversion)
resObj = (expr.getType() instanceof TypeInt) ? ((Object) new Integer((int) d)) : (new Double(d));
resObj = decodeFromDouble(expr.getType(), d);
resVals = new StateValuesMTBDD(JDD.Constant(d), model);
// Create explanation of result and print some details to log
resultExpl = "Minimum value over " + filterStatesString;
@ -1248,7 +1231,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
// Compute max
d = vals.maxOverBDD(ddFilter);
// Store as object/vector (note crazy Object cast to avoid Integer->int auto conversion)
resObj = (expr.getType() instanceof TypeInt) ? ((Object) new Integer((int) d)) : (new Double(d));
resObj = decodeFromDouble(expr.getType(), d);
resVals = new StateValuesMTBDD(JDD.Constant(d), model);
// Create explanation of result and print some details to log
resultExpl = "Maximum value over " + filterStatesString;
@ -1262,7 +1245,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
// Compute/display min
d = vals.minOverBDD(ddFilter);
mainLog.print("\nMinimum value over " + filterStatesString + ": ");
mainLog.println((expr.getType() instanceof TypeInt) ? ((Object) new Integer((int) d)) : (new Double(d)));
mainLog.println(decodeFromDouble(expr.getType(), d));
// Find states that (are close to) selected value
ddMatch = vals.getBDDFromCloseValue(d, prism.getTermCritParam(), prism.getTermCrit() == Prism.ABSOLUTE);
JDD.Ref(ddFilter);
@ -1278,7 +1261,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
// Compute/display max
d = vals.maxOverBDD(ddFilter);
mainLog.print("\nMaximum value over " + filterStatesString + ": ");
mainLog.println((expr.getType() instanceof TypeInt) ? ((Object) new Integer((int) d)) : (new Double(d)));
mainLog.println(decodeFromDouble(expr.getType(), d));
// Find states that (are close to) selected value
ddMatch = vals.getBDDFromCloseValue(d, prism.getTermCritParam(), prism.getTermCrit() == Prism.ABSOLUTE);
JDD.Ref(ddFilter);
@ -1305,7 +1288,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
// Compute sum
d = vals.sumOverBDD(ddFilter);
// Store as object/vector (note crazy Object cast to avoid Integer->int auto conversion)
resObj = (expr.getType() instanceof TypeInt) ? ((Object) new Integer((int) d)) : (new Double(d));
resObj = decodeFromDouble(expr.getType(), d);
resVals = new StateValuesMTBDD(JDD.Constant(d), model);
// Create explanation of result and print some details to log
resultExpl = "Sum over " + filterStatesString;
@ -1325,13 +1308,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
// Find first value
d = vals.firstFromBDD(ddFilter);
// Store as object/vector
if (expr.getType() instanceof TypeInt) {
resObj = new Integer((int) d);
} else if (expr.getType() instanceof TypeDouble) {
resObj = new Double(d);
} else {
resObj = new Boolean(d > 0);
}
resObj = decodeFromDouble(expr.getType(), d);
resVals = new StateValuesMTBDD(JDD.Constant(d), model);
// Create explanation of result and print some details to log
resultExpl = "Value in ";
@ -1432,15 +1409,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
// Find first (only) value
d = vals.firstFromBDD(ddFilter);
// Store as object/vector
if (expr.getType() instanceof TypeInt) {
resObj = new Integer((int) d);
} else if (expr.getType() instanceof TypeDouble) {
resObj = new Double(d);
} else if (expr.getType() instanceof TypeBool) {
resObj = new Boolean(d > 0);
} else {
throw new PrismException("Don't know how to handle result of type " + expr.getType());
}
resObj = decodeFromDouble(expr.getType(), d);
resVals = new StateValuesMTBDD(JDD.Constant(d), model);
}
// Create explanation of result and print some details to log
@ -1496,6 +1465,48 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
return resVals;
}
// Utility functions for symbolic model checkers
/**
* Convert a value stored as an Object to its encoding as a double (for the MTBDD).
*/
public static double encodeToDouble(Type type, Object val) throws PrismException {
// Integer type
if (type instanceof TypeInt) {
return ((TypeInt) type).castValueTo(val).intValue();
}
// Double type
else if (type instanceof TypeDouble) {
return ((TypeDouble) type).castValueTo(val).doubleValue();
}
// Boolean type
else if (type instanceof TypeBool) {
return ((TypeBool) type).castValueTo(val).booleanValue() ? 1.0 : 0.0;
}
// Anything else
throw new PrismException("Could not encode type " + type + " into an MTBDD");
}
/**
* Get a value as an Object, from its encoding as a double (for the MTBDD).
*/
public static Object decodeFromDouble(Type type, double val) {
// Integer type
if (type instanceof TypeInt) {
return (int) val;
}
// Double type
else if (type instanceof TypeDouble) {
return val;
}
// Boolean type
else if (type instanceof TypeBool) {
return val > 0;
}
// Anything else
return null;
}
/**
* Method for handling the recursive part of PCTL* checking, i.e.,
* recursively checking maximal state subformulas and replacing them

Write Preview
Loading…
Cancel
Save