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

@@ -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.
 	 */

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:
 
 	/**

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;
 }

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;

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;

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()
 	{

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<Expression>();

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()
 	{

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<String> 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);
 	}