s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Code tidy. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@745 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 18 years ago
parent
747dd1de38
commit
a295451149
3 changed files with 24 additions and 28 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      prism/src/jdd/JDD.java
  2. 42
      prism/src/prism/Modules2MTBDD.java
  3. 6
      prism/src/prism/ProbModel.java

4
prism/src/jdd/JDD.java
View File

@ -110,7 +110,7 @@ public class JDD
private static native void DD_PrintVectorFiltered(long dd, long filter, long vars, int num_vars, int accuracy);
// dd_export
private static native void DD_ExportDDToDotFile(long dd, String filename);
private static native void DD_ExportDDToDotFileLabelled(long dd, String filename, Vector var_names);
private static native void DD_ExportDDToDotFileLabelled(long dd, String filename, Vector<String> var_names);
private static native void DD_ExportMatrixToPPFile(long dd, long rvars, int num_rvars, long cvars, int num_cvars, String filename);
private static native void DD_ExportMatrixToMatlabFile(long dd, long rvars, int num_rvars, long cvars, int num_cvars, String name, String filename);
private static native void DD_ExportMatrixToSpyFile(long dd, long rvars, int num_rvars, long cvars, int num_cvars, int depth, String filename);
@ -911,7 +911,7 @@ public class JDD
// export dd to a dot file
// [ REFS: <none>, DEREFS: <none> ]
public static void ExportDDToDotFileLabelled(JDDNode dd, String filename, Vector varNames)
public static void ExportDDToDotFileLabelled(JDDNode dd, String filename, Vector<String> varNames)
{
DD_ExportDDToDotFileLabelled(dd.ptr(), filename, varNames);
}

42
prism/src/prism/Modules2MTBDD.java
View File

