From 28f49ddc167e953355568506319bebffb4d65509 Mon Sep 17 00:00:00 2001 From: Sascha Wunderlich Date: Fri, 21 Dec 2018 14:27:16 +0100 Subject: [PATCH] accumulation: deduplicate product code --- prism/src/explicit/AccumulationProduct.java | 100 ++++++++++++++- .../explicit/AccumulationProductComplex.java | 119 +----------------- .../AccumulationProductComplexCounting.java | 10 -- .../explicit/AccumulationProductSimple.java | 110 ---------------- prism/src/explicit/AccumulationState.java | 20 ++- 5 files changed, 109 insertions(+), 250 deletions(-) diff --git a/prism/src/explicit/AccumulationProduct.java b/prism/src/explicit/AccumulationProduct.java index cc77fedc..fd93235f 100644 --- a/prism/src/explicit/AccumulationProduct.java +++ b/prism/src/explicit/AccumulationProduct.java @@ -5,6 +5,7 @@ import java.util.BitSet; import java.util.Iterator; import java.util.Map; import parser.ast.AccumulationFactor; +import parser.ast.Expression; import prism.IntegerBound; import prism.PrismException; @@ -67,6 +68,90 @@ public abstract class AccumulationProduct extends Pro protected abstract Component updateComponent(Integer modelFromStateId, final AccumulationTrack track); + protected final AccumulationTrack updateTrack(Integer modelFromStateId, final AccumulationTrack track, final double[] weights) { + Component nextComponent = updateComponent(modelFromStateId, track); + + // If we are done, return null-Track + if (nextComponent == null) { return null; } + + // Otherwise, we update the weights and increase the step. + double[] newweights = new double[weights.length]; + for (int i = 0; i < weights.length; i++) { + newweights[i] = weights[i] + track.getWeights()[i]; + } + + return new AccumulationTrack(newweights, nextComponent); + } + + protected final AccumulationState updateAccumulationState(final int modelFromStateId, final AccumulationState accstate, final double[] weights) throws PrismException { + // If we are in singleTrack mode and the last restart is the numberOfTracks, we can stop... + if(ctx.singleTrack && (accstate.lastRestartNr == numberOfTracks-1)) { return accstate; } + + // Check if we even need to fire here. + if(ctx.accexp.hasFireOn()) { + boolean stutter = true; + for(Expression f : ctx.accexp.getFireOn()) { + if(ctx.mc.checkExpression(originalModel, f, null).getBitSet().get(modelFromStateId)) { + //mc.getLog().println("f:" + f); + stutter = false; + break; + } + } + // If this is a stutter action, we can return the same accstate. Copies are made on modification. + if(stutter) { return accstate; } + } + // ...otherwise proceed. + + // Get the old tracker and tracks. + AccumulationTracker oldTracker = accstate.getTracker(trackers); + ArrayList> oldTracks = oldTracker.getTracks(); + + // This restart will be... + int newLastRestartNr = accstate.getNextRestartNr(); + //mc.getLog().print(newLastRestartNr); + + // Build the new tracks and determine their goodness; + ArrayList> newTracks = new ArrayList<>(); + BitSet newGoodTracks = (BitSet)accstate.getGoodTracks().clone(); + + int trackNr = 0; + for(AccumulationTrack oldTrack : oldTracks) { + + AccumulationTrack newTrack; + + // restart or advance + if(trackNr == newLastRestartNr && !ctx.singleTrack) { + // If we have a restart, we produce an initial track and let it advance. + // The goodness is cleared. + AccumulationTrack freshTrack = new AccumulationTrack(numberOfWeights, getInitialComponent()); + //newTrack = updateTrack(modelFromStateId, freshTrack, accexp, weights, mc); + newTrack = freshTrack; + newGoodTracks.clear(trackNr); + } else if (oldTrack == null || (ctx.singleTrack && trackNr>0)) { + // If the old track is undefined, the new track is as well. + // Goodness stays! + newTrack = null; + } else { + // Otherwise, the track is defined and advances. + // If it is not good yet, we check it. + assert oldTrack != null; + newTrack = updateTrack(modelFromStateId, oldTrack, weights); + if(!newGoodTracks.get(trackNr)) { + newGoodTracks.set(trackNr, isGoalTrack(newTrack)); + } + } + + newTracks.add(newTrack); + trackNr++; + } + + //Create a new tracker with the right tracks and add it to storage. + AccumulationTracker newTracker = new AccumulationTracker<>(newTracks); + int newTrackerId = trackers.findOrAdd(newTracker); + + return new AccumulationState<>(newTrackerId, newLastRestartNr, numberOfTracks, newGoodTracks); + } + /** * Creates the initial state for the accumulation part of this of this accumulation product. Returns its ID. * @@ -74,7 +159,20 @@ public abstract class AccumulationProduct extends Pro * where the first restart is the first (0th) track. * @return */ - protected abstract int createInitialStateId(); + protected final int createInitialStateId() { + Component initialComponent = getInitialComponent(); + + // The initial active track is the first one, all tracks are non-good by default + int initialActiveTrack = 0; + + // Generate the initial track and product state + AccumulationTracker initialTracker = new AccumulationTracker(numberOfTracks, numberOfWeights, initialComponent); + int initialTrackerId = trackers.findOrAdd(initialTracker); + AccumulationState initialAccState = new AccumulationState(initialTrackerId, initialActiveTrack, numberOfTracks); + int initialAccStateId = accStates.findOrAdd(initialAccState); + + return initialAccStateId; + } protected boolean isGoalTrack(AccumulationTrack track) throws PrismException { return isFinalTrack(track) && constraintHolds(track); diff --git a/prism/src/explicit/AccumulationProductComplex.java b/prism/src/explicit/AccumulationProductComplex.java index efe94675..6ab26450 100644 --- a/prism/src/explicit/AccumulationProductComplex.java +++ b/prism/src/explicit/AccumulationProductComplex.java @@ -5,7 +5,6 @@ import java.util.BitSet; import java.util.Iterator; import java.util.Map; -import parser.ast.Expression; import prism.PrismException; import common.Dottable; @@ -45,21 +44,6 @@ public abstract class AccumulationProductComplex exte return goalStates.get(track); } - protected final int createInitialStateId() { - Component initialComponent = getInitialComponent(); - - // The initial active track is the first one, all tracks are non-good by default - int initialActiveTrack = 0; - - // Generate the initial track and product state - AccumulationTracker initialTracker = new AccumulationTracker(numberOfTracks, numberOfWeights, initialComponent); - int initialTrackerId = trackers.findOrAdd(initialTracker); - AccumulationState initialAccState = new AccumulationState(initialTrackerId, initialActiveTrack, numberOfTracks, false); - int initialAccStateId = accStates.findOrAdd(initialAccState); - - return initialAccStateId; - } - protected void generateTrackInfo(ProductState state, Integer index) throws PrismException { AccumulationState accState = accStates.getById(state.getSecondState()); AccumulationTracker tracker = accState.getTracker(trackers); @@ -69,7 +53,7 @@ public abstract class AccumulationProductComplex exte boolean isInitial = trackIdx==accState.lastRestartNr; boolean isRunning = track != null; - boolean isGoal = isGoalTrack(track); + boolean isGoal = accState.getGoodTracks().get(trackIdx); // isGoalTrack(track) // Is this an initial initStates.get(trackIdx).set(index, isInitial); @@ -82,106 +66,7 @@ public abstract class AccumulationProductComplex exte } } - /** Updates a single AccumulationTrack. Used in updateAccumulationState. - * - * Uses updateComponent to get the next Component, accumulates the current weights - * and makes a new track. - * @param modelFromStateId - * @param track - * @param accexp - * @param weights - * @param mc - * @return - */ - protected final AccumulationTrack updateTrack(Integer modelFromStateId, final AccumulationTrack track, final double[] weights) { - Component nextComponent = updateComponent(modelFromStateId, track); - - // If we are done, return null-Track - if (nextComponent == null) { return null; } - - // Otherwise, we update the weights and increase the step. - double[] newweights = new double[weights.length]; - for (int i = 0; i < weights.length; i++) { - newweights[i] = weights[i] + track.getWeights()[i]; - } - - return new AccumulationTrack(newweights, nextComponent); - } - - /** Generates a new accumulation state from an old one. - * - * To do so, it reads the necessary information from the model and its rewards - * and updates all tracks and their goodness accordingly. - * @param modelFromStateId - * @param accstate - * @param accexp - * @param weights - * @param mc - * @return - * @throws PrismException - */ - protected final AccumulationState updateAccumulationState(final int modelFromStateId, final AccumulationState accstate, final double[] weights) throws PrismException { - // If we are in singleTrack mode and the last restart is the numberOfTracks, we can stop... - if(ctx.singleTrack && (accstate.lastRestartNr == numberOfTracks-1)) { return accstate; } - - - // Check if we even need to fire here. - if(ctx.accexp.hasFireOn()) { - boolean stutter = true; - for(Expression f : ctx.accexp.getFireOn()) { - if(ctx.mc.checkExpression(originalModel, f, null).getBitSet().get(modelFromStateId)) { - //mc.getLog().println("f:" + f); - stutter = false; - break; - } - } - // If this is a stutter action, we can return the same accstate. Copies are made on modification. - if(stutter) { return accstate; } - } - // ...otherwise proceed. - - // Get the old tracker and tracks. - AccumulationTracker oldTracker = accstate.getTracker(trackers); - ArrayList> oldTracks = oldTracker.getTracks(); - - // This restart will be... - int newLastRestartNr = accstate.getNextRestartNr(); - //mc.getLog().print(newLastRestartNr); - - // Build the new tracks and determine their goodness; - ArrayList> newTracks = new ArrayList<>(); - - int trackNr = 0; - for(AccumulationTrack oldTrack : oldTracks) { - - AccumulationTrack newTrack; - - // restart or advance - if(trackNr == newLastRestartNr && !ctx.singleTrack) { - // If we have a restart, we produce an initial track and let it advance. - AccumulationTrack freshTrack = new AccumulationTrack(numberOfWeights, getInitialComponent()); - //newTrack = updateTrack(modelFromStateId, freshTrack, accexp, weights, mc); - newTrack = freshTrack; - } else if (oldTrack == null || (ctx.singleTrack && trackNr>0)) { - // If the old track is undefined, the new track is as well. - newTrack = null; - } else { - // Otherwise, the track is defined and advances. - assert oldTrack != null; - newTrack = updateTrack(modelFromStateId, oldTrack, weights); - } - - newTracks.add(newTrack); - trackNr++; - } - - //Create a new tracker with the right tracks and add it to storage. - AccumulationTracker newTracker = new AccumulationTracker<>(newTracks); - int newTrackerId = trackers.findOrAdd(newTracker); - - return new AccumulationState<>(newTrackerId, newLastRestartNr, numberOfTracks); - } - + @Override protected String labelString(Integer stateId) { StringBuffer result = new StringBuffer(); diff --git a/prism/src/explicit/AccumulationProductComplexCounting.java b/prism/src/explicit/AccumulationProductComplexCounting.java index 90bd48a7..b435893d 100644 --- a/prism/src/explicit/AccumulationProductComplexCounting.java +++ b/prism/src/explicit/AccumulationProductComplexCounting.java @@ -178,16 +178,6 @@ public class AccumulationProductComplexCounting extends Accumul return nextStep; } - /** - * Populates fields: - * - numberOfTracks with the highest relevant integer plus one, and - * - numberOfWeights with the size of the reward vector. - * @param graph - * @param accexp - * @param rewards - * @param mc - * @throws PrismException - */ protected void createAuxData(final Model graph) throws PrismException { numberOfTracks = IntegerBound.fromTemporalOperatorBound(ctx.accexp.getBoundExpression(), ctx.mc.getConstantValues(), true).getHighestInteger()+1; numberOfWeights = ctx.rewards.size(); diff --git a/prism/src/explicit/AccumulationProductSimple.java b/prism/src/explicit/AccumulationProductSimple.java index 3283e1dd..392a48af 100644 --- a/prism/src/explicit/AccumulationProductSimple.java +++ b/prism/src/explicit/AccumulationProductSimple.java @@ -1,6 +1,5 @@ package explicit; -import java.util.ArrayList; import java.util.BitSet; import java.util.Iterator; import java.util.Map; @@ -32,120 +31,11 @@ public abstract class AccumulationProductSimple exten return goodStates; } - protected final int createInitialStateId() { - Component initialComponent = getInitialComponent(); - - // The initial active track is the first one, all tracks are non-good by default - int initialActiveTrack = 0; - - // Generate the initial track and product state - AccumulationTracker initialTracker = new AccumulationTracker(numberOfTracks, numberOfWeights, initialComponent); - int initialTrackerId = trackers.findOrAdd(initialTracker); - AccumulationState initialAccState = new AccumulationState(initialTrackerId, initialActiveTrack, numberOfTracks, true); - int initialAccStateId = accStates.findOrAdd(initialAccState); - - return initialAccStateId; - } - protected void generateStateInfo(ProductState state, Integer index) throws PrismException { AccumulationState accState = accStates.getById(state.getSecondState()); goodStates.set(index, accState.hasGoodTracks()); } - /** Updates a single AccumulationTrack. Used in updateAccumulationState. - * - * Uses updateComponent to get the next Component, accumulates the current weights - * and makes a new track. - * @param modelFromStateId - * @param track - * @param accexp - * @param weights - * @param mc - * @return - */ - protected final AccumulationTrack updateTrack(Integer modelFromStateId, final AccumulationTrack track, final double[] weights) { - Component nextComponent = updateComponent(modelFromStateId, track); - - // If we are done, return null-Track - if (nextComponent == null) { return null; } - - // Otherwise, we update the weights and increase the step. - double[] newweights = new double[weights.length]; - for (int i = 0; i < weights.length; i++) { - newweights[i] = weights[i] + track.getWeights()[i]; - } - - return new AccumulationTrack(newweights, nextComponent); - } - - /** Generates a new accumulation state from an old one. - * - * To do so, it reads the necessary information from the model and its rewards - * and updates all tracks and their goodness accordingly. - * @param modelFromStateId - * @param accstate - * @param accexp - * @param weights - * @param mc - * @return - * @throws PrismException - */ - protected final AccumulationState updateAccumulationState(final int modelFromStateId, final AccumulationState accstate, final double[] weights) throws PrismException { - // If we are in singleTrack mode and the last restart is the numberOfTracks, we can stop... - if(ctx.singleTrack && (accstate.lastRestartNr == numberOfTracks-1)) { return accstate; } - - // Get the old tracker and tracks. - AccumulationTracker oldTracker = accstate.getTracker(trackers); - ArrayList> oldTracks = oldTracker.getTracks(); - - // This restart will be... - int newLastRestartNr = accstate.getNextRestartNr(); - //mc.getLog().print(newLastRestartNr); - - // Build the new tracks and determine their goodness; - ArrayList> newTracks = new ArrayList<>(); - BitSet newGoodTracks = (BitSet)accstate.getGoodTracks().clone(); - - int trackNr = 0; - for(AccumulationTrack oldTrack : oldTracks) { - - AccumulationTrack newTrack; - - // restart or advance - if(trackNr == newLastRestartNr && !ctx.singleTrack) { - // If we have a restart, we produce an initial track and let it advance. - // The goodness is cleared. - AccumulationTrack freshTrack = new AccumulationTrack(numberOfWeights, getInitialComponent()); - //newTrack = updateTrack(modelFromStateId, freshTrack, accexp, weights, mc); - newTrack = freshTrack; - newGoodTracks.clear(trackNr); - } else if (oldTrack == null || (ctx.singleTrack && trackNr>0)) { - // If the old track is undefined, the new track is as well. - // Goodness stays! - newTrack = null; - } else { - // Otherwise, the track is defined and advances. - // If it is not good yet, we check it. - assert oldTrack != null; - newTrack = updateTrack(modelFromStateId, oldTrack, weights); - if(!newGoodTracks.get(trackNr)) { - newGoodTracks.set(trackNr, isGoalTrack(newTrack)); - } - } - - newTracks.add(newTrack); - trackNr++; - } - - //Create a new tracker with the right tracks and add it to storage. - AccumulationTracker newTracker = new AccumulationTracker<>(newTracks); - int newTrackerId = trackers.findOrAdd(newTracker); - - //Create the new AccState and its Goodness - AccumulationState newAccState = new AccumulationState<>(newTrackerId, newLastRestartNr, numberOfTracks, newGoodTracks); - return newAccState; - } - protected String labelString(Integer stateId) { StringBuffer result = new StringBuffer(); if(goodStates.get(stateId)) { result.append("G: "); } diff --git a/prism/src/explicit/AccumulationState.java b/prism/src/explicit/AccumulationState.java index 0a0bb380..6bd17095 100644 --- a/prism/src/explicit/AccumulationState.java +++ b/prism/src/explicit/AccumulationState.java @@ -12,28 +12,24 @@ import java.util.Objects; * */ public class AccumulationState { - final int trackerId; + protected final int trackerId; - int lastRestartNr; - int numberOfTracks; + protected int lastRestartNr; + protected int numberOfTracks; - BitSet goodTracks; - - public AccumulationState(int trackerId, int lastRestartNr, int numberOfTracks) { - this(trackerId, lastRestartNr, numberOfTracks, false); - } + protected BitSet goodTracks; public AccumulationState(int trackerId, int lastRestartNr, int numberOfTracks, BitSet goodTracks) { this(trackerId, lastRestartNr, numberOfTracks); this.goodTracks = goodTracks; } - public AccumulationState(int trackerId, int lastRestartNr, int numberOfTracks, boolean withGoodTracks) { + public AccumulationState(int trackerId, int lastRestartNr, int numberOfTracks) { super(); - if(withGoodTracks) { goodTracks = new BitSet(numberOfTracks); } - this.trackerId = trackerId; - this.lastRestartNr = lastRestartNr; + this.trackerId = trackerId; + this.lastRestartNr = lastRestartNr; this.numberOfTracks = numberOfTracks; + this.goodTracks = new BitSet(); } public int getTrackerId() {