From d5ccd1468a0bbf31078a2ee67cd6f9747b0d6271 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 14 May 2013 08:21:23 +0000 Subject: [PATCH] Tidy + updates to UndefinedConstants, including ability to remove constants after creation (for parametric stuff). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6759 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/UndefinedConstants.java | 514 +++++++++++++++--------- 1 file changed, 316 insertions(+), 198 deletions(-) diff --git a/prism/src/prism/UndefinedConstants.java b/prism/src/prism/UndefinedConstants.java index 8172679c..c17fef1c 100644 --- a/prism/src/prism/UndefinedConstants.java +++ b/prism/src/prism/UndefinedConstants.java @@ -26,6 +26,7 @@ package prism; +import java.util.ArrayList; import java.util.List; import java.util.Vector; @@ -35,118 +36,164 @@ import parser.type.*; /** * Class to handle the undefined constants in model and/or properties file. + * This may not be *all* of the constants in the file(s); it may be just + * the ones that are required to execute model checking or some other task. + * Really, the main purpose of this class is to manage an "experiment", + * i.e. to iterate through several different values of one or more constants, + * but this includes the special case where all undefined constants are given a single value. */ public class UndefinedConstants { + // info used to construct this object // parsed model/properties files - private ModulesFile modulesFile; - private PropertiesFile propertiesFile; - + private ModulesFile modulesFile = null; + private PropertiesFile propertiesFile = null; + // optionally, specific properties to get constants from + private List props = null; + // just get constants from labels (in properties file)? + private boolean justLabels = false; + // info about constants private int mfNumConsts = 0; - private DefinedConstant mfConsts[] = null; + private List mfConsts = null; private int pfNumConsts = 0; - private DefinedConstant pfConsts[] = null; - + private List pfConsts = null; + // stuff for iterating through constant values private Values mfValues = null; private Values pfValues = null; - + // class-wide storage for info from -const switch private Vector constSwitchNames; private Vector constSwitchLows; private Vector constSwitchHighs; private Vector constSwitchSteps; - + /** * Construct information about undefined constants from a model and/or properties file. * If either is not required, it can be left as null. All undefined constants, * whether used or not, are assumed to be required to be provided. */ - public UndefinedConstants(ModulesFile mf, PropertiesFile pf) + public UndefinedConstants(ModulesFile modulesFile, PropertiesFile propertiesFile) { - this(mf, pf, false); + this(modulesFile, propertiesFile, false); } - + /** * Construct information about undefined constants from a model and/or properties file. * If either is not required, it can be left as null. If {@code justLabels} is false, * all constants, whether used or not, are assumed to be required to be provided. * If {@code justLabels} is true, only properties file constants that are needed for labels are. */ - public UndefinedConstants(ModulesFile mf, PropertiesFile pf, boolean justLabels) + public UndefinedConstants(ModulesFile modulesFile, PropertiesFile propertiesFile, boolean justLabels) { - Vector mfv, pfv; - // store model/properties files - modulesFile = mf; - propertiesFile = pf; - // determine which constants are undefined - mfv = (modulesFile == null) ? new Vector() : modulesFile.getUndefinedConstants(); - pfv = (propertiesFile == null) ? new Vector() : propertiesFile.getUndefinedConstants(); - if (propertiesFile == null) { - pfv = new Vector(); - } else { - if (justLabels) { - pfv = propertiesFile.getUndefinedConstantsUsedInLabels(); - pfv = orderConstantsByPropertiesFile(pfv, pf); - } else { - pfv = propertiesFile.getUndefinedConstants(); - } - } - // create data structures - initialise(mfv, pfv); + setModulesFile(modulesFile); + setPropertiesFile(propertiesFile); + setJustLabels(justLabels); + initialise(); } - + /** * Construct information about undefined constants for a specific property. - * It is assumed that all undefined constants from model file are needed, + * It is assumed that all undefined constants from the model file are needed, * plus any from the properties file that are use in the property {@code prop}. */ - public UndefinedConstants(ModulesFile mf, PropertiesFile pf, Property prop) + public UndefinedConstants(ModulesFile modulesFile, PropertiesFile propertiesFile, Property prop) { - Vector mfv, pfv; - // store model/properties files - modulesFile = mf; - propertiesFile = pf; - // determine which constants are undefined - mfv = (modulesFile == null) ? new Vector() : modulesFile.getUndefinedConstants(); - if (propertiesFile == null || prop == null) { - pfv = new Vector(); - } else { - pfv = propertiesFile.getUndefinedConstantsUsedInProperty(prop); - pfv = orderConstantsByPropertiesFile(pfv, pf); - } - // create data structures - initialise(mfv, pfv); + setModulesFile(modulesFile); + setPropertiesFile(propertiesFile); + addProperty(prop); + initialise(); } /** * Construct information about undefined constants for specific properties. - * It is assumed that all undefined constants from model file are needed, + * It is assumed that all undefined constants from the model file are needed, * plus any from the properties file that are use in the properties {@code props}. */ - public UndefinedConstants(ModulesFile mf, PropertiesFile pf, List props) + public UndefinedConstants(ModulesFile modulesFile, PropertiesFile propertiesFile, List props) + { + setModulesFile(modulesFile); + setPropertiesFile(propertiesFile); + setProperties(props); + initialise(); + } + + // Setters + + public void setModulesFile(ModulesFile modulesFile) + { + this.modulesFile = modulesFile; + } + + public void setPropertiesFile(PropertiesFile propertiesFile) + { + this.propertiesFile = propertiesFile; + } + + public void setProperties(List props) + { + this.props = props; + } + + public void addProperty(Property prop) + { + if (props == null) + props = new ArrayList(); + props.add(prop); + } + + public void setJustLabels(boolean justLabels) + { + this.justLabels = justLabels; + } + + /** + * Initialise this UndefinedConstants object: + * determine which constants are undefined and then set up data structures. + */ + public void initialise() { Vector mfv, pfv; - // store model/properties files - modulesFile = mf; - propertiesFile = pf; // determine which constants are undefined mfv = (modulesFile == null) ? new Vector() : modulesFile.getUndefinedConstants(); - if (propertiesFile == null || props == null) { + if (propertiesFile == null) { pfv = new Vector(); } else { - pfv = propertiesFile.getUndefinedConstantsUsedInProperties(props); - pfv = orderConstantsByPropertiesFile(pfv, pf); + if (props == null) { + if (justLabels) { + pfv = propertiesFile.getUndefinedConstantsUsedInLabels(); + pfv = orderConstantsByPropertiesFile(pfv, propertiesFile); + } else { + pfv = propertiesFile.getUndefinedConstants(); + } + } else { + pfv = propertiesFile.getUndefinedConstantsUsedInProperties(props); + pfv = orderConstantsByPropertiesFile(pfv, propertiesFile); + } } // create data structures - initialise(mfv, pfv); + setUpDataStructures(mfv, pfv); + } + + /** + * Create a new copy of a list of constant names, sorted by their occurrence in a PropertiesFile. + */ + private Vector orderConstantsByPropertiesFile(Vector oldList, PropertiesFile propertiesFile) + { + Vector newList = new Vector(); + Vector pfList = propertiesFile.getUndefinedConstants(); + for (String s : pfList) { + if (oldList.contains(s)) + newList.add(s); + } + return newList; } /** * Set up data structures (as required by constructor methods) */ - private void initialise(Vector mfv, Vector pfv) + private void setUpDataStructures(Vector mfv, Vector pfv) { int i; String s; @@ -154,51 +201,107 @@ public class UndefinedConstants mfNumConsts = mfv.size(); pfNumConsts = pfv.size(); // create storage for info about constant definitions - mfConsts = new DefinedConstant[mfNumConsts]; + mfConsts = new ArrayList(mfNumConsts); for (i = 0; i < mfNumConsts; i++) { - s = (String)mfv.elementAt(i); - mfConsts[i] = new DefinedConstant(s, modulesFile.getConstantList().getConstantType(modulesFile.getConstantList().getConstantIndex(s))); + s = (String) mfv.elementAt(i); + mfConsts.add(new DefinedConstant(s, modulesFile.getConstantList().getConstantType(modulesFile.getConstantList().getConstantIndex(s)))); } - pfConsts = new DefinedConstant[pfNumConsts]; + pfConsts = new ArrayList(pfNumConsts); for (i = 0; i < pfNumConsts; i++) { - s = (String)pfv.elementAt(i); - pfConsts[i] = new DefinedConstant(s, propertiesFile.getConstantList().getConstantType(propertiesFile.getConstantList().getConstantIndex(s))); + s = (String) pfv.elementAt(i); + pfConsts.add(new DefinedConstant(s, propertiesFile.getConstantList().getConstantType(propertiesFile.getConstantList().getConstantIndex(s)))); } // initialise storage just created clearAllDefinitions(); } - + /** - * Create a new copy of a list of constant names, sorted by their occurrence in a PropertiesFile. + * Remove a constant. This is used if you decide that you do not want to treat + * some constant as undefined once you have created the UndefinedConstants object. + * @return whether a constant was actually removed. */ - private Vector orderConstantsByPropertiesFile(Vector oldList, PropertiesFile propertiesFile) + public boolean removeConstant(String constName) { - Vector newList = new Vector(); - Vector pfList = propertiesFile.getUndefinedConstants(); - for (String s : pfList) { - if (oldList.contains(s)) - newList.add(s); + int i = getMFConstIndex(constName); + if (i != -1) { + mfNumConsts--; + mfConsts.remove(i); + return true; + } else { + i = getPFConstIndex(constName); + if (i != -1) { + pfNumConsts--; + pfConsts.remove(i); + return true; + } } - return newList; + return false; + } + + /** + * Remove some constants. This is used if you decide that you do not want to treat + * some constants as undefined once you have created the UndefinedConstants object. + * @return how many constants were actually removed. + */ + public int removeConstants(String constNames[]) + { + int removed = 0, n = constNames.length; + for (int i = 0; i < n; i++) { + if (removeConstant(constNames[i])) + removed++; + } + return removed; + } + + // Accessor methods for info about undefined constants + + public int getMFNumUndefined() + { + return mfNumConsts; + } + + public int getPFNumUndefined() + { + return pfNumConsts; + } + + public String getMFUndefinedName(int i) + { + return mfConsts.get(i).getName(); + } + + public String getPFUndefinedName(int i) + { + return pfConsts.get(i).getName(); + } + + public Type getMFUndefinedType(int i) + { + return mfConsts.get(i).getType(); + } + + public Type getPFUndefinedType(int i) + { + return pfConsts.get(i).getType(); + } + + public int getMFConstIndex(String s) + { + for (int i = 0; i < mfNumConsts; i++) { + if (mfConsts.get(i).getName().equals(s)) + return i; + } + return -1; + } + + public int getPFConstIndex(String s) + { + for (int i = 0; i < pfNumConsts; i++) { + if (pfConsts.get(i).getName().equals(s)) + return i; + } + return -1; } - - // accessor methods for info about undefined constants - - public int getMFNumUndefined() { return mfNumConsts; } - - public int getPFNumUndefined() { return pfNumConsts; } - - public String getMFUndefinedName(int i) { return mfConsts[i].getName(); } - - public String getPFUndefinedName(int i) { return pfConsts[i].getName(); } - - public Type getMFUndefinedType(int i) { return mfConsts[i].getType(); } - - public Type getPFUndefinedType(int i) { return pfConsts[i].getType(); } - - public int getMFConstIndex(String s) { for (int i = 0; i < mfNumConsts; i++) { if (mfConsts[i].getName().equals(s)) return i; } return -1; } - - public int getPFConstIndex(String s) { for (int i = 0; i < pfNumConsts; i++) { if (pfConsts[i].getName().equals(s)) return i; } return -1; } /** * Clear definitions of all undefined constants. @@ -206,14 +309,15 @@ public class UndefinedConstants public void clearAllDefinitions() { int i; - + // constants from model file for (i = 0; i < mfNumConsts; i++) { - mfConsts[i].clear();; + mfConsts.get(i).clear(); + ; } // constants from properties file for (i = 0; i < pfNumConsts; i++) { - pfConsts[i].clear(); + pfConsts.get(i).clear(); } } @@ -227,13 +331,13 @@ public class UndefinedConstants String name; boolean dupe; boolean useAll = false; - + // clear any previous definitions clearAllDefinitions(); - + // parse and store info from switch argument parseConstSwitch(constSwitch); - + // if there are no undefined consts... if (useAll && (mfNumConsts + pfNumConsts == 0)) { if (constSwitchNames.size() > 0) { @@ -241,25 +345,25 @@ public class UndefinedConstants } return; } - + // go thru parts of -const switch one by one for (i = 0; i < constSwitchNames.size(); i++) { - + // get name name = constSwitchNames.elementAt(i); - + // define constant using info from switch dupe = defineConstant(name, constSwitchLows.elementAt(i), constSwitchHighs.elementAt(i), constSwitchSteps.elementAt(i), useAll); - + // check for duplication if (dupe) { throw new PrismException("Duplicate definitions for undefined constant \"" + name + "\""); } } - + // check all undefined consts have now been defined checkAllDefined(); - + // initialise info for iterating initialiseIterators(); } @@ -271,36 +375,40 @@ public class UndefinedConstants { int i, j; String parts[], args[]; - + // create storage for info constSwitchNames = new Vector(); constSwitchLows = new Vector(); constSwitchHighs = new Vector(); constSwitchSteps = new Vector(); - + // if string is null, nothing more to do - if (constSwitch == null) return; - + if (constSwitch == null) + return; + // split into comma separated parts... parts = constSwitch.split(","); - + // ...and treat each separately for (i = 0; i < parts.length; i++) { - + // ignore blanks - if (parts[i].length() == 0) continue; - + if (parts[i].length() == 0) + continue; + // split either size of "=", store lhs (name) j = parts[i].indexOf('='); - if (j < 1 || j+2 > parts[i].length()) throw new PrismException("Invalid format in definition of undefined constants"); + if (j < 1 || j + 2 > parts[i].length()) + throw new PrismException("Invalid format in definition of undefined constants"); constSwitchNames.add(parts[i].substring(0, j)); - + // check for trailing colon(s) // this is a formatting error not detected by split(":") below - if (parts[i].charAt(parts[i].length()-1) == ':') throw new PrismException("Invalid format in definition of undefined constants"); - + if (parts[i].charAt(parts[i].length() - 1) == ':') + throw new PrismException("Invalid format in definition of undefined constants"); + // split into colon separated parts - args = parts[i].substring(j+1).split(":"); + args = parts[i].substring(j + 1).split(":"); // simple case - no colons, e.g. x=0 if (args.length == 1) { constSwitchLows.add(args[0]); @@ -328,9 +436,9 @@ public class UndefinedConstants /** Define value for a single undefined constant. * Returns whether or not an existing definition was overwritten. - * Actually just helper method for more general method {@link #defineConstant(String, String, String, String) below}. - * - * The method {@link #initialiseIterators() initialiseIterators} must be called after all constants are defined. + * Actually just helper method for more general method {@link #defineConstant(String, String, String, String) below}. + * + * The method {@link #initialiseIterators() initialiseIterators} must be called after all constants are defined. * * @param name The name of the constant. * @param val The value to be assigned. @@ -359,7 +467,7 @@ public class UndefinedConstants { return defineConstant(name, sl, sh, ss, false); } - + /** Define value for a single undefined constant. * Returns whether or not an existing definition was overwritten. * @@ -377,23 +485,21 @@ public class UndefinedConstants { int index = 0; boolean overwrite = false; // did definition exist already? - + // find out if const is in model or properties file (or neither) // also check for overwriting index = getMFConstIndex(name); if (index != -1) { // const is in modules file - overwrite = (mfConsts[index].isDefined()); - mfConsts[index].define(sl, sh, ss); - } - else { + overwrite = (mfConsts.get(index).isDefined()); + mfConsts.get(index).define(sl, sh, ss); + } else { index = getPFConstIndex(name); if (index != -1) { // const is in properties file - overwrite = (pfConsts[index].isDefined()); - pfConsts[index].define(sl, sh, ss); - } - else { + overwrite = (pfConsts.get(index).isDefined()); + pfConsts.get(index).define(sl, sh, ss); + } else { // If we are required to use all supplied const values, check for this // (by default we don't care about un-needed or non-existent const values) if (useAll) @@ -407,7 +513,7 @@ public class UndefinedConstants } } } - + // return whether or not we overwrote an existing definition return overwrite; } @@ -421,27 +527,28 @@ public class UndefinedConstants int i, n; String s; Vector v = new Vector(); - + for (i = 0; i < mfNumConsts; i++) { - if (mfConsts[i].getLow() == null) { - v.add(mfConsts[i].getName()); + if (mfConsts.get(i).getLow() == null) { + v.add(mfConsts.get(i).getName()); } } for (i = 0; i < pfNumConsts; i++) { - if (pfConsts[i].getLow() == null) { - v.add(pfConsts[i].getName()); + if (pfConsts.get(i).getLow() == null) { + v.add(pfConsts.get(i).getName()); } } n = v.size(); if (n > 0) { if (n == 1) { s = "Undefined constant \"" + v.get(0) + "\" must be defined"; - } - else { + } else { s = "Undefined constants"; for (i = 0; i < n; i++) { - if (i > 0 && i < n-1) s += ","; - else if (i == n-1) s += " and"; + if (i > 0 && i < n - 1) + s += ","; + else if (i == n - 1) + s += " and"; s += " \"" + v.get(i) + "\""; } s += " must be defined"; @@ -458,45 +565,45 @@ public class UndefinedConstants intialiseModelIterator(); intialisePropertyIterator(); } - + /** * Initialise iterator for stepping through model constant values. */ private void intialiseModelIterator() { int i; - + // set all consts to lowest values for (i = 0; i < mfNumConsts; i++) { - mfConsts[i].setValue(mfConsts[i].getLow()); + mfConsts.get(i).setValue(mfConsts.get(i).getLow()); } // create Values object mfValues = new Values(); for (i = 0; i < mfNumConsts; i++) { - mfValues.addValue(mfConsts[i].getName(), mfConsts[i].getValue()); + mfValues.addValue(mfConsts.get(i).getName(), mfConsts.get(i).getValue()); } } - + /** * Initialise iterator for stepping through property constant values. */ private void intialisePropertyIterator() { int i; - + // set all consts to lowest values for (i = 0; i < pfNumConsts; i++) { - pfConsts[i].setValue(pfConsts[i].getLow()); + pfConsts.get(i).setValue(pfConsts.get(i).getLow()); } // create Values object pfValues = new Values(); for (i = 0; i < pfNumConsts; i++) { - pfValues.addValue(pfConsts[i].getName(), pfConsts[i].getValue()); + pfValues.addValue(pfConsts.get(i).getName(), pfConsts.get(i).getValue()); } } // Accessor methods for info about values of defined constants, iterators, etc. - + /** * Get a string showing the values/ranges of all constants. * (e.g. "x=1,y=1:100,z=1:10:100,b=true") @@ -505,20 +612,23 @@ public class UndefinedConstants { int i; String s = ""; - + for (i = 0; i < mfNumConsts; i++) { - s += mfConsts[i]; - if (i < mfNumConsts-1) s += ","; + s += mfConsts.get(i); + if (i < mfNumConsts - 1) + s += ","; } for (i = 0; i < pfNumConsts; i++) { - if (i == 0 && mfNumConsts > 0) s += ","; - s += pfConsts[i]; - if (i < pfNumConsts-1) s += ","; + if (i == 0 && mfNumConsts > 0) + s += ","; + s += pfConsts.get(i); + if (i < pfNumConsts - 1) + s += ","; } - + return s; } - + /** * Get a string showing the values/ranges of all properties file constants. * (e.g. "x=1,y=1:100,z=1:10:100,b=true") @@ -527,22 +637,24 @@ public class UndefinedConstants { int i; String s = ""; - + for (i = 0; i < pfNumConsts; i++) { - s += pfConsts[i]; - if (i < pfNumConsts-1) s += ","; + s += pfConsts.get(i); + if (i < pfNumConsts - 1) + s += ","; } - + return s; } - + public int getNumModelIterations() { int i, res; - + res = 1; - for (i = 0; i < mfNumConsts; i++) res *= mfConsts[i].getNumSteps(); - + for (i = 0; i < mfNumConsts; i++) + res *= mfConsts.get(i).getNumSteps(); + return res; } @@ -552,20 +664,23 @@ public class UndefinedConstants public int getNumModelRangingConstants() { int i, res; - + res = 0; - for (i = 0; i < mfNumConsts; i++) if (mfConsts[i].getNumSteps() > 1) res++; - + for (i = 0; i < mfNumConsts; i++) + if (mfConsts.get(i).getNumSteps() > 1) + res++; + return res; } public int getNumPropertyIterations() { int i, res; - + res = 1; - for (i = 0; i < pfNumConsts; i++) res *= pfConsts[i].getNumSteps(); - + for (i = 0; i < pfNumConsts; i++) + res *= pfConsts.get(i).getNumSteps(); + return res; } @@ -575,10 +690,12 @@ public class UndefinedConstants public int getNumPropertyRangingConstants() { int i, res; - + res = 0; - for (i = 0; i < pfNumConsts; i++) if (pfConsts[i].getNumSteps() > 1) res++; - + for (i = 0; i < pfNumConsts; i++) + if (pfConsts.get(i).getNumSteps() > 1) + res++; + return res; } @@ -595,28 +712,31 @@ public class UndefinedConstants { int i; Vector res; - + res = new Vector(); - for (i = 0; i < mfNumConsts; i++) if (mfConsts[i].getNumSteps() > 1) res.addElement(mfConsts[i]); - for (i = 0; i < pfNumConsts; i++) if (pfConsts[i].getNumSteps() > 1) res.addElement(pfConsts[i]); - + for (i = 0; i < mfNumConsts; i++) + if (mfConsts.get(i).getNumSteps() > 1) + res.addElement(mfConsts.get(i)); + for (i = 0; i < pfNumConsts; i++) + if (pfConsts.get(i).getNumSteps() > 1) + res.addElement(pfConsts.get(i)); + return res; } - + public void iterateModel() { int i, ptr; - + // pointer to which constant we are looking at - ptr = mfNumConsts-1; + ptr = mfNumConsts - 1; // cycle backwards through contants while (ptr >= -1) { // general case if (ptr >= 0) { - if (!mfConsts[ptr].incr()) { + if (!mfConsts.get(ptr).incr()) { break; - } - else { + } else { ptr--; continue; } @@ -624,33 +744,32 @@ public class UndefinedConstants // special case - have reached last iteration and need to restart else { for (i = 0; i < mfNumConsts; i++) { - mfConsts[i].setValue(mfConsts[i].getLow()); + mfConsts.get(i).setValue(mfConsts.get(i).getLow()); } break; } } - + // create Values objects mfValues = new Values(); for (i = 0; i < mfNumConsts; i++) { - mfValues.addValue(mfConsts[i].getName(), mfConsts[i].getValue()); + mfValues.addValue(mfConsts.get(i).getName(), mfConsts.get(i).getValue()); } } - + public void iterateProperty() { int i, ptr; - + // pointer to which constant we are looking at - ptr = pfNumConsts-1; + ptr = pfNumConsts - 1; // cycle backwards through contants while (ptr >= -1) { // general case if (ptr >= 0) { - if (!pfConsts[ptr].incr()) { + if (!pfConsts.get(ptr).incr()) { break; - } - else { + } else { ptr--; continue; } @@ -658,27 +777,26 @@ public class UndefinedConstants // special case - have reached last iteration and need to restart else { for (i = 0; i < pfNumConsts; i++) { - pfConsts[i].setValue(pfConsts[i].getLow()); + pfConsts.get(i).setValue(pfConsts.get(i).getLow()); } break; } } - + // create Values objects pfValues = new Values(); for (i = 0; i < pfNumConsts; i++) { - pfValues.addValue(pfConsts[i].getName(), pfConsts[i].getValue()); + pfValues.addValue(pfConsts.get(i).getName(), pfConsts.get(i).getValue()); } } - + public Values getMFConstantValues() { return mfValues; } - + public Values getPFConstantValues() { return pfValues; } } -