@ -68,7 +68,7 @@ public class Modules2MTBDD
private Values constantValues; // values of constants
// synch info
private int numSynchs; // number of synchronisations
private Vector synchs; // synchronisations
private Vector<String> synchs; // synchronisations
// rewards
private int numRewardStructs; // number of reward structs
private String[] rewardStructNames; // reward struct names
@ -109,7 +109,7 @@ public class Modules2MTBDD
private JDDNode[] ddSchedVars; // individual dd vars for scheduling non-det.
private JDDNode[] ddChoiceVars; // individual dd vars for local non-det.
// names for all dd vars used
private Vector ddVarNames;
private Vector<String> ddVarNames;
// flags for keeping track of which variables have been used
private boolean[] varsUsed;
@ -137,11 +137,11 @@ public class Modules2MTBDD
public ComponentDDs ind; // for independent bit (i.e. tau action)
public ComponentDDs[] synchs; // for each synchronising action
public JDDNode id; // mtbdd for identity matrix
public HashSet allSynchs; // set of all synchs used (syntactic)
public HashSet<String> allSynchs; // set of all synchs used (syntactic)
public SystemDDs(int n)
{
synchs = new ComponentDDs[n];
allSynchs = new HashSet();
allSynchs = new HashSet<String>();
}
}
@ -294,9 +294,9 @@ public class Modules2MTBDD
private void allocateDDVars()
{
JDDNode v, vr, vc;
int i, j, l, m, n, last;
int i, j, m, n, last;
int ddVarsUsed = 0;
ddVarNames = new Vector();
ddVarNames = new Vector<String>();
switch (prism.getOrdering()) {
@ -632,10 +632,8 @@ public class Modules2MTBDD
private void translateModules() throws PrismException
{
SystemFullParallel sys;
Module module;
String synch;
JDDNode moduleDD, indDD = null, synchDD, id, dd, tmp;
int i, j, m, numCommands;
JDDNode tmp;
int i;
varsUsed = new boolean[numVars];
@ -840,7 +838,7 @@ public class Modules2MTBDD
sysDDs.ind = translateModule(m, module, "", 0);
// build mtbdd for each synchronising action
for (i = 0; i < numSynchs; i++) {
synch = (String)synchs.elementAt(i);
synch = synchs.elementAt(i);
sysDDs.synchs[i] = translateModule(m, module, synch, synchMin[i]);
}
// store identity matrix
@ -963,7 +961,7 @@ public class Modules2MTBDD
// go thru all synchronising actions and decide if we will synchronise on each one
synchBool = new boolean[numSynchs];
for (i = 0; i < numSynchs; i++) {
synchBool[i] = sys.containsAction((String)synchs.elementAt(i));
synchBool[i] = sys.containsAction(synchs.elementAt(i));
}
// construct mtbdds for first operand
@ -1015,15 +1013,14 @@ public class Modules2MTBDD
private SystemDDs translateSystemHide(SystemHide sys, int[] synchMin) throws PrismException
{
SystemDDs sysDDs1, sysDDs;
JDDNode v, tmp;
int[] newSynchMin;
int i, j;
int i;
// reset synchMin to 0 for actions to be hidden
// store this in new array - old one may still be used elsewhere
newSynchMin = new int[numSynchs];
for (i = 0; i < numSynchs; i++) {
if (sys.containsAction((String)synchs.elementAt(i))) {
if (sys.containsAction(synchs.elementAt(i))) {
newSynchMin[i] = 0;
}
else {
@ -1046,7 +1043,7 @@ public class Modules2MTBDD
// if the action is in the set to be hidden, hide it...
// note that it doesn't matter if an action is included more than once in the set
// (although this would be picked up during the syntax check anyway)
if (sys.containsAction((String)synchs.elementAt(i))) {
if (sys.containsAction(synchs.elementAt(i))) {
// move these transitions into the independent bit
sysDDs.ind = combineComponentDDs(sysDDs.ind, sysDDs1.synchs[i]);
@ -1082,11 +1079,10 @@ public class Modules2MTBDD
private SystemDDs translateSystemRename(SystemRename sys, int[] synchMin) throws PrismException
{
SystemDDs sysDDs1, sysDDs;
JDDNode v, tmp;
int[] newSynchMin;
int i, j;
String s;
Iterator iter;
Iterator<String> iter;
// swap some values in synchMin due to renaming
// store this in new array - old one may still be used elsewhere
@ -1094,7 +1090,7 @@ public class Modules2MTBDD
for (i = 0; i < numSynchs; i++) {
// find out what this action is renamed to
// (this may be itself, i.e. it's not renamed)
s = sys.getNewName((String)synchs.elementAt(i));
s = sys.getNewName(synchs.elementAt(i));
j = synchs.indexOf(s);
if (j == -1) {
throw new PrismLangException("Invalid action name \"" + s + "\" in renaming", sys);
@ -1127,7 +1123,7 @@ public class Modules2MTBDD
// find out what this action is renamed to
// (this may be itself, i.e. it's not renamed)
// then add it to result
s = sys.getNewName((String)synchs.elementAt(i));
s = sys.getNewName(synchs.elementAt(i));
j = synchs.indexOf(s);
if (j == -1) {
throw new PrismLangException("Invalid action name \"" + s + "\" in renaming", sys);
@ -1141,7 +1137,7 @@ public class Modules2MTBDD
// modify list of synchs
iter = sysDDs1.allSynchs.iterator();
while (iter.hasNext()) {
sysDDs.allSynchs.add(sys.getNewName((String)iter.next()));
sysDDs.allSynchs.add(sys.getNewName(iter.next()));
}
return sysDDs;
@ -1295,7 +1291,7 @@ public class Modules2MTBDD
private ComponentDDs translateModule(int m, Module module, String synch, int synchMin) throws PrismException
{
ComponentDDs compDDs;
JDDNode guardDDs[], upDDs[], rewDDs[], tmp;
JDDNode guardDDs[], upDDs[], tmp;
Command command;
int l, numCommands;
double dmin = 0, dmax = 0;
@ -1564,7 +1560,7 @@ public class Modules2MTBDD
{
ComponentDDs compDDs;
int i, j, k, maxChoices, numDDChoiceVarsUsed;
JDDNode covered, transDD, overlaps, equalsi, tmp, tmp2, tmp3, v;
JDDNode covered, transDD, overlaps, equalsi, tmp, tmp2, tmp3;
//JDDNode rewardsDD;
JDDNode[] transDDbits, frees;
//JDDNode[] rewardsDDbits;

6
prism/src/prism/ProbModel.java
View File

@ -84,7 +84,7 @@ public class ProbModel implements Model
protected JDDVars allDDRowVars; // all dd vars (rows)
protected JDDVars allDDColVars; // all dd vars (cols)
// names for all dd vars used
protected Vector ddVarNames;
protected Vector<String> ddVarNames;
protected ODDNode odd; // odd
@ -355,7 +355,7 @@ public class ProbModel implements Model
return allDDRowVars.n() * 2;
}
public Vector getDDVarNames()
public Vector<String> getDDVarNames()
{
return ddVarNames;
}
@ -378,7 +378,7 @@ public class ProbModel implements Model
// constructor
public ProbModel(JDDNode tr, JDDNode tr01, JDDNode s, JDDNode r, JDDNode dl, JDDNode sr[], JDDNode trr[],
String rsn[], JDDVars arv, JDDVars acv, Vector ddvn, int nm, String[] mn, JDDVars[] mrv, JDDVars[] mcv,
String rsn[], JDDVars arv, JDDVars acv, Vector<String> ddvn, int nm, String[] mn, JDDVars[] mrv, JDDVars[] mcv,
int nv, VarList vl, JDDVars[] vrv, JDDVars[] vcv, Values cv)
{
int i;

Write Preview
Loading…
Cancel
Save