From 385884a590db7c6e77fb7557b5f2a6345a0d946f Mon Sep 17 00:00:00 2001 From: Sascha Wunderlich Date: Tue, 15 Nov 2016 14:54:45 +0100 Subject: [PATCH] accumulation: further refactoring of Product --- prism/src/explicit/AccumulationProduct.java | 19 ++++- .../explicit/AccumulationProductCounting.java | 70 +------------------ .../explicit/AccumulationProductRegular.java | 24 ++----- 3 files changed, 23 insertions(+), 90 deletions(-) diff --git a/prism/src/explicit/AccumulationProduct.java b/prism/src/explicit/AccumulationProduct.java index 46adf7c6..5842abd2 100644 --- a/prism/src/explicit/AccumulationProduct.java +++ b/prism/src/explicit/AccumulationProduct.java @@ -60,6 +60,7 @@ public abstract class AccumulationProduct extends Pro 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; @@ -106,8 +107,6 @@ public abstract class AccumulationProduct extends Pro protected 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 = accstate.getTracker(trackers); ArrayList> oldTracks = oldTracker.getTracks(); @@ -162,6 +161,22 @@ public abstract class AccumulationProduct extends Pro return new AccumulationState<>(newTrackerId, newLastRestartNr, numberOfTracks, newGoodTracks); } + protected int createInitialStateId(int numberOfRewards) { + Component initialComponent = getInitialComponent(); + + // 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, initialComponent); + int initialTrackerId = trackers.findOrAdd(initialTracker); + AccumulationState initialAccState = new AccumulationState(initialTrackerId, initialActiveTrack, numberOfTracks, initialGoodTracks); + int initialAccStateId = accStates.findOrAdd(initialAccState); + + return initialAccStateId; + } + @Override public String toDot() { StringBuffer result = new StringBuffer(); diff --git a/prism/src/explicit/AccumulationProductCounting.java b/prism/src/explicit/AccumulationProductCounting.java index 2afc149f..e9b4e91b 100644 --- a/prism/src/explicit/AccumulationProductCounting.java +++ b/prism/src/explicit/AccumulationProductCounting.java @@ -1,6 +1,5 @@ package explicit; -import java.util.ArrayList; import java.util.BitSet; import java.util.Vector; @@ -170,58 +169,6 @@ public class AccumulationProductCounting extends AccumulationPr protected Integer getInitialComponent() { return 0; } - - protected 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 = accstate.getTracker(trackers); - 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 = updateTrack(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); - } @Override protected AccumulationTrack updateTrack(Integer modelFromStateId, final AccumulationTrack track, @@ -246,23 +193,10 @@ public class AccumulationProductCounting extends AccumulationPr 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; - } - /** * Populates fields: - * - numberOfTracks + * - numberOfTracks with the highest relevant integer plus one, and + * - numberOfWeights with the size of the reward vector. * @param graph * @param accexp * @param rewards diff --git a/prism/src/explicit/AccumulationProductRegular.java b/prism/src/explicit/AccumulationProductRegular.java index 18913919..d4488d02 100644 --- a/prism/src/explicit/AccumulationProductRegular.java +++ b/prism/src/explicit/AccumulationProductRegular.java @@ -215,34 +215,18 @@ public class AccumulationProductRegular extends AccumulationPro 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; - } - /** * Populates fields: - * - automaton with a trimmed deterministic finite automaton and - * - numberOfTracks with the length of its longest path. + * - automaton with a trimmed deterministic finite automaton, + * - numberOfTracks with the length of its longest path plus one, and + * - numberOfWeights with the size of the reward vector. * * @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 { + protected void createAuxData(final Model graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc) throws PrismException { // Build labels and DFA AccumulationModelChecker accMc = new AccumulationModelChecker(); ExpressionRegular reg = (ExpressionRegular)accMc.checkMaximalStateFormulas(mc, graph, accexp.getRegularExpression(), labels);