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

Encapsulate action storage in explicit.MDPSimple to new class ChoiceActionsSimple.

accumulation-v4.7
Dave Parker 6 years ago
parent
e1abc932a4
commit
eddb5defc8
3 changed files with 194 additions and 84 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 182
      prism/src/explicit/ChoiceActionsSimple.java
  2. 76
      prism/src/explicit/MDPSimple.java
  3. 20
      prism/src/explicit/MDPSparse.java

182
prism/src/explicit/ChoiceActionsSimple.java
View File

@ -0,0 +1,182 @@
//==============================================================================
//
// Copyright (c) 2020-
// Authors:
// * Dave Parker <d.a.parker@cs.bham.ac.uk> (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<ArrayList<Object>> 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<ArrayList<Object>>(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<ArrayList<Object>>(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<ArrayList<Object>>();
}
// 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<Object> list;
if ((list = actions.get(s)) == null) {
actions.set(s, (list = new ArrayList<Object>()));
}
// 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;
}
}
}

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

@ -53,8 +53,7 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple
protected List<List<Distribution>> trans; protected List<List<Distribution>> trans;
// Action labels // Action labels
// (null list means no actions; null in element s means no actions for state s)
protected List<List<Object>> actions;
protected ChoiceActionsSimple actions;
// Flag: allow duplicates in distribution sets? // Flag: allow duplicates in distribution sets?
protected boolean allowDupes = false; protected boolean allowDupes = false;
@ -97,21 +96,7 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple
distrs.add(new Distribution(distr)); distrs.add(new Distribution(distr));
} }
} }
if (mdp.actions != null) {
actions = new ArrayList<List<Object>>(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<Object> list = new ArrayList<Object>(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 // Copy flags/stats too
allowDupes = mdp.allowDupes; allowDupes = mdp.allowDupes;
numDistrs = mdp.numDistrs; numDistrs = mdp.numDistrs;
@ -151,21 +136,7 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple
distrs.add(new Distribution(distr, permut)); distrs.add(new Distribution(distr, permut));
} }
} }
if (mdp.actions != null) {
actions = new ArrayList<List<Object>>(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<Object> list = new ArrayList<Object>(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 // Copy flags/stats too
allowDupes = mdp.allowDupes; allowDupes = mdp.allowDupes;
numDistrs = mdp.numDistrs; numDistrs = mdp.numDistrs;
@ -213,7 +184,7 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple
for (int i = 0; i < numStates; i++) { for (int i = 0; i < numStates; i++) {
trans.add(new ArrayList<Distribution>()); trans.add(new ArrayList<Distribution>());
} }
actions = null;
actions = new ChoiceActionsSimple();
} }
@Override @Override
@ -230,8 +201,7 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple
} }
maxNumDistrsOk = false; maxNumDistrsOk = false;
trans.get(s).clear(); trans.get(s).clear();
if (actions != null && actions.get(s) != null)
actions.get(s).clear();
actions.clearState(s);
} }
@Override @Override
@ -246,8 +216,6 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple
{ {
for (int i = 0; i < numToAdd; i++) { for (int i = 0; i < numToAdd; i++) {
trans.add(new ArrayList<Distribution>()); trans.add(new ArrayList<Distribution>());
if (actions != null)
actions.add(null);
numStates++; numStates++;
} }
} }
@ -376,9 +344,6 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple
} }
set = trans.get(s); set = trans.get(s);
set.add(distr); set.add(distr);
// Add null action if necessary
if (actions != null && actions.get(s) != null)
actions.get(s).add(null);
// Update stats // Update stats
numDistrs++; numDistrs++;
maxNumDistrs = Math.max(maxNumDistrs, set.size()); maxNumDistrs = Math.max(maxNumDistrs, set.size());
@ -407,11 +372,8 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple
} }
set = trans.get(s); set = trans.get(s);
set.add(distr); set.add(distr);
// Add null action if necessary
if (actions != null && actions.get(s) != null)
actions.get(s).add(null);
// Set action // Set action
setAction(s, set.size() - 1, action);
actions.setAction(s, set.size() - 1, action);
// Update stats // Update stats
numDistrs++; numDistrs++;
maxNumDistrs = Math.max(maxNumDistrs, set.size()); 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) 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<List<Object>>(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<Object> list = new ArrayList<Object>(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) // Accessors (for Model)
@ -522,10 +465,7 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple
@Override @Override
public Object getAction(int s, int i) public Object getAction(int s, int i)
{ {
List<Object> list;
if (i < 0 || actions == null || (list = actions.get(s)) == null)
return null;
return list.get(i);
return actions.getAction(s, i);
} }
@Override @Override

20
prism/src/explicit/MDPSparse.java
View File

@ -188,7 +188,7 @@ public class MDPSparse extends MDPExplicit
*/ */
public MDPSparse(MDPSimple mdp, boolean sort) public MDPSparse(MDPSimple mdp, boolean sort)
{ {
int i, j, k, n;
int i, j, k;
TreeMap<Integer, Double> sorted = null; TreeMap<Integer, Double> sorted = null;
initialise(mdp.getNumStates()); initialise(mdp.getNumStates());
copyFrom(mdp); copyFrom(mdp);
@ -204,16 +204,9 @@ public class MDPSparse extends MDPExplicit
cols = new int[numTransitions]; cols = new int[numTransitions];
choiceStarts = new int[numDistrs + 1]; choiceStarts = new int[numDistrs + 1];
rowStarts = new int[numStates + 1]; rowStarts = new int[numStates + 1];
actions = mdp.actions == null ? null : new Object[numDistrs];
j = k = 0; j = k = 0;
for (i = 0; i < numStates; i++) { for (i = 0; i < numStates; i++) {
rowStarts[i] = j; 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)) { for (Distribution distr : mdp.trans.get(i)) {
choiceStarts[j] = k; choiceStarts[j] = k;
for (Map.Entry<Integer, Double> e : distr) { for (Map.Entry<Integer, Double> e : distr) {
@ -238,6 +231,7 @@ public class MDPSparse extends MDPExplicit
} }
choiceStarts[numDistrs] = numTransitions; choiceStarts[numDistrs] = numTransitions;
rowStarts[numStates] = numDistrs; 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[]) public MDPSparse(MDPSimple mdp, boolean sort, int permut[])
{ {
int i, j, k, n;
int i, j, k;
TreeMap<Integer, Double> sorted = null; TreeMap<Integer, Double> sorted = null;
int permutInv[]; int permutInv[];
initialise(mdp.getNumStates()); initialise(mdp.getNumStates());
@ -274,16 +268,9 @@ public class MDPSparse extends MDPExplicit
cols = new int[numTransitions]; cols = new int[numTransitions];
choiceStarts = new int[numDistrs + 1]; choiceStarts = new int[numDistrs + 1];
rowStarts = new int[numStates + 1]; rowStarts = new int[numStates + 1];
actions = mdp.actions == null ? null : new Object[numDistrs];
j = k = 0; j = k = 0;
for (i = 0; i < numStates; i++) { for (i = 0; i < numStates; i++) {
rowStarts[i] = j; 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])) { for (Distribution distr : mdp.trans.get(permutInv[i])) {
choiceStarts[j] = k; choiceStarts[j] = k;
for (Map.Entry<Integer, Double> e : distr) { for (Map.Entry<Integer, Double> e : distr) {
@ -308,6 +295,7 @@ public class MDPSparse extends MDPExplicit
} }
choiceStarts[numDistrs] = numTransitions; choiceStarts[numDistrs] = numTransitions;
rowStarts[numStates] = numDistrs; rowStarts[numStates] = numDistrs;
actions = mdp.actions.convertToSparseStorage(mdp);
} }
/** /**

Write Preview
Loading…
Cancel
Save