Implement reduceTransitions to allow efficient accumulation over transitions

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:
 	 * <br>
 	 * Call {@code accept(s,t,d)} where t is the successor state and,
@@ -80,15 +80,136 @@ 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<Entry<Integer, Double>> it = getTransitionsIterator(s); it.hasNext(); ) {
+		reduceTransitions(state, null, (r, s, t, d) -> {c.accept(s,t,d); return r;});
+	}
+
+	/**
+	 * 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 <T> type of first argument and result
+	 */
+	@FunctionalInterface
+	public static interface ObjTransitionFunction<T>
+	{
+		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:
+	 * <br/>
+	 * 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.
+	 * <p>
+	 * <i>Default implementation</i>: The default implementation relies on iterating over the
+	 * iterator returned by {@code getTransitionsIterator()}.
+	 * <p><i>Note</i>: 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> T reduceTransitions(int state, T init, ObjTransitionFunction<T> fn)
+	{
+		T result = init;
+		for (Iterator<Entry<Integer, Double>> it = getTransitionsIterator(state); it.hasNext(); ) {
+			Entry<Integer, Double> 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<Entry<Integer, Double>> it = getTransitionsIterator(state); it.hasNext(); ) {
+			Entry<Integer, Double> 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<Entry<Integer, Double>> it = getTransitionsIterator(state); it.hasNext(); ) {
 			Entry<Integer, Double> e = it.next();
-			c.accept(s, e.getKey(), e.getValue());
+			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<Entry<Integer, Double>> it = getTransitionsIterator(state); it.hasNext(); ) {
+			Entry<Integer, Double> e = it.next();
+			result = fn.apply(result, state, e.getKey(), e.getValue());
+		}
+		return result;
 	}
 
 	/**
@@ -103,29 +224,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:
 	 * <br>
-	 * 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));
 	}
 
 	/**

prism/src/explicit/DTMCEmbeddedSimple.java

@@ -257,17 +257,63 @@ public Double setValue(Double value)
 	}
 
 	@Override
-	public void forEachTransition(int s, TransitionConsumer c)
+	public <T> T reduceTransitions(int state, T init, ObjTransitionFunction<T> fn)
 	{
-		final double er = exitRates[s];
+		double er = exitRates[state];
+		T result = init;
 		if (er == 0) {
 			// exit rate = 0 -> prob 1 self loop
-			c.accept(s, s, 1.0);
+			fn.apply(result, state, state, 1.0);
 		} else {
-			ctmc.forEachTransition(s, (s_,t,rate) -> {
-				c.accept(s_, t, rate / er);
-			});
+			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[])

prism/src/explicit/DTMCFromMDPAndMDStrategy.java

@@ -182,14 +182,41 @@ public Iterator<Entry<Integer, Double>> getTransitionsIterator(int s)
 	}
 
 	@Override
-	public void forEachTransition(int s, TransitionConsumer c)
+	public <T> T reduceTransitions(int state, T init, ObjTransitionFunction<T> fn)
 	{
-		if (!strat.isChoiceDefined(s)) {
-			return;
+		if (!strat.isChoiceDefined(state)) {
+			return init;
 		}
-		mdp.forEachTransition(s, strat.getChoiceIndex(s), c::accept);
+		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[])
 	{

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
 

prism/src/explicit/DTMCSparse.java

@@ -228,11 +228,43 @@ public void buildFromPrismExplicit(String filename) throws PrismException
 	//--- DTMC ---
 
 	@Override
-	public void forEachTransition(int state, TransitionConsumer consumer)
+	public <T> T reduceTransitions(int state, T init, ObjTransitionFunction<T> fn)
 	{
-		for (int col = rows[state], stop = rows[state+1]; col < stop; col++) {
-			consumer.accept(state, columns[col], probabilities[col]);
+		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