Browse Source

Remove getTransitionsIterator from NondetModel.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8861 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 12 years ago
parent
commit
afd1c35480
  1. 5
      prism/src/explicit/MDP.java
  2. 11
      prism/src/explicit/NondetModel.java
  3. 41
      prism/src/explicit/SubNondetModel.java

5
prism/src/explicit/MDP.java

@ -39,11 +39,6 @@ import explicit.rewards.MDPRewards;
*/
public interface MDP extends NondetModel
{
/**
* Get the number of transitions from choice {@code i} of state {@code s}.
*/
public int getNumTransitions(int s, int i);
/**
* Get an iterator over the transitions from choice {@code i} of state {@code s}.
*/

11
prism/src/explicit/NondetModel.java

@ -27,12 +27,8 @@
package explicit;
import java.util.BitSet;
import java.util.Iterator;
import java.util.Map.Entry;
import prism.PrismException;
import prism.PrismLog;
import strat.MDStrategy;
/**
@ -67,6 +63,11 @@ public interface NondetModel extends Model
*/
public boolean areAllChoiceActionsUnique();
/**
* Get the number of transitions from choice {@code i} of state {@code s}.
*/
public int getNumTransitions(int s, int i);
/**
* Check if all the successor states from choice {@code i} of state {@code s} are in the set {@code set}.
* @param s The state to check
@ -86,7 +87,7 @@ public interface NondetModel extends Model
/**
* Get an iterator over the transitions of state s and action i.
*/
public Iterator<Entry<Integer, Double>> getTransitionsIterator(int s, int i);
//public Iterator<Entry<Integer, Double>> getTransitionsIterator(int s, int i);
/**
* Construct a model that is induced by applying strategy {@code strat} to this model.

41
prism/src/explicit/SubNondetModel.java

@ -34,7 +34,6 @@ import java.util.HashMap;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import parser.State;
import parser.Values;
@ -150,8 +149,7 @@ public class SubNondetModel implements NondetModel
@Override
public List<State> getStatesList()
{
//We use lazy generation because in many cases the state list is not
//needed
// We use lazy generation because in many cases the state list is not needed
if (statesList == null) {
statesList = generateSubStateList(states);
}
@ -191,14 +189,13 @@ public class SubNondetModel implements NondetModel
public Iterator<Integer> getSuccessorsIterator(int s)
{
s = translateState(s);
List<Integer> succ = new ArrayList<Integer>();
for (int i = 0; i < model.getNumChoices(s); i++) {
if (actions.get(s).get(i)) {
Iterator<Entry<Integer, Double>> it = model.getTransitionsIterator(s, i);
Iterator<Integer> it = model.getSuccessorsIterator(s);
while (it.hasNext()) {
int succc = it.next().getKey();
succ.add(inverseTranslateState(succc));
int j = it.next();
succ.add(inverseTranslateState(j));
}
}
}
@ -361,6 +358,14 @@ public class SubNondetModel implements NondetModel
throw new RuntimeException("Not implemented");
}
@Override
public int getNumTransitions(int s, int i)
{
s = translateState(s);
i = translateAction(s, i);
return model.getNumTransitions(s, i);
}
@Override
public boolean allSuccessorsInSet(int s, int i, BitSet set)
{
@ -405,31 +410,13 @@ public class SubNondetModel implements NondetModel
{
int transitions = 0;
for (int i = 0; i < model.getNumChoices(state); i++) {
Iterator<Entry<Integer, Double>> it = model.getTransitionsIterator(state, i);
while (it.hasNext()) {
it.next();
transitions += 1;
if (actions.get(state).get(i)) {
transitions += model.getNumTransitions(state, i);
}
}
return transitions;
}
@Override
public Iterator<Entry<Integer, Double>> getTransitionsIterator(int s, int i)
{
s = translateState(s);
i = translateAction(s, i);
Map<Integer, Double> distrs = new HashMap<Integer, Double>();
Iterator<Entry<Integer, Double>> it = model.getTransitionsIterator(s, i);
while (it.hasNext()) {
Entry<Integer, Double> e = it.next();
int succ = inverseTranslateState(e.getKey());
distrs.put(succ, e.getValue());
}
return distrs.entrySet().iterator();
}
@Override
public Model constructInducedModel(MDStrategy strat)
{

Loading…
Cancel
Save