Browse Source

Generalise MDPSimple copy constructor from MDPSparse to MDP.

Also requires updating ModelExplicit.copyFrom (to copy from Model).
accumulation-v4.7
Dave Parker 6 years ago
parent
commit
985e4516a5
  1. 45
      prism/src/explicit/MDPSimple.java
  2. 32
      prism/src/explicit/ModelExplicit.java

45
prism/src/explicit/MDPSimple.java

@ -35,6 +35,7 @@ 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 prism.PrismException;
@ -176,42 +177,28 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple
/**
* Construct an MDPSimple object from an MDPSparse one.
*/
public MDPSimple(MDPSparse mdp)
public MDPSimple(MDP mdp)
{
this(mdp.numStates);
this(mdp.getNumStates());
copyFrom(mdp);
// Copy storage directly to avoid worrying about duplicate distributions (and for efficiency)
for (int s = 0; s < numStates; s++) {
for (int c = 0; c < mdp.getNumChoices(s); c++) {
int numStates = getNumStates();
for (int i = 0; i < numStates; i++) {
int numChoices = getNumChoices(i);
for (int j = 0; j < numChoices; j++) {
Object action = getAction(i, j);
Distribution distr = new Distribution();
Iterator<Entry<Integer, Double>> it = mdp.getTransitionsIterator(s, c);
while (it.hasNext()) {
Entry<Integer, Double> entry = it.next();
distr.add(entry.getKey(), entry.getValue());
Iterator<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i, j);
while (iter.hasNext()) {
Map.Entry<Integer, Double> e = iter.next();
distr.set(e.getKey(), e.getValue());
}
this.addChoice(s, 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++) {
int n = mdp.getNumChoices(s);
List<Object> list = new ArrayList<Object>(n);
for (int i = 0; i < n; i++) {
list.add(mdp.getAction(s, i));
if (action == null) {
addActionLabelledChoice(i, distr, action);
} else {
addChoice(i, distr);
}
actions.set(s, list);
}
}
// Copy flags/stats too
allowDupes = false; // TODO check this
numDistrs = mdp.numDistrs;
numTransitions = mdp.numTransitions;
maxNumDistrs = mdp.maxNumDistrs;
maxNumDistrsOk = true; // TODO not sure
}
// Mutators (for ModelSimple)

32
prism/src/explicit/ModelExplicit.java

@ -77,47 +77,47 @@ public abstract class ModelExplicit implements Model
// Mutators
/**
* Copy data from another ModelExplicit (used by superclass copy constructors).
* Copy data from another Model (used by superclass copy constructors).
* Assumes that this has already been initialise()ed.
*/
public void copyFrom(ModelExplicit model)
public void copyFrom(Model model)
{
numStates = model.numStates;
for (int in : model.initialStates) {
numStates = model.getNumStates();
for (int in : model.getInitialStates()) {
addInitialState(in);
}
for (int dl : model.deadlocks) {
for (int dl : model.getDeadlockStates()) {
addDeadlockState(dl);
}
// Shallow copy of read-only stuff
statesList = model.statesList;
constantValues = model.constantValues;
labels = model.labels;
varList = model.varList;
statesList = model.getStatesList();
constantValues = model.getConstantValues();
labels = model.getLabelToStatesMap();
varList = model.getVarList();
}
/**
* Copy data from another ModelExplicit and a state index permutation,
* Copy data from another Model and a state index permutation,
* i.e. state index i becomes index permut[i]
* (used by superclass copy constructors).
* Assumes that this has already been initialise()ed.
* Pointer to states list is NOT copied (since now wrong).
*/
public void copyFrom(ModelExplicit model, int permut[])
public void copyFrom(Model model, int permut[])
{
numStates = model.numStates;
for (int in : model.initialStates) {
numStates = model.getNumStates();
for (int in : model.getInitialStates()) {
addInitialState(permut[in]);
}
for (int dl : model.deadlocks) {
for (int dl : model.getDeadlockStates()) {
addDeadlockState(permut[dl]);
}
// Shallow copy of (some) read-only stuff
// (i.e. info that is not broken by permute)
statesList = null;
constantValues = model.constantValues;
constantValues = model.getConstantValues();
labels.clear();
varList = model.varList;
varList = model.getVarList();
}
/**

Loading…
Cancel
Save