Revised/expanded STPG interface.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3401 bbc10eb1-c90d-0410-af57-cb519fbb1720

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).
+ * <br><br>
+ * 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.
+ * <br><br>
+ * 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<Entry<Integer, Double>> 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<Entry<Integer, Double>> 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] }

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<Entry<Integer,Double>> 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<Distribution> 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<Entry<Integer, Double>> getNestedTransitionsIterator(int s, int i, int j)
+	{
+		DistributionSet ds = trans.get(s).get(i);
+		Iterator<Distribution> 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)
 	{