Browse Source

Improve implementations of DTMC::vmMult

- scope of variables and naming
- usage of Arrays#fill instead of manual loop for array initialisation
- superflous casts
master
Steffen Märcker 8 years ago
committed by Dave Parker
parent
commit
5898c55afe
  1. 12
      prism/src/explicit/DTMC.java
  2. 27
      prism/src/explicit/DTMCEmbeddedSimple.java
  3. 4
      prism/src/explicit/DTMCSparse.java
  4. 29
      prism/src/explicit/DTMCUniformisedSimple.java

12
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];
});
}

27
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<Integer, Double> e : distr) {
j = (Integer) e.getKey();
prob = (Double) e.getValue();
result[j] += (prob / er) * vect[i];
}
for (Iterator<Entry<Integer, Double>> transitions = ctmc.getTransitionsIterator(state); transitions.hasNext();) {
Entry<Integer, Double> trans = transitions.next();
int target = trans.getKey();
double prob = trans.getValue() / er;
result[target] += prob * vect[state];
}
}
}

4
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];
}
}

29
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<Integer, Double> e : distr) {
j = (Integer) e.getKey();
prob = (Double) e.getValue();
for (int state = 0; state < numStates; state++) {
double sum = 0.0;
for (Iterator<Entry<Integer, Double>> transitions = ctmc.getTransitionsIterator(state); transitions.hasNext();) {
Entry<Integer, Double> 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];
}
}

Loading…
Cancel
Save