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

Added -extraddinfo command-line switch to display extra info about some (MT)BDDs. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@309 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 19 years ago
parent
4c05bfcab6
commit
1ab82223c8
6 changed files with 35 additions and 12 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/dd/dd_info.cc
  2. 3
      prism/src/prism/Model.java
  3. 12
      prism/src/prism/NondetModel.java
  4. 10
      prism/src/prism/PrismCL.java
  5. 9
      prism/src/prism/ProbModel.java
  6. 9
      prism/src/prism/StochModel.java

4
prism/src/dd/dd_info.cc
View File

@ -176,7 +176,7 @@ bool and_numbers)
Cudd_Ref(dd);
tmp = dd;
// Check the min (will use at end)
min = Cudd_V(Cudd_addFindMin(ddman, dd));
min = Cudd_V(Cudd_addFindMin(ddman, tmp));
// Loop through terminals in descending order
while (tmp != Cudd_ReadMinusInfinity(ddman)) {
// Find next (max) terminal and display
@ -195,7 +195,7 @@ bool and_numbers)
Cudd_RecursiveDeref(ddman, tmp);
// Finally, print if there are (and possibly how many) minus infinities
if (and_numbers) {
if (count < pow(2, num_vars)) fprintf(dd_out, "-inf (%.0f)", pow(2, num_vars) - count);
if (count < (1<<num_vars)) fprintf(dd_out, "-inf (%.0f)", pow(2, num_vars) - count);
} else {
if (min == -HUGE_VAL) fprintf(dd_out, "-inf");
}

3
prism/src/prism/Model.java
View File

@ -96,7 +96,8 @@ public interface Model
void fixDeadlocks();
void printTrans();
void printTrans01();
void printTransInfo(PrismLog log);
public void printTransInfo(PrismLog log);
public void printTransInfo(PrismLog log, boolean extra);
void exportToFile(int exportType, boolean explicit, File file) throws FileNotFoundException;
String exportStateRewardsToFile(int exportType, File file) throws FileNotFoundException, PrismException;
String exportTransRewardsToFile(int exportType, boolean explicit, File file) throws FileNotFoundException, PrismException;

12
prism/src/prism/NondetModel.java
View File

@ -287,7 +287,8 @@ public class NondetModel implements Model
// JDD.PrintMatrix(trans01, allDDRowVars, allDDColVars, JDD.ZERO_ONE);
}
public void printTransInfo(PrismLog log)
public void printTransInfo(PrismLog log) { printTransInfo(log, false); }
public void printTransInfo(PrismLog log, boolean extra)
{
int i;
@ -302,10 +303,13 @@ public class NondetModel implements Model
log.print(JDD.GetNumTerminals(trans) + " terminal), ");
log.print(JDD.GetNumMintermsString(trans, getNumDDVarsInTrans()) + " minterms, ");
log.print("vars: " + getNumDDRowVars() + "r/" + getNumDDColVars() + "c/" + getNumDDNondetVars() + "nd\n");
if (extra) log.println("DD var names: " + getDDVarNames());
if (extra) log.print("Transition matrix terminals: " + JDD.GetTerminalsAndNumbersString(trans, getNumDDVarsInTrans())+"\n");
//log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n");
if (extra) log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n");
//log.print("Mask: " + JDD.GetNumNodes(nondetMask) + " nodes\n");
if (extra) log.print("Mask: " + JDD.GetNumNodes(nondetMask) + " nodes, ");
if (extra) log.print(JDD.GetNumMintermsString(nondetMask, getNumDDRowVars()+getNumDDNondetVars()) + " minterms\n");
for (i = 0; i < numRewardStructs; i++) {
if (stateRewards[i] != null && !stateRewards[i].equals(JDD.ZERO)) {
@ -313,12 +317,14 @@ public class NondetModel implements Model
log.print(JDD.GetNumNodes(stateRewards[i]) + " nodes (");
log.print(JDD.GetNumTerminals(stateRewards[i]) + " terminal), ");
log.print(JDD.GetNumMintermsString(stateRewards[i], getNumDDRowVars()) + " minterms\n");
if (extra) log.print("State rewards ("+i+") terminals : " + JDD.GetTerminalsAndNumbersString(stateRewards[i], getNumDDRowVars())+"\n");
}
if (transRewards[i] != null && !transRewards[i].equals(JDD.ZERO)) {
log.print("Transition rewards ("+i+"): ");
log.print(JDD.GetNumNodes(transRewards[i]) + " nodes (");
log.print(JDD.GetNumTerminals(transRewards[i]) + " terminal), ");
log.print(JDD.GetNumMintermsString(transRewards[i], getNumDDVarsInTrans()) + " minterms\n");
if (extra) log.print("Transition rewards ("+i+") terminals : " + JDD.GetTerminalsAndNumbersString(transRewards[i], getNumDDVarsInTrans())+"\n");
}
}
}

10
prism/src/prism/PrismCL.java
View File

