From 9900e78cbfe0c8f7d50e830caa82085caee7768e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffen=20M=C3=A4rcker?= Date: Tue, 6 Mar 2018 15:34:02 +0100 Subject: [PATCH 1/3] Implement reduceTransitions for DTMCs to allow efficient accumulation over transitions --- prism/src/explicit/DTMC.java | 148 ++++++++++++++++++--- prism/src/explicit/DTMCEmbeddedSimple.java | 60 +++++++++ prism/src/explicit/DTMCModelChecker.java | 6 +- prism/src/explicit/DTMCSparse.java | 40 ++++++ 4 files changed, 231 insertions(+), 23 deletions(-) diff --git a/prism/src/explicit/DTMC.java b/prism/src/explicit/DTMC.java index b936a9f842..516fb04f79 100644 --- a/prism/src/explicit/DTMC.java +++ b/prism/src/explicit/DTMC.java @@ -91,6 +91,130 @@ public default void forEachTransition(int s, TransitionConsumer c) } } + /** + * Quaternary function that maps an Object of type {@code T}, + * and a transition from state {@code s} to state {@code t} + * with probabiliy/rate {@code d} + * to an Object of type {@code T}. + * + * @param type of first argument and result + */ + @FunctionalInterface + public static interface ObjTransitionFunction + { + T apply(T result, int s, int t, double d); + } + + /** + * Iterate over the outgoing transitions of state {@code state} + * and apply the reducing function {@code fn} + * to the intermediate result and the transition: + *
+ * Call {@code apply(r,s,t,d)} where + * {@code r} is the intermediate result, + * {@code t} is the successor state and, + * in a DTMC, {@code d} = P(s,t) is the probability from {@code s} to {@code t}, + * while in CTMC, {@code d} = R(s,t) is the rate from {@code s} to {@code t}. + * The return value of apply is the intermediate result for the next transition. + *

+ * Default implementation: The default implementation relies on iterating over the + * iterator returned by {@code getTransitionsIterator()}. + *

Note: This method is the base for the default implementation of the numerical + * computation methods (mvMult, etc). In derived classes, it may thus be worthwhile to + * provide a specialised implementation for this method that avoids using the Iterator mechanism. + * + * @param state the state + * @param init initial result value + * @param fn the reducing function + */ + public default T reduceTransitions(int state, T init, ObjTransitionFunction fn) + { + T result = init; + for (Iterator> it = getTransitionsIterator(state); it.hasNext(); ) { + Entry e = it.next(); + result = fn.apply(result, state, e.getKey(), e.getValue()); + } + return result; + } + + /** + * Primitive specialisation of {@code ObjTransitionFunction} for {@code double} results. + * + * @see ObjTransitionFunction + */ + @FunctionalInterface + public static interface DoubleTransitionFunction + { + double apply(double result, int s, int t, double d); + } + + /** + * Primitive specialisation of {@code reduce} for {@code double} values. + * + * @see #reduceTransitions(int, Object, ObjTransitionFunction) + */ + public default double reduceTransitions(int state, double init, DoubleTransitionFunction fn) + { + double result = init; + for (Iterator> it = getTransitionsIterator(state); it.hasNext(); ) { + Entry e = it.next(); + result = fn.apply(result, state, e.getKey(), e.getValue()); + } + return result; + } + + /** + * Primitive specialisation of {@code ObjTransitionFunction} for {@code int} values. + * + * @see ObjTransitionFunction + */ + @FunctionalInterface + public interface IntTransitionFunction + { + int apply(int result, int s, int t, double d); + } + + /** + * Primitive specialisation of {@code reduce} for {@code int} values. + * + * @see #reduceTransitions(int, Object, ObjTransitionFunction) + */ + public default int reduceTransitions(int state, int init, IntTransitionFunction fn) + { + int result = init; + for (Iterator> it = getTransitionsIterator(state); it.hasNext(); ) { + Entry e = it.next(); + result = fn.apply(result, state, e.getKey(), e.getValue()); + } + return result; + } + + /** + * Primitive specialisation of {@code ObjTransitionFunction} for {@code long} values. + * + * @see ObjTransitionFunction + */ + @FunctionalInterface + public interface LongTransitionFunction + { + long apply(long result, int s, int t, double d); + } + + /** + * Primitive specialisation of {@code reduce} for {@code long} values. + * + * @see #reduceTransitions(int, Object, ObjTransitionFunction) + */ + public default long reduceTransitions(int state, long init, LongTransitionFunction fn) + { + long result = init; + for (Iterator> it = getTransitionsIterator(state); it.hasNext(); ) { + Entry e = it.next(); + result = fn.apply(result, state, e.getKey(), e.getValue()); + } + return result; + } + /** * Functional interface for a function * mapping transitions (s,t,d), i.e., @@ -103,29 +227,17 @@ public interface TransitionToDoubleFunction { } /** - * Iterate over the outgoing transitions of state {@code s}, call the function {@code f} + * Iterate over the outgoing transitions of state {@code state}, call the function {@code f} * and return the sum of the result values: *
- * Return sum_t f(s, t, P(s,t)), where t ranges over the successors of s. + * Return sum_t f(state, t, P(s,t)), where t ranges over the successors of state. * - * @param s the state s - * @param c the consumer + * @param state the state + * @param f the function */ - public default double sumOverTransitions(final int s, final TransitionToDoubleFunction f) + public default double sumOverTransitions(int state, TransitionToDoubleFunction f) { - class Sum { - double sum = 0.0; - - void accept(int s, int t, double d) - { - sum += f.apply(s, t, d); - } - } - - Sum sum = new Sum(); - forEachTransition(s, sum::accept); - - return sum.sum; + return reduceTransitions(state, 0.0, (r, s, t, d) -> r + f.apply(s, t, d)); } /** diff --git a/prism/src/explicit/DTMCEmbeddedSimple.java b/prism/src/explicit/DTMCEmbeddedSimple.java index 717d6e9234..2e0543b1c0 100644 --- a/prism/src/explicit/DTMCEmbeddedSimple.java +++ b/prism/src/explicit/DTMCEmbeddedSimple.java @@ -270,6 +270,66 @@ public void forEachTransition(int s, TransitionConsumer c) } } + @Override + public T reduceTransitions(int state, T init, ObjTransitionFunction fn) + { + double er = exitRates[state]; + T result = init; + if (er == 0) { + // exit rate = 0 -> prob 1 self loop + fn.apply(result, state, state, 1.0); + } else { + ctmc.reduceTransitions(state, result, (r, s, t, rate) -> + fn.apply(r, s, t, rate / er)); + } + return result; + } + + @Override + public double reduceTransitions(int state, double init, DoubleTransitionFunction fn) + { + double er = exitRates[state]; + double result = init; + if (er == 0) { + // exit rate = 0 -> prob 1 self loop + fn.apply(result, state, state, 1.0); + } else { + ctmc.reduceTransitions(state, result, (r, s, t, rate) -> + fn.apply(r, s, t, rate / er)); + } + return result; + } + + @Override + public int reduceTransitions(int state, int init, IntTransitionFunction fn) + { + double er = exitRates[state]; + int result = init; + if (er == 0) { + // exit rate = 0 -> prob 1 self loop + fn.apply(result, state, state, 1.0); + } else { + ctmc.reduceTransitions(state, result, (int r, int s, int t, double rate) -> + fn.apply(r, s, t, rate / er)); + } + return result; + } + + @Override + public long reduceTransitions(int state, long init, LongTransitionFunction fn) + { + double er = exitRates[state]; + long result = init; + if (er == 0) { + // exit rate = 0 -> prob 1 self loop + fn.apply(result, state, state, 1.0); + } else { + ctmc.reduceTransitions(state, result, (long r, int s, int t, double rate) -> + fn.apply(r, s, t, rate / er)); + } + return result; + } + public double mvMultSingle(int s, double vect[]) { int k; diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index ef20196365..b97f3a802b 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -2491,11 +2491,7 @@ public ModelCheckerResult computeSteadyStateProbsForBSCC(DTMC dtmc, BitSet state // Note: diagsQ[state] = 0.0, as it was freshly created // Compute negative exit rate (ignoring a possible self-loop) - dtmc.forEachTransition(state, (s, t, prob) -> { - if (s != t) { - diagsQ[state] -= prob; - } - }); + diagsQ[state] -= dtmc.reduceTransitions(state, 0.0, (r, s, t, p) -> (s == t) ? r : r + p); // Note: If there are no outgoing transitions, diagsQ[state] = 0, which is fine diff --git a/prism/src/explicit/DTMCSparse.java b/prism/src/explicit/DTMCSparse.java index a0f33456e3..a70cef6389 100644 --- a/prism/src/explicit/DTMCSparse.java +++ b/prism/src/explicit/DTMCSparse.java @@ -235,6 +235,46 @@ public void forEachTransition(int state, TransitionConsumer consumer) } } + @Override + public T reduceTransitions(int state, T init, ObjTransitionFunction fn) + { + T result = init; + for (int col = rows[state], stop = rows[state+1]; col < stop; col++){ + result = fn.apply(result, state, columns[col], probabilities[col]); + } + return result; + } + + @Override + public double reduceTransitions(int state, double init, DoubleTransitionFunction fn) + { + double result = init; + for (int col = rows[state], stop = rows[state+1]; col < stop; col++){ + result = fn.apply(result, state, columns[col], probabilities[col]); + } + return result; + } + + @Override + public int reduceTransitions(int state, int init, IntTransitionFunction fn) + { + int result = init; + for (int col = rows[state], stop = rows[state+1]; col < stop; col++){ + result = fn.apply(result, state, columns[col], probabilities[col]); + } + return result; + } + + @Override + public long reduceTransitions(int state, long init, LongTransitionFunction fn) + { + long result = init; + for (int col = rows[state], stop = rows[state+1]; col < stop; col++){ + result = fn.apply(result, state, columns[col], probabilities[col]); + } + return result; + } + @Override public int getNumTransitions(int state) { From f1eeeda27709056008b64a7bc88fcd739e4a6270 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffen=20M=C3=A4rcker?= Date: Wed, 8 May 2019 11:36:08 +0200 Subject: [PATCH 2/3] Implement reduceTransitions for MDPs to allow efficient accumulation over transitions --- .../explicit/DTMCFromMDPAndMDStrategy.java | 38 +++++- prism/src/explicit/MDP.java | 112 ++++++++++++++---- prism/src/explicit/MDPSparse.java | 52 ++++++++ 3 files changed, 175 insertions(+), 27 deletions(-) diff --git a/prism/src/explicit/DTMCFromMDPAndMDStrategy.java b/prism/src/explicit/DTMCFromMDPAndMDStrategy.java index fe9ca18ec8..9d1e002d21 100644 --- a/prism/src/explicit/DTMCFromMDPAndMDStrategy.java +++ b/prism/src/explicit/DTMCFromMDPAndMDStrategy.java @@ -187,9 +187,45 @@ public void forEachTransition(int s, TransitionConsumer c) if (!strat.isChoiceDefined(s)) { return; } - mdp.forEachTransition(s, strat.getChoiceIndex(s), c::accept); + mdp.forEachTransition(s, strat.getChoiceIndex(s), c); } + @Override + public T reduceTransitions(int state, T init, ObjTransitionFunction fn) + { + if (!strat.isChoiceDefined(state)) { + return init; + } + return mdp.reduceTransitions(state, strat.getChoiceIndex(state), init, fn); + } + + @Override + public double reduceTransitions(int state, double init, DoubleTransitionFunction fn) + { + if (!strat.isChoiceDefined(state)) { + return init; + } + return mdp.reduceTransitions(state, strat.getChoiceIndex(state), init, fn); + } + + @Override + public int reduceTransitions(int state, int init, IntTransitionFunction fn) + { + if (!strat.isChoiceDefined(state)) { + return init; + } + return mdp.reduceTransitions(state, strat.getChoiceIndex(state), init, fn); + } + + @Override + public long reduceTransitions(int state, long init, LongTransitionFunction fn) + { + if (!strat.isChoiceDefined(state)) { + return init; + } + return mdp.reduceTransitions(state, strat.getChoiceIndex(state), init, fn); +} + @Override public double mvMultSingle(int s, double vect[]) { diff --git a/prism/src/explicit/MDP.java b/prism/src/explicit/MDP.java index 613d0a2040..1b3791578a 100644 --- a/prism/src/explicit/MDP.java +++ b/prism/src/explicit/MDP.java @@ -35,6 +35,11 @@ import java.util.PrimitiveIterator.OfInt; import common.IterableStateSet; +import explicit.DTMC.DoubleTransitionFunction; +import explicit.DTMC.IntTransitionFunction; +import explicit.DTMC.LongTransitionFunction; +import explicit.DTMC.ObjTransitionFunction; +import explicit.DTMC.TransitionConsumer; import explicit.rewards.MCRewards; import explicit.rewards.MDPRewards; import prism.PrismUtils; @@ -53,16 +58,6 @@ public interface MDP extends MDPGeneric */ public Iterator> getTransitionsIterator(int s, int i); - /** - * Functional interface for a consumer, - * accepting transitions (s,t,d), i.e., - * from state s to state t with value d. - */ - @FunctionalInterface - public interface TransitionConsumer { - void accept(int s, int t, double d); - } - /** * Iterate over the outgoing transitions of state {@code s} and choice {@code i} * and call the accept method of the consumer for each of them: @@ -88,6 +83,83 @@ public default void forEachTransition(int s, int i, TransitionConsumer c) } } + /** + * Iterate over the outgoing transitions of state {@code state} and choice {@code c} + * and apply the reducing function {@code fn} + * to the intermediate result and the transition: + *
+ * Call {@code apply(r,s,t,d)} where + * {@code r} is the intermediate result, + * {@code t} is the successor state and, + * {@code d} = P(s,c,t) is the probability from {@code s} to {@code t} with choice {@code c}, + * The return value of apply is the intermediate result for the next transition. + *

+ * Default implementation: The default implementation relies on iterating over the + * iterator returned by {@code getTransitionsIterator()}. + *

Note: This method is the base for the default implementation of the numerical + * computation methods (mvMult, etc). In derived classes, it may thus be worthwhile to + * provide a specialised implementation for this method that avoids using the Iterator mechanism. + * + * @param state the state + * @param choice the choice + * @param init initial result value + * @param fn the reducing function + */ + public default T reduceTransitions(int state, int choice, T init, ObjTransitionFunction fn) + { + T result = init; + for (Iterator> it = getTransitionsIterator(state, choice); it.hasNext(); ) { + Entry e = it.next(); + result = fn.apply(result, state, e.getKey(), e.getValue()); + } + return result; + } + + /** + * Primitive specialisation of {@code reduce} for {@code double} values. + * + * @see #reduceTransitions(int, Object, ObjTransitionFunction) + */ + public default double reduceTransitions(int state, int choice, double init, DoubleTransitionFunction fn) + { + double result = init; + for (Iterator> it = getTransitionsIterator(state, choice); it.hasNext(); ) { + Entry e = it.next(); + result = fn.apply(result, state, e.getKey(), e.getValue()); + } + return result; + } + + /** + * Primitive specialisation of {@code reduce} for {@code int} values. + * + * @see #reduceTransitions(int, Object, ObjTransitionFunction) + */ + public default int reduceTransitions(int state, int choice, int init, IntTransitionFunction fn) + { + int result = init; + for (Iterator> it = getTransitionsIterator(state, choice); it.hasNext(); ) { + Entry e = it.next(); + result = fn.apply(result, state, e.getKey(), e.getValue()); + } + return result; + } + + /** + * Primitive specialisation of {@code reduce} for {@code long} values. + * + * @see #reduceTransitions(int, Object, ObjTransitionFunction) + */ + public default long reduceTransitions(int state, int choice, long init, LongTransitionFunction fn) + { + long result = init; + for (Iterator> it = getTransitionsIterator(state, choice); it.hasNext(); ) { + Entry e = it.next(); + result = fn.apply(result, state, e.getKey(), e.getValue()); + } + return result; + } + /** * Functional interface for a function * mapping transitions (s,t,d), i.e., @@ -105,24 +177,12 @@ public interface TransitionToDoubleFunction { *
* Return sum_t f(s, t, P(s,i,t)), where t ranges over the i-successors of s. * - * @param s the state s - * @param c the consumer + * @param state the state s + * @param choice the consumer */ - public default double sumOverTransitions(final int s, final int i, final TransitionToDoubleFunction f) + public default double sumOverTransitions(int state, int choice, TransitionToDoubleFunction f) { - class Sum { - double sum = 0.0; - - void accept(int s, int t, double d) - { - sum += f.apply(s, t, d); - } - } - - Sum sum = new Sum(); - forEachTransition(s, i, sum::accept); - - return sum.sum; + return reduceTransitions(state, choice, 0.0, (r, s, t, d) -> r + f.apply(s, t, d)); } /** diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java index 4180d0dfc8..e6b2aba5a7 100644 --- a/prism/src/explicit/MDPSparse.java +++ b/prism/src/explicit/MDPSparse.java @@ -41,6 +41,10 @@ import java.util.TreeMap; import common.IterableStateSet; +import explicit.DTMC.DoubleTransitionFunction; +import explicit.DTMC.IntTransitionFunction; +import explicit.DTMC.LongTransitionFunction; +import explicit.DTMC.ObjTransitionFunction; import explicit.rewards.MCRewards; import explicit.rewards.MDPRewards; import parser.State; @@ -574,6 +578,54 @@ public SuccessorsIterator getSuccessors(final int s, final int i) // Accessors (for MDP) + @Override + public T reduceTransitions(int state, int choice, T init, ObjTransitionFunction fn) + { + T result = init; + int start = choiceStarts[rowStarts[state] + choice]; + int stop = choiceStarts[rowStarts[state] + choice + 1]; + for (int col = start; col < stop; col++) { + result = fn.apply(result, state, cols[col], nonZeros[col]); + } + return result; + } + + @Override + public double reduceTransitions(int state, int choice, double init, DoubleTransitionFunction fn) + { + double result = init; + int start = choiceStarts[rowStarts[state] + choice]; + int stop = choiceStarts[rowStarts[state] + choice + 1]; + for (int col = start; col < stop; col++) { + result = fn.apply(result, state, cols[col], nonZeros[col]); + } + return result; + } + + @Override + public int reduceTransitions(int state, int choice, int init, IntTransitionFunction fn) + { + int result = init; + int start = choiceStarts[rowStarts[state] + choice]; + int stop = choiceStarts[rowStarts[state] + choice + 1]; + for (int col = start; col < stop; col++) { + result = fn.apply(result, state, cols[col], nonZeros[col]); + } + return result; + } + + @Override + public long reduceTransitions(int state, int choice, long init, LongTransitionFunction fn) + { + long result = init; + int start = choiceStarts[rowStarts[state] + choice]; + int stop = choiceStarts[rowStarts[state] + choice + 1]; + for (int col = start; col < stop; col++) { + result = fn.apply(result, state, cols[col], nonZeros[col]); + } + return result; + } + @Override public int getNumTransitions(int s, int i) { From c1f16b255e41829de9ebf46b143f3c63b4ca9dd1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffen=20M=C3=A4rcker?= Date: Wed, 8 May 2019 11:58:53 +0200 Subject: [PATCH 3/3] Implement forEachTransition in terms of reduce --- prism/src/explicit/DTMC.java | 11 ++++------- prism/src/explicit/DTMCEmbeddedSimple.java | 14 -------------- prism/src/explicit/DTMCFromMDPAndMDStrategy.java | 9 --------- prism/src/explicit/DTMCSparse.java | 8 -------- prism/src/explicit/MDP.java | 9 +++------ 5 files changed, 7 insertions(+), 44 deletions(-) diff --git a/prism/src/explicit/DTMC.java b/prism/src/explicit/DTMC.java index 516fb04f79..ed6b593f60 100644 --- a/prism/src/explicit/DTMC.java +++ b/prism/src/explicit/DTMC.java @@ -67,7 +67,7 @@ public interface TransitionConsumer { } /** - * Iterate over the outgoing transitions of state {@code s} and call the accept method + * Iterate over the outgoing transitions of state {@code state} and call the accept method * of the consumer for each of them: *
* Call {@code accept(s,t,d)} where t is the successor state and, @@ -80,15 +80,12 @@ public interface TransitionConsumer { * computation methods (mvMult, etc). In derived classes, it may thus be worthwhile to * provide a specialised implementation for this method that avoids using the Iterator mechanism. * - * @param s the state s + * @param state the state * @param c the consumer */ - public default void forEachTransition(int s, TransitionConsumer c) + public default void forEachTransition(int state, TransitionConsumer c) { - for (Iterator> it = getTransitionsIterator(s); it.hasNext(); ) { - Entry e = it.next(); - c.accept(s, e.getKey(), e.getValue()); - } + reduceTransitions(state, null, (r, s, t, d) -> {c.accept(s,t,d); return r;}); } /** diff --git a/prism/src/explicit/DTMCEmbeddedSimple.java b/prism/src/explicit/DTMCEmbeddedSimple.java index 2e0543b1c0..cbc2a0709c 100644 --- a/prism/src/explicit/DTMCEmbeddedSimple.java +++ b/prism/src/explicit/DTMCEmbeddedSimple.java @@ -256,20 +256,6 @@ public Double setValue(Double value) } } - @Override - public void forEachTransition(int s, TransitionConsumer c) - { - final double er = exitRates[s]; - if (er == 0) { - // exit rate = 0 -> prob 1 self loop - c.accept(s, s, 1.0); - } else { - ctmc.forEachTransition(s, (s_,t,rate) -> { - c.accept(s_, t, rate / er); - }); - } - } - @Override public T reduceTransitions(int state, T init, ObjTransitionFunction fn) { diff --git a/prism/src/explicit/DTMCFromMDPAndMDStrategy.java b/prism/src/explicit/DTMCFromMDPAndMDStrategy.java index 9d1e002d21..8ee7a29388 100644 --- a/prism/src/explicit/DTMCFromMDPAndMDStrategy.java +++ b/prism/src/explicit/DTMCFromMDPAndMDStrategy.java @@ -181,15 +181,6 @@ public Iterator> getTransitionsIterator(int s) } } - @Override - public void forEachTransition(int s, TransitionConsumer c) - { - if (!strat.isChoiceDefined(s)) { - return; - } - mdp.forEachTransition(s, strat.getChoiceIndex(s), c); - } - @Override public T reduceTransitions(int state, T init, ObjTransitionFunction fn) { diff --git a/prism/src/explicit/DTMCSparse.java b/prism/src/explicit/DTMCSparse.java index a70cef6389..5b9f656f72 100644 --- a/prism/src/explicit/DTMCSparse.java +++ b/prism/src/explicit/DTMCSparse.java @@ -227,14 +227,6 @@ public void buildFromPrismExplicit(String filename) throws PrismException //--- DTMC --- - @Override - public void forEachTransition(int state, TransitionConsumer consumer) - { - for (int col = rows[state], stop = rows[state+1]; col < stop; col++) { - consumer.accept(state, columns[col], probabilities[col]); - } - } - @Override public T reduceTransitions(int state, T init, ObjTransitionFunction fn) { diff --git a/prism/src/explicit/MDP.java b/prism/src/explicit/MDP.java index 1b3791578a..f456f20519 100644 --- a/prism/src/explicit/MDP.java +++ b/prism/src/explicit/MDP.java @@ -59,7 +59,7 @@ public interface MDP extends MDPGeneric public Iterator> getTransitionsIterator(int s, int i); /** - * Iterate over the outgoing transitions of state {@code s} and choice {@code i} + * Iterate over the outgoing transitions of state {@code state} and choice {@code i} * and call the accept method of the consumer for each of them: *
* Call {@code accept(s,t,d)} where t is the successor state d = P(s,i,t) @@ -75,12 +75,9 @@ public interface MDP extends MDPGeneric * @param i the choice i * @param c the consumer */ - public default void forEachTransition(int s, int i, TransitionConsumer c) + public default void forEachTransition(int state, int choice, TransitionConsumer c) { - for (Iterator> it = getTransitionsIterator(s, i); it.hasNext(); ) { - Entry e = it.next(); - c.accept(s, e.getKey(), e.getValue()); - } + reduceTransitions(state, choice, null, (r, s, t, d) -> {c.accept(s,t,d); return r;}); } /**