diff --git a/prism/src/explicit/ChoiceActionsSimple.java b/prism/src/explicit/ChoiceActionsSimple.java new file mode 100644 index 00000000..31e83477 --- /dev/null +++ b/prism/src/explicit/ChoiceActionsSimple.java @@ -0,0 +1,182 @@ +//============================================================================== +// +// Copyright (c) 2020- +// Authors: +// * Dave Parker (University of Birmingham) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package explicit; + +import java.util.ArrayList; + +/** + * Explicit-state storage of the action labels attached to choices in a model. + * + * Uses simple, mutable data structures, matching the "Simple" range of models. + */ +public class ChoiceActionsSimple +{ + // Action labels for each choice in each state + // (null list means no actions; null in element s means no actions for state s) + // Note: The number of states and choices per state is unknown, + // so lists may be under-sized, in which case missing entries are assumed to be null. + protected ArrayList> actions; + + // Constructors + + /** + * Constructor: empty action storage + */ + public ChoiceActionsSimple() + { + actions = null; + } + + /** + * Copy constructor + */ + public ChoiceActionsSimple(ChoiceActionsSimple cas) + { + actions = null; + if (cas.actions != null) { + int numStates = cas.actions.size(); + actions = new ArrayList>(numStates); + for (int s = 0; s < numStates; s++) { + actions.add(null); + } + for (int s = 0; s < numStates; s++) { + if (cas.actions.get(s) != null) { + actions.set(s, new ArrayList<>(cas.actions.get(s))); + } + } + } + } + + /** + * Copy constructor, but with a state index permutation, + * i.e. in which state index i becomes index permut[i]. + */ + public ChoiceActionsSimple(ChoiceActionsSimple cas, int permut[]) + { + actions = null; + if (cas.actions != null) { + int numStates = cas.actions.size(); + actions = new ArrayList>(numStates); + for (int s = 0; s < numStates; s++) { + actions.add(null); + } + for (int s = 0; s < numStates; s++) { + if (cas.actions.get(s) != null) { + actions.set(permut[s], new ArrayList<>(cas.actions.get(s))); + } + } + } + } + + // Mutators + + /** + * Clear all actions for state {@code s} + */ + public void clearState(int s) + { + if (actions != null && actions.get(s) != null) { + actions.get(s).clear(); + } + } + + /** + * Set the action label for choice {@code i} of state {@code s}. + */ + public void setAction(int s, int i, Object action) + { + // Create main list if not done yet + if (actions == null) { + actions = new ArrayList>(); + } + // Expand main list up to state s if needed, + // storing null for newly added items + if (s >= actions.size()) { + int n = s - actions.size() + 1; + for (int j = 0; j < n; j++) { + actions.add(null); + } + } + // Create action list for state s if needed + ArrayList list; + if ((list = actions.get(s)) == null) { + actions.set(s, (list = new ArrayList())); + } + // Expand action list up to choice i if needed, + // storing null for newly added items + if (i >= list.size()) { + int n = i - list.size() + 1; + for (int j = 0; j < n; j++) { + list.add(null); + } + } + // Store the action + list.set(i, action); + } + + // Accessors + + public Object getAction(int s, int i) + { + // Empty list means no (null) actions everywhere + if (actions == null) { + return null; + } + try { + return actions.get(s).get(i); + } + // Lists may be under-sized, indicating no action added + catch (IndexOutOfBoundsException e) { + return null; + } + } + + /** + * Convert to "sparse" storage for a given model, + * i.e., a single array where all actions are stored in + * order, per state and then per choice. + * If this action storage is completely empty, + * then this method may simply return null. + */ + public Object[] convertToSparseStorage(NondetModel model) + { + if (actions == null) { + return null; + } else { + Object arr[] = new Object[model.getNumChoices()]; + int numStates = model.getNumStates(); + int count = 0; + for (int s = 0; s < numStates; s++) { + int numChoices = model.getNumChoices(s); + for (int i = 0; i < numChoices; i++) { + arr[count++] = model.getAction(s, i); + } + } + return arr; + } + } +} diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index 26070b1d..eda66a0f 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/prism/src/explicit/MDPSimple.java @@ -53,8 +53,7 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple protected List> trans; // Action labels - // (null list means no actions; null in element s means no actions for state s) - protected List> actions; + protected ChoiceActionsSimple actions; // Flag: allow duplicates in distribution sets? protected boolean allowDupes = false; @@ -97,21 +96,7 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple distrs.add(new Distribution(distr)); } } - 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); - } - } - } + actions = new ChoiceActionsSimple(mdp.actions); // Copy flags/stats too allowDupes = mdp.allowDupes; numDistrs = mdp.numDistrs; @@ -151,21 +136,7 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple distrs.add(new Distribution(distr, permut)); } } - 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); - } - } - } + actions = new ChoiceActionsSimple(mdp.actions, permut); // Copy flags/stats too allowDupes = mdp.allowDupes; numDistrs = mdp.numDistrs; @@ -213,7 +184,7 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple for (int i = 0; i < numStates; i++) { trans.add(new ArrayList()); } - actions = null; + actions = new ChoiceActionsSimple(); } @Override @@ -230,8 +201,7 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple } maxNumDistrsOk = false; trans.get(s).clear(); - if (actions != null && actions.get(s) != null) - actions.get(s).clear(); + actions.clearState(s); } @Override @@ -246,8 +216,6 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple { for (int i = 0; i < numToAdd; i++) { trans.add(new ArrayList()); - if (actions != null) - actions.add(null); numStates++; } } @@ -376,9 +344,6 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple } set = trans.get(s); set.add(distr); - // Add null action if necessary - if (actions != null && actions.get(s) != null) - actions.get(s).add(null); // Update stats numDistrs++; maxNumDistrs = Math.max(maxNumDistrs, set.size()); @@ -407,11 +372,8 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple } set = trans.get(s); set.add(distr); - // Add null action if necessary - if (actions != null && actions.get(s) != null) - actions.get(s).add(null); // Set action - setAction(s, set.size() - 1, action); + actions.setAction(s, set.size() - 1, action); // Update stats numDistrs++; maxNumDistrs = Math.max(maxNumDistrs, set.size()); @@ -427,26 +389,7 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple */ 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); - for (int j = 0; j < numStates; j++) - actions.add(null); - } - // If no actions for state i yet, create list - if (actions.get(s) == null) { - int n = trans.get(s).size(); - List list = new ArrayList(n); - for (int j = 0; j < n; j++) { - list.add(null); - } - actions.set(s, list); - } - // Set actions - actions.get(s).set(i, o); + actions.setAction(s, i, o); } // Accessors (for Model) @@ -522,10 +465,7 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple @Override public Object getAction(int s, int i) { - List list; - if (i < 0 || actions == null || (list = actions.get(s)) == null) - return null; - return list.get(i); + return actions.getAction(s, i); } @Override diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java index 9f2e8763..f7df0539 100644 --- a/prism/src/explicit/MDPSparse.java +++ b/prism/src/explicit/MDPSparse.java @@ -188,7 +188,7 @@ public class MDPSparse extends MDPExplicit */ public MDPSparse(MDPSimple mdp, boolean sort) { - int i, j, k, n; + int i, j, k; TreeMap sorted = null; initialise(mdp.getNumStates()); copyFrom(mdp); @@ -204,16 +204,9 @@ public class MDPSparse extends MDPExplicit cols = new int[numTransitions]; choiceStarts = new int[numDistrs + 1]; rowStarts = new int[numStates + 1]; - actions = mdp.actions == null ? null : new Object[numDistrs]; j = k = 0; for (i = 0; i < numStates; i++) { rowStarts[i] = j; - if (mdp.actions != null) { - n = mdp.getNumChoices(i); - for (int l = 0; l < n; l++) { - actions[j + l] = mdp.getAction(i, l); - } - } for (Distribution distr : mdp.trans.get(i)) { choiceStarts[j] = k; for (Map.Entry e : distr) { @@ -238,6 +231,7 @@ public class MDPSparse extends MDPExplicit } choiceStarts[numDistrs] = numTransitions; rowStarts[numStates] = numDistrs; + actions = mdp.actions.convertToSparseStorage(mdp); } /** @@ -252,7 +246,7 @@ public class MDPSparse extends MDPExplicit */ public MDPSparse(MDPSimple mdp, boolean sort, int permut[]) { - int i, j, k, n; + int i, j, k; TreeMap sorted = null; int permutInv[]; initialise(mdp.getNumStates()); @@ -274,16 +268,9 @@ public class MDPSparse extends MDPExplicit cols = new int[numTransitions]; choiceStarts = new int[numDistrs + 1]; rowStarts = new int[numStates + 1]; - actions = mdp.actions == null ? null : new Object[numDistrs]; j = k = 0; for (i = 0; i < numStates; i++) { rowStarts[i] = j; - if (mdp.actions != null) { - n = mdp.getNumChoices(permutInv[i]); - for (int l = 0; l < n; l++) { - actions[j + l] = mdp.getAction(permutInv[i], l); - } - } for (Distribution distr : mdp.trans.get(permutInv[i])) { choiceStarts[j] = k; for (Map.Entry e : distr) { @@ -308,6 +295,7 @@ public class MDPSparse extends MDPExplicit } choiceStarts[numDistrs] = numTransitions; rowStarts[numStates] = numDistrs; + actions = mdp.actions.convertToSparseStorage(mdp); } /**