diff --git a/prism/src/explicit/DTMC.java b/prism/src/explicit/DTMC.java index 65cc776a..b936a9f8 100644 --- a/prism/src/explicit/DTMC.java +++ b/prism/src/explicit/DTMC.java @@ -593,17 +593,11 @@ public interface DTMC extends Model */ public default void vmMult(double vect[], double result[]) { - int i; - - int numStates = getNumStates(); // Initialise result to 0 - for (i = 0; i < numStates; i++) { - result[i] = 0; - } - + Arrays.fill(result, 0); // Go through matrix elements (by row) - for (i = 0; i < numStates; i++) { - forEachTransition(i, (s, t, prob) -> { + for (int state = 0, numStates = getNumStates(); state < numStates; state++) { + forEachTransition(state, (s, t, prob) -> { result[t] += prob * vect[s]; }); } diff --git a/prism/src/explicit/DTMCEmbeddedSimple.java b/prism/src/explicit/DTMCEmbeddedSimple.java index dd2ceb69..717d6e92 100644 --- a/prism/src/explicit/DTMCEmbeddedSimple.java +++ b/prism/src/explicit/DTMCEmbeddedSimple.java @@ -397,29 +397,22 @@ public class DTMCEmbeddedSimple extends DTMCExplicit @Override public void vmMult(double vect[], double result[]) { - int i, j; - double prob, er; - Distribution distr; - // Initialise result to 0 - for (j = 0; j < numStates; j++) { - result[j] = 0; - } + Arrays.fill(result, 0); // Go through matrix elements (by row) - for (i = 0; i < numStates; i++) { - distr = ctmc.getTransitions(i); - er = exitRates[i]; + for (int state = 0; state < numStates; state++) { + double er = exitRates[state]; // Exit rate 0: prob 1 self-loop if (er == 0) { - result[i] += vect[i]; + result[state] += vect[state]; + continue; } // Exit rate > 0 - else { - for (Map.Entry e : distr) { - j = (Integer) e.getKey(); - prob = (Double) e.getValue(); - result[j] += (prob / er) * vect[i]; - } + for (Iterator> transitions = ctmc.getTransitionsIterator(state); transitions.hasNext();) { + Entry trans = transitions.next(); + int target = trans.getKey(); + double prob = trans.getValue() / er; + result[target] += prob * vect[state]; } } } diff --git a/prism/src/explicit/DTMCSparse.java b/prism/src/explicit/DTMCSparse.java index c4fee9c4..a0f33456 100644 --- a/prism/src/explicit/DTMCSparse.java +++ b/prism/src/explicit/DTMCSparse.java @@ -350,8 +350,8 @@ public class DTMCSparse extends DTMCExplicit // Go through matrix elements (by row) for (int state = 0; state < numStates; state++) { for (int i=rows[state], stop=rows[state+1]; i < stop; i++) { - final int target = columns[i]; - final double probability = probabilities[i]; + int target = columns[i]; + double probability = probabilities[i]; result[target] += probability * vect[state]; } } diff --git a/prism/src/explicit/DTMCUniformisedSimple.java b/prism/src/explicit/DTMCUniformisedSimple.java index ec766b86..12770ec8 100644 --- a/prism/src/explicit/DTMCUniformisedSimple.java +++ b/prism/src/explicit/DTMCUniformisedSimple.java @@ -26,6 +26,7 @@ package explicit; +import java.util.Arrays; import java.util.BitSet; import java.util.Iterator; import java.util.List; @@ -281,29 +282,23 @@ public class DTMCUniformisedSimple extends DTMCExplicit @Override public void vmMult(double vect[], double result[]) { - int i, j; - double prob, sum; - Distribution distr; - // Initialise result to 0 - for (j = 0; j < numStates; j++) { - result[j] = 0; - } + Arrays.fill(result, 0); // Go through matrix elements (by row) - for (i = 0; i < numStates; i++) { - distr = ctmc.getTransitions(i); - sum = 0.0; - for (Map.Entry e : distr) { - j = (Integer) e.getKey(); - prob = (Double) e.getValue(); + for (int state = 0; state < numStates; state++) { + double sum = 0.0; + for (Iterator> transitions = ctmc.getTransitionsIterator(state); transitions.hasNext();) { + Entry trans = transitions.next(); + int target = trans.getKey(); + double prob = trans.getValue() / q; // Non-diagonal entries only - if (j != i) { + if (target != state) { sum += prob; - result[j] += (prob / q) * vect[i]; + result[target] += prob * vect[state]; } } - // Diagonal entry is 1 - sum/q - result[i] += (1 - sum / q) * vect[i]; + // Diagonal entry is 1 - sum + result[state] += (1 - sum) * vect[state]; } }