diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java index 1b0fc6f1..cc94d132 100644 --- a/prism/src/explicit/MDPSparse.java +++ b/prism/src/explicit/MDPSparse.java @@ -77,6 +77,100 @@ public class MDPSparse extends MDPExplicit // Constructors + /** + * Constructor: Build new MDPSparse from arbitrary MDP type. + * + * @param mdp some MDP + */ + public MDPSparse(final MDP mdp) + { + this(mdp, false); + } + + /** + * Constructor: Build new MDPSparse from arbitrary MDP type. + * + * @param mdp some MDP + * @param sort Whether or not to sort column indices + */ + public MDPSparse(final MDP mdp, boolean sort) + { + initialise(mdp.getNumStates()); + + setStatesList(mdp.getStatesList()); + setConstantValues(mdp.getConstantValues()); + for (String label : mdp.getLabels()) { + addLabel(label, mdp.getLabelStates(label)); + } + + // Copy stats + numDistrs = mdp.getNumChoices(); + numTransitions = mdp.getNumTransitions(); + maxNumDistrs = mdp.getMaxNumChoices(); + // Initialise transition function + nonZeros = new double[numTransitions]; + cols = new int[numTransitions]; + choiceStarts = new int[numDistrs + 1]; + rowStarts = new int[numStates + 1]; + actions = hasActionLabels(mdp) ? new Object[numDistrs] : null; + + // Copy transition function + final TreeMap sorted = sort ? new TreeMap() : null; + int rowIndex = 0, choiceIndex = 0; + for (int state = 0; state < numStates; state++) { + if (mdp.isInitialState(state)) { + addInitialState(state); + } + if (mdp.isDeadlockState(state)) { + deadlocks.add(state); + } + + rowStarts[state] = rowIndex; + if (actions != null) { + for (int choice = 0, numChoices = mdp.getNumChoices(state); choice < numChoices; choice++) { + actions[rowIndex + choice] = mdp.getAction(state, choice); + } + } + for (int choice = 0, numChoices = mdp.getNumChoices(state); choice < numChoices; choice++) { + choiceStarts[rowIndex] = choiceIndex; + for (Iterator> transitions = mdp.getTransitionsIterator(state, choice); transitions.hasNext();) { + final Map.Entry trans = transitions.next(); + if (sort) { + sorted.put(trans.getKey(), trans.getValue()); + } else { + cols[choiceIndex] = trans.getKey(); + nonZeros[choiceIndex] = trans.getValue(); + choiceIndex++; + } + } + if (sort) { + for (Map.Entry e : sorted.entrySet()) { + cols[choiceIndex] = e.getKey(); + nonZeros[choiceIndex] = e.getValue(); + choiceIndex++; + } + sorted.clear(); + } + rowIndex++; + } + } + choiceStarts[numDistrs] = numTransitions; + rowStarts[numStates] = numDistrs; + } + + /** Helper: Does the given MDP have action labels on any of the choices? */ + private static boolean hasActionLabels(final MDP mdp) + { + for (int state = 0, numStates = mdp.getNumStates(); state < numStates; state++) { + for (int choice = 0, numChoices = mdp.getNumChoices(state); choice < numChoices; choice++) { + if (mdp.getAction(state, choice) != null) { + return true; + } + } + } + return false; + } + /** * Copy constructor (from MDPSimple). */