Add -exportstrat switch (currently operates in parallel to -exportadv switch).

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

prism/src/explicit/MDPModelChecker.java

@@ -324,7 +324,6 @@ public class MDPModelChecker extends ProbModelChecker
 		int i, n, numYes, numNo;
 		long timer, timerProb0, timerProb1;
 		int strat[] = null;
-		boolean genStrat;
 		// Local copy of setting
 		MDPSolnMethod mdpSolnMethod = this.mdpSolnMethod;
 
@@ -342,9 +341,6 @@ public class MDPModelChecker extends ProbModelChecker
 				throw new PrismException("Value iteration from above only works for minimum probabilities");
 		}
 
-		// Are we generating an optimal strategy?
-		genStrat = exportAdv;
-
 		// Start probabilistic reachability
 		timer = System.currentTimeMillis();
 		mainLog.println("\nStarting probabilistic reachability (" + (min ? "min" : "max") + ")...");
@@ -357,7 +353,7 @@ public class MDPModelChecker extends ProbModelChecker
 
 		// If required, create/initialise strategy storage
 		// Set all choices to -1, denoting unknown/arbitrary
-		if (genStrat) {
+		if (genStrat || exportAdv) {
 			strat = new int[n];
 			for (i = 0; i < n; i++) {
 				strat[i] = -1;
@@ -397,7 +393,7 @@ public class MDPModelChecker extends ProbModelChecker
 		// 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 (genStrat) {
+		if (genStrat || exportAdv) {
 			if (min) {
 				for (i = yes.nextSetBit(0); i >= 0; i = yes.nextSetBit(i + 1)) {
 					if (!target.get(i))
@@ -442,7 +438,7 @@ public class MDPModelChecker extends ProbModelChecker
 			res.strat = new MDStrategyArray(strat);
 		}
 		// Export adversary
-		if (genStrat && exportAdv) {
+		if (exportAdv) {
 			// Prune strategy
 			restrictStrategyToReachableStates(mdp, strat);
 			// Print strategy
@@ -1189,7 +1185,6 @@ public class MDPModelChecker extends ProbModelChecker
 		int i, n, numTarget, numInf;
 		long timer, timerProb1;
 		int strat[] = null;
-		boolean genStrat;
 		// Local copy of setting
 		MDPSolnMethod mdpSolnMethod = this.mdpSolnMethod;
 
@@ -1199,9 +1194,6 @@ public class MDPModelChecker extends ProbModelChecker
 			mainLog.printWarning("Switching to MDP solution method \"" + mdpSolnMethod.fullName() + "\"");
 		}
 
-		// Are we generating an optimal strategy?
-		genStrat = exportAdv;
-
 		// Start expected reachability
 		timer = System.currentTimeMillis();
 		mainLog.println("\nStarting expected reachability (" + (min ? "min" : "max") + ")...");
@@ -1214,7 +1206,7 @@ public class MDPModelChecker extends ProbModelChecker
 
 		// If required, create/initialise strategy storage
 		// Set all choices to -1, denoting unknown/arbitrary
-		if (genStrat) {
+		if (genStrat || exportAdv) {
 			strat = new int[n];
 			for (i = 0; i < n; i++) {
 				strat[i] = -1;
@@ -1242,7 +1234,7 @@ public class MDPModelChecker extends ProbModelChecker
 		mainLog.println("target=" + numTarget + ", inf=" + numInf + ", rest=" + (n - (numTarget + numInf)));
 
 		// If required, generate strategy for "inf" states.
-		if (genStrat) {
+		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. 
@@ -1277,7 +1269,7 @@ public class MDPModelChecker extends ProbModelChecker
 		}
 
 		// Export adversary
-		if (genStrat && exportAdv) {
+		if (exportAdv) {
 			// Prune strategy
 			restrictStrategyToReachableStates(mdp, strat);
 			// Print strategy

prism/src/prism/PrismCL.java

@@ -81,6 +81,7 @@ public class PrismCL implements PrismModelListener
 	private boolean exportModelNoBasename = false;
 	private int exportType = Prism.EXPORT_PLAIN;
 	private boolean exportordered = true;
+	private boolean exportstrat = false;
 	private boolean simulate = false;
 	private boolean simpath = false;
 	private boolean param = false;
@@ -130,6 +131,7 @@ public class PrismCL implements PrismModelListener
 	private String exportResultsFilename = null;
 	private String exportSteadyStateFilename = null;
 	private String exportTransientFilename = null;
+	private String exportStratFilename = null;
 	private String simpathFilename = null;
 
 	// logs
@@ -1241,6 +1243,14 @@ public class PrismCL implements PrismModelListener
 						errorAndExit("No file specified for -" + sw + " switch");
 					}
 				}
+				// export strategy
+				else if (sw.equals("exportstrat")) {
+					if (i < args.length - 1) {
+						processExportStratSwitch(args[++i]);
+					} else {
+						errorAndExit("No file/options specified for -" + sw + " switch");
+					}
+				}
 				// export prism model to file
 				else if (sw.equals("exportprism")) {
 					if (i < args.length - 1) {
@@ -1729,6 +1739,33 @@ public class PrismCL implements PrismModelListener
 		}
 	}
 
+	/**
+	 * Process the arguments (files, options) to the -exportstrat switch
+	 */
+	private void processExportStratSwitch(String filesOptionsString) throws PrismException
+	{
+		// Split into files/options (on :)
+		String halves[] = splitFilesAndOptions(filesOptionsString);
+		String fileString = halves[0];
+		String optionsString = halves[1];
+		// Store some settings (here and in PRISM)
+		exportstrat = true;
+		exportStratFilename = fileString;
+		prism.setGenStrat(true);
+		// Process options
+		String options[] = optionsString.split(",");
+		for (String opt : options) {
+			// Ignore ""
+			if (opt.equals("")) {
+			}
+			// TODO: add some options
+			// Unknown option
+			else {
+				throw new PrismException("Unknown option \"" + opt + "\" for -exportstrat switch");
+			}
+		}
+	}
+
 	/**
 	 * Split a string of the form <files>:<options> into its two parts.
 	 * The latter can be empty, in which case the : is optional.