From d781584dfbefd7c51ccd0aa7dfdf4ba7323fb1d3 Mon Sep 17 00:00:00 2001 From: Sascha Wunderlich Date: Tue, 18 Dec 2018 18:07:02 +0100 Subject: [PATCH] accumulation: support simple trafo --- prism/src/explicit/AccumulationProduct.java | 134 +-------- .../explicit/AccumulationProductComplex.java | 33 ++- .../explicit/AccumulationProductSimple.java | 277 ++++++++++++++++++ .../AccumulationProductSimpleCounting.java | 213 ++++++++++++++ .../AccumulationProductSimpleRegular.java | 244 +++++++++++++++ prism/src/explicit/AccumulationState.java | 46 +-- .../explicit/AccumulationTransformation.java | 100 +++---- ...ReplaceAccumulationExpressionComplex.java} | 48 +-- .../ReplaceAccumulationExpressionSimple.java | 61 ++++ 9 files changed, 915 insertions(+), 241 deletions(-) create mode 100644 prism/src/explicit/AccumulationProductSimple.java create mode 100644 prism/src/explicit/AccumulationProductSimpleCounting.java create mode 100644 prism/src/explicit/AccumulationProductSimpleRegular.java rename prism/src/parser/visitor/{ReplaceAccumulationExpression.java => ReplaceAccumulationExpressionComplex.java} (53%) create mode 100644 prism/src/parser/visitor/ReplaceAccumulationExpressionSimple.java diff --git a/prism/src/explicit/AccumulationProduct.java b/prism/src/explicit/AccumulationProduct.java index c92ebc12..6252d698 100644 --- a/prism/src/explicit/AccumulationProduct.java +++ b/prism/src/explicit/AccumulationProduct.java @@ -44,119 +44,26 @@ public abstract class AccumulationProduct extends Pro return numberOfTracks; } - protected abstract void generateTrackInfo(ProductState state, Integer index, ExpressionAccumulation accexp, ProbModelChecker mc) throws PrismException; - - - /** Checks whether a track is good. - * - * Tracks are good, if they are final and fulfill the constraint in the accumulation expression with context mc. - * @param track - * @param accexp - * @param mc - * @return - * @throws PrismException - */ - protected final boolean isGoalTrack(final AccumulationTrack track, final ExpressionAccumulation accexp, final ProbModelChecker mc) - throws PrismException { - // Only final tracks can be good - if (!isFinalTrack(track,accexp,mc)) { return false; } - boolean isGood = false; - - //TODO: these should be double later on - // Collect the weight linear combination, factor*weight+... - int lhs = 0; - int factorNr = 0; - for (AccumulationFactor factor : accexp.getConstraint().getFactors()) { - lhs += factor.getFactor().evaluateInt(mc.getConstantValues()) - * track.getWeight(factorNr); - } - - // Check the bound - IntegerBound rhs = IntegerBound.fromTemporalOperatorBound(accexp.getConstraint().getBound(), mc.getConstantValues(), true); + protected final boolean constraintHolds(final AccumulationTrack track, final ExpressionAccumulation accexp, final ProbModelChecker mc) throws PrismException { + // Collect the weight linear combination, factor*weight+... + int lhs = 0; + int factorNr = 0; + for (AccumulationFactor factor : accexp.getConstraint().getFactors()) { + lhs += factor.getFactor().evaluateInt(mc.getConstantValues()) + * track.getWeight(factorNr); + } - // For DIA operators, we just check the bound. - // For BOX operators, we check the INVERTED bound. - - // TODO: THIS MAY BE BROKEN - switch(accexp.getSymbol()) { - case ACCBOXMINUS: - case ACCBOXPLUS: - if (!rhs.isInBounds(lhs)) { - isGood = true; - } - mc.getLog().println("WARNING: This may be wrong."); - break; - case ACCDIAMINUS: - case ACCDIAPLUS: - case ACCUNTIL: - if (rhs.isInBounds(lhs)) { - isGood = true; - } - break; - default: - throw new RuntimeException("Accumulation symbol cannot be handled..."); - } - //if(isGood) {mc.getLog().print("+");} else {mc.getLog().print("-");} - return isGood; - } - - - - /** Checks whether a track is final according to the bound in the accumulation expression and the context in mc. - * @param track - * @param accexp - * @param mc - * @return - * @throws PrismException - */ - protected abstract boolean isFinalTrack(final AccumulationTrack track, final ExpressionAccumulation accexp, final ProbModelChecker mc) - throws PrismException; + // Check the bound + IntegerBound rhs = IntegerBound.fromTemporalOperatorBound(accexp.getConstraint().getBound(), mc.getConstantValues(), true); + + return rhs.isInBounds(lhs); + } /** Get the initial Component of the accumulation monitor. * @return */ protected abstract Component getInitialComponent(); - /** Update the Component of the accumulation monitor when leaving modelFromStateId. - * @param modelFromStateId - * @param track - * @param accexp - * @param mc - * @return - */ - protected abstract Component updateComponent(Integer modelFromStateId, final AccumulationTrack track, - final ExpressionAccumulation accexp, final StateModelChecker mc); - - /** 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 abstract AccumulationTrack updateTrack(Integer modelFromStateId, final AccumulationTrack track, - final ExpressionAccumulation accexp, final double[] weights, final StateModelChecker mc); - - /** 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 abstract AccumulationState updateAccumulationState(final int modelFromStateId, - final AccumulationState accstate, final ExpressionAccumulation accexp, - final double[] weights, final ProbModelChecker mc) throws PrismException; - /** * Creates the initial state for the accumulation part of this of this accumulation product. Returns its ID. * @@ -164,20 +71,7 @@ public abstract class AccumulationProduct extends Pro * where the first restart is the first (0th) track. * @return */ - 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 abstract int createInitialStateId(); protected abstract String labelString(Integer stateId); diff --git a/prism/src/explicit/AccumulationProductComplex.java b/prism/src/explicit/AccumulationProductComplex.java index 4605deae..2dc3f587 100644 --- a/prism/src/explicit/AccumulationProductComplex.java +++ b/prism/src/explicit/AccumulationProductComplex.java @@ -4,15 +4,12 @@ import java.util.ArrayList; import java.util.BitSet; import java.util.Iterator; import java.util.Map; -import java.util.Vector; import parser.ast.ExpressionAccumulation; import parser.ast.Expression; import prism.PrismException; import common.Dottable; -import explicit.rewards.MCRewards; -import explicit.rewards.Rewards; /** * An AccumulationProduct has ProductStates, where the first component is the @@ -49,6 +46,21 @@ 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, ExpressionAccumulation accexp, ProbModelChecker mc) throws PrismException { AccumulationState accState = accStates.getById(state.getSecondState()); AccumulationTracker tracker = accState.getTracker(trackers); @@ -73,6 +85,21 @@ public abstract class AccumulationProductComplex exte } } + + /** Checks whether a track is good. + * + * Tracks are good, if they are final and fulfill the constraint in the accumulation expression with context mc. + * @param track + * @param accexp + * @param mc + * @return + * @throws PrismException + */ + protected final boolean isGoalTrack(final AccumulationTrack track, final ExpressionAccumulation accexp, final ProbModelChecker mc) + throws PrismException { + return isFinalTrack(track,accexp,mc) && constraintHolds(track,accexp,mc); + } + /** Checks whether a track is final according to the bound in the accumulation expression and the context in mc. * @param track * @param accexp diff --git a/prism/src/explicit/AccumulationProductSimple.java b/prism/src/explicit/AccumulationProductSimple.java new file mode 100644 index 00000000..bd91ab97 --- /dev/null +++ b/prism/src/explicit/AccumulationProductSimple.java @@ -0,0 +1,277 @@ +package explicit; + +import java.util.ArrayList; +import java.util.BitSet; +import java.util.HashMap; +import java.util.Iterator; +import java.util.Map; + +import parser.ast.ExpressionAccumulation; +import prism.PrismException; + +import common.Dottable; + +/** + * An AccumulationProduct has ProductStates, where the first component is the + * stateId in the original model, and the second component is the index of an + * AccumulationTracker. + * + * @author Sascha Wunderlich + * + * @param + */ + +public abstract class AccumulationProductSimple extends AccumulationProduct implements Dottable +{ + protected final BitSet goodStates; + + public AccumulationProductSimple(M originalModel) { + super(originalModel); + goodStates = new BitSet(); + } + + public final BitSet getGoodStates() { + 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()); + } + + + /** Checks whether a track is good. + * + * Tracks are good, if they are final and fulfill the constraint in the accumulation expression with context mc. + * @param track + * @param accexp + * @param mc + * @return + * @throws PrismException + */ + protected final boolean isGoalTrack(final AccumulationTrack track, final ExpressionAccumulation accexp, final ProbModelChecker mc) + throws PrismException { + // Only final tracks can be good + if (!isFinalTrack(track,accexp,mc)) { return false; } + + // For DIA operators, we just check the bound. + // For BOX operators, we check the INVERTED bound. + + // TODO: THIS MAY BE BROKEN + switch(accexp.getSymbol()) { + case ACCBOXMINUS: + case ACCBOXPLUS: + mc.getLog().println("WARNING: This may be wrong."); + return !constraintHolds(track,accexp,mc); + case ACCDIAMINUS: + case ACCDIAPLUS: + return constraintHolds(track,accexp,mc); + default: + throw new RuntimeException("Accumulation symbol cannot be handled..."); + } + } + + /** Checks whether a track is final according to the bound in the accumulation expression and the context in mc. + * @param track + * @param accexp + * @param mc + * @return + * @throws PrismException + */ + protected abstract boolean isFinalTrack(final AccumulationTrack track, final ExpressionAccumulation accexp, final ProbModelChecker mc) + throws PrismException; + + /** Get the initial Component of the accumulation monitor. + * @return + */ + protected abstract Component getInitialComponent(); + + /** Update the Component of the accumulation monitor when leaving modelFromStateId. + * @param modelFromStateId + * @param track + * @param accexp + * @param mc + * @return + */ + protected abstract Component updateComponent(Integer modelFromStateId, final AccumulationTrack track, + final ExpressionAccumulation accexp, final StateModelChecker mc); + + /** 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 ExpressionAccumulation accexp, final double[] weights, final StateModelChecker mc) { + Component nextComponent = updateComponent(modelFromStateId, track, accexp, mc); + + // 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 ExpressionAccumulation accexp, + final double[] weights, final ProbModelChecker mc) throws PrismException { + + // 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) { + // 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) { + // 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, accexp, weights, mc); + if(!newGoodTracks.get(trackNr)) { + newGoodTracks.set(trackNr, isGoalTrack(newTrack, accexp, mc)); + } + } + + 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: "); } + + for(int t=0; t accState = accStates.getById(fromState.getSecondState()); + AccumulationTracker tracker = accState.getTracker(trackers); + result.append("" + + i + + "[shape=box, color=black" + + " label= < " + + "" + + "" + + "" + + "" + + "" + + "" + + "" + + "" + + "" + + "
" + i + "=" + fromState + "
" + accState + "
" + labelString(i) + "
\"" + Dottable.quoteForDot(tracker.toString()) + "\"
>]\n"); + + switch(productModel.getModelType()) { + case DTMC: + DTMCExplicit castDTMC = (DTMCExplicit)productModel; + Iterator> dtmcIter = castDTMC.getTransitionsIterator(i); + while (dtmcIter.hasNext()) { + Map.Entry e = dtmcIter.next(); + result.append(i + " -> " + e.getKey() + " [ label=\""); + result.append(e.getValue() + "\" ];\n"); + } + break; + case MDP: + MDPExplicit castMDP = (MDPExplicit)productModel; + for(int c = 0; c < castMDP.getNumChoices(i); c++) { + Iterator> mdpIter = castMDP.getTransitionsIterator(i, c); + while (mdpIter.hasNext()) { + Map.Entry e = mdpIter.next(); + result.append(i + " -> " + e.getKey() + " [ label=\""); + result.append(c + "," + e.getValue() + "\" ];\n"); + } + } + break; + default: + break; + } + } + + result.append("}"); + + return result.toString(); + } +} diff --git a/prism/src/explicit/AccumulationProductSimpleCounting.java b/prism/src/explicit/AccumulationProductSimpleCounting.java new file mode 100644 index 00000000..ecf86daa --- /dev/null +++ b/prism/src/explicit/AccumulationProductSimpleCounting.java @@ -0,0 +1,213 @@ +package explicit; + +import java.util.BitSet; +import java.util.Vector; + +import explicit.rewards.MCRewards; +import explicit.rewards.MDPRewards; +import explicit.rewards.Rewards; +import parser.ast.ExpressionAccumulation; +import prism.IntegerBound; +import prism.PrismException; + +/** + * An AccumulationProduct has ProductStates, where the first component is the + * stateId in the original model, and the second component is the index of an + * AccumulationTracker. + * + * @author Sascha Wunderlich + * + * @param + */ + +public class AccumulationProductSimpleCounting extends AccumulationProductSimple +{ + + public AccumulationProductSimpleCounting(M originalModel) { + super(originalModel); + } + + @SuppressWarnings("unchecked") + public static AccumulationProductSimpleCounting generate(final Model graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + switch(graph.getModelType()) { + case DTMC: + return (AccumulationProductSimpleCounting)generate((DTMC) graph, accexp, (Vector) rewards, mc, statesOfInterest); + case MDP: + return (AccumulationProductSimpleCounting)generate((MDP) graph, accexp, (Vector) rewards, mc, statesOfInterest); + default: + throw new PrismException("Can't handle accumulation product for " + graph.getModelType()); + } + } + + public static AccumulationProductSimpleCounting generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + final AccumulationProductSimpleCounting result = new AccumulationProductSimpleCounting(graph); + // Create auxiliary data + result.createAuxData(graph, accexp, rewards, mc); + + // Build an operator + class AccumulationDTMCProductOperator implements DTMCProductOperator + { + @Override + public ProductState getInitialState(Integer dtmc_state) + throws PrismException { + int initialAccStateId = result.createInitialStateId(); + return new ProductState(dtmc_state, initialAccStateId); + } + + @Override + public ProductState getSuccessor(ProductState from_state, + Integer dtmc_to_state) throws PrismException { + // Get the current accumulation state + AccumulationState from_accstate = result.accStates.getById(from_state.getSecondState()); + + // Get step weights + double[] weights = new double[rewards.size()]; + + for (int i=0; i < rewards.size(); i++) { + weights[i] = rewards.get(i).getStateReward(from_state.getFirstState()); + } + + // Update accumulation product state, store it and get its ID. + AccumulationState to_accproduct = result.updateAccumulationState(from_state.getFirstState(), from_accstate, accexp, weights, mc); + int to_accproduct_id = result.accStates.findOrAdd(to_accproduct); + + return new ProductState(dtmc_to_state, to_accproduct_id); + } + + @Override + public void notify(ProductState state, Integer index) + throws PrismException { + result.generateStateInfo(state, index); + } + + @Override + public void finish() throws PrismException { + // Do nothing + } + + @Override + public DTMC getGraph() { + return graph; + } + } + + // Apply the operator + AccumulationDTMCProductOperator op = new AccumulationDTMCProductOperator(); + ProductWithProductStates.generate(op, result, statesOfInterest); + + return result; + } + + public static AccumulationProductSimpleCounting generate(final MDP graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + // This is basically the same thing as for DTMCs + final AccumulationProductSimpleCounting result = new AccumulationProductSimpleCounting(graph); + + // Create auxiliary data + result.createAuxData(graph, accexp, rewards, mc); + + class AccumulationMDPProductOperator implements MDPProductOperator + { + + @Override + public ProductState getInitialState(final Integer MDP_state) + throws PrismException { + int initialAccStateId = result.createInitialStateId(); + return new ProductState(MDP_state, initialAccStateId); + } + + @Override + public ProductState getSuccessor(final ProductState from_state, + final int choice_i, final Integer mdp_to_state) throws PrismException { + // Get the current accumulation state + AccumulationState from_accstate = result.accStates.getById(from_state.getSecondState()); + + // Get step weights + // THIS IS DIFFERENT FROM ABOVE! + double[] weights = new double[rewards.size()]; + + for (int i=0; i < rewards.size(); i++) { + double currentWeight = rewards.get(i).getStateReward(from_state.getFirstState()); + currentWeight += rewards.get(i).getTransitionReward(from_state.getFirstState(), choice_i); + weights[i] = currentWeight; + } + + // Update accumulation product state, store it and get its ID. + AccumulationState to_accproduct = result.updateAccumulationState(from_state.getFirstState(), from_accstate, accexp, weights, mc); + int to_accproduct_id = result.accStates.findOrAdd(to_accproduct); + return new ProductState(mdp_to_state, to_accproduct_id); + } + + @Override + public void notify(final ProductState state, final Integer index) + throws PrismException { + result.generateStateInfo(state, index); + } + + @Override + public void finish() throws PrismException { + // Do nothing + //mc.getLog().println("."); + } + + @Override + public MDP getGraph() { + return graph; + } + } + + AccumulationMDPProductOperator op = new AccumulationMDPProductOperator(); + ProductWithProductStates.generate(op, result, statesOfInterest); + return result; + } + + @Override + protected boolean isFinalTrack(final AccumulationTrack track, final ExpressionAccumulation accexp, final ProbModelChecker mc) + throws PrismException { + boolean isFinal = false; + if ( track != null ) { + Integer step = track.getComponent(); + if ( step > 0 ) { // if the step is 0, we cannot have a goal state. + IntegerBound stepBound = IntegerBound.fromTemporalOperatorBound(accexp.getBoundExpression(), mc.getConstantValues(), true); + isFinal = stepBound.isInBounds(step); + } + } + return isFinal; + } + + @Override + protected Integer getInitialComponent() { + return 0; + } + + @Override + protected Integer updateComponent(Integer modelFromStateId, final AccumulationTrack track, + final ExpressionAccumulation accexp, final StateModelChecker mc) { + int currentStep = track.getComponent(); + + int maxStep = 0; + try { + maxStep = IntegerBound.fromTemporalOperatorBound(accexp.getBoundExpression(), mc.getConstantValues(), true).getHighestInteger(); + } catch(PrismException e) { + throw new RuntimeException("..."); + } + + int nextStep = currentStep+1; + if(nextStep > maxStep) { return null; } + 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, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc) throws PrismException { + numberOfTracks = IntegerBound.fromTemporalOperatorBound(accexp.getBoundExpression(), mc.getConstantValues(), true).getHighestInteger()+2; + numberOfWeights = rewards.size(); + } +} diff --git a/prism/src/explicit/AccumulationProductSimpleRegular.java b/prism/src/explicit/AccumulationProductSimpleRegular.java new file mode 100644 index 00000000..838b9a47 --- /dev/null +++ b/prism/src/explicit/AccumulationProductSimpleRegular.java @@ -0,0 +1,244 @@ +package explicit; + +import java.util.ArrayList; +import java.util.BitSet; +import java.util.Vector; + +import automata.finite.DeterministicFiniteAutomaton; +import automata.finite.EdgeLabel; +import automata.finite.NondeterministicFiniteAutomaton; +import automata.finite.State; +import explicit.rewards.MCRewards; +import explicit.rewards.MDPRewards; +import explicit.rewards.Rewards; +import parser.ast.ExpressionAccumulation; +import parser.ast.ExpressionRegular; +import prism.PrismException; +import prism.PrismSettings; + +/** + * An AccumulationProduct has ProductStates, where the first component is the + * stateId in the original model, and the second component is the index of an + * AccumulationTracker. + * + * @author Sascha Wunderlich + * + * @param + */ + +public class AccumulationProductSimpleRegular extends AccumulationProductSimple +{ + protected DeterministicFiniteAutomaton automaton; + + public AccumulationProductSimpleRegular(M originalModel) { + super(originalModel); + } + + @SuppressWarnings("unchecked") + public static AccumulationProductSimpleRegular generate(final Model graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + switch(graph.getModelType()) { + case DTMC: + return (AccumulationProductSimpleRegular)generate((DTMC) graph, accexp, (Vector) rewards, mc, statesOfInterest); + case MDP: + return (AccumulationProductSimpleRegular)generate((MDP) graph, accexp, (Vector) rewards, mc, statesOfInterest); + default: + throw new PrismException("Can't handle accumulation product for " + graph.getModelType()); + } + } + + public static AccumulationProductSimpleRegular generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + final AccumulationProductSimpleRegular result = new AccumulationProductSimpleRegular(graph); + // Create auxiliary data + result.createAuxData(graph, accexp, rewards, mc); + + // Build an operator + class AccumulationDTMCProductOperator implements DTMCProductOperator + { + @Override + public ProductState getInitialState(Integer dtmc_state) + throws PrismException { + int initialAccStateId = result.createInitialStateId(); + return new ProductState(dtmc_state, initialAccStateId); + } + + @Override + public ProductState getSuccessor(ProductState from_state, + Integer dtmc_to_state) throws PrismException { + // Get the current accumulation state + AccumulationState from_accstate = result.accStates.getById(from_state.getSecondState()); + + // Get step weights + double[] weights = new double[rewards.size()]; + + for (int i=0; i < rewards.size(); i++) { + weights[i] = rewards.get(i).getStateReward(from_state.getFirstState()); + } + + // Update accumulation product state, store it and get its ID. + AccumulationState to_accproduct = result.updateAccumulationState(from_state.getFirstState(), from_accstate, accexp, weights, mc); + int to_accproduct_id = result.accStates.findOrAdd(to_accproduct); + + return new ProductState(dtmc_to_state, to_accproduct_id); + } + + @Override + public void notify(ProductState state, Integer index) + throws PrismException { + result.generateStateInfo(state, index); + } + + @Override + public void finish() throws PrismException { + // Do nothing + } + + @Override + public DTMC getGraph() { + return graph; + } + } + + // Apply the operator + AccumulationDTMCProductOperator op = new AccumulationDTMCProductOperator(); + ProductWithProductStates.generate(op, result, statesOfInterest); + + return result; + } + + public static AccumulationProductSimpleRegular generate(final MDP graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + // This is basically the same thing as for DTMCs + final AccumulationProductSimpleRegular result = new AccumulationProductSimpleRegular(graph); + + // Create auxiliary data + result.createAuxData(graph, accexp, rewards, mc); + + class AccumulationMDPProductOperator implements MDPProductOperator + { + + @Override + public ProductState getInitialState(final Integer MDP_state) + throws PrismException { + int initialAccStateId = result.createInitialStateId(); + return new ProductState(MDP_state, initialAccStateId); + } + + @Override + public ProductState getSuccessor(final ProductState from_state, + final int choice_i, final Integer mdp_to_state) throws PrismException { + // Get the current accumulation state + AccumulationState from_accstate = result.accStates.getById(from_state.getSecondState()); + + // Get step weights + // THIS IS DIFFERENT FROM ABOVE! + double[] weights = new double[rewards.size()]; + + for (int i=0; i < rewards.size(); i++) { + double currentWeight = rewards.get(i).getStateReward(from_state.getFirstState()); + currentWeight += rewards.get(i).getTransitionReward(from_state.getFirstState(), choice_i); + weights[i] = currentWeight; + } + + // Update accumulation product state, store it and get its ID. + AccumulationState to_accproduct = result.updateAccumulationState(from_state.getFirstState(), from_accstate, accexp, weights, mc); + int to_accproduct_id = result.accStates.findOrAdd(to_accproduct); + return new ProductState(mdp_to_state, to_accproduct_id); + } + + @Override + public void notify(final ProductState state, final Integer index) + throws PrismException { + result.generateStateInfo(state, index); + } + + @Override + public void finish() throws PrismException { + // Do nothing + //mc.getLog().println("."); + } + + @Override + public MDP getGraph() { + return graph; + } + } + + AccumulationMDPProductOperator op = new AccumulationMDPProductOperator(); + ProductWithProductStates.generate(op, result, statesOfInterest); + return result; + } + + @Override + protected boolean isFinalTrack(AccumulationTrack track, ExpressionAccumulation accexp, ProbModelChecker mc) throws PrismException { + boolean isFinal = false; + if ( track != null ) { + isFinal = automaton.isAcceptingState(track.getComponent()); + } + + return isFinal; + } + + @Override + protected State getInitialComponent() { + return automaton.getInitialState(); + } + + @Override + protected State updateComponent(Integer modelFromStateId, final AccumulationTrack track, + final ExpressionAccumulation accexp, final StateModelChecker mc) { + State currentState = track.getComponent(); + + // Build EdgeLabel from labels. + // labels is a BitSet with labels L0,...,Ln + ArrayList edgeSymbols = new ArrayList<>(); + BitSet edgeValues = new BitSet(); + + for (int i=0; i < labels.size(); i++) { + // Each bitLabel contains one L + edgeSymbols.add(i, "L"+i); + if(labels.get(i).get(modelFromStateId)) { + edgeValues.set(i); + } + } + + EdgeLabel edgeLabel = new EdgeLabel<>(edgeSymbols, edgeValues); + + State nextState = automaton.getSuccessor(currentState,edgeLabel); + if(nextState == null) { return null; } + return nextState; + } + + /** + * 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, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc) throws PrismException { + // Build labels and DFA + AccumulationModelChecker accMc = new AccumulationModelChecker(); + ExpressionRegular reg = (ExpressionRegular)accMc.checkMaximalStateFormulas(mc, graph, accexp.getRegularExpression(), labels); + + // Create and store the actual DFA + NondeterministicFiniteAutomaton nfa = NondeterministicFiniteAutomaton.fromExpressionRegular(reg); + //System.out.println(nfa.toDot()); + + automaton = nfa.determinize(); + automaton.trim(); // This should remove cycles. + + if(mc.getSettings().getBoolean(PrismSettings.ACC_GENERATE_DOTS)) { + nfa.exportToDotFile("DEBUG-automaton-nfa.dot"); + automaton.exportToDotFile("DEBUG-automaton-dfa.dot"); + } + + if (!automaton.isAcyclic()) { + throw new PrismException("Cannot handle cyclic automata!"); + } + + numberOfTracks = automaton.getLongestPathLength()+1; + numberOfWeights= rewards.size(); + } +} diff --git a/prism/src/explicit/AccumulationState.java b/prism/src/explicit/AccumulationState.java index 4cba6367..cd6d6739 100644 --- a/prism/src/explicit/AccumulationState.java +++ b/prism/src/explicit/AccumulationState.java @@ -1,9 +1,12 @@ package explicit; +import java.util.BitSet; +import java.util.Objects; + /** * An AccumulationState contains a reference to an AccumulationTracker, - * a pointer to the latest restart and - * the numberOfTracks in the tracker. + * a pointer to the latest restart and the numberOfTracks in the tracker. + * It can optionally contain a BitSet marking the goodTracks. * * @author Sascha Wunderlich * @@ -14,8 +17,20 @@ public class AccumulationState { int lastRestartNr; int numberOfTracks; + BitSet goodTracks; + public AccumulationState(int trackerId, int lastRestartNr, int numberOfTracks) { + this(trackerId, lastRestartNr, numberOfTracks, false); + } + + 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) { super(); + if(withGoodTracks) { goodTracks = new BitSet(numberOfTracks); } this.trackerId = trackerId; this.lastRestartNr = lastRestartNr; this.numberOfTracks = numberOfTracks; @@ -33,17 +48,19 @@ public class AccumulationState { return (lastRestartNr + 1) % numberOfTracks; } - + public boolean hasGoodTracks() { + return !goodTracks.isEmpty(); + } + + public BitSet getGoodTracks() { + return goodTracks; + } + @Override public int hashCode() { - final int prime = 31; - int result = 1; - result = prime * result + lastRestartNr; - result = prime * result + numberOfTracks; - result = prime * result + trackerId; - return result; + return Objects.hash(goodTracks, lastRestartNr, numberOfTracks, trackerId); } - + @Override public boolean equals(Object obj) { if (this == obj) @@ -53,13 +70,8 @@ public class AccumulationState { if (getClass() != obj.getClass()) return false; AccumulationState other = (AccumulationState) obj; - if (lastRestartNr != other.lastRestartNr) - return false; - if (numberOfTracks != other.numberOfTracks) - return false; - if (trackerId != other.trackerId) - return false; - return true; + return Objects.equals(goodTracks, other.goodTracks) && lastRestartNr == other.lastRestartNr + && numberOfTracks == other.numberOfTracks && trackerId == other.trackerId; } @Override diff --git a/prism/src/explicit/AccumulationTransformation.java b/prism/src/explicit/AccumulationTransformation.java index 3f0e0fb4..a71ac457 100644 --- a/prism/src/explicit/AccumulationTransformation.java +++ b/prism/src/explicit/AccumulationTransformation.java @@ -10,18 +10,19 @@ import parser.ast.Expression; import parser.ast.ExpressionAccumulation; import parser.ast.ExpressionReward; import parser.ast.RewardStruct; -import parser.visitor.ReplaceAccumulationExpression; +import parser.visitor.ReplaceAccumulationExpressionComplex; +import parser.visitor.ReplaceAccumulationExpressionSimple; import prism.PrismException; import prism.PrismSettings; public class AccumulationTransformation implements ModelExpressionTransformation { - final private Expression originalExpression; - final private M originalModel; - final private BitSet statesOfInterest; - final ProbModelChecker mc; + final protected Expression originalExpression; + final protected M originalModel; + final protected BitSet statesOfInterest; + final protected ProbModelChecker mc; - private Expression transformedExpression; - private AccumulationProduct product; + protected Expression transformedExpression; + protected AccumulationProduct product; public AccumulationTransformation( ProbModelChecker mc, @@ -63,7 +64,7 @@ public class AccumulationTransformation implements ModelExpress return product.projectToOriginalModel(svTransformedModel); } - private void doTransformation() throws PrismException { + protected void doTransformation() throws PrismException { mc.getLog().println("Performing accumulation transformation..."); // We work on a copy transformedExpression = originalExpression.deepCopy(); @@ -71,8 +72,8 @@ public class AccumulationTransformation implements ModelExpress // Get the first ExpressionAccumulation ExpressionAccumulation accexp = transformedExpression.getFirstAccumulationExpression(); mc.getLog().println(" [AT] for " + accexp); - - // Get the rewards and build the product + + // Get the rewards Vector rewards = new Vector(); for (int i=0; i < accexp.getConstraint().getFactors().size(); i++) { @@ -85,19 +86,19 @@ public class AccumulationTransformation implements ModelExpress Rewards reward = constructRewards.buildRewardStructure(originalModel, rewStruct, mc.getConstantValues()); rewards.add(i,reward); } - - boolean isComplex = mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_COMPLEX) || accexp.hasFireOn() || !accexp.isNullary(); - if (isComplex) { - mc.getLog().println(" ... which is COMPLEX."); - doTransformationComplex(accexp, rewards); - } else { - mc.getLog().println(" ... which is SIMPLE."); - doTransformationSimple(accexp, rewards); - } + + // Figure out if we need a complex or a simple trafo... + boolean isComplex = mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_COMPLEX) || accexp.hasFireOn() || !accexp.isNullary(); + if(isComplex) { + mc.getLog().println(" ... which is complex!"); + doTransformationComplex(accexp, rewards); + } else { + mc.getLog().println(" ... which is simple!"); + doTransformationSimple(accexp, rewards); + } } - - @SuppressWarnings("unchecked") - private void doTransformationComplex(ExpressionAccumulation accexp, Vector rewards) throws PrismException { + + protected void doTransformationComplex(ExpressionAccumulation accexp, Vector rewards) throws PrismException { // Build the product if(accexp.hasRegularExpression()) { product = (AccumulationProductComplexRegular) AccumulationProductComplexRegular.generate(originalModel, accexp, rewards, mc, statesOfInterest); @@ -116,70 +117,55 @@ public class AccumulationTransformation implements ModelExpress ArrayList runLabels = new ArrayList(); ArrayList goalLabels = new ArrayList(); - AccumulationProductComplex productComplex = (AccumulationProductComplex) product; - - for(int track=0; track < productComplex.getNumberOfTracks(); track++) { - BitSet initStates = productComplex.getInitStates(track); - BitSet runStates = productComplex.getRunStates(track); - BitSet goalStates = productComplex.getGoalStates(track); + for(int track=0; track < product.getNumberOfTracks(); track++) { + BitSet initStates = ((AccumulationProductComplex)product).getInitStates(track); + BitSet runStates = ((AccumulationProductComplex)product).getRunStates(track); + BitSet goalStates = ((AccumulationProductComplex)product).getGoalStates(track); - String initLabel = ((ModelExplicit)productComplex.getTransformedModel()).addUniqueLabel("init" + track, initStates, productComplex.getTransformedModel().getLabels()); + String initLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("init" + track, initStates, product.getTransformedModel().getLabels()); initLabels.add(initLabel); - String runLabel = ((ModelExplicit)productComplex.getTransformedModel()).addUniqueLabel("run" + track, runStates, productComplex.getTransformedModel().getLabels()); + String runLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("run" + track, runStates, product.getTransformedModel().getLabels()); runLabels.add(runLabel); - String goalLabel = ((ModelExplicit)productComplex.getTransformedModel()).addUniqueLabel("goal" + track, goalStates, productComplex.getTransformedModel().getLabels()); + String goalLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("goal" + track, goalStates, product.getTransformedModel().getLabels()); goalLabels.add(goalLabel); - - //mc.getLog().println(initStates + " | " + initLabel); - //mc.getLog().println(runStates + " | " + runLabel); - //mc.getLog().println(goalStates + " | " + goalLabel); } // Transform the expression mc.getLog().println(" [AT] replacing the formula..."); - ReplaceAccumulationExpression replace = new ReplaceAccumulationExpression(accexp, mc, initLabels, runLabels, goalLabels, product.getNumberOfTracks()-1); + ReplaceAccumulationExpressionComplex replace = new ReplaceAccumulationExpressionComplex(accexp, initLabels, runLabels, goalLabels, product.getNumberOfTracks()-1); transformedExpression = (Expression)transformedExpression.accept(replace); mc.getLog().println(" [AT] " + originalExpression.toString() + "\n" + " -> " + transformedExpression.toString()); if(mc.getSettings().getBoolean(PrismSettings.ACC_GENERATE_DOTS)) { product.exportToDotFile("DEBUG-product.dot"); } -} + } - @SuppressWarnings("unchecked") - private void doTransformationSimple(ExpressionAccumulation accexp, Vector rewards) throws PrismException { - throw new PrismException("Stop, Hammer Time!"); - /* - AccumulationProductSimple productSimple = (AccumulationProductSimple) product; - + protected void doTransformationSimple(ExpressionAccumulation accexp, Vector rewards) throws PrismException { // Build the product if(accexp.hasRegularExpression()) { - productSimple = (AccumulationProductSimpleRegular) AccumulationProductSimpleRegular.generate(originalModel, accexp, rewards, mc, statesOfInterest); + //throw new PrismException("I don't know how to do regular things..."); + product = (AccumulationProductSimpleRegular) AccumulationProductSimpleRegular.generate(originalModel, accexp, rewards, mc, statesOfInterest); } else if (accexp.hasBoundExpression()) { - productSimple = (AccumulationProductSimpleCounting) AccumulationProductSimpleCounting.generate(originalModel, accexp, rewards, mc, statesOfInterest); + product = (AccumulationProductSimpleCounting) AccumulationProductSimpleCounting.generate(originalModel, accexp, rewards, mc, statesOfInterest); } else { throw new PrismException("Accumulation Expression has no valid monitor!"); } - mc.getLog().println(" [AT] finished product construction: " + productSimple.getTransformedModel().getNumStates()); + mc.getLog().println(" [AT] finished product construction: " + product.getTransformedModel().getNumStates()); // Transform the model - mc.getLog().println(" [AT] getting the init/run/goal states: "); - - ArrayList goalLabels = new ArrayList(); - - BitSet goodStates = productSimple.getGoodStates(); - String goalLabel = ((ModelExplicit)productSimple.getTransformedModel()).addUniqueLabel("good", goodStates, productSimple.getTransformedModel().getLabels()); - goalLabels.add(goalLabel); + mc.getLog().println(" [AT] getting the good states: "); + BitSet goodStates = ((AccumulationProductSimple)product).getGoodStates(); + String goodLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("goal", goodStates, product.getTransformedModel().getLabels()); // Transform the expression mc.getLog().println(" [AT] replacing the formula..."); - ReplaceAccumulationExpression replace = new ReplaceAccumulationExpression(accexp, mc, null, null, goalLabels, productSimple.getNumberOfTracks()-1); + ReplaceAccumulationExpressionSimple replace = new ReplaceAccumulationExpressionSimple(accexp, goodLabel, product.getNumberOfTracks()-1); transformedExpression = (Expression)transformedExpression.accept(replace); mc.getLog().println(" [AT] " + originalExpression.toString() + "\n" + " -> " + transformedExpression.toString()); if(mc.getSettings().getBoolean(PrismSettings.ACC_GENERATE_DOTS)) { - productSimple.exportToDotFile("DEBUG-product.dot"); + product.exportToDotFile("DEBUG-product.dot"); } - */ } -} +} \ No newline at end of file diff --git a/prism/src/parser/visitor/ReplaceAccumulationExpression.java b/prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java similarity index 53% rename from prism/src/parser/visitor/ReplaceAccumulationExpression.java rename to prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java index 6b0709c7..83fef902 100644 --- a/prism/src/parser/visitor/ReplaceAccumulationExpression.java +++ b/prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java @@ -2,34 +2,25 @@ package parser.visitor; import java.util.ArrayList; -import explicit.ProbModelChecker; -import parser.ast.AccumulationSymbol; import parser.ast.Expression; import parser.ast.ExpressionAccumulation; import parser.ast.ExpressionBinaryOp; import parser.ast.ExpressionLabel; import parser.ast.ExpressionTemporal; -import parser.ast.ExpressionUnaryOp; -import parser.ast.TemporalOperatorBound; -import parser.ast.TemporalOperatorBounds; -import prism.IntegerBound; import prism.PrismLangException; -import prism.PrismSettings; -public class ReplaceAccumulationExpression extends ASTTraverseModify { +public class ReplaceAccumulationExpressionComplex extends ASTTraverseModify { private ExpressionAccumulation accexp; - private ProbModelChecker mc; private ArrayList initLabels; private ArrayList runLabels; private ArrayList goalLabels; private int accLength; - public ReplaceAccumulationExpression(ExpressionAccumulation accexp, ProbModelChecker mc, ArrayList initLabels, ArrayList runLabels, ArrayList goalLabels, int accLength) { + public ReplaceAccumulationExpressionComplex(ExpressionAccumulation accexp, ArrayList initLabels, ArrayList runLabels, ArrayList goalLabels, int accLength) { super(); this.accexp = accexp; - this.mc = mc; this.initLabels = initLabels; this.runLabels = runLabels; this.goalLabels = goalLabels; @@ -73,42 +64,11 @@ public class ReplaceAccumulationExpression extends ASTTraverseModify { return result; } - private Object replaceWithReach(ExpressionAccumulation expr) throws PrismLangException { - AccumulationSymbol sym = accexp.getSymbol(); - - ExpressionLabel label = new ExpressionLabel(goalLabels.get(0)); - - if (sym.isPlus()) { - ExpressionTemporal fExpr = new ExpressionTemporal(ExpressionTemporal.P_F, null, label); - TemporalOperatorBounds fBounds = new TemporalOperatorBounds(); - TemporalOperatorBound fBound = IntegerBound.fromEqualBounds(accLength).toTemporalOperatorBound(); - fBounds.setDefaultBound(fBound); - fExpr.setBounds(fBounds); - // If its a BOX, negate it - if (sym.isBox()) { - return new ExpressionUnaryOp(ExpressionUnaryOp.NOT, fExpr); - } else { - return fExpr; - } - } else { //isMinus - if (sym.isBox()) { - return new ExpressionUnaryOp(ExpressionUnaryOp.NOT, label); - } else { - return label; - } - } - } - public Object visit(ExpressionAccumulation expr) throws PrismLangException { if (expr == accexp) { - if (mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_COMPLEX) || accexp.hasFireOn() || !accexp.isNullary()) { - // This is a complex accumulation expression. Rewrite to until formula. - return replaceWithUntil(expr); - } else { - // This is a simple accumulation expression. Rewrite to F=.... - return replaceWithReach(expr); - } + // This is a complex accumulation expression. Rewrite to until formula. + return replaceWithUntil(expr); } else { return expr; } diff --git a/prism/src/parser/visitor/ReplaceAccumulationExpressionSimple.java b/prism/src/parser/visitor/ReplaceAccumulationExpressionSimple.java new file mode 100644 index 00000000..80402efd --- /dev/null +++ b/prism/src/parser/visitor/ReplaceAccumulationExpressionSimple.java @@ -0,0 +1,61 @@ +package parser.visitor; + +import parser.ast.AccumulationSymbol; +import parser.ast.ExpressionAccumulation; +import parser.ast.ExpressionLabel; +import parser.ast.ExpressionTemporal; +import parser.ast.ExpressionUnaryOp; +import parser.ast.TemporalOperatorBound; +import parser.ast.TemporalOperatorBounds; +import prism.IntegerBound; +import prism.PrismLangException; + +public class ReplaceAccumulationExpressionSimple extends ASTTraverseModify { + + private ExpressionAccumulation accexp; + private String goodLabel; + private int accLength; + + public ReplaceAccumulationExpressionSimple(ExpressionAccumulation accexp, String goodLabel, int accLength) { + super(); + this.accexp = accexp; + this.goodLabel = goodLabel; + this.accLength = accLength; + } + + private Object replaceWithReach(ExpressionAccumulation expr) throws PrismLangException { + AccumulationSymbol sym = accexp.getSymbol(); + + ExpressionLabel label = new ExpressionLabel(goodLabel); + + if (sym.isPlus()) { + ExpressionTemporal fExpr = new ExpressionTemporal(ExpressionTemporal.P_F, null, label); + TemporalOperatorBounds fBounds = new TemporalOperatorBounds(); + TemporalOperatorBound fBound = IntegerBound.fromEqualBounds(accLength).toTemporalOperatorBound(); + fBounds.setDefaultBound(fBound); + fExpr.setBounds(fBounds); + // If its a BOX, negate it + if (sym.isBox()) { + return new ExpressionUnaryOp(ExpressionUnaryOp.NOT, fExpr); + } else { + return fExpr; + } + } else { //isMinus + if (sym.isBox()) { + return new ExpressionUnaryOp(ExpressionUnaryOp.NOT, label); + } else { + return label; + } + } + } + + public Object visit(ExpressionAccumulation expr) throws PrismLangException + { + if (expr == accexp) { + // This is a simple accumulation expression. Rewrite to F=.... + return replaceWithReach(expr); + } else { + return expr; + } + } +}