Strategy synthesis for reach rewards in the explicit engine: choices for inf states and do export.

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

prism/src/explicit/MDP.java

@@ -65,14 +65,21 @@ public interface MDP extends Model
 	public Iterator<Entry<Integer, Double>> getTransitionsIterator(int s, int i);
 
 	/**
-	 * Check if all the successor states from choice {@code i} of state {@code s} are in the set  {@code set}.
-	 * Get an iterator over the transitions .
+	 * 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
 	 * @param i Choice index
 	 * @param set The set to test for inclusion
 	 */
 	public boolean allSuccessorsInSet(int s, int i, BitSet set);
 	
+	/**
+	 * Check if some successor state from choice {@code i} of state {@code s} is in the set {@code set}.
+	 * @param s The state to check
+	 * @param i Choice index
+	 * @param set The set to test for inclusion
+	 */
+	public boolean someSuccessorsInSet(int s, int i, BitSet set);
+	
 	/**
 	 * 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 choices,

prism/src/explicit/MDPModelChecker.java

@@ -1235,6 +1235,29 @@ public class MDPModelChecker extends ProbModelChecker
 		numInf = inf.cardinality();
 		mainLog.println("target=" + numTarget + ", inf=" + numInf + ", rest=" + (n - (numTarget + numInf)));
 
+		// If required, generate strategy for "inf" states.
+		if (genStrat) {
+			if (min) {
+				// If min reward is infinite, all choices give infinity.
+				// So just pick the first choice (0) for all "inf" states. 
+				for (i = inf.nextSetBit(0); i >= 0; i = inf.nextSetBit(i + 1)) {
+					strat[i] = 0;
+				}
+			} else {
+				// If max reward is infinite, there is at least one choice giving infinity.
+				// So we pick, for all "inf" states, the first choice for which some transitions stays in "inf".
+				for (i = inf.nextSetBit(0); i >= 0; i = inf.nextSetBit(i + 1)) {
+					int numChoices = mdp.getNumChoices(i);
+					for (int k = 0; k < numChoices; k++) {
+						if (mdp.allSuccessorsInSet(i, k, inf)) {
+							strat[i] = k;
+							continue;
+						}
+					}
+				}
+			}
+		}
+
 		// Compute rewards
 		switch (mdpSolnMethod) {
 		case VALUE_ITERATION:
@@ -1247,6 +1270,21 @@ public class MDPModelChecker extends ProbModelChecker
 			throw new PrismException("Unknown MDP solution method " + mdpSolnMethod.fullName());
 		}
 
+		// Export adversary
+		if (genStrat && exportAdv) {
+			// Prune strategy
+			restrictStrategyToReachableStates(mdp, strat);
+			// Print strategy
+			mainLog.print("Strat:");
+			for (i = 0; i < n; i++) {
+				mainLog.print(" " + i + ":" + strat[i]);
+			}
+			mainLog.println();
+			// Export
+			PrismLog out = new PrismFileLog(exportAdvFilename);
+			new DTMCFromMDPMemorylessAdversary(mdp, strat).exportToPrismExplicitTra(out);
+		}
+
 		// Finished expected reachability
 		timer = System.currentTimeMillis() - timer;
 		mainLog.println("Expected reachability took " + timer / 1000.0 + " seconds.");

prism/src/explicit/MDPSimple.java

@@ -560,6 +560,12 @@ public class MDPSimple extends MDPExplicit implements ModelSimple
 		return trans.get(s).get(i).isSubsetOf(set);
 	}
 	
+	@Override
+	public boolean someSuccessorsInSet(int s, int i, BitSet set)
+	{
+		return trans.get(s).get(i).containsOneOf(set);
+	}
+	
 	@Override
 	public void prob0step(BitSet subset, BitSet u, boolean forall, BitSet result)
 	{

prism/src/explicit/MDPSparse.java

@@ -577,7 +577,23 @@ public class MDPSparse extends MDPExplicit
 		}
 		return true;
 	}
-	
+
+	@Override
+	public boolean someSuccessorsInSet(int s, int i, BitSet set)
+	{
+		int j, k, l2, h2;
+		j = rowStarts[s] + i;
+		l2 = choiceStarts[j];
+		h2 = choiceStarts[j + 1];
+		for (k = l2; k < h2; k++) {
+			// Assume that only non-zero entries are stored
+			if (set.get(cols[k])) {
+				return true;
+			}
+		}
+		return false;
+	}
+
 	@Override
 	public void prob0step(BitSet subset, BitSet u, boolean forall, BitSet result)
 	{