Browse Source

accumulation: add track status to Product.toDot

accumulation
Sascha Wunderlich 7 years ago
parent
commit
c2ceb299dd
  1. 18
      prism/src/explicit/AccumulationProduct.java

18
prism/src/explicit/AccumulationProduct.java

@ -292,6 +292,20 @@ public abstract class AccumulationProduct<M extends Model,Component> extends Pro
return initialAccStateId;
}
private String labelString(Integer stateId) {
StringBuffer result = new StringBuffer();
for(int t=0; t<numberOfTracks; t++) {
result.append(" " + t);
if(initStates.get(t).get(stateId)) { result.append("I"); continue; }
if(goalStates.get(t).get(stateId)) { result.append("G"); continue; }
if(runStates.get(t).get(stateId)) { result.append("R"); continue; }
result.append("_");
}
return result.toString();
}
@Override
public String toDot() {
StringBuffer result = new StringBuffer();
@ -309,7 +323,9 @@ public abstract class AccumulationProduct<M extends Model,Component> extends Pro
+ "<TR>"
+ "<TD>" + i + "=" + fromState + "</TD>"
+ "</TR><TR>"
+ "<TD> " + accState + "</TD>"
+ "<TD> " + accState + "</TD>"
+ "</TR><TR>"
+ "<TD> " + labelString(i) + "</TD>"
+ "</TR><TR>"
+ "<TD>\"" + Dottable.quoteForDot(tracker.toString()) + "\"</TD>"
+ "</TR>"

Loading…
Cancel
Save