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

Improvements to output of DD vars for -extraddinfo switch. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@322 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 19 years ago
parent
988e8cd89a
commit
2b39714fda
3 changed files with 51 additions and 19 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. 31
      prism/src/prism/NondetModel.java
  2. 20
      prism/src/prism/ProbModel.java
  3. 19
      prism/src/prism/StochModel.java

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

@ -290,7 +290,7 @@ public class NondetModel implements Model
public void printTransInfo(PrismLog log) { printTransInfo(log, false); }
public void printTransInfo(PrismLog log, boolean extra)
{
int i;
int i, j, n;
log.print("States: " + getNumStatesString() + " (" + getNumStartStatesString() + " initial)" + "\n");
log.print("Transitions: " + getNumTransitionsString() + "\n");
@ -303,13 +303,28 @@ 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");
if (extra) log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n");
if (extra) log.print("Mask: " + JDD.GetNumNodes(nondetMask) + " nodes, ");
if (extra) log.print(JDD.GetNumMintermsString(nondetMask, getNumDDRowVars()+getNumDDNondetVars()) + " minterms\n");
if (extra) {
log.print("DD vars (nd):");
n = allDDNondetVars.getNumVars();
for (i = 0; i < n; i++) {
j = allDDNondetVars.getVarIndex(i);
log.print(" "+j+":"+ddVarNames.get(j));
}
log.println();
log.print("DD vars (r/c):");
n = allDDRowVars.getNumVars();
for (i = 0; i < n; i++) {
j = allDDRowVars.getVarIndex(i);
log.print(" "+j+":"+ddVarNames.get(j));
j = allDDColVars.getVarIndex(i);
log.print(" "+j+":"+ddVarNames.get(j));
}
log.println();
log.print("Transition matrix terminals: " + JDD.GetTerminalsAndNumbersString(trans, getNumDDVarsInTrans())+"\n");
log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n");
log.print("Mask: " + JDD.GetNumNodes(nondetMask) + " nodes, ");
log.print(JDD.GetNumMintermsString(nondetMask, getNumDDRowVars()+getNumDDNondetVars()) + " minterms\n");
}
for (i = 0; i < numRewardStructs; i++) {
if (stateRewards[i] != null && !stateRewards[i].equals(JDD.ZERO)) {

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

@ -251,7 +251,7 @@ public class ProbModel implements Model
public void printTransInfo(PrismLog log) { printTransInfo(log, false); }
public void printTransInfo(PrismLog log, boolean extra)
{
int i;
int i, j, n;
log.print("States: " + getNumStatesString() + " (" + getNumStartStatesString() + " initial)" + "\n");
log.print("Transitions: " + getNumTransitionsString() + "\n");
@ -263,11 +263,19 @@ 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");
if (extra) log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n");
if (extra) {
log.print("DD vars (r/c):");
n = allDDRowVars.getNumVars();
for (i = 0; i < n; i++) {
j = allDDRowVars.getVarIndex(i);
log.print(" "+j+":"+ddVarNames.get(j));
j = allDDColVars.getVarIndex(i);
log.print(" "+j+":"+ddVarNames.get(j));
}
log.println();
log.print("Transition matrix terminals: " + JDD.GetTerminalsAndNumbersString(trans, getNumDDVarsInTrans())+"\n");
log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n");
}
for (i = 0; i < numRewardStructs; i++) {
if (stateRewards[i] != null && !stateRewards[i].equals(JDD.ZERO)) {
log.print("State rewards ("+i+"): ");

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

@ -251,7 +251,7 @@ public class StochModel implements Model
public void printTransInfo(PrismLog log) { printTransInfo(log, false); }
public void printTransInfo(PrismLog log, boolean extra)
{
int i;
int i, j, n;
log.print("States: " + getNumStatesString() + " (" + getNumStartStatesString() + " initial)" + "\n");
log.print("Transitions: " + getNumTransitionsString() + "\n");
@ -263,10 +263,19 @@ 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");
if (extra) log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n");
if (extra) {
log.print("DD vars (r/c):");
n = allDDRowVars.getNumVars();
for (i = 0; i < n; i++) {
j = allDDRowVars.getVarIndex(i);
log.print(" "+j+":"+ddVarNames.get(j));
j = allDDColVars.getVarIndex(i);
log.print(" "+j+":"+ddVarNames.get(j));
}
log.println();
log.print("Rate matrix terminals: " + JDD.GetTerminalsAndNumbersString(trans, getNumDDVarsInTrans())+"\n");
log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n");
}
for (i = 0; i < numRewardStructs; i++) {
if (stateRewards[i] != null && !stateRewards[i].equals(JDD.ZERO)) {

Write Preview
Loading…
Cancel
Save