From 9b5245f04fe001d8f1c773e44b516f9a603c7b91 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 21 Jul 2017 13:30:04 +0000 Subject: [PATCH] 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 --- prism/src/explicit/DTMCSimple.java | 87 -------- prism/src/explicit/MDPSimple.java | 347 +---------------------------- 2 files changed, 1 insertion(+), 433 deletions(-) diff --git a/prism/src/explicit/DTMCSimple.java b/prism/src/explicit/DTMCSimple.java index ec2f67d5..7e1cdc46 100644 --- a/prism/src/explicit/DTMCSimple.java +++ b/prism/src/explicit/DTMCSimple.java @@ -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 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 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 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 e : distr) { - j = (Integer) e.getKey(); - prob = (Double) e.getValue(); - result[j] += prob * vect[i]; - } - - } - } - // Accessors (other) /** diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index 4a33a7ee..c803a343 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/prism/src/explicit/MDPSimple.java @@ -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 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 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 mvMultMinMaxSingleChoices(int s, double vect[], boolean min, double val) - { - int j, k; - double d, prob; - List res; - List step; - - // Create data structures to store strategy - res = new ArrayList(); - // 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 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 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 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 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 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 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 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 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 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 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 mvMultRewMinMaxSingleChoices(int s, double vect[], MDPRewards mdpRewards, boolean min, double val) - { - int j, k; - double d, prob; - List res; - List step; - - // Create data structures to store strategy - res = new ArrayList(); - // 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 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> it = this.getTransitionsIterator(s, strat[s]); - while (it.hasNext()) { - Entry next = it.next(); - int col = next.getKey(); - double prob = next.getValue(); - dest[col] += prob * source[s]; - } - } - } // Accessors (other)