From 0fd6f9ac5c1ff89cc22176d199f0eda7e8ae1238 Mon Sep 17 00:00:00 2001 From: Sascha Wunderlich Date: Tue, 18 Dec 2018 15:01:15 +0100 Subject: [PATCH] Begin support for simple accumulation trafo --- prism/src/explicit/AccumulationProduct.java | 241 ++++------------ .../explicit/AccumulationProductComplex.java | 270 ++++++++++++++++++ ...> AccumulationProductComplexCounting.java} | 18 +- ...=> AccumulationProductComplexRegular.java} | 18 +- .../explicit/AccumulationTransformation.java | 89 ++++-- .../ReplaceAccumulationExpression.java | 115 +++++--- prism/src/prism/PrismSettings.java | 9 +- 7 files changed, 494 insertions(+), 266 deletions(-) create mode 100644 prism/src/explicit/AccumulationProductComplex.java rename prism/src/explicit/{AccumulationProductCounting.java => AccumulationProductComplexCounting.java} (83%) rename prism/src/explicit/{AccumulationProductRegular.java => AccumulationProductComplexRegular.java} (85%) diff --git a/prism/src/explicit/AccumulationProduct.java b/prism/src/explicit/AccumulationProduct.java index b85e24cb..c92ebc12 100644 --- a/prism/src/explicit/AccumulationProduct.java +++ b/prism/src/explicit/AccumulationProduct.java @@ -7,7 +7,6 @@ import java.util.Map; import parser.ast.ExpressionAccumulation; import parser.ast.AccumulationFactor; -import parser.ast.Expression; import prism.IntegerBound; import prism.PrismException; @@ -27,10 +26,6 @@ public abstract class AccumulationProduct extends Pro { protected final StoragePool> trackers; protected final StoragePool> accStates; - - protected final ArrayList initStates; - protected final ArrayList runStates; - protected final ArrayList goalStates; protected final ArrayList labels; @@ -42,106 +37,68 @@ public abstract class AccumulationProduct extends Pro trackers = new StoragePool<>(); accStates = new StoragePool<>(); - initStates = new ArrayList<>(); - runStates = new ArrayList<>(); - goalStates = new ArrayList<>(); - labels = new ArrayList(); } public final int getNumberOfTracks() { return numberOfTracks; } - - public final BitSet getInitStates(int track) { - return initStates.get(track); - } - - public final BitSet getRunStates(int track) { - return runStates.get(track); - } - public final BitSet getGoalStates(int track) { - return goalStates.get(track); - } + protected abstract void generateTrackInfo(ProductState state, Integer index, ExpressionAccumulation accexp, ProbModelChecker mc) throws PrismException; - protected void generateTrackInfo(ProductState state, Integer index, ExpressionAccumulation accexp, ProbModelChecker mc) throws PrismException { - AccumulationState accState = accStates.getById(state.getSecondState()); - AccumulationTracker tracker = accState.getTracker(trackers); - - for(int trackIdx=0; trackIdx track = tracker.getTracks().get(trackIdx); - - // Is this an initial - if (trackIdx==accState.lastRestartNr) { - initStates.get(trackIdx).set(index); - } - - // Is this a running track? - if (track != null) { - runStates.get(trackIdx).set(index); - } - - // Is this a goal track? - if (isGoalTrack(track, accexp, mc)) { - goalStates.get(trackIdx).set(index); - } - } - } - - - /** 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); - - // 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 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); + + // 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; + } @@ -181,21 +138,8 @@ public abstract class AccumulationProduct extends Pro * @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); - } + 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. * @@ -209,66 +153,9 @@ public abstract class AccumulationProduct extends Pro * @return * @throws PrismException */ - protected final AccumulationState updateAccumulationState(final int modelFromStateId, + protected abstract AccumulationState updateAccumulationState(final int modelFromStateId, final AccumulationState accstate, final ExpressionAccumulation accexp, - final double[] weights, final ProbModelChecker mc) throws PrismException { - - // Check if we even need to fire here. - if(accexp.hasFireOn()) { - boolean stutter = true; - for(Expression f : accexp.getFireOn()) { - if(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) { - // 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) { - // 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, accexp, weights, 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); - - return new AccumulationState<>(newTrackerId, newLastRestartNr, numberOfTracks); - } + 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. @@ -292,19 +179,7 @@ public abstract class AccumulationProduct extends Pro return initialAccStateId; } - private String labelString(Integer stateId) { - StringBuffer result = new StringBuffer(); - - for(int t=0; t + */ + +public abstract class AccumulationProductComplex extends AccumulationProduct implements Dottable +{ + protected final ArrayList initStates; + protected final ArrayList runStates; + protected final ArrayList goalStates; + + public AccumulationProductComplex(M originalModel) { + super(originalModel); + initStates = new ArrayList<>(); + runStates = new ArrayList<>(); + goalStates = new ArrayList<>(); + } + + public final BitSet getInitStates(int track) { + return initStates.get(track); + } + + public final BitSet getRunStates(int track) { + return runStates.get(track); + } + + public final BitSet getGoalStates(int track) { + return goalStates.get(track); + } + + protected void generateTrackInfo(ProductState state, Integer index, ExpressionAccumulation accexp, ProbModelChecker mc) throws PrismException { + AccumulationState accState = accStates.getById(state.getSecondState()); + AccumulationTracker tracker = accState.getTracker(trackers); + + for(int trackIdx=0; trackIdx track = tracker.getTracks().get(trackIdx); + + // Is this an initial + if (trackIdx==accState.lastRestartNr) { + initStates.get(trackIdx).set(index); + } + + // Is this a running track? + if (track != null) { + runStates.get(trackIdx).set(index); + } + + // Is this a goal track? + if (isGoalTrack(track, accexp, mc)) { + goalStates.get(trackIdx).set(index); + } + } + } + + /** 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 { + + // Check if we even need to fire here. + if(accexp.hasFireOn()) { + boolean stutter = true; + for(Expression f : accexp.getFireOn()) { + if(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) { + // 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) { + // 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, accexp, weights, 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); + + return new AccumulationState<>(newTrackerId, newLastRestartNr, numberOfTracks); + } + + protected String labelString(Integer stateId) { + StringBuffer result = new StringBuffer(); + + 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/AccumulationProductCounting.java b/prism/src/explicit/AccumulationProductComplexCounting.java similarity index 83% rename from prism/src/explicit/AccumulationProductCounting.java rename to prism/src/explicit/AccumulationProductComplexCounting.java index 0a21b5d5..0d7e4f5d 100644 --- a/prism/src/explicit/AccumulationProductCounting.java +++ b/prism/src/explicit/AccumulationProductComplexCounting.java @@ -20,27 +20,27 @@ import prism.PrismException; * @param */ -public class AccumulationProductCounting extends AccumulationProduct +public class AccumulationProductComplexCounting extends AccumulationProductComplex { - public AccumulationProductCounting(M originalModel) { + public AccumulationProductComplexCounting(M originalModel) { super(originalModel); } @SuppressWarnings("unchecked") - public static AccumulationProductCounting generate(final Model graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + public static AccumulationProductComplexCounting generate(final Model graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { switch(graph.getModelType()) { case DTMC: - return (AccumulationProductCounting)generate((DTMC) graph, accexp, (Vector) rewards, mc, statesOfInterest); + return (AccumulationProductComplexCounting)generate((DTMC) graph, accexp, (Vector) rewards, mc, statesOfInterest); case MDP: - return (AccumulationProductCounting)generate((MDP) graph, accexp, (Vector) rewards, mc, statesOfInterest); + return (AccumulationProductComplexCounting)generate((MDP) graph, accexp, (Vector) rewards, mc, statesOfInterest); default: throw new PrismException("Can't handle accumulation product for " + graph.getModelType()); } } - public static AccumulationProductCounting generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { - final AccumulationProductCounting result = new AccumulationProductCounting(graph); + public static AccumulationProductComplexCounting generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + final AccumulationProductComplexCounting result = new AccumulationProductComplexCounting(graph); // Create auxiliary data result.createAuxData(graph, accexp, rewards, mc); @@ -98,9 +98,9 @@ public class AccumulationProductCounting extends AccumulationPr return result; } - public static AccumulationProductCounting generate(final MDP graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + public static AccumulationProductComplexCounting 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 AccumulationProductCounting result = new AccumulationProductCounting(graph); + final AccumulationProductComplexCounting result = new AccumulationProductComplexCounting(graph); // Create auxiliary data result.createAuxData(graph, accexp, rewards, mc); diff --git a/prism/src/explicit/AccumulationProductRegular.java b/prism/src/explicit/AccumulationProductComplexRegular.java similarity index 85% rename from prism/src/explicit/AccumulationProductRegular.java rename to prism/src/explicit/AccumulationProductComplexRegular.java index 367974c6..23e0cc4e 100644 --- a/prism/src/explicit/AccumulationProductRegular.java +++ b/prism/src/explicit/AccumulationProductComplexRegular.java @@ -26,28 +26,28 @@ import prism.PrismSettings; * @param */ -public class AccumulationProductRegular extends AccumulationProduct +public class AccumulationProductComplexRegular extends AccumulationProductComplex { protected DeterministicFiniteAutomaton automaton; - public AccumulationProductRegular(M originalModel) { + public AccumulationProductComplexRegular(M originalModel) { super(originalModel); } @SuppressWarnings("unchecked") - public static AccumulationProductRegular generate(final Model graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + public static AccumulationProductComplexRegular generate(final Model graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { switch(graph.getModelType()) { case DTMC: - return (AccumulationProductRegular)generate((DTMC) graph, accexp, (Vector) rewards, mc, statesOfInterest); + return (AccumulationProductComplexRegular)generate((DTMC) graph, accexp, (Vector) rewards, mc, statesOfInterest); case MDP: - return (AccumulationProductRegular)generate((MDP) graph, accexp, (Vector) rewards, mc, statesOfInterest); + return (AccumulationProductComplexRegular)generate((MDP) graph, accexp, (Vector) rewards, mc, statesOfInterest); default: throw new PrismException("Can't handle accumulation product for " + graph.getModelType()); } } - public static AccumulationProductRegular generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { - final AccumulationProductRegular result = new AccumulationProductRegular(graph); + public static AccumulationProductComplexRegular generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + final AccumulationProductComplexRegular result = new AccumulationProductComplexRegular(graph); // Create auxiliary data result.createAuxData(graph, accexp, rewards, mc); @@ -105,9 +105,9 @@ public class AccumulationProductRegular extends AccumulationPro return result; } - public static AccumulationProductRegular generate(final MDP graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException { + public static AccumulationProductComplexRegular 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 AccumulationProductRegular result = new AccumulationProductRegular(graph); + final AccumulationProductComplexRegular result = new AccumulationProductComplexRegular(graph); // Create auxiliary data result.createAuxData(graph, accexp, rewards, mc); diff --git a/prism/src/explicit/AccumulationTransformation.java b/prism/src/explicit/AccumulationTransformation.java index ac2bf4d0..3f0e0fb4 100644 --- a/prism/src/explicit/AccumulationTransformation.java +++ b/prism/src/explicit/AccumulationTransformation.java @@ -63,19 +63,15 @@ public class AccumulationTransformation implements ModelExpress return product.projectToOriginalModel(svTransformedModel); } - @SuppressWarnings("unchecked") - private void doTransformation() throws PrismException { + private void doTransformation() throws PrismException { mc.getLog().println("Performing accumulation transformation..."); // We work on a copy transformedExpression = originalExpression.deepCopy(); - + // Get the first ExpressionAccumulation ExpressionAccumulation accexp = transformedExpression.getFirstAccumulationExpression(); mc.getLog().println(" [AT] for " + accexp); - if (accexp.isNullary() && !accexp.hasFireOn()) { - mc.getLog().println(" ... a simple expression."); - } - + // Get the rewards and build the product Vector rewards = new Vector(); @@ -86,13 +82,27 @@ public class AccumulationTransformation implements ModelExpress ConstructRewards constructRewards = new ConstructRewards(); constructRewards.allowNegativeRewards(); - Rewards dtmc_reward = constructRewards.buildRewardStructure(originalModel, rewStruct, mc.getConstantValues()); - rewards.add(i,dtmc_reward); + 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); + } + } + + @SuppressWarnings("unchecked") + private void doTransformationComplex(ExpressionAccumulation accexp, Vector rewards) throws PrismException { + // Build the product if(accexp.hasRegularExpression()) { - product = (AccumulationProductRegular) AccumulationProductRegular.generate(originalModel, accexp, rewards, mc, statesOfInterest); + product = (AccumulationProductComplexRegular) AccumulationProductComplexRegular.generate(originalModel, accexp, rewards, mc, statesOfInterest); } else if (accexp.hasBoundExpression()) { - product = (AccumulationProductCounting) AccumulationProductCounting.generate(originalModel, accexp, rewards, mc, statesOfInterest); + product = (AccumulationProductComplexCounting) AccumulationProductComplexCounting.generate(originalModel, accexp, rewards, mc, statesOfInterest); } else { throw new PrismException("Accumulation Expression has no valid monitor!"); } @@ -106,33 +116,70 @@ public class AccumulationTransformation implements ModelExpress ArrayList runLabels = new ArrayList(); ArrayList goalLabels = new ArrayList(); - for(int track=0; track < product.getNumberOfTracks(); track++) { - BitSet initStates = product.getInitStates(track); - BitSet runStates = product.getRunStates(track); - BitSet goalStates = product.getGoalStates(track); + 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); - String initLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("init" + track, initStates, product.getTransformedModel().getLabels()); + String initLabel = ((ModelExplicit)productComplex.getTransformedModel()).addUniqueLabel("init" + track, initStates, productComplex.getTransformedModel().getLabels()); initLabels.add(initLabel); - String runLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("run" + track, runStates, product.getTransformedModel().getLabels()); + String runLabel = ((ModelExplicit)productComplex.getTransformedModel()).addUniqueLabel("run" + track, runStates, productComplex.getTransformedModel().getLabels()); runLabels.add(runLabel); - String goalLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("goal" + track, goalStates, product.getTransformedModel().getLabels()); + String goalLabel = ((ModelExplicit)productComplex.getTransformedModel()).addUniqueLabel("goal" + track, goalStates, productComplex.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); + 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; + + // Build the product + if(accexp.hasRegularExpression()) { + productSimple = (AccumulationProductSimpleRegular) AccumulationProductSimpleRegular.generate(originalModel, accexp, rewards, mc, statesOfInterest); + } else if (accexp.hasBoundExpression()) { + productSimple = (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()); + + // Transform the model + mc.getLog().println(" [AT] getting the init/run/goal states: "); - mc.getLog().println(" [AT] model transformation done. " + product.trackers.size() + " trackers."); + ArrayList goalLabels = new ArrayList(); + + BitSet goodStates = productSimple.getGoodStates(); + String goalLabel = ((ModelExplicit)productSimple.getTransformedModel()).addUniqueLabel("good", goodStates, productSimple.getTransformedModel().getLabels()); + goalLabels.add(goalLabel); // Transform the expression mc.getLog().println(" [AT] replacing the formula..."); - ReplaceAccumulationExpression replace = new ReplaceAccumulationExpression(accexp, initLabels, runLabels, goalLabels, product.getNumberOfTracks()-1); + ReplaceAccumulationExpression replace = new ReplaceAccumulationExpression(accexp, mc, null, null, goalLabels, productSimple.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"); + productSimple.exportToDotFile("DEBUG-product.dot"); } + */ } } diff --git a/prism/src/parser/visitor/ReplaceAccumulationExpression.java b/prism/src/parser/visitor/ReplaceAccumulationExpression.java index b7b9259b..6b0709c7 100644 --- a/prism/src/parser/visitor/ReplaceAccumulationExpression.java +++ b/prism/src/parser/visitor/ReplaceAccumulationExpression.java @@ -2,6 +2,7 @@ package parser.visitor; import java.util.ArrayList; +import explicit.ProbModelChecker; import parser.ast.AccumulationSymbol; import parser.ast.Expression; import parser.ast.ExpressionAccumulation; @@ -9,76 +10,104 @@ 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 { private ExpressionAccumulation accexp; + private ProbModelChecker mc; private ArrayList initLabels; private ArrayList runLabels; private ArrayList goalLabels; private int accLength; - - - public ReplaceAccumulationExpression(ExpressionAccumulation accexp, ArrayList initLabels, ArrayList runLabels, ArrayList goalLabels, int accLength) { + public ReplaceAccumulationExpression(ExpressionAccumulation accexp, ProbModelChecker mc, ArrayList initLabels, ArrayList runLabels, ArrayList goalLabels, int accLength) { super(); this.accexp = accexp; + this.mc = mc; this.initLabels = initLabels; this.runLabels = runLabels; this.goalLabels = goalLabels; this.accLength = accLength; } - public Object visit(ExpressionAccumulation expr) throws PrismLangException - { - if (expr == accexp) { - AccumulationSymbol sym = expr.getSymbol(); + private Object replaceWithUntil(ExpressionAccumulation accexpr) throws PrismLangException { + // This expression is of the form OR{0..(l-1)}(init_i AND (run_i UNTIL goal_i)) + + // Build all the subexpressions... + ArrayList clauses = new ArrayList<>(); + Expression result = null; + + for(int i=0; i clauses = new ArrayList<>(); - Expression result = null; + // until: (run_i UNTIL goal_i) + ExpressionTemporal until = new ExpressionTemporal(ExpressionTemporal.P_U, run, goal); + // and: (init_i AND until) + ExpressionBinaryOp and = new ExpressionBinaryOp(ExpressionBinaryOp.AND, init, until); - for(int i=0; i