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

Some bugfixes and adds in explicit MDP classes, mainly relating to action labels. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3330 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 15 years ago
parent
edab23b581
commit
3403e8b417
2 changed files with 118 additions and 90 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 62
      prism/src/explicit/MDPSimple.java
  2. 146
      prism/src/explicit/MDPSparse.java

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

@ -49,7 +49,7 @@ public class MDPSimple extends ModelSimple implements MDP
protected List<List<Distribution>> 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<List<Object>> 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<Distribution> 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<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);
}
}
}
// 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<Distribution> 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<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);
}
}
}
// 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<List<Object>>(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

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

@ -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<Integer> states, List<List<Integer>> actions)
{
initialise(states.size());
for (int in : mdp.getInitialStates()) {
addInitialState(in);
}
// statesList = new ArrayList<State>(states.size());
statesList = new ArrayList<parser.State>();
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<Entry<Integer, Double>> it = mdp.getTransitionsIterator(s, a);
while (it.hasNext()) {
Entry<Integer, Double> 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<Integer> states, List<List<Integer>> actions)
{
initialise(states.size());
for (int in : mdp.getInitialStates()) {
addInitialState(in);
}
statesList = new ArrayList<State>();
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<Entry<Integer, Double>> it = mdp.getTransitionsIterator(s, a);
while (it.hasNext()) {
Entry<Integer, Double> 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 += "{";

Write Preview
Loading…
Cancel
Save