Browse Source

Fix format of exported transient/steady-state vectors.

Introduced in symbolic engines during recent-ish refactoring.
Seems to have been wrong in explicit engines for longer.
Format is 0=0.27109177824020264, not 0:=0.27109177824020264
accumulation-v4.7
Dave Parker 6 years ago
parent
commit
1e0ffc1c49
  1. 10
      prism/src/explicit/StateValues.java
  2. 8
      prism/src/prism/StateAndValuePrinter.java

10
prism/src/explicit/StateValues.java

@ -1706,15 +1706,19 @@ public class StateValues implements StateVector
} else {
if (printIndices) {
log.print(n);
log.print(":");
}
if (printStates && statesList != null)
if (printStates && statesList != null) {
if (printIndices) {
log.print(":");
}
log.print(statesList.get(n).toString());
}
if (printSparse && type instanceof TypeBool) {
log.println();
} else {
if (printIndices || printStates)
if (printIndices || printStates) {
log.print("=");
}
log.println(getValue(n));
}
}

8
prism/src/prism/StateAndValuePrinter.java

@ -94,9 +94,12 @@ class StateAndValuePrinter implements StateAndValueConsumer
// PRISM format
if (printIndices) {
outputLog.print(stateIndex + ":");
outputLog.print(stateIndex);
}
if (printStates) {
if (printIndices) {
outputLog.print(":");
}
outputLog.print("(");
int n = varList.getNumVars();
for (int i = 0; i < n; i++) {
@ -114,8 +117,9 @@ class StateAndValuePrinter implements StateAndValueConsumer
}
outputLog.print(")");
}
if (printIndices || printStates)
if (printIndices || printStates) {
outputLog.print("=");
}
outputLog.println(value);
}

Loading…
Cancel
Save