Some additions to Strategy classes + better integration of symbolic strategy generation.

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

prism/src/prism/NondetModelChecker.java

@@ -1961,14 +1961,13 @@ public class NondetModelChecker extends NonProbModelChecker
 				case Prism.SPARSE:
 					IntegerVector strat = null;
 					if (genStrat) {
-						strat = new IntegerVector((int) model.getNumStates());
+						JDDNode ddStrat = JDD.ITE(yes, JDD.Constant(-2), JDD.Constant(-1));
+						strat = new IntegerVector(ddStrat, allDDRowVars, odd);
+						JDD.Deref(ddStrat);
 					}
 					probsDV = PrismSparse.NondetUntil(tr, tra, model.getSynchs(), odd, allDDRowVars, allDDColVars, allDDNondetVars, yes, maybe, min, strat);
 					if (genStrat) {
-						mainLog.println();
-						MDStrategyIV strategy = new MDStrategyIV(model, strat);
-						strategy.exportActions(mainLog);
-						strategy.clear();
+						result.setStrategy(new MDStrategyIV(model, strat));
 					}
 					probs = new StateValuesDV(probsDV, model);
 					break;

prism/src/sparse/PS_NondetUntil.cc

@@ -179,14 +179,19 @@ jlong _strat				// strategy storage
 	// if required, create storage for adversary and initialise
 	if (export_adv_enabled != EXPORT_ADV_NONE || strat != NULL) {
 		PS_PrintToMainLog(env, "Allocating adversary vector... ");
-		adv = (strat == NULL) ? new int[n] : strat;
+		// Use passed in (pre-filled) array, if provided
+		if (strat) {
+			adv = strat;
+		} else {
+			adv = new int[n];
+			// Initialise all entries to -1 ("don't know")
+			for (i = 0; i < n; i++) {
+				adv[i] = -1;
+			}
+		}
 		kb = n*sizeof(int)/1024.0;
 		kbt += kb;
 		PS_PrintMemoryToMainLog(env, "[", kb, "]\n");
-		// Initialise all entries to -1 ("don't know")
-		for (i = 0; i < n; i++) {
-			adv[i] = -1;
-		}
 	}
 	
 	// print total memory usage
@@ -362,7 +367,7 @@ jlong _strat				// strategy storage
 	if (ndsm) delete ndsm;
 	if (yes_vec) delete[] yes_vec;
 	if (soln2) delete[] soln2;
