s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

explicit DTMCSimple, MDPSimple refactor: remove mv... specialisations so the default methods from DTMC/MDP are used 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12104 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 9 years ago
parent
dc8e331a36
commit
9b5245f04f
2 changed files with 1 additions and 433 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 87
      prism/src/explicit/DTMCSimple.java
  2. 347
      prism/src/explicit/MDPSimple.java

87
prism/src/explicit/DTMCSimple.java
View File

@ -30,9 +30,6 @@ import java.util.*;
import java.util.Map.Entry;
import java.io.*;
import common.IterableStateSet;
import explicit.rewards.*;
import prism.PrismException;
/**
@ -274,90 +271,6 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple
return trans.get(s).iterator();
}
@Override
public double mvMultSingle(int s, double vect[])
{
int k;
double d, prob;
Distribution distr;
distr = trans.get(s);
d = 0.0;
for (Map.Entry<Integer, Double> e : distr) {
k = (Integer) e.getKey();
prob = (Double) e.getValue();
d += prob * vect[k];
}
return d;
}
@Override
public double mvMultJacSingle(int s, double vect[])
{
int k;
double diag, d, prob;
Distribution distr;
distr = trans.get(s);
diag = 1.0;
d = 0.0;
for (Map.Entry<Integer, Double> e : distr) {
k = (Integer) e.getKey();
prob = (Double) e.getValue();
if (k != s) {
d += prob * vect[k];
} else {
diag -= prob;
}
}
if (diag > 0)
d /= diag;
return d;
}
@Override
public double mvMultRewSingle(int s, double vect[], MCRewards mcRewards)
{
int k;
double d, prob;
Distribution distr;
distr = trans.get(s);
d = mcRewards.getStateReward(s);
for (Map.Entry<Integer, Double> e : distr) {
k = (Integer) e.getKey();
prob = (Double) e.getValue();
d += prob * vect[k];
}
return d;
}
@Override
public void vmMult(double vect[], double result[])
{
int i, j;
double prob;
Distribution distr;
// Initialise result to 0
for (j = 0; j < numStates; j++) {
result[j] = 0;
}
// Go through matrix elements (by row)
for (i = 0; i < numStates; i++) {
distr = trans.get(i);
for (Map.Entry<Integer, Double> e : distr) {
j = (Integer) e.getKey();
prob = (Double) e.getValue();
result[j] += prob * vect[i];
}
}
}
// Accessors (other)
/**

347
prism/src/explicit/MDPSimple.java
View File

@ -35,15 +35,10 @@ import java.util.ArrayList;
import java.util.BitSet;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import common.IterableStateSet;
import prism.PrismException;
import prism.PrismUtils;
import explicit.rewards.MCRewards;
import explicit.rewards.MDPRewards;
/**
* Simple explicit-state representation of an MDP.
@ -573,347 +568,7 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple
return trans.get(s).get(i).iterator();
}
@Override
public double mvMultMinMaxSingle(int s, double vect[], boolean min, int strat[])
{
int j, k, stratCh = -1;
double d, prob, minmax;
boolean first;
List<Distribution> step;
j = 0;
minmax = 0;
first = true;
step = trans.get(s);
for (Distribution distr : step) {
// Compute sum for this distribution
d = 0.0;
for (Map.Entry<Integer, Double> e : distr) {
k = (Integer) e.getKey();
prob = (Double) e.getValue();
d += prob * vect[k];
}
// Check whether we have exceeded min/max so far
if (first || (min && d < minmax) || (!min && d > minmax)) {
minmax = d;
// If strategy generation is enabled, remember optimal choice
if (strat != null)
stratCh = j;
}
first = false;
j++;
}
// If strategy generation is enabled, store optimal choice
if (strat != null & !first) {
// For max, only remember strictly better choices
if (min) {
strat[s] = stratCh;
} else if (strat[s] == -1 || minmax > vect[s]) {
strat[s] = stratCh;
}
}
return minmax;
}
@Override
public List<Integer> mvMultMinMaxSingleChoices(int s, double vect[], boolean min, double val)
{
int j, k;
double d, prob;
List<Integer> res;
List<Distribution> step;
// Create data structures to store strategy
res = new ArrayList<Integer>();
// One row of matrix-vector operation
j = -1;
step = trans.get(s);
for (Distribution distr : step) {
j++;
// Compute sum for this distribution
d = 0.0;
for (Map.Entry<Integer, Double> e : distr) {
k = (Integer) e.getKey();
prob = (Double) e.getValue();
d += prob * vect[k];
}
// Store strategy info if value matches
//if (PrismUtils.doublesAreClose(val, d, termCritParam, termCrit == TermCrit.ABSOLUTE)) {
if (PrismUtils.doublesAreClose(val, d, 1e-12, false)) {
res.add(j);
//res.add(distrs.getAction());
}
}
return res;
}
@Override
public double mvMultSingle(int s, int i, double vect[])
{
double d, prob;
int k;
Distribution distr = trans.get(s).get(i);
// Compute sum for this distribution
d = 0.0;
for (Map.Entry<Integer, Double> e : distr) {
k = (Integer) e.getKey();
prob = (Double) e.getValue();
d += prob * vect[k];
}
return d;
}
@Override
public double mvMultJacMinMaxSingle(int s, double vect[], boolean min, int strat[])
{
int j, k, stratCh = -1;
double diag, d, prob, minmax;
boolean first;
List<Distribution> step;
j = 0;
minmax = 0;
first = true;
step = trans.get(s);
for (Distribution distr : step) {
diag = 1.0;
// Compute sum for this distribution
d = 0.0;
for (Map.Entry<Integer, Double> e : distr) {
k = (Integer) e.getKey();
prob = (Double) e.getValue();
if (k != s) {
d += prob * vect[k];
} else {
diag -= prob;
}
}
if (diag > 0)
d /= diag;
// Check whether we have exceeded min/max so far
if (first || (min && d < minmax) || (!min && d > minmax)) {
minmax = d;
// If strategy generation is enabled, remember optimal choice
if (strat != null) {
stratCh = j;
}
}
first = false;
j++;
}
// If strategy generation is enabled, store optimal choice
if (strat != null & !first) {
// For max, only remember strictly better choices
if (min) {
strat[s] = stratCh;
} else if (strat[s] == -1 || minmax > vect[s]) {
strat[s] = stratCh;
}
}
return minmax;
}
@Override
public double mvMultJacSingle(int s, int i, double vect[])
{
double diag, d, prob;
int k;
Distribution distr;
distr = trans.get(s).get(i);
diag = 1.0;
// Compute sum for this distribution
d = 0.0;
for (Map.Entry<Integer, Double> e : distr) {
k = (Integer) e.getKey();
prob = (Double) e.getValue();
if (k != s) {
d += prob * vect[k];
} else {
diag -= prob;
}
}
if (diag > 0)
d /= diag;
return d;
}
@Override
public double mvMultRewMinMaxSingle(int s, double vect[], MDPRewards mdpRewards, boolean min, int strat[])
{
int j, k, stratCh = -1;
double d, prob, minmax;
boolean first;
List<Distribution> step;
minmax = 0;
first = true;
j = -1;
step = trans.get(s);
for (Distribution distr : step) {
j++;
// Compute sum for this distribution
d = mdpRewards.getTransitionReward(s, j);
for (Map.Entry<Integer, Double> e : distr) {
k = (Integer) e.getKey();
prob = (Double) e.getValue();
d += prob * vect[k];
}
// Check whether we have exceeded min/max so far
if (first || (min && d < minmax) || (!min && d > minmax)) {
minmax = d;
// If strategy generation is enabled, remember optimal choice
if (strat != null)
stratCh = j;
}
first = false;
}
// Add state reward (doesn't affect min/max)
minmax += mdpRewards.getStateReward(s);
// If strategy generation is enabled, store optimal choice
if (strat != null & !first) {
// For max, only remember strictly better choices
if (min) {
strat[s] = stratCh;
} else if (strat[s] == -1 || minmax > vect[s]) {
strat[s] = stratCh;
}
}
return minmax;
}
@Override
public double mvMultRewSingle(int s, int i, double[] vect, MCRewards mcRewards)
{
double d, prob;
int k;
Distribution distr = trans.get(s).get(i);
// Compute sum for this distribution
// TODO: use transition rewards when added to DTMCss
// d = mcRewards.getTransitionReward(s);
d = 0;
for (Map.Entry<Integer, Double> e : distr) {
k = (Integer) e.getKey();
prob = (Double) e.getValue();
d += prob * vect[k];
}
d += mcRewards.getStateReward(s);
return d;
}
@Override
public double mvMultRewJacMinMaxSingle(int s, double vect[], MDPRewards mdpRewards, boolean min, int strat[])
{
int j, k = -1, stratCh = -1;
double diag, d, prob, minmax;
boolean first;
List<Distribution> step;
minmax = 0;
first = true;
j = -1;
step = trans.get(s);
for (Distribution distr : step) {
j++;
diag = 1.0;
// Compute sum for this distribution
// (note: have to add state rewards in the loop for Jacobi)
d = mdpRewards.getStateReward(s);
d += mdpRewards.getTransitionReward(s, j);
for (Map.Entry<Integer, Double> e : distr) {
k = (Integer) e.getKey();
prob = (Double) e.getValue();
if (k != s) {
d += prob * vect[k];
} else {
diag -= prob;
}
}
if (diag > 0)
d /= diag;
// Catch special case of probability 1 self-loop (Jacobi does it wrong)
if (distr.size() == 1 && k == s) {
d = Double.POSITIVE_INFINITY;
}
// Check whether we have exceeded min/max so far
if (first || (min && d < minmax) || (!min && d > minmax)) {
minmax = d;
// If strategy generation is enabled, remember optimal choice
if (strat != null) {
stratCh = j;
}
}
first = false;
}
// If strategy generation is enabled, store optimal choice
if (strat != null & !first) {
// For max, only remember strictly better choices
if (min) {
strat[s] = stratCh;
} else if (strat[s] == -1 || minmax > vect[s]) {
strat[s] = stratCh;
}
}
return minmax;
}
@Override
public List<Integer> mvMultRewMinMaxSingleChoices(int s, double vect[], MDPRewards mdpRewards, boolean min, double val)
{
int j, k;
double d, prob;
List<Integer> res;
List<Distribution> step;
// Create data structures to store strategy
res = new ArrayList<Integer>();
// One row of matrix-vector operation
j = -1;
step = trans.get(s);
for (Distribution distr : step) {
j++;
// Compute sum for this distribution
d = mdpRewards.getTransitionReward(s, j);
for (Map.Entry<Integer, Double> e : distr) {
k = (Integer) e.getKey();
prob = (Double) e.getValue();
d += prob * vect[k];
}
d += mdpRewards.getStateReward(s);
// Store strategy info if value matches
//if (PrismUtils.doublesAreClose(val, d, termCritParam, termCrit == TermCrit.ABSOLUTE)) {
if (PrismUtils.doublesAreClose(val, d, 1e-12, false)) {
res.add(j);
//res.add(distrs.getAction());
}
}
return res;
}
@Override
public void mvMultRight(int[] states, int[] strat, double[] source, double[] dest)
{
for (int s : states) {
Iterator<Entry<Integer, Double>> it = this.getTransitionsIterator(s, strat[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)

Write Preview
Loading…
Cancel
Save