Browse Source

Code tidy.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3331 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 15 years ago
parent
commit
25b8626a51
  1. 6
      prism/src/explicit/MDP.java
  2. 28
      prism/src/explicit/MDPSimple.java
  3. 29
      prism/src/explicit/MDPSparse.java

6
prism/src/explicit/MDP.java

@ -190,14 +190,12 @@ public interface MDP extends Model
* and only those columns in the probability matrix are considered, that
* are elements of {@code states}.
*
* The result of this multiplication is added to the contents
* of {@code dest}.
* The result of this multiplication is added to the contents of {@code dest}.
*
* @param states States for which to multiply
* @param adv Strategy to use
* @param source Vector to multiply matrix with
* @param dest Vector to write result to.
*/
public void mvMultRight(int[] states, int[] adv, double[] source,
double[] dest);
public void mvMultRight(int[] states, int[] adv, double[] source, double[] dest);
}

28
prism/src/explicit/MDPSimple.java

@ -1024,6 +1024,20 @@ public class MDPSimple extends ModelSimple implements MDP
return res;
}
@Override
public void mvMultRight(int[] states, int[] adv, double[] source,
double[] dest) {
for (int s : states) {
Iterator<Entry<Integer, Double>> it = this.getTransitionsIterator(s, adv[s]);
while (it.hasNext()) {
Entry<Integer, Double> next = it.next();
int col = next.getKey();
double prob = next.getValue();
dest[col] += prob * source[s];
}
}
}
// Accessors (other)
/**
@ -1162,18 +1176,4 @@ public class MDPSimple extends ModelSimple implements MDP
// TODO: compare actions (complicated: null = null,null,null,...)
return true;
}
@Override
public void mvMultRight(int[] states, int[] adv, double[] source,
double[] dest) {
for (int s : states) {
Iterator<Entry<Integer, Double>> it = this.getTransitionsIterator(s, adv[s]);
while (it.hasNext()) {
Entry<Integer, Double> next = it.next();
int col = next.getKey();
double prob = next.getValue();
dest[col] += prob * source[s];
}
}
}
}

29
prism/src/explicit/MDPSparse.java

@ -1015,6 +1015,20 @@ public class MDPSparse extends ModelSparse implements MDP
return res;
}
@Override
public void mvMultRight(int[] states, int[] adv, double[] source, double[] dest)
{
for (int s : states) {
int j, l2, h2;
int k = adv[s];
j = rowStarts[s] + k;
l2 = choiceStarts[j];
h2 = choiceStarts[j + 1];
for (k = l2; k < h2; k++) {
dest[cols[k]] += nonZeros[k] * source[s];
}
}
}
// Standard methods
@Override
@ -1074,19 +1088,4 @@ public class MDPSparse extends ModelSparse implements MDP
// TODO: compare actions (complicated: null = null,null,null,...)
return true;
}
@Override
public void mvMultRight(int[] states, int[] adv, double[] source, double[] dest)
{
for (int s : states) {
int j, l2, h2;
int k = adv[s];
j = rowStarts[s] + k;
l2 = choiceStarts[j];
h2 = choiceStarts[j + 1];
for (k = l2; k < h2; k++) {
dest[cols[k]] += nonZeros[k] * source[s];
}
}
}
}
Loading…
Cancel
Save