-	//if (strat == NULL && adv) delete[] adv;
+	if (strat == NULL && adv) delete[] adv;
 	if (actions != NULL) {
 		delete[] actions;
 		release_string_array_from_java(env, action_names_jstrings, action_names, num_actions);

prism/src/strat/MDStrategy.java

@@ -39,12 +39,17 @@ public abstract class MDStrategy implements Strategy
 	 */
 	public abstract int getNumStates();
 
+	/**
+	 * Get the type of choice information stored for state s.
+	 */
+	public abstract Strategy.Choice getChoice(int s);
+
 	/**
 	 * 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);
+	public abstract int getChoiceIndex(int s);
 
 	/**
 	 * Get the action taken in state s.
@@ -57,7 +62,7 @@ public abstract class MDStrategy implements Strategy
 		int n = getNumStates();
 		for (int s = 0; s < n; s++) {
 			// Only print actions for reachable states
-			if (getChoice(s) != -3)
+			if (getChoice(s) != Choice.UNREACHABLE)
 				out.println(s + ":" + getChoiceAction(s));
 		}
 	}

prism/src/strat/MDStrategyArray.java

@@ -48,6 +48,8 @@ public class MDStrategyArray extends MDStrategy
 		this.choices = choices;
 	}
 	
+	// Methods for MDStrategy
+	
 	@Override
 	public int getNumStates()
 	{
@@ -55,7 +57,22 @@ public class MDStrategyArray extends MDStrategy
 	}
 	
 	@Override
-	public int getChoice(int s)
+	public Strategy.Choice getChoice(int s)
+	{
+		switch (choices[s]) {
+		case -1:
+			return Choice.UNKNOWN;
+		case -2:
+			return Choice.ARBITRARY;
+		case -3:
+			return Choice.UNREACHABLE;
+		default:
+			return Choice.INDEX;
+		}
+	}
+	
+	@Override
+	public int getChoiceIndex(int s)
 	{
 		return choices[s];
 	}
@@ -66,4 +83,12 @@ public class MDStrategyArray extends MDStrategy
 		int c = choices[s];
 		return c >= 0 ? model.getAction(s, c) : c == -1 ? "?" : c == -2 ? "*" : "-";
 	}
+
+	// Methods for Strategy
+	
+	@Override
+	public void clear()
+	{
+		choices = null;
+	}
 }

prism/src/strat/MDStrategyIV.java

@@ -31,34 +31,23 @@ import java.util.List;
 import dv.IntegerVector;
 
 import prism.Model;
+import strat.Strategy.Choice;
 
 /**
- * Class to store a memoryless deterministic (MD) strategy, as a IntegerVector (i.e. stored natively as an array).
+ * Class to store a memoryless deterministic (MD) strategy, as an IntegerVector (i.e. stored natively as an array).
  */
 public class MDStrategyIV extends MDStrategy
 {
 	// Model associated with the strategy
 	private Model model;
-	
-	private IntegerVector iv;
-	
-	private List<String> actions;
-	
+	// Other model info
 	private int numStates;
-	private long ptr;
-	
-	/**
-	 * Creates...
-	 */
-	public MDStrategyIV(Model model)
-	{
-		this.model = model;
-		numStates = (int) model.getNumStates();
-		actions = model.getSynchs();
-	}
+	private List<String> actions;
+	// Array storing MD strategy (action index for each state)
+	private IntegerVector iv;
 	
 	/**
-	 * Creates...
+	 * Create an MDStrategyIV from an IntegerVector.
 	 */
 	public MDStrategyIV(Model model, IntegerVector iv)
 	{
@@ -68,10 +57,7 @@ public class MDStrategyIV extends MDStrategy
 		this.iv = iv;
 	}
 	
-	public void setPointer(long ptr)
-	{
-		this.ptr = ptr;
-	}
+	// Methods for MDStrategy
 	
 	@Override
 	public int getNumStates()
@@ -80,19 +66,37 @@ public class MDStrategyIV extends MDStrategy
 	}
 	
 	@Override
-	public int getChoice(int s)
+	public Strategy.Choice getChoice(int s)
+	{
+		int c = iv.getElement(s);
+		switch (c) {
+		case -1:
+			return Choice.UNKNOWN;
+		case -2:
+			return Choice.ARBITRARY;
+		case -3:
+			return Choice.UNREACHABLE;
+		default:
+			return Choice.INDEX;
+		}
+	}
+	
+	@Override
+	public int getChoiceIndex(int s)
 	{
-		return 99;
+		throw new UnsupportedOperationException();
 	}
 	
 	@Override
 	public Object getChoiceAction(int s)
 	{
 		int c = iv.getElement(s);
-		//return ""+c; //c >= 0 ? actions.get(c) : "?";
 		return c >= 0 ? actions.get(c) : c == -1 ? "?" : c == -2 ? "*" : "-";
 	}
 	
+	// Methods for Strategy
+	
+	@Override
 	public void clear()
 	{
 		iv.clear();

prism/src/strat/Strategy.java

@@ -34,8 +34,18 @@ import prism.PrismLog;
  */
 public interface Strategy
 {
+	// Types of info stored for each choice
+	public enum Choice {
+		INDEX, ACTION, UNKNOWN, ARBITRARY, UNREACHABLE;
+	};
+	
 	/**
 	 * Export the strategy to a PrismLog, displaying strategy choices as action names.
 	 */
 	public void exportActions(PrismLog out);
+	
+	/**
+	 * Clear storage of the strategy.
+	 */
+	public void clear();
 }