Browse Source

PathToText respects new "change" option + bugfixes.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5397 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 14 years ago
parent
commit
6d9806ad16
  1. 18
      prism/src/simulator/GenerateSimulationPath.java
  2. 80
      prism/src/simulator/PathToText.java

18
prism/src/simulator/GenerateSimulationPath.java

@ -60,6 +60,7 @@ public class GenerateSimulationPath
private boolean simLoopCheck = true;
private int simPathRepeat = 1;
private boolean simPathShowRewards = false;
private boolean simPathShowChangesOnly = false;
private boolean simPathSnapshots = false;
private double simPathSnapshotTime = 0.0;
@ -224,15 +225,24 @@ public class GenerateSimulationPath
} catch (NumberFormatException e) {
throw new PrismException("Value for \"snapshot\" option must be a positive double");
}
} else if (ss[i].equals("rewards=")) {
} else if (ss[i].indexOf("rewards=") == 0) {
// display rewards?
String bool = ss[i].substring(8).toLowerCase();
if (bool.equals("true"))
simPathShowRewards = true;
else if (bool.equals("true"))
simPathShowRewards = true;
else if (bool.equals("false"))
simPathShowRewards = false;
else
throw new PrismException("Value for \"rewards\" option must \"true\" or \"false\"");
} else if (ss[i].indexOf("changes=") == 0) {
// display changes only?
String bool = ss[i].substring(8).toLowerCase();
if (bool.equals("true"))
simPathShowChangesOnly = true;
else if (bool.equals("false"))
simPathShowChangesOnly = false;
else
throw new PrismException("Value for \"changes\" option must \"true\" or \"false\"");
} else {
// path of fixed number of steps
simPathType = PathType.SIM_PATH_NUM_STEPS;
@ -275,6 +285,7 @@ public class GenerateSimulationPath
displayer.setColSep(simPathSep);
displayer.setVarsToShow(simVars);
displayer.setShowRewards(simPathShowRewards);
displayer.setShowChangesOnly(simPathShowChangesOnly);
if (simPathSnapshots)
displayer.setToShowSnapShots(simPathSnapshotTime);
@ -290,6 +301,7 @@ public class GenerateSimulationPath
displayer = new PathToGraph(graphModel, modulesFile);
displayer.setShowRewards(simPathShowRewards);
displayer.setShowChangesOnly(simPathShowChangesOnly);
if (simPathSnapshots)
displayer.setToShowSnapShots(simPathSnapshotTime);

80
prism/src/simulator/PathToText.java

@ -58,6 +58,8 @@ public class PathToText extends PathDisplayer
private State lastState;
/** Last state rewards */
private double[] lastStateRewards;
/** Did the displayed info change in the current step? */
private boolean changed;
/**
* Construct a {@link PathToText} object
@ -102,7 +104,7 @@ public class PathToText extends PathDisplayer
}
// Display methods
@Override
public void startDisplay(State initialState, double[] initialStateRewards)
{
@ -142,6 +144,7 @@ public class PathToText extends PathDisplayer
log.println();
// Display initial step
changed = true;
step = 0;
firstCol = true;
if (!getShowSnapshots()) {
@ -162,35 +165,28 @@ public class PathToText extends PathDisplayer
@Override
public void displayStep(double timeSpent, double timeCumul, Object action, double[] transitionRewards, State newState, double[] newStateRewards)
{
step++;
// (if required) see if relevant vars have changed
if (varsToShow != null && step > 0) {
boolean changed = false;
for (int v : varsToShow){
if (!newState.varValues[v].equals(lastState.varValues[v])) {
changed = true;
continue;
if (!showChangesOnly || changed) {
// display rewards for last state
if (getShowRewards()) {
for (int j = 0; j < numRewardStructs; j++) {
log.print(getColSep() + lastStateRewards[j]);
log.print(getColSep() + transitionRewards[j]);
}
}
if (!changed) {
return;
}
// display time spent in state
if (contTime && showTimeSpent)
log.print(getColSep() + timeSpent);
log.println();
}
// display rewards for last state
if (getShowRewards()) {
for (int j = 0; j < numRewardStructs; j++) {
log.print(getColSep() + lastStateRewards[j]);
log.print(getColSep() + transitionRewards[j]);
}
explicit.Utils.copyDoubleArray(newStateRewards, lastStateRewards);
// if required, check whether the info to be displayed changed
if (showChangesOnly) {
changed = stateChanged(lastState, newState) || rewardsChanged(lastStateRewards, newStateRewards);
if (!changed)
return;
}
// display time spent in state
if (contTime && showTimeSpent)
log.print(getColSep() + timeSpent);
log.println();
step++;
firstCol = true;
// display action
@ -202,6 +198,10 @@ public class PathToText extends PathDisplayer
log.print(getColSep() + timeCumul);
// display state
displayState(newState);
// store state rewards
if (getShowRewards()) {
explicit.Utils.copyDoubleArray(newStateRewards, lastStateRewards);
}
}
@Override
@ -251,10 +251,40 @@ public class PathToText extends PathDisplayer
}
}
private boolean stateChanged(State lastState, State newState)
{
if (varsToShow == null) {
for (int j = 0; j < numVars; j++) {
if (!newState.varValues[j].equals(lastState.varValues[j])) {
return true;
}
}
} else {
for (int v : varsToShow) {
if (!newState.varValues[v].equals(lastState.varValues[v])) {
return true;
}
}
}
return false;
}
private boolean rewardsChanged(double[] lastStateRewards, double[] newStateRewards)
{
if (!showRewards)
return false;
for (int j = 0; j < numRewardStructs; j++) {
if (newStateRewards[j] != lastStateRewards[j]) {
return true;
}
}
return false;
}
@Override
public void endDisplay()
{
if (!getShowSnapshots()) {
if (!getShowSnapshots() && (!showChangesOnly || changed)) {
// display state rewards for last state
// (transition rewards unknown because no outgoing transition)
if (getShowRewards()) {

Loading…
Cancel
Save