diff --git a/prism/src/explicit/STPG.java b/prism/src/explicit/STPG.java
index 309ddefb..0e6f1e6a 100644
--- a/prism/src/explicit/STPG.java
+++ b/prism/src/explicit/STPG.java
@@ -27,18 +27,75 @@
package explicit;
import java.util.*;
+import java.util.Map.Entry;
+
import explicit.rewards.STPGRewards;
/**
- * Interface for classes that provide (read) access to an explicit-state stochastic two-player game (STPG),
+ * Interface for classes that provide (read) access to an explicit-state stochastic two-player game (STPG).
+ *
+ * These are turn-based STPGs, i.e. at most one player controls each state.
+ * Probabilistic states do not need to be stored explicitly; instead, like in an MDP,
+ * players have several 'choices', each of which is a probability distribution over successor states.
+ *
+ * For convenience/efficiency, STPGs can actually store two transitions/choices in two ways.
+ * The first is as described above: a state has a list of choices which are distributions over states.
+ * {@link #getNumChoices(s)} gives the number of choices, {@link #getAction(s)} gives an (optional) action label
+ * for each one and {@link #getTransitionsIterator(s, i)} provides an iterator over target-state/probability pairs.
+ * The second way is 'nested' choices: the choices in a state are instead transitions directly to states of the other player.
+ * Each of those states then has has several choices that are distributions over states, as above.
+ * The middle layer of states are not stored explicitly, however. If the {@code i}th choice of state {@code s}
+ * is nested in this way, then {@link #isChoiceNested(s, i)} is true and {@link #getTransitionsIterator(s, i)} returns null.
+ * Use {@link #getNumNestedChoices(s, i)}, {@link #getNestedAction(s, i)} and {@link #getNestedTransitionsIterator(s, i, j)}
+ * to access the information.
*/
public interface STPG extends Model
{
/**
- * Get the action label (if any) for choice i of state s.
+ * Get the player (1 or 2) for state {@code s}.
+ */
+ public int getPlayer(int s);
+
+ /**
+ * Get the action label (if any) for choice {@code i} of state {@code s}.
*/
public Object getAction(int s, int i);
+ /**
+ * 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}.
+ */
+ public Iterator> getTransitionsIterator(int s, int i);
+
+ /**
+ * Is choice {@code i} of state {@code s} in nested form? (See {@link explicit.STPG} for details)
+ */
+ public boolean isChoiceNested(int s, int i);
+
+ /**
+ * Get the number of (nested) choices in choice {@code i} of state {@code s}.
+ */
+ public int getNumNestedChoices(int s, int i);
+
+ /**
+ * Get the action label (if any) for nested choice {@code i,j} of state {@code s}.
+ */
+ public Object getNestedAction(int s, int i, int j);
+
+ /**
+ * Get the number of transitions from nested choice {@code i,j} of state {@code s}.
+ */
+ public int getNumNestedTransitions(int s, int i, int j);
+
+ /**
+ * Get an iterator over the transitions from nested choice {@code i,j} of state {@code s}.
+ */
+ public Iterator> getNestedTransitionsIterator(int s, int i, int j);
+
/**
* Perform a single step of precomputation algorithm Prob0, i.e., for states i in {@code subset},
* set bit i of {@code result} iff, for all/some player 1 choices, for all/some player 2 choices,
@@ -51,7 +108,7 @@ public interface STPG extends Model
* @param result Store results here
*/
public void prob0step(BitSet subset, BitSet u, boolean forall1, boolean min2, BitSet result);
-
+
/**
* Perform a single step of precomputation algorithm Prob1, i.e., for states i in {@code subset},
* set bit i of {@code result} iff, for all/some player 1 choices, for all/some player 2 choices,
@@ -65,7 +122,7 @@ public interface STPG extends Model
* @param result Store results here
*/
public void prob1step(BitSet subset, BitSet u, BitSet v, boolean min1, boolean min2, BitSet result);
-
+
/**
* Do a matrix-vector multiplication followed by two min/max ops, i.e. one step of value iteration,
* i.e. for all s: result[s] = min/max_{k1,k2} { sum_j P_{k1,k2}(s,j)*vect[j] }
diff --git a/prism/src/explicit/STPGAbstrSimple.java b/prism/src/explicit/STPGAbstrSimple.java
index 4d2c6d61..41547d09 100644
--- a/prism/src/explicit/STPGAbstrSimple.java
+++ b/prism/src/explicit/STPGAbstrSimple.java
@@ -28,6 +28,7 @@
package explicit;
import java.util.*;
+import java.util.Map.Entry;
import java.io.*;
import explicit.rewards.STPGRewards;
@@ -453,13 +454,87 @@ public class STPGAbstrSimple extends ModelSimple implements STPG
// Accessors (for STPG)
+ @Override
+ public int getPlayer(int s)
+ {
+ // All states are player 1
+ return 1;
+ }
+
@Override
public Object getAction(int s, int i)
{
- // TODO
+ // No actions stored currently
+ return null;
+ }
+
+ @Override
+ public int getNumTransitions(int s, int i)
+ {
+ // All choices are nested
+ return 0;
+ }
+
+ @Override
+ public Iterator> getTransitionsIterator(int s, int i)
+ {
+ // All choices are nested
return null;
}
+ @Override
+ public boolean isChoiceNested(int s, int i)
+ {
+ // All choices are nested
+ return true;
+ }
+
+ @Override
+ public int getNumNestedChoices(int s, int i)
+ {
+ return trans.get(s).get(i).size();
+ }
+
+ @Override
+ public Object getNestedAction(int s, int i, int j)
+ {
+ return trans.get(s).get(i).getAction();
+ }
+
+ @Override
+ public int getNumNestedTransitions(int s, int i, int j)
+ {
+ DistributionSet ds = trans.get(s).get(i);
+ Iterator iter = ds.iterator();
+ Distribution distr = null;
+ int k = 0;
+ while (iter.hasNext() && k <= j) {
+ distr = iter.next();
+ k++;
+ }
+ if (k <= j)
+ return 0;
+ else
+ return distr.size();
+ }
+
+ @Override
+ public Iterator> getNestedTransitionsIterator(int s, int i, int j)
+ {
+ DistributionSet ds = trans.get(s).get(i);
+ Iterator iter = ds.iterator();
+ Distribution distr = null;
+ int k = 0;
+ while (iter.hasNext() && k <= j) {
+ distr = iter.next();
+ k++;
+ }
+ if (k <= j)
+ return null;
+ else
+ return distr.iterator();
+ }
+
@Override
public void prob0step(BitSet subset, BitSet u, boolean forall1, boolean forall2, BitSet result)
{