From 19b66ffa2e75c8f6c9f16ad1c89de12610ef354e Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 12 Sep 2019 17:48:55 +0100 Subject: [PATCH] Use VarList decodeFromInt methods in a few places (and move/tidy them). --- prism/src/parser/VarList.java | 36 ++++----- prism/src/prism/StateAndValuePrinter.java | 10 +-- prism/src/prism/StateListMTBDD.java | 19 +---- prism/src/prism/StateModelChecker.java | 95 +++++++++++++---------- 4 files changed, 76 insertions(+), 84 deletions(-) diff --git a/prism/src/parser/VarList.java b/prism/src/parser/VarList.java index 1321a074..985de787 100644 --- a/prism/src/parser/VarList.java +++ b/prism/src/parser/VarList.java @@ -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)); } } diff --git a/prism/src/prism/StateAndValuePrinter.java b/prism/src/prism/StateAndValuePrinter.java index 2ee1772d..cffcdac5 100644 --- a/prism/src/prism/StateAndValuePrinter.java +++ b/prism/src/prism/StateAndValuePrinter.java @@ -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(")"); } diff --git a/prism/src/prism/StateListMTBDD.java b/prism/src/prism/StateListMTBDD.java index bf6e0770..176b726c 100644 --- a/prism/src/prism/StateListMTBDD.java +++ b/prism/src/prism/StateListMTBDD.java @@ -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); } diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index 3a9a7aa7..b642bcf7 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -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