diff --git a/prism/src/explicit/AccumulationModelChecker.java b/prism/src/explicit/AccumulationModelChecker.java new file mode 100644 index 00000000..f3231173 --- /dev/null +++ b/prism/src/explicit/AccumulationModelChecker.java @@ -0,0 +1,53 @@ +package explicit; + +import java.util.ArrayList; +import java.util.BitSet; + +import parser.ast.Expression; +import parser.ast.ExpressionLabel; +import parser.ast.ExpressionRegular; +import parser.type.TypeBool; +import prism.PrismComponent; +import prism.PrismException; + +public class AccumulationModelChecker extends PrismComponent { + public Expression checkMaximalStateFormulas(ProbModelChecker mc, Model model, Expression expr, ArrayList labelBS) + throws PrismException + { + // This is basically copied from DM + // A state formula + if (expr.getType() instanceof TypeBool) { + // Model check + StateValues sv = mc.checkExpression(model, expr, null); + BitSet bs = sv.getBitSet(); + // Detect special cases (true, false) for optimisation + if (bs.isEmpty()) { + return Expression.False(); + } + if (bs.cardinality() == model.getNumStates()) { + return Expression.True(); + } + // See if we already have an identical result + // (in which case, reuse it) + int i = labelBS.indexOf(bs); + if (i != -1) { + sv.clear(); + return new ExpressionLabel("L" + i); + } + // Otherwise, add result to list, return new label + labelBS.add(bs); + return new ExpressionLabel("L" + (labelBS.size() - 1)); + } + // A path formula (recurse, modify, return) + else if (expr instanceof ExpressionRegular) { + ExpressionRegular reg = (ExpressionRegular)expr; + if(reg.getOperand1() != null) { + reg.setOperand1(checkMaximalStateFormulas(mc, model, reg.getOperand1(), labelBS)); + } + if(reg.getOperand2() != null) { + reg.setOperand2(checkMaximalStateFormulas(mc, model, reg.getOperand2(), labelBS)); + } + } + return expr; + } +} diff --git a/prism/src/explicit/AccumulationProduct.java b/prism/src/explicit/AccumulationProduct.java new file mode 100644 index 00000000..6c34d93c --- /dev/null +++ b/prism/src/explicit/AccumulationProduct.java @@ -0,0 +1,121 @@ +package explicit; + +import java.util.ArrayList; +import java.util.BitSet; +import java.util.Iterator; +import java.util.Map; + +import prism.PrismException; +import prism.PrismFileLog; +import prism.PrismLog; + +/** + * 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 AccumulationProduct extends ProductWithProductStates +{ + final StoragePool> trackers; + final StoragePool accStates; + + final BitSet goodStates; + + final ArrayList labels; + + int numberOfTracks; + int numberOfWeights; + + public AccumulationProduct(M originalModel) { + super(originalModel); + trackers = new StoragePool<>(); + accStates = new StoragePool<>(); + + goodStates = new BitSet(); + labels = new ArrayList(); + } + + public BitSet getGoodStates() { + return goodStates; + } + + public int getNumberOfTracks() { + return numberOfTracks; + } + + public void exportToDotFile(String filename) throws PrismException { + try (PrismFileLog log = PrismFileLog.create(filename)) { + exportToDotFile(log); + } + } + + public void exportToDotFile(PrismLog out) { + out.print(toDot()); + } + + public String quoteForDot(String original) { + String result = original; + result = result.replaceAll("&", "&"); + result = result.replaceAll("<", "<"); + result = result.replaceAll(">", ">"); + return result; + } + + public String toDot() { + StringBuffer result = new StringBuffer(); + + result.append("digraph " + originalModel.getModelType() + " {\n"); + + for(int i = 0; i < prod_states.size(); i++) { + ProductState fromState = prod_states.get(i); + AccumulationState accState = accStates.getById(fromState.getSecondState()); + AccumulationTracker tracker = trackers.getById(accState.getTrackerId()); + result.append("" + + i + + "[shape=box, color=black" + + " label= < " + + "" + + "" + + "" + + "" + + "" + + "" + + "" + + "
" + i + "=" + fromState + "
" + accState + "
\"" + 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/AccumulationProductCounting.java new file mode 100644 index 00000000..1f613bfe --- /dev/null +++ b/prism/src/explicit/AccumulationProductCounting.java @@ -0,0 +1,301 @@ +package explicit; + +import java.util.ArrayList; +import java.util.BitSet; +import java.util.Vector; + +import explicit.rewards.MCRewards; +import explicit.rewards.MDPRewards; +import explicit.rewards.Rewards; +import parser.ast.AccumulationFactor; +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 AccumulationProductCounting extends AccumulationProduct +{ + + public AccumulationProductCounting(M originalModel) { + super(originalModel); + } + + 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); + // 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(rewards.size()); + 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 { + AccumulationState accState = result.accStates.getById(state.getSecondState()); + if (result.isGoodAccState(accState, accexp, mc)) { + result.goodStates.set(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 AccumulationProductCounting 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); + + // 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(rewards.size()); + 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 { + AccumulationState accState = result.accStates.getById(state.getSecondState()); + if (result.isGoodAccState(accState, accexp, mc)) { + result.goodStates.set(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; + } + + private boolean isFinalTrack(final AccumulationTrack track, final ExpressionAccumulation accexp, final ProbModelChecker mc) + throws PrismException { + boolean isFinal = false; + if ( track != null ) { + IntegerBound stepBound = IntegerBound.fromTemporalOperatorBound(accexp.getBoundExpression(), mc.getConstantValues(), true); + isFinal = stepBound.isInBounds(track.getComponent()); + } + return isFinal; + } + + private boolean isGoodAccState(final AccumulationState state, final ExpressionAccumulation accexp, final ProbModelChecker mc) + throws PrismException { + return state.hasGoodTrack(); + } + + private boolean isGoodTrack(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; + + // 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. + switch(accexp.getSymbol()) { + case ACCBOXMINUS: + case ACCBOXPLUS: + if (!rhs.isInBounds(lhs)) { + isGood = true; + } + break; + case ACCDIAMINUS: + case ACCDIAPLUS: + if (rhs.isInBounds(lhs)) { + isGood = true; + } + break; + default: + throw new RuntimeException("Oh boy!"); + } + if(isGood) {mc.getLog().print("+");} else {mc.getLog().print("-");} + return isGood; + } + + private AccumulationState updateAccumulationState(final int modelFromStateId, + final AccumulationState accstate, final ExpressionAccumulation accexp, + final double[] weights, final ProbModelChecker mc) throws PrismException { + // We have the current accumulation state, the current model id and the accumulation expression. + + // Get the old tracker and tracks. + AccumulationTracker oldTracker = trackers.getById(accstate.getTrackerId()); + ArrayList> oldTracks = oldTracker.getTracks(); + + BitSet oldGoodTracks = accstate.getGoodTracks(); + BitSet newGoodTracks = (BitSet) oldGoodTracks.clone(); + + // This restart will be... + int newLastRestartNr = accstate.getNextRestartNr(); + mc.getLog().print(newLastRestartNr); + + // Build the new tracks. + ArrayList> newTracks = new ArrayList<>(); + + int trackNr = 0; + for(AccumulationTrack oldTrack : oldTracks) { + AccumulationTrack newTrack; + + // restart or advance + if(trackNr == newLastRestartNr) { + //assert oldTrack == null : "Track " + newLastRestartNr + " is not null!"; + newTrack = new AccumulationTrack(numberOfWeights, 0); //TODO: off-by-one? + newGoodTracks.clear(trackNr); + } else if (oldTrack == null) { + newTrack = null; + } else { + assert oldTrack != null; + newTrack = updateTrackBounds(oldTrack, accexp, weights, mc); + } + + // check whether the track is good + if(!newGoodTracks.get(trackNr)) { + newGoodTracks.set(trackNr, isGoodTrack(newTrack, accexp, mc)); + } + + newTracks.add(newTrack); + trackNr++; + } + + AccumulationTracker newTracker = new AccumulationTracker<>(newTracks); + + + int newTrackerId = trackers.findOrAdd(newTracker); + + return new AccumulationState(newTrackerId, newLastRestartNr, numberOfTracks, newGoodTracks); + } + + private AccumulationTrack updateTrackBounds(final AccumulationTrack track, + final ExpressionAccumulation accexp, final double[] weights, final StateModelChecker mc) throws PrismException { + int currentStep = track.getComponent(); + int maxStep = IntegerBound.fromTemporalOperatorBound(accexp.getBoundExpression(), mc.getConstantValues(), true).getHighestInteger(); + + // If we are done, return null-Track + if (currentStep >= maxStep) { 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, currentStep+1); + } + + protected int createInitialStateId(final int numberOfRewards) { + // The initial active track is the first one, all tracks are non-good by default + int initialActiveTrack = 0; + BitSet initialGoodTracks = new BitSet(); + + // Generate the initial tracker and product state + AccumulationTracker initialTracker = new AccumulationTracker<>(numberOfTracks, numberOfRewards, 0); + int initialTrackerId = trackers.findOrAdd(initialTracker); + AccumulationState initialAccState = new AccumulationState(initialTrackerId, initialActiveTrack, numberOfTracks, initialGoodTracks); + int initialAccStateId = accStates.findOrAdd(initialAccState); + + return initialAccStateId; + } + + 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()+1; + numberOfWeights = rewards.size(); + } +} diff --git a/prism/src/explicit/AccumulationProductRegular.java b/prism/src/explicit/AccumulationProductRegular.java new file mode 100644 index 00000000..7d7d9602 --- /dev/null +++ b/prism/src/explicit/AccumulationProductRegular.java @@ -0,0 +1,345 @@ +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 parser.ast.AccumulationFactor; +import parser.ast.ExpressionAccumulation; +import parser.ast.ExpressionRegular; +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 AccumulationProductRegular extends AccumulationProduct +{ + DeterministicFiniteAutomaton automaton; + + public AccumulationProductRegular(M originalModel) { + super(originalModel); + } + + 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); + // Create auxiliary data + result.createAuxData(graph, accexp, mc); + + // Build an operator + class AccumulationDTMCProductOperator implements DTMCProductOperator + { + @Override + public ProductState getInitialState(Integer dtmc_state) + throws PrismException { + int initialAccStateId = result.createInitialStateId(rewards.size()); + 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 { + AccumulationState accState = result.accStates.getById(state.getSecondState()); + if (result.isGoodAccState(accState, accexp, mc)) { + result.goodStates.set(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 AccumulationProductRegular 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); + + // Create auxiliary data + result.createAuxData(graph, accexp, mc); + + class AccumulationMDPProductOperator implements MDPProductOperator + { + + @Override + public ProductState getInitialState(Integer MDP_state) + throws PrismException { + int initialAccStateId = result.createInitialStateId(rewards.size()); + return new ProductState(MDP_state, initialAccStateId); + } + + @Override + public ProductState getSuccessor(ProductState from_state, + int choice_i, 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(ProductState state, Integer index) + throws PrismException { + AccumulationState accState = result.accStates.getById(state.getSecondState()); + if (result.isGoodAccState(accState, accexp, mc)) { + result.goodStates.set(index); + } + } + + @Override + public void finish() throws PrismException { + // Do nothing + + } + + @Override + public MDP getGraph() { + return graph; + } + } + + AccumulationMDPProductOperator op = new AccumulationMDPProductOperator(); + ProductWithProductStates.generate(op, result, statesOfInterest); + return result; + } + + private boolean isFinalTrack(AccumulationTrack track, ExpressionAccumulation accexp, ProbModelChecker mc) throws PrismException { + boolean isFinal = false; + if ( track != null ) { + isFinal = automaton.isAcceptingState(track.getComponent()); + } + + return isFinal; + } + + private boolean isGoodAccState(AccumulationState state, ExpressionAccumulation accexp, ProbModelChecker mc) throws PrismException { + //TODO: fill me! + return false; + } + + private boolean isGoodTrack(AccumulationTrack track, ExpressionAccumulation accexp, ProbModelChecker mc) throws PrismException { + //System.out.println("Checking " + track + " for goodness..."); + // Only final tracks can be good + if (!isFinalTrack(track,accexp,mc)) { return false; } + boolean isGood = false; + + //System.out.println("Final: " + track); + + // 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. + switch(accexp.getSymbol()) { + case ACCBOXMINUS: + case ACCBOXPLUS: + if (!rhs.isInBounds(lhs)) { + isGood = true; + } + break; + case ACCDIAMINUS: + case ACCDIAPLUS: + if (rhs.isInBounds(lhs)) { + isGood = true; + } + break; + default: + throw new RuntimeException("Oh boy!"); + } + + //System.out.println("Good? " + isGood); + + return isGood; + } + + private AccumulationState updateAccumulationState(final int modelFromStateId, + final AccumulationState accstate, final ExpressionAccumulation accexp, + final double[] weights, final ProbModelChecker mc) throws PrismException { + // We have the current accumulation state, the current model id and the accumulation expression. + + // Get the old tracker and tracks. + AccumulationTracker oldTracker = trackers.getById(accstate.getTrackerId()); + ArrayList> oldTracks = oldTracker.getTracks(); + + BitSet oldGoodTracks = accstate.getGoodTracks(); + BitSet newGoodTracks = (BitSet) oldGoodTracks.clone(); + + // This restart will be... + int newLastRestartNr = accstate.getNextRestartNr(); + mc.getLog().print(newLastRestartNr); + + // Build the new tracks. + ArrayList> newTracks = new ArrayList<>(); + + int trackNr = 0; + for(AccumulationTrack oldTrack : oldTracks) { + AccumulationTrack newTrack; + + // restart or advance + if(trackNr == newLastRestartNr) { + //assert oldTrack == null : "Track " + newLastRestartNr + " is not null!"; + newTrack = new AccumulationTrack(numberOfWeights, automaton.getInitialState()); //TODO: off-by-one? + newGoodTracks.clear(trackNr); + } else if (oldTrack == null) { + newTrack = null; + } else { + assert oldTrack != null; + newTrack = updateTrackRegular(modelFromStateId, oldTrack, accexp, weights, mc); + } + + // check whether the track is good + if(!newGoodTracks.get(trackNr)) { + newGoodTracks.set(trackNr, isGoodTrack(newTrack, accexp, mc)); + } + + newTracks.add(newTrack); + trackNr++; + } + + AccumulationTracker newTracker = new AccumulationTracker<>(newTracks); + + + int newTrackerId = trackers.findOrAdd(newTracker); + + return new AccumulationState(newTrackerId, newLastRestartNr, numberOfTracks, newGoodTracks); + } + private AccumulationTrack updateTrackRegular(Integer modelFromStateId, AccumulationTrack track, ExpressionAccumulation accexp, double[] weights, 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); + //System.out.println("Successor of " + currentState + " via " + edgeLabel + ":" + nextState); + + // Undefined behavior, return the null-Track + if (nextState == null) { return null; } + + // If we have defined behavior, update the weights and get the new stateId. + 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, nextState); + } + + protected int createInitialStateId(int numberOfRewards) { + // Find the initial state id (0 or automaton state) + State initialState = automaton.getInitialState(); + + // The initial active track is the first one, all tracks are non-good by default + int initialActiveTrack = 0; + BitSet initialGoodTracks = new BitSet(); + + // Generate the initial track and product state + AccumulationTracker initialTracker = new AccumulationTracker<>(numberOfTracks, numberOfRewards, initialState); + int initialTrackerId = trackers.findOrAdd(initialTracker); + AccumulationState initialAccState = new AccumulationState(initialTrackerId, initialActiveTrack, numberOfTracks, initialGoodTracks); + int initialAccStateId = accStates.findOrAdd(initialAccState); + + return initialAccStateId; + } + + public void createAuxData(final Model graph, final ExpressionAccumulation accexp, final ProbModelChecker mc) throws PrismException { + mc.getLog().println(" [AP] generating aux data for " + graph + "\n and " + accexp); + // 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. + + System.out.println(nfa.toDot()); + + if (!automaton.isAcyclic()) { + throw new PrismException("Cannot handle cyclic automata!"); + } + + numberOfTracks = automaton.getLongestPathLength(); + } +} diff --git a/prism/src/explicit/AccumulationState.java b/prism/src/explicit/AccumulationState.java new file mode 100644 index 00000000..78c22ee9 --- /dev/null +++ b/prism/src/explicit/AccumulationState.java @@ -0,0 +1,104 @@ +package explicit; + +import java.util.BitSet; + +/** + * An AccumulationState contains a reference to an AccumulationTracker, a BitSet + * of successful tracks goodTracks, a pointer to the latest restart and the + * numberOfTracks in the tracker. + * + * @author Sascha Wunderlich + * + */ +public class AccumulationState { + final int trackerId; + + final BitSet goodTracks; + + int lastRestartNr; + int numberOfTracks; + + public AccumulationState(int trackerId, int lastRestartNr, int numberOfTracks, + BitSet goodTracks) { + super(); + this.trackerId = trackerId; + this.lastRestartNr = lastRestartNr; + this.numberOfTracks = numberOfTracks; + this.goodTracks = goodTracks; + } + + public int getTrackerId() { + return trackerId; + } + + public int getLastRestartNr() { + return lastRestartNr; + } + + public void setLastRestartNr(int lastRestartNr) { + this.lastRestartNr = lastRestartNr; + } + + public BitSet getGoodTracks() { + return goodTracks; + } + + public boolean isGoodTrack(int trackNr) { + return goodTracks.get(trackNr); + } + + public boolean hasGoodTrack() { + return !goodTracks.isEmpty(); + } + + public int getNextRestartNr() { + return (lastRestartNr + 1) % numberOfTracks; + } + + public void advance() { + lastRestartNr = getNextRestartNr(); + } + + @Override + public int hashCode() { + final int prime = 31; + int result = 1; + result = prime * result + ((goodTracks == null) ? 0 : goodTracks.hashCode()); + result = prime * result + lastRestartNr; + result = prime * result + trackerId; + return result; + } + + @Override + public boolean equals(Object obj) { + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; + AccumulationState other = (AccumulationState) obj; + if (goodTracks == null) { + if (other.goodTracks != null) + return false; + } else if (!goodTracks.equals(other.goodTracks)) + return false; + if (lastRestartNr != other.lastRestartNr) + return false; + if (trackerId != other.trackerId) + return false; + return true; + } + + @Override + public String toString() { + StringBuffer result = new StringBuffer(); + result.append("S"); + + result.append(trackerId); + result.append(goodTracks); + + return result.toString(); + } + +} diff --git a/prism/src/explicit/AccumulationTrack.java b/prism/src/explicit/AccumulationTrack.java new file mode 100644 index 00000000..3f9a1419 --- /dev/null +++ b/prism/src/explicit/AccumulationTrack.java @@ -0,0 +1,83 @@ +package explicit; + +import java.util.Arrays; + +/** + * An AccumulationTrack contains a double array of weights + * and a Component representing the current progress of the accumulation window. + * @author Sascha Wunderlich + * + * @param + */ +public class AccumulationTrack { + final private double[] weights; + final private Component component; + + public AccumulationTrack(int numberOfWeights, Component component) { + weights = new double[numberOfWeights]; + for (int i=0; i + */ +public class AccumulationTracker { + final private ArrayList> tracks; + + public AccumulationTracker(int numberOfTracks, int numberOfWeights, Component component) { + super(); + this.tracks = new ArrayList>(numberOfTracks); + this.tracks.add(new AccumulationTrack<>(numberOfWeights, component)); + while(this.tracks.size() < numberOfTracks) { + this.tracks.add(null); + } + assert(this.tracks.size() == numberOfTracks); + } + + public AccumulationTracker(ArrayList> tracks) { + super(); + this.tracks = new ArrayList>(tracks.size()); + this.tracks.addAll(tracks); + } + + public ArrayList> getTracks() { + return tracks; + } + + @Override + public int hashCode() { + final int prime = 31; + int result = 1; + result = prime * result + ((tracks == null) ? 0 : tracks.hashCode()); + return result; + } + + @SuppressWarnings("rawtypes") + @Override + public boolean equals(Object obj) { + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; + AccumulationTracker other = (AccumulationTracker) obj; + if (tracks == null) { + if (other.tracks != null) + return false; + } else if (!tracks.equals(other.tracks)) + return false; + return true; + } + + + @Override + public String toString() { + StringBuffer result = new StringBuffer(); + result.append(tracks); + return result.toString(); + } +} diff --git a/prism/src/explicit/AccumulationTransformation.java b/prism/src/explicit/AccumulationTransformation.java new file mode 100644 index 00000000..c7d1c7ec --- /dev/null +++ b/prism/src/explicit/AccumulationTransformation.java @@ -0,0 +1,162 @@ +package explicit; + +import java.util.BitSet; +import java.util.Vector; + +import explicit.rewards.ConstructRewards; +import explicit.rewards.MCRewards; +import explicit.rewards.MDPRewards; +import parser.ast.Expression; +import parser.ast.ExpressionAccumulation; +import parser.ast.ExpressionReward; +import parser.ast.RewardStruct; +import parser.visitor.ReplaceAccumulationExpression; +import prism.PrismException; + +public class AccumulationTransformation implements ModelExpressionTransformation { + final private Expression originalExpression; + final private M originalModel; + final private BitSet statesOfInterest; + final ProbModelChecker mc; + + private Expression transformedExpression; + private AccumulationProduct product; + + public AccumulationTransformation( + ProbModelChecker mc, + M originalModel, Expression expr, + BitSet statesOfInterest) throws PrismException{ + super(); + this.originalExpression = expr; + this.originalModel = originalModel; + this.mc = mc; + this.statesOfInterest = statesOfInterest; + doTransformation(); + } + + @Override + public M getOriginalModel() { + return originalModel; + } + @Override + public Expression getTransformedExpression() { + return transformedExpression; + } + @Override + public Expression getOriginalExpression() { + return originalExpression; + } + + @Override + public BitSet getTransformedStatesOfInterest() { + return product.getTransformedStatesOfInterest(); + } + + @Override + public M getTransformedModel() { + return product.getTransformedModel(); + } + @Override + public StateValues projectToOriginalModel(StateValues svTransformedModel) + throws PrismException { + return product.projectToOriginalModel(svTransformedModel); + } + + @SuppressWarnings("unchecked") + 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(); + + // Get the rewards and build the product + switch(originalModel.getModelType()) { + case DTMC: + Vector dtmc_rewards = new Vector(); + + for (int i=0; i < accexp.getConstraint().getFactors().size(); i++) { + Object rewardIndex = accexp.getConstraint().getFactors().get(i).getFunction().getRewardIndex(); + + RewardStruct rewStruct = ExpressionReward.getRewardStructByIndexObject(rewardIndex, mc.modulesFile, originalModel.getConstantValues()); + ConstructRewards constructRewards = new ConstructRewards(); + constructRewards.allowNegativeRewards(); + + MCRewards dtmc_reward = constructRewards.buildMCRewardStructure((DTMC)originalModel, rewStruct, mc.getConstantValues()); + dtmc_rewards.add(i,dtmc_reward); + } + mc.getLog().println(" [AT] performing product construction..."); + if(accexp.hasRegularExpression()) { + product = (AccumulationProductRegular) AccumulationProductRegular.generate((DTMC)originalModel, accexp, dtmc_rewards, mc, statesOfInterest); + } else if (accexp.hasBoundExpression()) { + product = (AccumulationProductCounting) AccumulationProductCounting.generate((DTMC)originalModel, accexp, dtmc_rewards, mc, statesOfInterest); + } else { + throw new PrismException("Accumulation Expression has no valid monitor!"); + } + break; + case MDP: + Vector mdp_rewards = new Vector(); + + for (int i=0; i < accexp.getConstraint().getFactors().size(); i++) { + Object rewardIndex = accexp.getConstraint().getFactors().get(i).getFunction().getRewardIndex(); + + RewardStruct rewStruct = ExpressionReward.getRewardStructByIndexObject(rewardIndex, mc.modulesFile, originalModel.getConstantValues()); + ConstructRewards constructRewards = new ConstructRewards(); + constructRewards.allowNegativeRewards(); + + MDPRewards mdp_reward = constructRewards.buildMDPRewardStructure((MDP)originalModel, rewStruct, mc.getConstantValues()); + mdp_rewards.add(i,mdp_reward); + } + mc.getLog().println(" [AT] performing product construction..."); + if(accexp.hasRegularExpression()) { + product = (AccumulationProductRegular) AccumulationProductRegular.generate((MDP)originalModel, accexp, mdp_rewards, mc, statesOfInterest); + } else if (accexp.hasBoundExpression()) { + product = (AccumulationProductCounting) AccumulationProductCounting.generate((MDP)originalModel, accexp, mdp_rewards, mc, statesOfInterest); + } else { + throw new PrismException("Accumulation Expression has no valid monitor!"); + } + + break; + default: + throw new PrismException("Can't handle weight functions for " + originalModel.getModelType()); + } + + // Transform the model + BitSet goodStates = product.getGoodStates(); + String label = gensymLabel("good", product.getTransformedModel()); + + ((ModelExplicit)product.getTransformedModel()).addLabel(label, goodStates); + + //System.out.println("Good states " + goodStates); + + // Transform the expression + ReplaceAccumulationExpression replace = new ReplaceAccumulationExpression(accexp, label, product.getNumberOfTracks()); + transformedExpression = (Expression)transformedExpression.accept(replace); + mc.getLog().println("Transformed " + originalExpression.toString() + + "\n into " + transformedExpression.toString()); + //DEBUG: output dotfile + product.exportToDotFile("./out.dot"); + } + + public String gensymLabel(String prefix, Model model) { + int suffix = 0; + String label = prefix + "_" + suffix; + while(product.getTransformedModel().getLabels().contains(label)) { + suffix++; + label = prefix + "_" + suffix; + } + return label; + } + + @Override + public Integer mapToTransformedModel(int state) { + return product.mapToTransformedModel(state); + } + + @Override + public BitSet mapToTransformedModel(BitSet states) { + return product.mapToTransformedModel(states); + } + +} diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 20845e4a..29b495e2 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -80,6 +80,19 @@ public class DTMCModelChecker extends ProbModelChecker super(parent); } + protected StateValues checkProbPathFormulaAccumulationExpression(Model model, Expression expr, BitSet statesOfInterest) throws PrismException + { + // Do a transformation and a projection + AccumulationTransformation accTrans = new AccumulationTransformation(this, (DTMC)model, expr, statesOfInterest); + StateValues transValues = this.checkProbPathFormula(accTrans.getTransformedModel(), accTrans.getTransformedExpression(), MinMax.blank(), accTrans.getTransformedStatesOfInterest()); + //this.getLog().println("TransValues"); + //transValues.print(this.getLog()); + StateValues projectedValues = accTrans.projectToOriginalModel(transValues); + //this.getLog().println("ProjectedValues"); + //projectedValues.print(this.getLog()); + return projectedValues; + } + // Model checking functions @Override diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 304dca87..8c130c76 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -90,6 +90,15 @@ public class MDPModelChecker extends ProbModelChecker // Model checking functions + protected StateValues checkProbPathFormulaAccumulationExpression(Model model, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException + { + // Do a transformation and a projection + AccumulationTransformation accTrans = new AccumulationTransformation(this, (MDP)model, expr, statesOfInterest); + StateValues transValues = this.checkProbPathFormula(accTrans.getTransformedModel(), accTrans.getTransformedExpression(), minMax, accTrans.getTransformedStatesOfInterest()); + StateValues projectedValues = accTrans.projectToOriginalModel(transValues); + return projectedValues; + } + @Override protected StateValues checkProbPathFormulaSimple(Model model, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException { diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index db224f80..0874a24d 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -622,7 +622,15 @@ public class ProbModelChecker extends NonProbModelChecker if (useSimplePathAlgo) { return checkProbPathFormulaSimple(model, expr, minMax, statesOfInterest); - } else { + } else if (Expression.containsAccumulationExpression(expr)) { + if (model.getModelType() == ModelType.DTMC) { + return ((DTMCModelChecker)this).checkProbPathFormulaAccumulationExpression(model, expr, statesOfInterest); + } else if (model.getModelType() == ModelType.MDP) { + return ((MDPModelChecker)this).checkProbPathFormulaAccumulationExpression(model, expr, minMax, statesOfInterest); + } else { + throw new PrismException("Model checking of accumulation expressions formulas is not supported for "+model.getModelType().name()); + } + } else { return checkProbPathFormulaLTL(model, expr, false, minMax, statesOfInterest); } } diff --git a/prism/src/explicit/StoragePool.java b/prism/src/explicit/StoragePool.java new file mode 100644 index 00000000..ecf3c40f --- /dev/null +++ b/prism/src/explicit/StoragePool.java @@ -0,0 +1,45 @@ +package explicit; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.Iterator; + +/** + * A generic pool of things of type T, which can only grow. + * Uses an ArrayList and a HashMap internally. + * Provides a findOrAdd method. + * + * @author sw + * + * @param + */ +public class StoragePool implements Iterable { + final ArrayList things; + final HashMap thingIds; + + public StoragePool() { + things = new ArrayList(); + thingIds = new HashMap(); + } + + public T getById(final int thingId) { + return things.get(thingId); + } + + public int findOrAdd(final T thing) { + Integer thingId = thingIds.get(thing); + + if (thingId == null) { + thingId = things.size(); + things.add(thingId, thing); + thingIds.put(thing, thingId); + } + + return thingId; + } + + @Override + public Iterator iterator() { + return things.iterator(); + } +} diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj index 79727a57..f01ee5af 100644 --- a/prism/src/parser/PrismParser.jj +++ b/prism/src/parser/PrismParser.jj @@ -493,16 +493,16 @@ TOKEN : | < RPARENTH: ")" > | < LBRACKET: "[" > | < RBRACKET: "]" > -| < DLBRACKET: "[[" > -| < DRBRACKET: "]]" > +//| < DLBRACKET: "[[" > +//| < DRBRACKET: "]]" > | < LBRACE: "{" > | < RBRACE: "}" > | < EQ: "=" > | < NE: "!=" > | < LT: "<" > | < GT: ">" > -| < DLT: "<<" > -| < DGT: ">>" > +//| < DLT: "<<" > +//| < DGT: ">>" > | < LE: "<=" > | < GE: ">=" > | < PLUS: "+" > @@ -513,6 +513,11 @@ TOKEN : | < RENAME: "<-" > | < QMARK: "?" > | < CARET: "^" > + // Accumulation +| < ACCDIAPLUS: "<+>" > +| < ACCDIAMINUS: "<->" > +| < ACCBOXPLUS: "[+]" > +| < ACCBOXMINUS: "[-]" > // Regular expressions | < REG_INT: (["1"-"9"](["0"-"9"])*)|("0") > | < REG_DOUBLE: (["0"-"9"])*(".")?(["0"-"9"])+(["e","E"](["-","+"])?(["0"-"9"])+)? > @@ -1184,10 +1189,119 @@ Expression ExpressionTemporalUnary(boolean prop, boolean pathprop) : { exprTemp.setOperand2(expr); exprTemp.setPosition(begin, getToken(0)); ret = exprTemp; } | ret = ExpressionITE(prop, pathprop) + | + ret = ExpressionAccumulation(prop, pathprop) ) { return ret; } } +/* START + Accumulation Specification */ +ExpressionAccumulation ExpressionAccumulation(boolean prop, boolean pathprop) : +{ + ExpressionAccumulation ret; + AccumulationConstraint constr; + TemporalOperatorBound bound; + Expression reg; +} +{ + // Accumulation symbol + ( + ( { ret = new ExpressionAccumulation(AccumulationSymbol.ACCDIAPLUS); } ) + | ( { ret = new ExpressionAccumulation(AccumulationSymbol.ACCDIAMINUS); } ) + | ( { ret = new ExpressionAccumulation(AccumulationSymbol.ACCBOXPLUS); } ) + | ( { ret = new ExpressionAccumulation(AccumulationSymbol.ACCBOXMINUS); } ) + ) + // Regular expression, should be star-free + + ( + ( reg = ExpressionRegularUnary(prop, false) { ret.setRegularExpression((ExpressionRegular)reg); } ) + | ( bound = BoundExpression() { ret.setBoundExpression(bound); } ) + ) + + // Weight constraint + + ( + constr = ExpressionAccumulationConstraint() + { ret.setConstraint(constr); } + ) + + { return ret; } +} + +AccumulationConstraint ExpressionAccumulationConstraint() : +{ + AccumulationConstraint ret; + ArrayList factors; + TemporalOperatorBound bound; +} +{ + // (LiCo = Constant) + factors = ExpressionAccumulationLinearCombination() + bound = BoundExpression() + { return new AccumulationConstraint(factors, bound); } +} + +ArrayList ExpressionAccumulationLinearCombination() : +{ + AccumulationFactor factor; + ArrayList factors = new ArrayList(); +} +{ + factor = ExpressionAccumulationLinearFactor() { factors.add(factor); } + ( + + factor = ExpressionAccumulationLinearFactor() { factors.add(factor); } + )* + { return factors; } +} + +AccumulationFactor ExpressionAccumulationLinearFactor() : +{ + Expression factor = null; + AccumulationFunction func; +} +{ + // (Factor*Function) + ( + ( LOOKAHEAD({ getToken(1).kind==REG_IDENT && + ( getToken(1).image.equals("time") || getToken(1).image.equals("steps") || getToken(1).image.equals("reward") )}) + func = ExpressionAccumulationFunction() ) + | + ( factor = ExpressionBasic(false,false) + func = ExpressionAccumulationFunction() ) + ) + { return new AccumulationFactor(func,factor); } +} + +// This is taken from TemporalOpBound +AccumulationFunction ExpressionAccumulationFunction() : +{ + AccumulationFunction func = null; + Object rewardIndex = null; +} +{ + ( (LOOKAHEAD({ getToken(1).kind==REG_IDENT && getToken(1).image.equals("time") }) + Identifier() {func = AccumulationFunction.ACC_TIME;}) + | (LOOKAHEAD({ getToken(1).kind==REG_IDENT && getToken(1).image.equals("steps") }) + Identifier() {func = AccumulationFunction.ACC_STEPS;}) + + // SWDO: We also want "weight" here + | (LOOKAHEAD({ getToken(1).kind==REG_IDENT && getToken(1).image.equals("reward") }) + Identifier() + (rewardIndex = RewardIndex())? + { + func = AccumulationFunction.ACC_REWARD; + func.setRewardIndex(rewardIndex); + }) + ) + {return func;} +} + +/* END + Accumulation Specification */ + + //Regular Expressions Expression ExpressionRegularUnary(boolean prop, boolean pathprop) : { @@ -1579,7 +1693,7 @@ Expression ExpressionLiteral(boolean prop, boolean pathprop) : { try { int i = Integer.parseInt(getToken(0).image); - ret = new ExpressionLiteral(TypeInt.getInstance(), new Integer(i)); + ret = new ExpressionLiteral(TypeInt.getInstance(), i); } catch (NumberFormatException e) { // Need to catch this because some matches for regexp REG_INT // are not valid integers (e.g. too big). @@ -1591,8 +1705,8 @@ Expression ExpressionLiteral(boolean prop, boolean pathprop) : | { try { - double d = Double.parseDouble(getToken(0).image); - ret = new ExpressionLiteral(TypeDouble.getInstance(), new Double(d), getToken(0).image); + Double d = Double.valueOf(getToken(0).image); + ret = new ExpressionLiteral(TypeDouble.getInstance(), d, getToken(0).image); } catch (NumberFormatException e) { // Need to catch this because some matches for regexp REG_DOUBLE // may not be valid doubles. @@ -1600,9 +1714,9 @@ Expression ExpressionLiteral(boolean prop, boolean pathprop) : // NB: can't call generateParseException() here; it crashes }} | - { ret = new ExpressionLiteral(TypeBool.getInstance(), new Boolean(true)); } + { ret = new ExpressionLiteral(TypeBool.getInstance(), true); } | - { ret = new ExpressionLiteral(TypeBool.getInstance(), new Boolean(false)); } + { ret = new ExpressionLiteral(TypeBool.getInstance(), false); } ) { ret.setPosition(getToken(0)); return ret; } } @@ -1968,8 +2082,8 @@ Expression ExpressionStrategy(boolean prop, boolean pathprop) : { if (!prop) throw generateParseException(); } ( // <<...>> or [[...]] - (( begin = { ret = new ExpressionStrategy(true); } ExpressionStrategyCoalition(ret) ) - | (begin = { ret = new ExpressionStrategy(false); } ExpressionStrategyCoalition(ret) )) + (( begin = { ret = new ExpressionStrategy(true); } ExpressionStrategyCoalition(ret) ) + | (begin = { ret = new ExpressionStrategy(false); } ExpressionStrategyCoalition(ret) )) // Child expression ( ( expr = ExpressionProb(prop, pathprop) | expr = ExpressionReward(prop, pathprop) ) diff --git a/prism/src/parser/ast/AccumulationConstraint.java b/prism/src/parser/ast/AccumulationConstraint.java new file mode 100644 index 00000000..0b5864c5 --- /dev/null +++ b/prism/src/parser/ast/AccumulationConstraint.java @@ -0,0 +1,67 @@ +package parser.ast; + +import java.util.ArrayList; + +import parser.visitor.ASTVisitor; +import prism.PrismLangException; + +public class AccumulationConstraint extends ASTElement { + + private ArrayList factors; + private TemporalOperatorBound bound; + + public AccumulationConstraint(ArrayList factors, + TemporalOperatorBound bound) { + this.factors = factors; + this.bound = bound; + } + + public ArrayList getFactors() { + return factors; + } + + public void setFactors(ArrayList factors) { + this.factors = factors; + } + + public TemporalOperatorBound getBound() { + return bound; + } + + public void setBound(TemporalOperatorBound bound) { + this.bound = bound; + } + + public AccumulationConstraint deepCopy() { + ArrayList factorscopy = new ArrayList(); + TemporalOperatorBound boundcopy = bound.deepCopy(); + + for (AccumulationFactor factor : factors) { + factorscopy.add(factor.deepCopy()); + } + + return new AccumulationConstraint(factorscopy,boundcopy); + } + + public String toString() + { + boolean first = true; + String ret = ""; + + for (AccumulationFactor factor : factors) { + if (!first) ret += " + "; + first = false; + + ret += factor.toString(); + } + + ret += bound.toString(); + + return ret; + } + + @Override + public Object accept(ASTVisitor v) throws PrismLangException { + return v.visit(this); + } +} diff --git a/prism/src/parser/ast/AccumulationFactor.java b/prism/src/parser/ast/AccumulationFactor.java new file mode 100644 index 00000000..0e1a9b00 --- /dev/null +++ b/prism/src/parser/ast/AccumulationFactor.java @@ -0,0 +1,59 @@ +package parser.ast; + +import parser.visitor.ASTVisitor; +import prism.PrismLangException; +import parser.type.TypeInt; + +public class AccumulationFactor extends ASTElement { + + private Expression factor; + private AccumulationFunction func; + + public AccumulationFactor(AccumulationFunction func) + { + this(func, null); + } + + public AccumulationFactor(AccumulationFunction func, Expression factor) { + this.func = func; + if (factor != null) { + this.factor = factor; + } else { + this.factor = new ExpressionLiteral(TypeInt.getInstance(), 1); + } + } + + public Expression getFactor() { + return factor; + } + + public void setFactor(Expression factor) { + this.factor = factor; + } + + public AccumulationFunction getFunction() { + return func; + } + + public void setFunction(AccumulationFunction func) { + this.func = func; + } + + public AccumulationFactor deepCopy() { + return new AccumulationFactor(func,factor.deepCopy()); + } + + public String toString() + { + if (factor != null) { + return factor.toString() + " * " + func.toString(); + } else { + return func.toString(); + } + } + + @Override + public Object accept(ASTVisitor v) throws PrismLangException { + return v.visit(this); + } +} diff --git a/prism/src/parser/ast/AccumulationFunction.java b/prism/src/parser/ast/AccumulationFunction.java new file mode 100644 index 00000000..53b839a4 --- /dev/null +++ b/prism/src/parser/ast/AccumulationFunction.java @@ -0,0 +1,36 @@ +package parser.ast; + +public enum AccumulationFunction { + ACC_TIME, ACC_STEPS, ACC_REWARD; + + private Object rewardIndex = null; + + public Object getRewardIndex() { + return rewardIndex; + } + + public void setRewardIndex(Object index) { + rewardIndex = index; + } + + public String toString() { + switch(this) { + case ACC_REWARD: + return "reward" + indexString(); + case ACC_STEPS: + return "steps"; + case ACC_TIME: + return "time"; + default: + throw new RuntimeException("Unknown accumulation function"); + } + } + + private String indexString() { + if (rewardIndex == null) return ""; + + if (rewardIndex instanceof String) return "{\"" + rewardIndex + "\"}"; + else return "{" + rewardIndex.toString() + "}"; + + } +} diff --git a/prism/src/parser/ast/AccumulationSymbol.java b/prism/src/parser/ast/AccumulationSymbol.java new file mode 100644 index 00000000..d12e4e3b --- /dev/null +++ b/prism/src/parser/ast/AccumulationSymbol.java @@ -0,0 +1,38 @@ +package parser.ast; + +public enum AccumulationSymbol { + ACCDIAPLUS, ACCDIAMINUS, ACCBOXPLUS, ACCBOXMINUS; + + public String toString() + { + switch(this) { + case ACCBOXMINUS: + return "[-]"; + case ACCBOXPLUS: + return "[+]"; + case ACCDIAMINUS: + return "<->"; + case ACCDIAPLUS: + return "<+>"; + default: + throw new RuntimeException("Unknown accumulation symbol"); + } + } + + public boolean isDia() { + return (this == ACCDIAPLUS) || (this == ACCDIAMINUS); + } + + public boolean isBox() { + return (this == ACCBOXPLUS) || (this == ACCBOXMINUS); + } + + public boolean isMinus() { + return (this == ACCDIAMINUS) || (this == ACCBOXMINUS); + } + + public boolean isPlus() { + return (this == ACCDIAPLUS) || (this == ACCBOXPLUS); + } + +} diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java index 91eed94a..4e33b276 100644 --- a/prism/src/parser/ast/Expression.java +++ b/prism/src/parser/ast/Expression.java @@ -170,6 +170,14 @@ public abstract class Expression extends ASTElement return this instanceof ExpressionRegular; } + /** + * Determine whether the expression is an accumulation expression, i.e. a formula + * of the form ACC{DIA|BOX}{PLUS|MINUS}(...) + */ + public boolean isAccumulationExpression() throws PrismLangException { + return this instanceof ExpressionAccumulation; + } + /** * Convert a property expression (an LTL formula) into the classes used by * the jltl2ba (and jltl2dstar) libraries. @@ -951,7 +959,7 @@ public abstract class Expression extends ASTElement try { ASTTraverse astt = new ASTTraverse() { - public void visitPost(ExpressionFunc e) throws PrismLangException + public void visitPre(ExpressionFunc e) throws PrismLangException { if (e.getNameCode() == ExpressionFunc.MULTI) throw new PrismLangException("Found one", e); @@ -964,6 +972,40 @@ public abstract class Expression extends ASTElement return false; } + + /** + * Test if an expression contains an accumulation symbol + */ + public static boolean containsAccumulationExpression(Expression expr) + { + return (expr.getFirstAccumulationExpression() != null); + } + + /** + * Get the first Accumulation Subexpression + */ + + public ExpressionAccumulation getFirstAccumulationExpression() + { + try { + ASTTraverse astt = new ASTTraverse() + { + public Object visit(ExpressionProb probexp) + { + return null; + } + public Object visit(ExpressionAccumulation accexp) throws PrismLangException + { + throw new PrismLangException("Found accumulation!", accexp); + } + }; + this.accept(astt); + } catch (PrismLangException e) { + return (ExpressionAccumulation)e.getASTElement(); + } + return null; + } + /** * Test if an expression is an LTL formula and is in positive normal form, * i.e. where negation only occurs at the level of state formulae. diff --git a/prism/src/parser/ast/ExpressionAccumulation.java b/prism/src/parser/ast/ExpressionAccumulation.java new file mode 100644 index 00000000..d7a202da --- /dev/null +++ b/prism/src/parser/ast/ExpressionAccumulation.java @@ -0,0 +1,142 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford, formerly University of Birmingham) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package parser.ast; + +import parser.EvaluateContext; +import parser.type.TypePathBool; +import parser.visitor.ASTVisitor; +import prism.PrismLangException; + +public class ExpressionAccumulation extends Expression +{ + AccumulationSymbol symbol; + AccumulationConstraint constraint; + ExpressionRegular regexp; + TemporalOperatorBound bound; + + public ExpressionAccumulation(AccumulationSymbol symbol) { + this.symbol = symbol; + this.setType(TypePathBool.getInstance()); + } + + public boolean hasRegularExpression() { + return regexp != null; + } + + public boolean hasBoundExpression() { + return bound != null; + } + + public AccumulationSymbol getSymbol() { + return symbol; + } + public void setSymbol(AccumulationSymbol symbol) { + this.symbol = symbol; + } + public AccumulationConstraint getConstraint() { + return constraint; + } + public void setConstraint(AccumulationConstraint constraint) { + this.constraint = constraint; + } + public ExpressionRegular getRegularExpression() { + if ( hasRegularExpression() ) { return regexp; } + else throw new RuntimeException("getRegularExpression called without RegularExpression"); + } + public void setRegularExpression(ExpressionRegular regexp) { + this.bound = null; + this.regexp = regexp; + } + + public TemporalOperatorBound getBoundExpression() { + if ( hasBoundExpression() ) { return bound; } + else throw new RuntimeException("getBoundExpression called without BoundExpression"); + } + + public void setBoundExpression(TemporalOperatorBound bound) { + if ( bound.isDefaultBound() && bound.hasUpperBound() ) { + this.regexp= null; + this.bound = bound; + } else { + throw new RuntimeException("Bounds need to be upper and default."); + } + } + + // Add a toString + public String toString() { + String ret = ""; + ret += symbol.toString(); + if ( hasRegularExpression() ) { ret += "( Reg:" + regexp.toString() + ")"; } + else if ( hasBoundExpression() ) { ret += "(" + bound.toString() + ")"; } + else throw new RuntimeException("Cannot stringify AccumulationExpression without fragment bounds."); + ret += "(" + constraint.toString() + ")"; + return ret; + } + + @Override + public boolean isConstant() { + return false; + } + + @Override + public boolean isProposition() { + return false; + } + + @Override + public Object evaluate(EvaluateContext ec) throws PrismLangException { + return null; + } + + @Override + public boolean returnsSingleValue() { + return false; + } + + @Override + public Expression deepCopy() { + ExpressionAccumulation ret = new ExpressionAccumulation(this.getSymbol()); + + ret.setConstraint(this.getConstraint().deepCopy()); + if ( this.hasBoundExpression() ) { + ret.setBoundExpression(this.getBoundExpression().deepCopy()); + } + if ( this.hasRegularExpression() ) { + ret.setRegularExpression((ExpressionRegular) this.getRegularExpression().deepCopy()); + } + + return ret; + } + + @Override + public Object accept(ASTVisitor v) throws PrismLangException { + return v.visit(this); + } + +} + +//------------------------------------------------------------------------------ diff --git a/prism/src/parser/visitor/ASTTraverse.java b/prism/src/parser/visitor/ASTTraverse.java index 3272bcd7..194f65a2 100644 --- a/prism/src/parser/visitor/ASTTraverse.java +++ b/prism/src/parser/visitor/ASTTraverse.java @@ -405,6 +405,42 @@ public class ASTTraverse implements ASTVisitor } public void visitPost(ExpressionRegular e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- + public void visitPre(ExpressionAccumulation e) throws PrismLangException { defaultVisitPre(e); } + public Object visit(ExpressionAccumulation e) throws PrismLangException + { + visitPre(e); + // Descend into the path fragment expression + if (e.hasRegularExpression()) e.getRegularExpression().accept(this); + if (e.hasBoundExpression()) e.getBoundExpression().accept(this); + // Descend into the weight constraint + if (e.getConstraint() != null) e.getConstraint().accept(this); + visitPost(e); + return null; + } + public void visitPost(ExpressionAccumulation e) throws PrismLangException { defaultVisitPost(e); } + // ----------------------------------------------------------------------------------- + public void visitPre(AccumulationFactor e) throws PrismLangException { defaultVisitPre(e); } + public Object visit(AccumulationFactor e) throws PrismLangException + { + visitPre(e); + if (e.getFactor() != null) e.getFactor().accept(this); + visitPost(e); + return null; + } + public void visitPost(AccumulationFactor e) throws PrismLangException { defaultVisitPost(e); } + public void visitPre(AccumulationConstraint e) throws PrismLangException { defaultVisitPre(e); } + public Object visit(AccumulationConstraint e) throws PrismLangException + { + visitPre(e); + for (AccumulationFactor factor : e.getFactors()) { + factor.accept(this); + } + if (e.getBound() != null) e.getBound().accept(this); + visitPost(e); + return null; + } + public void visitPost(AccumulationConstraint e) throws PrismLangException { defaultVisitPost(e); } + // ----------------------------------------------------------------------------------- public void visitPre(ExpressionITE e) throws PrismLangException { defaultVisitPre(e); } public Object visit(ExpressionITE e) throws PrismLangException { diff --git a/prism/src/parser/visitor/ASTTraverseModify.java b/prism/src/parser/visitor/ASTTraverseModify.java index cbb08588..783824f9 100644 --- a/prism/src/parser/visitor/ASTTraverseModify.java +++ b/prism/src/parser/visitor/ASTTraverseModify.java @@ -416,6 +416,42 @@ public class ASTTraverseModify implements ASTVisitor } public void visitPost(ExpressionRegular e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- + public void visitPre(ExpressionAccumulation e) throws PrismLangException { defaultVisitPre(e); } + public Object visit(ExpressionAccumulation e) throws PrismLangException + { + visitPre(e); + // Descend into the path fragment expression + if (e.hasRegularExpression()) e.getRegularExpression().accept(this); + if (e.hasBoundExpression()) e.getBoundExpression().accept(this); + // Descend into the weight constraint + if (e.getConstraint() != null) e.getConstraint().accept(this); + visitPost(e); + return e; + } + public void visitPost(ExpressionAccumulation e) throws PrismLangException { defaultVisitPost(e); } + // ----------------------------------------------------------------------------------- + public void visitPre(AccumulationFactor e) throws PrismLangException { defaultVisitPre(e); } + public Object visit(AccumulationFactor e) throws PrismLangException + { + visitPre(e); + if (e.getFactor() != null) e.getFactor().accept(this); + visitPost(e); + return e; + } + public void visitPost(AccumulationFactor e) throws PrismLangException { defaultVisitPost(e); } + public void visitPre(AccumulationConstraint e) throws PrismLangException { defaultVisitPre(e); } + public Object visit(AccumulationConstraint e) throws PrismLangException + { + visitPre(e); + for (AccumulationFactor factor : e.getFactors()) { + factor.accept(this); + } + if (e.getBound() != null) e.getBound().accept(this); + visitPost(e); + return e; + } + public void visitPost(AccumulationConstraint e) throws PrismLangException { defaultVisitPost(e); } +// ----------------------------------------------------------------------------------- public void visitPre(ExpressionITE e) throws PrismLangException { defaultVisitPre(e); } public Object visit(ExpressionITE e) throws PrismLangException { diff --git a/prism/src/parser/visitor/ASTVisitor.java b/prism/src/parser/visitor/ASTVisitor.java index 6b373976..4d7e15fb 100644 --- a/prism/src/parser/visitor/ASTVisitor.java +++ b/prism/src/parser/visitor/ASTVisitor.java @@ -51,6 +51,8 @@ public interface ASTVisitor public Object visit(RenamedModule e) throws PrismLangException; public Object visit(RewardStruct e) throws PrismLangException; public Object visit(RewardStructItem e) throws PrismLangException; + public Object visit(AccumulationFactor e) throws PrismLangException; + public Object visit(AccumulationConstraint e) throws PrismLangException; public Object visit(QuotedString quotedString) throws PrismLangException; // ASTElement/SystemDefn classes public Object visit(SystemInterleaved e) throws PrismLangException; @@ -64,6 +66,7 @@ public interface ASTVisitor // ASTElement/Expression classes public Object visit(ExpressionTemporal e) throws PrismLangException; public Object visit(ExpressionRegular e) throws PrismLangException; + public Object visit(ExpressionAccumulation e) throws PrismLangException; public Object visit(ExpressionITE e) throws PrismLangException; public Object visit(ExpressionBinaryOp e) throws PrismLangException; public Object visit(ExpressionUnaryOp e) throws PrismLangException; diff --git a/prism/src/parser/visitor/ReplaceAccumulationExpression.java b/prism/src/parser/visitor/ReplaceAccumulationExpression.java new file mode 100644 index 00000000..d30c9512 --- /dev/null +++ b/prism/src/parser/visitor/ReplaceAccumulationExpression.java @@ -0,0 +1,67 @@ +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 ReplaceAccumulationExpression extends ASTTraverseModify { + + private ExpressionAccumulation accexp; + private String replacementLabel; + private int replacementPosition; + + + + public ReplaceAccumulationExpression(ExpressionAccumulation accexp, String replacementLabel) { + super(); + this.accexp = accexp; + this.replacementLabel = replacementLabel; + this.replacementPosition = 0; + } + + public ReplaceAccumulationExpression(ExpressionAccumulation accexp, String replacementLabel, int replacementPosition) + { + this(accexp, replacementLabel); + this.replacementPosition = replacementPosition; + } + + public Object visit(ExpressionAccumulation expr) throws PrismLangException + { + ExpressionLabel label = new ExpressionLabel(replacementLabel); + //System.out.println("Replacing "+expr.toString()+" with "+label.toString()); + if (expr == accexp) { + AccumulationSymbol sym = expr.getSymbol(); + + if (sym.isPlus()) { + // We are looking into a bright future, wrap it in F=position + ExpressionTemporal fLabel = new ExpressionTemporal(ExpressionTemporal.P_F, null, label); + TemporalOperatorBounds fBounds = new TemporalOperatorBounds(); + TemporalOperatorBound fBound = IntegerBound.fromEqualBounds(replacementPosition).toTemporalOperatorBound(); + fBounds.setDefaultBound(fBound); + fLabel.setBounds(fBounds); + // If its a BOX, negate it + if (sym.isBox()) { + return new ExpressionUnaryOp(ExpressionUnaryOp.NOT, fLabel); + } else { + return fLabel; + } + } else { + // This is a MINUS, just check for negation + if (sym.isBox()) { + return new ExpressionUnaryOp(ExpressionUnaryOp.NOT, label); + } else { + return label; + } + } + } else { + return expr; + } + } +} diff --git a/prism/src/prism/IntegerBound.java b/prism/src/prism/IntegerBound.java index c726d801..fb530cc7 100644 --- a/prism/src/prism/IntegerBound.java +++ b/prism/src/prism/IntegerBound.java @@ -29,8 +29,10 @@ package prism; import java.util.List; import parser.Values; +import parser.ast.ExpressionLiteral; import parser.ast.ExpressionTemporal; import parser.ast.TemporalOperatorBound; +import parser.type.TypeInt; /** * Canonical representation of an integer bound, with strict/non-strict lower and upper bound. @@ -63,6 +65,21 @@ public class IntegerBound } } + public static IntegerBound fromEqualBounds(int bound) { + return new IntegerBound(bound, false, bound, false); + } + + public TemporalOperatorBound toTemporalOperatorBound() { + TemporalOperatorBound bound = new TemporalOperatorBound(); + if ( lowest == highest ) { + bound.setEqualBounds(new ExpressionLiteral(TypeInt.getInstance(), lowest)); + } else { + bound.setLowerBound(new ExpressionLiteral(TypeInt.getInstance(), lowest)); + bound.setUpperBound(new ExpressionLiteral(TypeInt.getInstance(), highest)); + } + return bound; + } + /** * Extract the bounds from an {@code ExpressionTemporal} expression * and create the corresponding {@code IntegerBound}.