diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index 495c7e81..83f952a8 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/prism/src/explicit/MDPSimple.java @@ -49,7 +49,7 @@ public class MDPSimple extends ModelSimple implements MDP protected List> trans; // Action labels - // (null in element s means no actions for that state) + // (null list means no actions; null in element s means no actions for state s) protected List> actions; // Flag: allow duplicates in distribution sets? @@ -86,17 +86,34 @@ public class MDPSimple extends ModelSimple implements MDP { this(mdp.numStates); copyFrom(mdp); + // Copy storage directly to avoid worrying about duplicate distributions (and for efficiency) for (int s = 0; s < numStates; s++) { + List distrs = trans.get(s); for (Distribution distr : mdp.trans.get(s)) { - addChoice(s, new Distribution(distr)); + distrs.add(new Distribution(distr)); } } - for (int s = 0; s < numStates; s++) { - int n = mdp.getNumChoices(s); - for (int i = 0; i < n; i++) { - setAction(s, i, mdp.getAction(s, i)); + if (mdp.actions != null) { + actions = new ArrayList>(numStates); + for (int s = 0; s < numStates; s++) + actions.add(null); + for (int s = 0; s < numStates; s++) { + if (mdp.actions.get(s) != null) { + int n = mdp.trans.get(s).size(); + List list = new ArrayList(n); + for (int i = 0; i < n; i++) { + list.add(mdp.actions.get(s).get(i)); + } + actions.set(s, list); + } } } + // Copy flags/stats too + allowDupes = mdp.allowDupes; + numDistrs = mdp.numDistrs; + numTransitions = mdp.numTransitions; + maxNumDistrs = mdp.maxNumDistrs; + maxNumDistrsOk = mdp.maxNumDistrsOk; } /** @@ -107,6 +124,7 @@ public class MDPSimple extends ModelSimple implements MDP this(dtmc.getNumStates()); copyFrom(dtmc); for (int s = 0; s < numStates; s++) { + // Note: DTMCSimple has no actions so can ignore these addChoice(s, new Distribution(dtmc.getTransitions(s))); } } @@ -121,17 +139,35 @@ public class MDPSimple extends ModelSimple implements MDP { this(mdp.numStates); copyFrom(mdp, permut); + // Copy storage directly to avoid worrying about duplicate distributions (and for efficiency) + // (Since permut is a bijection, all structures and statistics are identical) for (int s = 0; s < numStates; s++) { + List distrs = trans.get(permut[s]); for (Distribution distr : mdp.trans.get(s)) { - addChoice(permut[s], new Distribution(distr, permut)); + distrs.add(new Distribution(distr, permut)); } } - for (int s = 0; s < numStates; s++) { - int n = mdp.getNumChoices(s); - for (int i = 0; i < n; i++) { - setAction(permut[s], i, mdp.getAction(s, i)); + if (mdp.actions != null) { + actions = new ArrayList>(numStates); + for (int s = 0; s < numStates; s++) + actions.add(null); + for (int s = 0; s < numStates; s++) { + if (mdp.actions.get(s) != null) { + int n = mdp.trans.get(s).size(); + List list = new ArrayList(n); + for (int i = 0; i < n; i++) { + list.add(mdp.actions.get(s).get(i)); + } + actions.set(permut[s], list); + } } } + // Copy flags/stats too + allowDupes = mdp.allowDupes; + numDistrs = mdp.numDistrs; + numTransitions = mdp.numTransitions; + maxNumDistrs = mdp.maxNumDistrs; + maxNumDistrsOk = mdp.maxNumDistrsOk; } // Mutators (for ModelSimple) @@ -401,6 +437,9 @@ public class MDPSimple extends ModelSimple implements MDP */ public void setAction(int s, int i, Object o) { + // If action to be set is null, nothing to do + if (o == null) + return; // If no actions array created yet, create it if (actions == null) { actions = new ArrayList>(numStates); @@ -477,7 +516,6 @@ public class MDPSimple extends ModelSimple implements MDP if (trans.get(i).isEmpty() && (except == null || !except.get(i))) throw new PrismException("MDP has a deadlock in state " + i); } - // TODO: Check for empty distributions too? } @Override diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java index c896edc5..b404cfec 100644 --- a/prism/src/explicit/MDPSparse.java +++ b/prism/src/explicit/MDPSparse.java @@ -32,7 +32,7 @@ import java.util.Map.Entry; import java.io.*; import explicit.rewards.MDPRewards; - +import parser.State; import prism.ModelType; import prism.PrismException; import prism.PrismUtils; @@ -57,7 +57,8 @@ public class MDPSparse extends ModelSparse implements MDP protected int rowStarts[]; // Action labels - /** Array of action labels for choices (is of size numDistrs) */ + /** Array of action labels for choices; + * if null, there are no actions; otherwise, is an array of size numDistrs */ protected Object actions[]; // Other statistics @@ -75,79 +76,6 @@ public class MDPSparse extends ModelSparse implements MDP this(mdp, false); } - /** - * Copy constructor for a (sub-)MDP from a given MDP. - * The states and actions will be indexed as given by the order - * of the lists {@code states} and {@code actions}. - * - * @param mdp MDP to copy from - * @param states States to copy - * @param actions Actions to copy - */ - public MDPSparse(MDP mdp, List states, List> actions) - { - initialise(states.size()); - for (int in : mdp.getInitialStates()) { - addInitialState(in); - } - - // statesList = new ArrayList(states.size()); - statesList = new ArrayList(); - for (int s : states) { - statesList.add(mdp.getStatesList().get(s)); - } - - numDistrs = 0; - numTransitions = 0; - maxNumDistrs = 0; - - for (int i = 0; i < states.size(); i++) { - int s = states.get(i); - - final int numChoices = actions.get(s).size(); - numDistrs += numChoices; - if (numChoices > maxNumDistrs) { - maxNumDistrs = numChoices; - } - for (int a : actions.get(s)) { - numTransitions += mdp.getNumTransitions(s, a); - } - } - - nonZeros = new double[numTransitions]; - cols = new int[numTransitions]; - choiceStarts = new int[numDistrs + 1]; - rowStarts = new int[numStates + 1]; - this.actions = new Object[numDistrs]; - int choiceIndex = 0; - int colIndex = 0; - - int[] reverseStates = new int[mdp.getNumStates()]; - for (int i = 0; i < states.size(); i++) { - reverseStates[states.get(i)] = i; - } - - for (int i = 0; i < states.size(); i++) { - int s = states.get(i); - rowStarts[i] = choiceIndex; - for (int a : actions.get(s)) { - choiceStarts[choiceIndex] = colIndex; - this.actions[choiceIndex] = mdp.getAction(s, a); - choiceIndex++; - Iterator> it = mdp.getTransitionsIterator(s, a); - while (it.hasNext()) { - Entry next = it.next(); - cols[colIndex] = reverseStates[next.getKey()]; - nonZeros[colIndex] = next.getValue(); - colIndex++; - } - } - } - - choiceStarts[numDistrs] = numTransitions; - rowStarts[numStates] = numDistrs; - } - /** * Copy constructor (from MDPSimple). Optionally, transitions within choices * are sorted (by ascending order of column index). @@ -279,6 +207,69 @@ public class MDPSparse extends ModelSparse implements MDP rowStarts[numStates] = numDistrs; } + /** + * Copy constructor for a (sub-)MDP from a given MDP. + * The states and actions will be indexed as given by the order + * of the lists {@code states} and {@code actions}. + * @param mdp MDP to copy from + * @param states States to copy + * @param actions Actions to copy + */ + public MDPSparse(MDP mdp, List states, List> actions) + { + initialise(states.size()); + for (int in : mdp.getInitialStates()) { + addInitialState(in); + } + statesList = new ArrayList(); + for (int s : states) { + statesList.add(mdp.getStatesList().get(s)); + } + numDistrs = 0; + numTransitions = 0; + maxNumDistrs = 0; + for (int i = 0; i < states.size(); i++) { + int s = states.get(i); + final int numChoices = actions.get(s).size(); + numDistrs += numChoices; + if (numChoices > maxNumDistrs) { + maxNumDistrs = numChoices; + } + for (int a : actions.get(s)) { + numTransitions += mdp.getNumTransitions(s, a); + } + } + nonZeros = new double[numTransitions]; + cols = new int[numTransitions]; + choiceStarts = new int[numDistrs + 1]; + rowStarts = new int[numStates + 1]; + this.actions = new Object[numDistrs]; + int choiceIndex = 0; + int colIndex = 0; + int[] reverseStates = new int[mdp.getNumStates()]; + for (int i = 0; i < states.size(); i++) { + reverseStates[states.get(i)] = i; + } + for (int i = 0; i < states.size(); i++) { + int s = states.get(i); + rowStarts[i] = choiceIndex; + for (int a : actions.get(s)) { + choiceStarts[choiceIndex] = colIndex; + this.actions[choiceIndex] = mdp.getAction(s, a); + choiceIndex++; + Iterator> it = mdp.getTransitionsIterator(s, a); + while (it.hasNext()) { + Entry next = it.next(); + cols[colIndex] = reverseStates[next.getKey()]; + nonZeros[colIndex] = next.getValue(); + colIndex++; + } + } + } + choiceStarts[numDistrs] = numTransitions; + rowStarts[numStates] = numDistrs; + } + // Mutators (for ModelSparse) @Override @@ -455,7 +446,6 @@ public class MDPSparse extends ModelSparse implements MDP if (getNumChoices(i) == 0 && (except == null || !except.get(i))) throw new PrismException("MDP has a deadlock in state " + i); } - // TODO: Check for empty distributions too? } @Override @@ -666,7 +656,7 @@ public class MDPSparse extends ModelSparse implements MDP @Override public Object getAction(int s, int i) { - return actions[rowStarts[s] + i]; + return actions == null ? null : actions[rowStarts[s] + i]; } @Override @@ -1043,7 +1033,7 @@ public class MDPSparse extends ModelSparse implements MDP for (j = l1; j < h1; j++) { if (j > l1) s += ","; - o = actions[j]; + o = getAction(i, j - l1); if (o != null) s += o + ":"; s += "{";