@ -60,6 +60,7 @@ public class PrismCL
private boolean exportordered = true;
private boolean simulate = false;
private boolean simpath = false;
private boolean extraDDInfo = false;
private int typeOverride = 0;
// property info
@ -557,7 +558,7 @@ public class PrismCL
// otherwise print error and bail out
else {
mainLog.println();
model.printTransInfo(mainLog);
model.printTransInfo(mainLog, extraDDInfo);
mainLog.print("\nError: Model contains " + states.size() + " deadlock states");
if (!verbose && states.size() > 10) {
mainLog.print(".\nThe first 10 deadlock states are displayed below. To view them all use the -v switch.\n");
@ -575,7 +576,7 @@ public class PrismCL
// print more model info
mainLog.println();
model.printTransInfo(mainLog);
model.printTransInfo(mainLog, extraDDInfo);
}
// do any exporting requested
@ -1156,6 +1157,10 @@ public class PrismCL
prism.setVerbose(true);
verbose = true;
}
// extra dd info on
else if (sw.equals("extraddinfo")) {
extraDDInfo = true;
}
// precomputation algs off
else if (sw.equals("nopre")) {
prism.setPrecomp(false);
@ -1485,6 +1490,7 @@ public class PrismCL
mainLog.println("-maxiters <n> .................. Set max number of iterations [default 10000]");
mainLog.println();
mainLog.println("-verbose (or -v) ............... Verbose mode: print out state lists and probability vectors");
mainLog.println("-extraddinfo ................... Display extra info about some (MT)BDDs");
mainLog.println("-nopre ......................... Skip precomputation algorithms");
mainLog.println("-fair .......................... Use fairness (when model checking PCTL on MDPs)");
mainLog.println("-nofair ........................ Don't use fairness (when model checking PCTL on MDPs) [default]");

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

@ -248,7 +248,8 @@ public class ProbModel implements Model
// JDD.PrintMatrix(trans01, allDDRowVars, allDDColVars, JDD.ZERO_ONE);
}
public void printTransInfo(PrismLog log)
public void printTransInfo(PrismLog log) { printTransInfo(log, false); }
public void printTransInfo(PrismLog log, boolean extra)
{
int i;
@ -262,8 +263,10 @@ public class ProbModel implements Model
log.print(JDD.GetNumTerminals(trans) + " terminal), ");
log.print(JDD.GetNumMintermsString(trans, getNumDDVarsInTrans()) + " minterms, ");
log.print("vars: " + getNumDDRowVars() + "r/" + getNumDDColVars() + "c\n");
if (extra) log.println("DD var names: " + getDDVarNames());
if (extra) log.print("Transition matrix terminals: " + JDD.GetTerminalsAndNumbersString(trans, getNumDDVarsInTrans())+"\n");
//log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n");
if (extra) log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n");
for (i = 0; i < numRewardStructs; i++) {
if (stateRewards[i] != null && !stateRewards[i].equals(JDD.ZERO)) {
@ -271,12 +274,14 @@ public class ProbModel implements Model
log.print(JDD.GetNumNodes(stateRewards[i]) + " nodes (");
log.print(JDD.GetNumTerminals(stateRewards[i]) + " terminal), ");
log.print(JDD.GetNumMintermsString(stateRewards[i], getNumDDRowVars()) + " minterms\n");
if (extra) log.print("State rewards ("+i+") terminals : " + JDD.GetTerminalsAndNumbersString(stateRewards[i], getNumDDRowVars())+"\n");
}
if (transRewards[i] != null && !transRewards[i].equals(JDD.ZERO)) {
log.print("Transition rewards ("+i+"): ");
log.print(JDD.GetNumNodes(transRewards[i]) + " nodes (");
log.print(JDD.GetNumTerminals(transRewards[i]) + " terminal), ");
log.print(JDD.GetNumMintermsString(transRewards[i], getNumDDVarsInTrans()) + " minterms\n");
if (extra) log.print("Transition rewards ("+i+") terminals : " + JDD.GetTerminalsAndNumbersString(transRewards[i], getNumDDVarsInTrans())+"\n");
}
}
}

9
prism/src/prism/StochModel.java
View File

@ -248,7 +248,8 @@ public class StochModel implements Model
// JDD.PrintMatrix(trans01, allDDRowVars, allDDColVars, JDD.ZERO_ONE);
}
public void printTransInfo(PrismLog log)
public void printTransInfo(PrismLog log) { printTransInfo(log, false); }
public void printTransInfo(PrismLog log, boolean extra)
{
int i;
@ -262,8 +263,10 @@ public class StochModel implements Model
log.print(JDD.GetNumTerminals(trans) + " terminal), ");
log.print(JDD.GetNumMintermsString(trans, getNumDDVarsInTrans()) + " minterms, ");
log.print("vars: " + getNumDDRowVars() + "r/" + getNumDDColVars() + "c\n");
if (extra) log.println("DD var names: " + getDDVarNames());
if (extra) log.print("Rate matrix terminals: " + JDD.GetTerminalsAndNumbersString(trans, getNumDDVarsInTrans())+"\n");
//log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n");
if (extra) log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n");
for (i = 0; i < numRewardStructs; i++) {
if (stateRewards[i] != null && !stateRewards[i].equals(JDD.ZERO)) {
@ -271,12 +274,14 @@ public class StochModel implements Model
log.print(JDD.GetNumNodes(stateRewards[i]) + " nodes (");
log.print(JDD.GetNumTerminals(stateRewards[i]) + " terminal), ");
log.print(JDD.GetNumMintermsString(stateRewards[i], getNumDDRowVars()) + " minterms\n");
if (extra) log.print("State rewards ("+i+") terminals : " + JDD.GetTerminalsAndNumbersString(stateRewards[i], getNumDDRowVars())+"\n");
}
if (transRewards[i] != null && !transRewards[i].equals(JDD.ZERO)) {
log.print("Transition rewards ("+i+"): ");
log.print(JDD.GetNumNodes(transRewards[i]) + " nodes (");
log.print(JDD.GetNumTerminals(transRewards[i]) + " terminal), ");
log.print(JDD.GetNumMintermsString(transRewards[i], getNumDDVarsInTrans()) + " minterms\n");
if (extra) log.print("Transition rewards ("+i+") terminals : " + JDD.GetTerminalsAndNumbersString(transRewards[i], getNumDDVarsInTrans())+"\n");
}
}
}

Write Preview
Loading…
Cancel
Save