diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index cd611c39..68536479 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/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 diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index de160835..ec764659 100644 --- a/prism/src/prism/PrismCL.java +++ b/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 : into its two parts. * The latter can be empty, in which case the : is optional.