Browse Source

Fix: undefined constants should be taken in the order they appear in the properties file (like they used to). And a small API tweak.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5354 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 14 years ago
parent
commit
cf4798f961
  1. 31
      prism/src/prism/UndefinedConstants.java

31
prism/src/prism/UndefinedConstants.java

@ -88,6 +88,7 @@ public class UndefinedConstants
} else { } else {
if (justLabels) { if (justLabels) {
pfv = propertiesFile.getUndefinedConstantsUsedInLabels(); pfv = propertiesFile.getUndefinedConstantsUsedInLabels();
pfv = orderConstantsByPropertiesFile(pfv, pf);
} else { } else {
pfv = propertiesFile.getUndefinedConstants(); pfv = propertiesFile.getUndefinedConstants();
} }
@ -113,6 +114,7 @@ public class UndefinedConstants
pfv = new Vector<String>(); pfv = new Vector<String>();
} else { } else {
pfv = propertiesFile.getUndefinedConstantsUsedInProperty(prop); pfv = propertiesFile.getUndefinedConstantsUsedInProperty(prop);
pfv = orderConstantsByPropertiesFile(pfv, pf);
} }
// create data structures // create data structures
initialise(mfv, pfv); initialise(mfv, pfv);
@ -135,6 +137,7 @@ public class UndefinedConstants
pfv = new Vector<String>(); pfv = new Vector<String>();
} else { } else {
pfv = propertiesFile.getUndefinedConstantsUsedInProperties(props); pfv = propertiesFile.getUndefinedConstantsUsedInProperties(props);
pfv = orderConstantsByPropertiesFile(pfv, pf);
} }
// create data structures // create data structures
initialise(mfv, pfv); initialise(mfv, pfv);
@ -165,6 +168,20 @@ public class UndefinedConstants
clearAllDefinitions(); clearAllDefinitions();
} }
/**
* Create a new copy of a list of constant names, sorted by their occurrence in a PropertiesFile.
*/
private Vector<String> orderConstantsByPropertiesFile(Vector<String> oldList, PropertiesFile propertiesFile)
{
Vector<String> newList = new Vector<String>();
Vector<String> pfList = propertiesFile.getUndefinedConstants();
for (String s : pfList) {
if (oldList.contains(s))
newList.add(s);
}
return newList;
}
// accessor methods for info about undefined constants // accessor methods for info about undefined constants
public int getMFNumUndefined() { return mfNumConsts; } public int getMFNumUndefined() { return mfNumConsts; }
@ -529,7 +546,10 @@ public class UndefinedConstants
return res; return res;
} }
public int getNumModelDimensions()
/**
* Get the number of ranging constants (constants with range > 1) from the model file.
*/
public int getNumModelRangingConstants()
{ {
int i, res; int i, res;
@ -549,7 +569,10 @@ public class UndefinedConstants
return res; return res;
} }
public int getNumPropertyDimensions()
/**
* Get the number of ranging constants (constants with range > 1) from the properties file.
*/
public int getNumPropertyRangingConstants()
{ {
int i, res; int i, res;
@ -564,6 +587,10 @@ public class UndefinedConstants
return getNumModelIterations() * getNumPropertyIterations(); return getNumModelIterations() * getNumPropertyIterations();
} }
/**
* Get a list of DefinedConstant objects: one for each ranging constant,
* i.e. each constant that has range > 1.
*/
public Vector<DefinedConstant> getRangingConstants() public Vector<DefinedConstant> getRangingConstants()
{ {
int i; int i;

Loading…
Cancel
Save