From fbec092acea6bd5ed91f88efe0545179ef930806 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 31 Oct 2010 22:09:30 +0000 Subject: [PATCH] Check for overflows added to simulator, but disabled for now. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2204 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/VarList.java | 67 +++++++++++++++++------- prism/src/parser/ast/Update.java | 19 +++++++ prism/src/simulator/Choice.java | 8 +++ prism/src/simulator/ChoiceList.java | 6 +++ prism/src/simulator/ChoiceListFlexi.java | 11 ++++ prism/src/simulator/ChoiceSingleton.java | 6 +++ prism/src/simulator/SimulatorEngine.java | 2 +- prism/src/simulator/TransitionList.java | 39 +++++++++----- prism/src/simulator/Updater.java | 7 ++- 9 files changed, 132 insertions(+), 33 deletions(-) diff --git a/prism/src/parser/VarList.java b/prism/src/parser/VarList.java index 8af42838..26d84930 100644 --- a/prism/src/parser/VarList.java +++ b/prism/src/parser/VarList.java @@ -35,7 +35,10 @@ import parser.type.*; /** * Class to store information about the set of variables in a PRISM model. * Assumes that any constants in the model have been given fixed values. -*/ + * Thus, initial/min/max values for all variables are known. + * VarList also takes care of how each variable will be encoded to an integer + * (e.g. for (MT)BDD representation). + */ public class VarList { // List of variables @@ -287,6 +290,50 @@ public class VarList return vars.get(i).start; } + /** + * Get the value (as an Object) of a variable, from the value encoded as an integer. + */ + public Object decodeFromInt(int var, int val) + { + Type type = getType(var); + // Integer type + if (type instanceof TypeInt) { + return new Integer(val + getLow(var)); + } + // Boolean type + else if (type instanceof TypeBool) { + return new Boolean(val != 0); + } + // Anything else + return null; + } + + /** + * Get the integer encoding of a value for a 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 + { + Type type = getType(var); + try { + // Integer type + if (type instanceof TypeInt) { + return ((Integer) val).intValue() - getLow(var); + } + // Boolean type + else if (type instanceof TypeBool) { + return ((Boolean) val).booleanValue() ? 1 : 0; + } + // Anything else + else { + throw new PrismLangException("Unknown type " + type + " for variable " + getName(var)); + } + } catch (ClassCastException e) { + throw new PrismLangException("Value " + val + " is wrong 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 @@ -356,24 +403,6 @@ public class VarList return state; } - /** - * Get the value (as an Object) of a variable, from the value encoded as an integer. - */ - public Object decodeFromInt(int var, int val) - { - Type type = getType(var); - // Integer type - if (type instanceof TypeInt) { - return new Integer(val + getLow(var)); - } - // Boolean type - else if (type instanceof TypeBool) { - return new Boolean(val != 0); - } - // Anything else - return null; - } - /** * Clone this list. */ diff --git a/prism/src/parser/ast/Update.java b/prism/src/parser/ast/Update.java index 66eb6db8..0199b7fb 100644 --- a/prism/src/parser/ast/Update.java +++ b/prism/src/parser/ast/Update.java @@ -233,6 +233,25 @@ public class Update extends ASTElement } } + /** + * Check whether this update (from a particular state) would cause any errors, mainly variable overflows. + * Variable ranges are specified in the passed in VarList. + * Throws an exception if such an error occurs. + */ + public State checkUpdate(State oldState, VarList varList) throws PrismLangException + { + int i, n, valNew; + State res; + res = new State(oldState); + n = exprs.size(); + for (i = 0; i < n; i++) { + valNew = varList.encodeToInt(i, getExpression(i).evaluate(oldState)); + if (valNew < varList.getLow(i) || valNew > varList.getHigh(i)) + throw new PrismLangException("Value of variable " + getVar(i) + " overflows", getExpression(i)); + } + return res; + } + // Methods required for ASTElement: /** diff --git a/prism/src/simulator/Choice.java b/prism/src/simulator/Choice.java index 96ce3bca..44f7c777 100644 --- a/prism/src/simulator/Choice.java +++ b/prism/src/simulator/Choice.java @@ -46,4 +46,12 @@ public interface Choice public void computeTarget(int i, State currentState, State newState) throws PrismLangException; public int getIndexByProbabilitySum(double x); public void checkValid(ModelType modelType) throws PrismException; + + /** + * Check whether the transitions in this choice (from a particular state) + * would cause any errors, mainly variable overflows. + * Variable ranges are specified in the passed in VarList. + * Throws an exception if such an error occurs. + */ + public void checkForErrors(State currentState, VarList varList) throws PrismException; } diff --git a/prism/src/simulator/ChoiceList.java b/prism/src/simulator/ChoiceList.java index 587ae2cd..2e4f2ea6 100644 --- a/prism/src/simulator/ChoiceList.java +++ b/prism/src/simulator/ChoiceList.java @@ -209,6 +209,12 @@ public class ChoiceList implements Choice // TODO } + @Override + public void checkForErrors(State currentState, VarList varList) throws PrismException + { + // TODO + } + public String toString() { int i, n; diff --git a/prism/src/simulator/ChoiceListFlexi.java b/prism/src/simulator/ChoiceListFlexi.java index b2fc705f..5f86dd79 100644 --- a/prism/src/simulator/ChoiceListFlexi.java +++ b/prism/src/simulator/ChoiceListFlexi.java @@ -293,6 +293,17 @@ public class ChoiceListFlexi implements Choice // Checks for bad probabilities/rates done earlier. } + @Override + public void checkForErrors(State currentState, VarList varList) throws PrismException + { + int i, n; + n = size(); + for (i = 0; i < n; i++) { + for (Update up : updates.get(i)) + up.checkUpdate(currentState, varList); + } + } + public String toString() { int i, n; diff --git a/prism/src/simulator/ChoiceSingleton.java b/prism/src/simulator/ChoiceSingleton.java index c2c7d383..efe52c1e 100644 --- a/prism/src/simulator/ChoiceSingleton.java +++ b/prism/src/simulator/ChoiceSingleton.java @@ -161,6 +161,12 @@ public class ChoiceSingleton implements Choice // TODO } + @Override + public void checkForErrors(State currentState, VarList varList) throws PrismException + { + // TODO + } + @Override public String toString() { diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 141b0db6..4d352907 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -614,7 +614,7 @@ public class SimulatorEngine transitionList = new TransitionList(); // Create updater for model - updater = new Updater(this, modulesFile); + updater = new Updater(this, modulesFile, varList); // Create storage for labels/properties labels = new ArrayList(); diff --git a/prism/src/simulator/TransitionList.java b/prism/src/simulator/TransitionList.java index f9471518..279201eb 100644 --- a/prism/src/simulator/TransitionList.java +++ b/prism/src/simulator/TransitionList.java @@ -73,17 +73,6 @@ public class TransitionList probSum += tr.getProbabilitySum(); } - /** - * Check the validity of the available transitions for a given model type. - * Throw a PrismExecption if an error is found. - */ - public void checkValid(ModelType modelType) throws PrismException - { - for (Choice ch : choices) { - ch.checkValid(modelType); - } - } - // ACCESSORS /** @@ -232,7 +221,9 @@ public class TransitionList { return getChoiceOfTransition(index).computeTarget(transitionOffsets.get(index), currentState); } - + + // Other checks and queries + /** * Is there a deadlock (i.e. no available transitions)? */ @@ -279,6 +270,30 @@ public class TransitionList return true; } + /** + * Check the validity of the available transitions for a given model type. + * Throw a PrismException if an error is found. + */ + public void checkValid(ModelType modelType) throws PrismException + { + for (Choice ch : choices) { + ch.checkValid(modelType); + } + } + + /** + * Check whether the available transitions (from a particular state) + * would cause any errors, mainly variable overflows. + * Variable ranges are specified in the passed in VarList. + * Throws an exception if such an error occurs. + */ + public void checkForErrors(State currentState, VarList varList) throws PrismException + { + for (Choice ch : choices) { + ch.checkForErrors(currentState, varList); + } + } + @Override public String toString() { diff --git a/prism/src/simulator/Updater.java b/prism/src/simulator/Updater.java index 29538d19..a0ae0e65 100644 --- a/prism/src/simulator/Updater.java +++ b/prism/src/simulator/Updater.java @@ -42,6 +42,7 @@ public class Updater protected ModulesFile modulesFile; protected ModelType modelType; protected int numModules; + protected VarList varList; // Synchronising action info protected Vector synchs; protected int numSynchs; @@ -61,7 +62,7 @@ public class Updater // (where j=0 denotes independent, otherwise 1-indexed action label) protected BitSet enabledModules[]; - public Updater(SimulatorEngine simulator, ModulesFile modulesFile) + public Updater(SimulatorEngine simulator, ModulesFile modulesFile, VarList varList) { int i, j; String s; @@ -75,6 +76,7 @@ public class Updater synchs = modulesFile.getSynchs(); numSynchs = synchs.size(); numRewardStructs = modulesFile.getNumRewardStructs(); + this.varList = varList; // Compute count of number of modules using each synch action synchModuleCounts = new int[numSynchs]; @@ -196,6 +198,9 @@ public class Updater // (not needed currently) //transitionList.checkValid(modelType); + // Check for errors (e.g. overflows) in the computed transitions + //transitionList.checkForErrors(state, varList); + //System.out.println(transitionList); }