Browse Source

accumulation: fix simple method

accumulation
Sascha Wunderlich 7 years ago
parent
commit
bb47b0a819
  1. 2
      prism/src/explicit/AccumulationProduct.java
  2. 4
      prism/src/explicit/AccumulationState.java
  3. 4
      prism/src/explicit/AccumulationTransformation.java

2
prism/src/explicit/AccumulationProduct.java

@ -262,7 +262,7 @@ public abstract class AccumulationProduct<M extends Model,Component> extends Pro
// If this is a simple Product, we only set the GoalState and return
if(ctx.simpleMethod) {
goalStates.get(0).set(index, accState.hasGoodTracks());
goalStates.get(0).set(index, accState.importantTrackIsGood());
return;
}

4
prism/src/explicit/AccumulationState.java

@ -48,6 +48,10 @@ public class AccumulationState<Component> {
return !goodTracks.isEmpty();
}
public boolean importantTrackIsGood() {
return goodTracks.get(getNextRestartNr());
}
public BitSet getGoodTracks() {
return goodTracks;
}

4
prism/src/explicit/AccumulationTransformation.java

@ -133,7 +133,9 @@ public class AccumulationTransformation<M extends ModelExplicit> implements Mode
// Build the AccumulationContext
AccumulationContext ctx = new AccumulationContext(accexp, rewards, mc);
ctx.singleTrack = isSingleTrack && !forceMulti;
ctx.simpleMethod = isSimple && !forceComplex && !forceMulti;
ctx.simpleMethod = isSimple && !forceComplex;
mc.getLog().println("Using optimizations single/simple " + ctx.singleTrack + "/" + ctx.simpleMethod);
// Build the product
clock.start("accumulation product construction");

Loading…
Cancel
Save