Update strategy generation in explicit engine to distinguish between: -1 (unknown), -2 (arbitrary), -3 (unreachable).

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

prism/src/explicit/MDPModelChecker.java

@@ -352,15 +352,6 @@ public class MDPModelChecker extends ProbModelChecker
 		// Store num states
 		n = mdp.getNumStates();
 
-		// If required, create/initialise strategy storage
-		// Set all choices to -1, denoting unknown/arbitrary
-		if (genStrat || exportAdv) {
-			strat = new int[n];
-			for (i = 0; i < n; i++) {
-				strat[i] = -1;
-			}
-		}
-
 		// Optimise by enlarging target set (if more info is available)
 		targetOrig = target;
 		if (init != null && known != null) {
@@ -370,6 +361,16 @@ public class MDPModelChecker extends ProbModelChecker
 			}
 		}
 
+		// If required, create/initialise strategy storage
+		// Set choices to -1, denoting unknown
+		// (except for target states, which are -2, denoting arbitrary)
+		if (genStrat || exportAdv) {
+			strat = new int[n];
+			for (i = 0; i < n; i++) {
+				strat[i] = target.get(i) ? -2 : -1;
+			}
+		}
+
 		// Precomputation
 		timerProb0 = System.currentTimeMillis();
 		if (precomp && prob0) {
@@ -391,18 +392,17 @@ public class MDPModelChecker extends ProbModelChecker
 		numNo = no.cardinality();
 		mainLog.println("target=" + target.cardinality() + ", yes=" + numYes + ", no=" + numNo + ", maybe=" + (n - (numYes + numNo)));
 
-		// If still required, generate strategy for no/yes (0/1) states.
-		// This is just for the cases max=0 and min=1, where arbitrary choices suffice.
-		// So just pick the first choice (0) for all these. 
+		// If still required, store strategy for no/yes (0/1) states.
+		// This is just for the cases max=0 and min=1, where arbitrary choices suffice (denoted by -2)
 		if (genStrat || exportAdv) {
 			if (min) {
 				for (i = yes.nextSetBit(0); i >= 0; i = yes.nextSetBit(i + 1)) {
 					if (!target.get(i))
-						strat[i] = 0;
+						strat[i] = -2;
 				}
 			} else {
 				for (i = no.nextSetBit(0); i >= 0; i = no.nextSetBit(i + 1)) {
-					strat[i] = 0;
+					strat[i] = -2;
 				}
 			}
 		}
@@ -1205,15 +1205,6 @@ public class MDPModelChecker extends ProbModelChecker
 		// Store num states
 		n = mdp.getNumStates();
 
-		// If required, create/initialise strategy storage
-		// Set all choices to -1, denoting unknown/arbitrary
-		if (genStrat || exportAdv) {
-			strat = new int[n];
-			for (i = 0; i < n; i++) {
-				strat[i] = -1;
-			}
-		}
-
 		// Optimise by enlarging target set (if more info is available)
 		if (init != null && known != null) {
 			BitSet targetNew = new BitSet(n);
@@ -1223,6 +1214,16 @@ public class MDPModelChecker extends ProbModelChecker
 			target = targetNew;
 		}
 
+		// If required, create/initialise strategy storage
+		// Set choices to -1, denoting unknown
+		// (except for target states, which are -2, denoting arbitrary)
+		if (genStrat || exportAdv) {
+			strat = new int[n];
+			for (i = 0; i < n; i++) {
+				strat[i] = target.get(i) ? -2 : -1;
+			}
+		}
+		
 		// Precomputation (not optional)
 		timerProb1 = System.currentTimeMillis();
 		inf = prob1(mdp, null, target, !min, null);
@@ -1237,10 +1238,10 @@ public class MDPModelChecker extends ProbModelChecker
 		// If required, generate strategy for "inf" states.
 		if (genStrat || exportAdv) {
 			if (min) {
-				// If min reward is infinite, all choices give infinity.
-				// So just pick the first choice (0) for all "inf" states. 
+				// If min reward is infinite, all choices give infinity
+				// So the choice can be arbitrary, denoted by -2; 
 				for (i = inf.nextSetBit(0); i >= 0; i = inf.nextSetBit(i + 1)) {
-					strat[i] = 0;
+					strat[i] = -2;
 				}
 			} else {
 				// If max reward is infinite, there is at least one choice giving infinity.
@@ -1535,7 +1536,7 @@ public class MDPModelChecker extends ProbModelChecker
 		// Set strategy choice for non-reachable state to -1
 		int n = mdp.getNumStates();
 		for (int s = restrict.nextClearBit(0); s < n; s = restrict.nextClearBit(s + 1)) {
-			strat[s] = -1;
+			strat[s] = -3;
 		}
 	}
 

prism/src/explicit/MDPSimple.java

@@ -537,7 +537,7 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple
 	public Object getAction(int s, int i)
 	{
 		List<Object> list;
-		if (actions == null || (list = actions.get(s)) == null)
+		if (i < 0 || actions == null || (list = actions.get(s)) == null)
 			return null;
 		return list.get(i);
 	}

prism/src/explicit/MDPSparse.java

@@ -499,7 +499,7 @@ public class MDPSparse extends MDPExplicit
 	@Override
 	public Object getAction(int s, int i)
 	{
-		return actions == null ? null : actions[rowStarts[s] + i];
+		return i < 0 || actions == null ? null : actions[rowStarts[s] + i];
 	}
 
 	@Override

prism/src/strat/MDStrategy.java

@@ -42,6 +42,7 @@ public abstract class MDStrategy implements Strategy
 	/**
 	 * Get the index of the choice taken in state s.
 	 * The index is defined with respect to a particular model, stored locally.
+	 * Other possible values: -1 (unknown), -2 (arbitrary), -3 (unreachable)
 	 */
 	public abstract int getChoice(int s);
 
@@ -55,7 +56,9 @@ public abstract class MDStrategy implements Strategy
 	{
 		int n = getNumStates();
 		for (int s = 0; s < n; s++) {
-			out.println(s + ":" + getChoiceAction(s));
+			// Only print actions for reachable states
+			if (getChoice(s) != -3)
+				out.println(s + ":" + getChoiceAction(s));
 		}
 	}
 }

prism/src/strat/MDStrategyArray.java

@@ -34,7 +34,8 @@ public class MDStrategyArray extends MDStrategy
 {
 	// Model associated with the strategy
 	private explicit.NondetModel model;
-	// Index of choice taken in each state 
+	// Index of choice taken in each state (wrt model above) 
+	// Other possible values: -1 (unknown), -2 (arbitrary), -3 (unreachable)
 	private int choices[];
 	
 	/**
@@ -62,6 +63,7 @@ public class MDStrategyArray extends MDStrategy
 	@Override
 	public Object getChoiceAction(int s)
 	{
-		return model.getAction(s, choices[s]);
+		int c = choices[s];
+		return c >= 0 ? model.getAction(s, c) : c == -1 ? "?" : c == -2 ? "*" : "-";
 	}
 }