From 6740da5171faeb55753d09bdf490b466dc616bb0 Mon Sep 17 00:00:00 2001 From: Sascha Wunderlich Date: Mon, 14 Nov 2016 14:14:49 +0100 Subject: [PATCH] accumulation: some fixes - length of longest path vs number of tracks - typed accumulation states --- prism/src/explicit/AccumulationProduct.java | 8 +-- .../explicit/AccumulationProductCounting.java | 36 +++++++----- .../explicit/AccumulationProductRegular.java | 56 ++++++++++++------- prism/src/explicit/AccumulationState.java | 23 +++----- prism/src/explicit/AccumulationTrack.java | 1 - .../explicit/AccumulationTransformation.java | 4 +- 6 files changed, 70 insertions(+), 58 deletions(-) diff --git a/prism/src/explicit/AccumulationProduct.java b/prism/src/explicit/AccumulationProduct.java index 6797291e..74a83960 100644 --- a/prism/src/explicit/AccumulationProduct.java +++ b/prism/src/explicit/AccumulationProduct.java @@ -22,7 +22,7 @@ import prism.PrismLog; public abstract class AccumulationProduct extends ProductWithProductStates { final StoragePool> trackers; - final StoragePool accStates; + final StoragePool> accStates; final BitSet goodStates; @@ -73,8 +73,8 @@ public abstract class AccumulationProduct extends Pro 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()); + AccumulationState accState = accStates.getById(fromState.getSecondState()); + AccumulationTracker tracker = accState.getTracker(trackers); result.append("" + i + "[shape=box, color=black" @@ -82,7 +82,7 @@ public abstract class AccumulationProduct extends Pro + "" + "" + i + "=" + fromState + "" + "" - + "" + accState + "" + + "" + accState + "" + "" + "\"" + quoteForDot(tracker.toString()) + "\"" + "" diff --git a/prism/src/explicit/AccumulationProductCounting.java b/prism/src/explicit/AccumulationProductCounting.java index 1f613bfe..8cd63924 100644 --- a/prism/src/explicit/AccumulationProductCounting.java +++ b/prism/src/explicit/AccumulationProductCounting.java @@ -48,7 +48,7 @@ public class AccumulationProductCounting extends AccumulationPr 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()); + AccumulationState from_accstate = result.accStates.getById(from_state.getSecondState()); // Get step weights double[] weights = new double[rewards.size()]; @@ -58,7 +58,7 @@ public class AccumulationProductCounting extends AccumulationPr } // Update accumulation product state, store it and get its ID. - AccumulationState to_accproduct = result.updateAccumulationState(from_state.getFirstState(), from_accstate, accexp, weights, mc); + 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); @@ -67,7 +67,7 @@ public class AccumulationProductCounting extends AccumulationPr @Override public void notify(ProductState state, Integer index) throws PrismException { - AccumulationState accState = result.accStates.getById(state.getSecondState()); + AccumulationState accState = result.accStates.getById(state.getSecondState()); if (result.isGoodAccState(accState, accexp, mc)) { result.goodStates.set(index); } @@ -112,7 +112,7 @@ public class AccumulationProductCounting extends AccumulationPr 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()); + AccumulationState from_accstate = result.accStates.getById(from_state.getSecondState()); // Get step weights // THIS IS DIFFERENT FROM ABOVE! @@ -125,7 +125,7 @@ public class AccumulationProductCounting extends AccumulationPr } // Update accumulation product state, store it and get its ID. - AccumulationState to_accproduct = result.updateAccumulationState(from_state.getFirstState(), from_accstate, accexp, weights, mc); + 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); } @@ -133,7 +133,7 @@ public class AccumulationProductCounting extends AccumulationPr @Override public void notify(final ProductState state, final Integer index) throws PrismException { - AccumulationState accState = result.accStates.getById(state.getSecondState()); + AccumulationState accState = result.accStates.getById(state.getSecondState()); if (result.isGoodAccState(accState, accexp, mc)) { result.goodStates.set(index); } @@ -166,7 +166,7 @@ public class AccumulationProductCounting extends AccumulationPr return isFinal; } - private boolean isGoodAccState(final AccumulationState state, final ExpressionAccumulation accexp, final ProbModelChecker mc) + private boolean isGoodAccState(final AccumulationState state, final ExpressionAccumulation accexp, final ProbModelChecker mc) throws PrismException { return state.hasGoodTrack(); } @@ -210,13 +210,13 @@ public class AccumulationProductCounting extends AccumulationPr return isGood; } - private AccumulationState updateAccumulationState(final int modelFromStateId, - final AccumulationState accstate, final ExpressionAccumulation accexp, + 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()); + AccumulationTracker oldTracker = accstate.getTracker(trackers); ArrayList> oldTracks = oldTracker.getTracks(); BitSet oldGoodTracks = accstate.getGoodTracks(); @@ -259,7 +259,7 @@ public class AccumulationProductCounting extends AccumulationPr int newTrackerId = trackers.findOrAdd(newTracker); - return new AccumulationState(newTrackerId, newLastRestartNr, numberOfTracks, newGoodTracks); + return new AccumulationState<>(newTrackerId, newLastRestartNr, numberOfTracks, newGoodTracks); } private AccumulationTrack updateTrackBounds(final AccumulationTrack track, @@ -287,14 +287,22 @@ public class AccumulationProductCounting extends AccumulationPr // 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); + 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 { + /** + * Populates fields: + * - numberOfTracks + * @param graph + * @param accexp + * @param rewards + * @param mc + * @throws PrismException + */ + protected void createAuxData(final Model graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc) throws PrismException { numberOfTracks = IntegerBound.fromTemporalOperatorBound(accexp.getBoundExpression(), mc.getConstantValues(), true).getHighestInteger()+1; numberOfWeights = rewards.size(); } diff --git a/prism/src/explicit/AccumulationProductRegular.java b/prism/src/explicit/AccumulationProductRegular.java index 7d7d9602..ecd0b855 100644 --- a/prism/src/explicit/AccumulationProductRegular.java +++ b/prism/src/explicit/AccumulationProductRegular.java @@ -10,6 +10,7 @@ import automata.finite.NondeterministicFiniteAutomaton; import automata.finite.State; import explicit.rewards.MCRewards; import explicit.rewards.MDPRewards; +import explicit.rewards.Rewards; import parser.ast.AccumulationFactor; import parser.ast.ExpressionAccumulation; import parser.ast.ExpressionRegular; @@ -37,7 +38,7 @@ public class AccumulationProductRegular extends AccumulationPro 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); + result.createAuxData(graph, accexp, rewards, mc); // Build an operator class AccumulationDTMCProductOperator implements DTMCProductOperator @@ -53,7 +54,7 @@ public class AccumulationProductRegular extends AccumulationPro 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()); + AccumulationState from_accstate = result.accStates.getById(from_state.getSecondState()); // Get step weights double[] weights = new double[rewards.size()]; @@ -63,7 +64,7 @@ public class AccumulationProductRegular extends AccumulationPro } // Update accumulation product state, store it and get its ID. - AccumulationState to_accproduct = result.updateAccumulationState(from_state.getFirstState(), from_accstate, accexp, weights, mc); + 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); @@ -72,7 +73,7 @@ public class AccumulationProductRegular extends AccumulationPro @Override public void notify(ProductState state, Integer index) throws PrismException { - AccumulationState accState = result.accStates.getById(state.getSecondState()); + AccumulationState accState = result.accStates.getById(state.getSecondState()); if (result.isGoodAccState(accState, accexp, mc)) { result.goodStates.set(index); } @@ -101,7 +102,7 @@ public class AccumulationProductRegular extends AccumulationPro final AccumulationProductRegular result = new AccumulationProductRegular(graph); // Create auxiliary data - result.createAuxData(graph, accexp, mc); + result.createAuxData(graph, accexp, rewards, mc); class AccumulationMDPProductOperator implements MDPProductOperator { @@ -117,7 +118,7 @@ public class AccumulationProductRegular extends AccumulationPro 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()); + AccumulationState from_accstate = result.accStates.getById(from_state.getSecondState()); // Get step weights // THIS IS DIFFERENT FROM ABOVE! @@ -130,7 +131,7 @@ public class AccumulationProductRegular extends AccumulationPro } // Update accumulation product state, store it and get its ID. - AccumulationState to_accproduct = result.updateAccumulationState(from_state.getFirstState(), from_accstate, accexp, weights, mc); + 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); @@ -139,7 +140,7 @@ public class AccumulationProductRegular extends AccumulationPro @Override public void notify(ProductState state, Integer index) throws PrismException { - AccumulationState accState = result.accStates.getById(state.getSecondState()); + AccumulationState accState = result.accStates.getById(state.getSecondState()); if (result.isGoodAccState(accState, accexp, mc)) { result.goodStates.set(index); } @@ -171,14 +172,14 @@ public class AccumulationProductRegular extends AccumulationPro return isFinal; } - private boolean isGoodAccState(AccumulationState state, ExpressionAccumulation accexp, ProbModelChecker mc) throws PrismException { - //TODO: fill me! - return false; + private boolean isGoodAccState(AccumulationState state, ExpressionAccumulation accexp, ProbModelChecker mc) throws PrismException { + return state.hasGoodTrack(); } private boolean isGoodTrack(AccumulationTrack track, ExpressionAccumulation accexp, ProbModelChecker mc) throws PrismException { - //System.out.println("Checking " + track + " for goodness..."); + mc.getLog().println("Checking " + track + " for goodness..."); // Only final tracks can be good + mc.getLog().println("Final? " + isFinalTrack(track,accexp,mc)); if (!isFinalTrack(track,accexp,mc)) { return false; } boolean isGood = false; @@ -214,13 +215,13 @@ public class AccumulationProductRegular extends AccumulationPro throw new RuntimeException("Oh boy!"); } - //System.out.println("Good? " + isGood); + mc.getLog().println("Good? " + lhs + rhs + " : " + isGood); return isGood; } - private AccumulationState updateAccumulationState(final int modelFromStateId, - final AccumulationState accstate, final ExpressionAccumulation accexp, + 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. @@ -268,7 +269,7 @@ public class AccumulationProductRegular extends AccumulationPro int newTrackerId = trackers.findOrAdd(newTracker); - return new AccumulationState(newTrackerId, newLastRestartNr, numberOfTracks, newGoodTracks); + return new AccumulationState(newTrackerId, newLastRestartNr, numberOfTracks, newGoodTracks); } private AccumulationTrack updateTrackRegular(Integer modelFromStateId, AccumulationTrack track, ExpressionAccumulation accexp, double[] weights, StateModelChecker mc) { State currentState = track.getComponent(); @@ -313,15 +314,25 @@ public class AccumulationProductRegular extends AccumulationPro BitSet initialGoodTracks = new BitSet(); // Generate the initial track and product state - AccumulationTracker initialTracker = new AccumulationTracker<>(numberOfTracks, numberOfRewards, initialState); + AccumulationTracker initialTracker = new AccumulationTracker(numberOfTracks, numberOfRewards, initialState); int initialTrackerId = trackers.findOrAdd(initialTracker); - AccumulationState initialAccState = new AccumulationState(initialTrackerId, initialActiveTrack, numberOfTracks, initialGoodTracks); + 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 { + /** + * Populates fields: + * - automaton with a trimmed deterministic finite automaton and + * - numberOfTracks with the length of its longest path. + * + * @param graph + * @param accexp + * @param mc + * @throws PrismException + */ + public void createAuxData(final Model graph, final ExpressionAccumulation accexp, final Vector rewards, 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(); @@ -334,12 +345,15 @@ public class AccumulationProductRegular extends AccumulationPro automaton = nfa.determinize(); automaton.trim(); // This should remove cycles. - System.out.println(nfa.toDot()); + nfa.exportToDotFile("DEBUG-automaton-nfa.dot"); if (!automaton.isAcyclic()) { throw new PrismException("Cannot handle cyclic automata!"); } - numberOfTracks = automaton.getLongestPathLength(); + numberOfTracks = automaton.getLongestPathLength()+1; + mc.getLog().println(" [AP] tracks: " + numberOfTracks); + numberOfWeights= rewards.size(); + mc.getLog().println(" [AP] weights: " + numberOfWeights); } } diff --git a/prism/src/explicit/AccumulationState.java b/prism/src/explicit/AccumulationState.java index 78c22ee9..108b47a1 100644 --- a/prism/src/explicit/AccumulationState.java +++ b/prism/src/explicit/AccumulationState.java @@ -10,7 +10,7 @@ import java.util.BitSet; * @author Sascha Wunderlich * */ -public class AccumulationState { +public class AccumulationState { final int trackerId; final BitSet goodTracks; @@ -30,23 +30,15 @@ public class AccumulationState { public int getTrackerId() { return trackerId; } - - public int getLastRestartNr() { - return lastRestartNr; - } - - public void setLastRestartNr(int lastRestartNr) { - this.lastRestartNr = lastRestartNr; + + public AccumulationTracker getTracker(StoragePool> trackers) { + return trackers.getById(trackerId); } public BitSet getGoodTracks() { return goodTracks; } - public boolean isGoodTrack(int trackNr) { - return goodTracks.get(trackNr); - } - public boolean hasGoodTrack() { return !goodTracks.isEmpty(); } @@ -55,16 +47,13 @@ public class AccumulationState { 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 + numberOfTracks; result = prime * result + trackerId; return result; } @@ -85,6 +74,8 @@ public class AccumulationState { return false; if (lastRestartNr != other.lastRestartNr) return false; + if (numberOfTracks != other.numberOfTracks) + return false; if (trackerId != other.trackerId) return false; return true; diff --git a/prism/src/explicit/AccumulationTrack.java b/prism/src/explicit/AccumulationTrack.java index 3f9a1419..b2ec8283 100644 --- a/prism/src/explicit/AccumulationTrack.java +++ b/prism/src/explicit/AccumulationTrack.java @@ -23,7 +23,6 @@ public class AccumulationTrack { } public AccumulationTrack(double[] weights, Component component) { - super(); this.weights = weights; this.component = component; } diff --git a/prism/src/explicit/AccumulationTransformation.java b/prism/src/explicit/AccumulationTransformation.java index c7d1c7ec..21d94604 100644 --- a/prism/src/explicit/AccumulationTransformation.java +++ b/prism/src/explicit/AccumulationTransformation.java @@ -131,12 +131,12 @@ public class AccumulationTransformation implements ModelExpress //System.out.println("Good states " + goodStates); // Transform the expression - ReplaceAccumulationExpression replace = new ReplaceAccumulationExpression(accexp, label, product.getNumberOfTracks()); + ReplaceAccumulationExpression replace = new ReplaceAccumulationExpression(accexp, label, product.getNumberOfTracks()-1); transformedExpression = (Expression)transformedExpression.accept(replace); mc.getLog().println("Transformed " + originalExpression.toString() + "\n into " + transformedExpression.toString()); //DEBUG: output dotfile - product.exportToDotFile("./out.dot"); + product.exportToDotFile("DEBUG-product.dot"); } public String gensymLabel(String prefix, Model model) {