diff --git a/prism/src/prism/ArgConsumer.java b/prism/src/prism/ArgConsumer.java new file mode 100644 index 000000000..b780ddb1e --- /dev/null +++ b/prism/src/prism/ArgConsumer.java @@ -0,0 +1,151 @@ +//============================================================================== +// +// Copyright (c) 2026- +// Authors: +// * Dave Parker (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package prism; + +/** + * Wraps a CLI argument array and current position for cleaner switch handling. + * Provides typed argument consumption that throws {@link PrismException}s on error. + */ +class ArgConsumer +{ + private final String[] args; + private int i; + private String optionsString; + + /** + * Creates a consumer over the full argument array, positioned before the first element. + * The caller drives iteration by calling {@link #advance()} then {@link #parseSwitch(String)}. + */ + ArgConsumer(String[] args) + { + this.args = args; + this.i = -1; + this.optionsString = null; + } + + /** + * Advances to and returns the next raw argument. + * The caller must check {@link #hasNext()} before calling this. + */ + String advance() + { + return args[++i]; + } + + /** + * Parses a raw CLI token as a switch: strips the leading {@code -} or {@code --}, + * splits on the first {@code :} to extract any sub-options, stores them in + * {@link #optionsString()}, and returns the switch name. + * Returns {@code null} if the token does not start with {@code -} (i.e. it is a filename). + * Throws if the switch name would be empty (bare {@code -} or {@code --}). + */ + String parseSwitch(String arg) throws PrismException + { + if (arg.isEmpty() || arg.charAt(0) != '-') { + optionsString = null; + return null; + } + String sw = arg.substring(1); + if (sw.isEmpty()) throw new PrismException("Invalid empty switch"); + if (sw.charAt(0) == '-') { + sw = sw.substring(1); + if (sw.isEmpty()) throw new PrismException("Invalid empty switch"); + } + int colon = sw.indexOf(':'); + if (colon == -1) { + optionsString = null; + return sw; + } + optionsString = sw.substring(colon + 1); + return sw.substring(0, colon); + } + + /** Colon sub-options from {@code -switch:opts} syntax (e.g. {@code "upper,lower"} from {@code -intervaliter:upper,lower}), or {@code null}. */ + String optionsString() + { + return optionsString; + } + + /** Returns the current index (updated by any {@code next*()} calls). */ + int index() + { + return i; + } + + /** Whether a next argument is available. */ + boolean hasNext() + { + return i < args.length - 1; + } + + /** Returns the next argument without consuming it, or {@code null} if there is none. */ + String peek() + { + return hasNext() ? args[i + 1] : null; + } + + /** Consume and return the next argument, or throw a descriptive error for switch {@code sw}. */ + String next(String sw) throws PrismException + { + if (!hasNext()) + throw new PrismException("No value specified for -" + sw + " switch"); + return args[++i]; + } + + /** Consume the next argument, parse it as an {@code int}, and return it. */ + int nextInt(String sw) throws PrismException + { + String s = next(sw); + try { + return Integer.parseInt(s); + } catch (NumberFormatException e) { + throw new PrismException("Invalid value \"" + s + "\" for -" + sw + " switch"); + } + } + + /** Consume the next argument, parse it as a {@code double}, and return it. */ + double nextDouble(String sw) throws PrismException + { + String s = next(sw); + try { + return Double.parseDouble(s); + } catch (NumberFormatException e) { + throw new PrismException("Invalid value \"" + s + "\" for -" + sw + " switch"); + } + } + + /** Consume the next argument, parse it as a {@code long}, and return it. */ + long nextLong(String sw) throws PrismException + { + String s = next(sw); + try { + return Long.parseLong(s); + } catch (NumberFormatException e) { + throw new PrismException("Invalid value \"" + s + "\" for -" + sw + " switch"); + } + } +} diff --git a/prism/src/prism/OptionParser.java b/prism/src/prism/OptionParser.java new file mode 100644 index 000000000..ef6993597 --- /dev/null +++ b/prism/src/prism/OptionParser.java @@ -0,0 +1,371 @@ +//============================================================================== +// +// Copyright (c) 2026- +// Authors: +// * Dave Parker (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package prism; + +import java.util.ArrayList; +import java.util.LinkedHashMap; +import java.util.List; +import java.util.function.IntPredicate; + +/** + * Builder for parsing a comma-separated list of sub-options within a CLI switch argument + * (e.g. the {@code opt1,key=val,...} portion of {@code -switch files:opt1,key=val,...}). + * Handles four option styles: bare flags, boolean {@code key=true|false}, fixed-choice + * {@code key=val}, and raw-string {@code key=anything}. + * + *

Each registration method has three variants: + *

+ * + *

All error messages include the option name and switch name automatically. + */ +class OptionParser +{ + @FunctionalInterface interface FlagAction { void run() throws PrismException; } + @FunctionalInterface interface StringAction { void accept(String v) throws PrismException; } + @FunctionalInterface interface BoolAction { void accept(boolean b) throws PrismException; } + @FunctionalInterface interface IntAction { void accept(int n) throws PrismException; } + + /** Internal handler for key=value options. */ + @FunctionalInterface + private interface ValueHandler + { + void accept(String key, String val, String switchName) throws PrismException; + } + + /** One entry in the human-readable option table printed by {@link #printOptions}. */ + private static class HelpEntry + { + final String type; // "flag", "bool", "string", "choice" + final String name; + final String argHint; // null for flag/bool; "" for string; "a/b/c" for choice + final String description; + + HelpEntry(String type, String name, String argHint, String description) + { + this.type = type; this.name = name; this.argHint = argHint; this.description = description; + } + } + + private final LinkedHashMap flagHandlers = new LinkedHashMap<>(); + private final LinkedHashMap valueHandlers = new LinkedHashMap<>(); + private final List helpEntries = new ArrayList<>(); + + // ── Flag options ────────────────────────────────────────────────────────── + + /** Register a bare flag option (action only, no help metadata). */ + OptionParser flag(String name, FlagAction action) + { + flagHandlers.put(name, action); + return this; + } + + /** Record a bare flag option for help output only (no execution handler). */ + OptionParser flag(String name, String description) + { + helpEntries.add(new HelpEntry("flag", name, null, description)); + return this; + } + + /** Register a bare flag option with both execution handler and help metadata. */ + OptionParser flag(String name, String description, FlagAction action) + { + flagHandlers.put(name, action); + helpEntries.add(new HelpEntry("flag", name, null, description)); + return this; + } + + // ── String options ──────────────────────────────────────────────────────── + + /** Register a {@code key=value} option (action only; action receives the raw value string). */ + OptionParser string(String name, StringAction action) + { + valueHandlers.put(name, (key, val, sw) -> action.accept(val)); + return this; + } + + /** Record a {@code key=} string option for help output only. */ + OptionParser string(String name, String argHint, String description) + { + helpEntries.add(new HelpEntry("string", name, argHint, description)); + return this; + } + + /** Register a {@code key=value} option with both execution handler and help metadata. */ + OptionParser string(String name, String argHint, String description, StringAction action) + { + valueHandlers.put(name, (key, val, sw) -> action.accept(val)); + helpEntries.add(new HelpEntry("string", name, argHint, description)); + return this; + } + + // ── Integer options ─────────────────────────────────────────────────────── + + /** Register a {@code key=} integer option (action only; no extra validation beyond being a valid int). */ + OptionParser integer(String name, IntAction action) + { + valueHandlers.put(name, intHandler(null, action)); + return this; + } + + /** Record a {@code key=} integer option for help output only. */ + OptionParser integer(String name, String argHint, String description) + { + helpEntries.add(new HelpEntry("string", name, argHint, description)); + return this; + } + + /** Register a {@code key=} integer option with both execution handler and help metadata (no extra validation). */ + OptionParser integer(String name, String argHint, String description, IntAction action) + { + valueHandlers.put(name, intHandler(null, action)); + helpEntries.add(new HelpEntry("string", name, argHint, description)); + return this; + } + + /** + * Register a {@code key=} integer option with both execution handler and help metadata, + * additionally validated by {@code valid} (e.g. a range check) beyond being a valid int. + */ + OptionParser integer(String name, String argHint, IntPredicate valid, String description, IntAction action) + { + valueHandlers.put(name, intHandler(valid, action)); + helpEntries.add(new HelpEntry("string", name, argHint, description)); + return this; + } + + /** Build a {@link ValueHandler} that parses an int, optionally checks {@code valid}, then dispatches. */ + private static ValueHandler intHandler(IntPredicate valid, IntAction action) + { + return (key, val, sw) -> { + int n; + try { + n = Integer.parseInt(val); + } catch (NumberFormatException e) { + throw new PrismException("Invalid value \"" + val + "\" for \"" + key + "\" option of -" + sw); + } + if (valid != null && !valid.test(n)) + throw new PrismException("Invalid value \"" + val + "\" for \"" + key + "\" option of -" + sw); + action.accept(n); + }; + } + + // ── Toggle options ──────────────────────────────────────────────────────── + + /** + * Register a {@code [no]name} boolean toggle: bare {@code name} calls {@code action(true)}, + * bare {@code noname} calls {@code action(false)}. + */ + OptionParser toggle(String name, String description, BoolAction action) + { + flagHandlers.put(name, () -> action.accept(true)); + flagHandlers.put("no" + name, () -> action.accept(false)); + helpEntries.add(new HelpEntry("flag", "[no]" + name, null, description)); + return this; + } + + // ── Boolean options ─────────────────────────────────────────────────────── + + /** Register a {@code key=true|false} option (action only). */ + OptionParser bool(String name, BoolAction action) + { + valueHandlers.put(name, (key, val, sw) -> { + if (val.equals("true")) action.accept(true); + else if (val.equals("false")) action.accept(false); + else throw new PrismException("Unknown value \"" + val + "\" for \"" + key + "\" option of -" + sw + + " (expected true or false)"); + }); + return this; + } + + /** Record a {@code key=true|false} option for help output only. */ + OptionParser bool(String name, String description) + { + helpEntries.add(new HelpEntry("bool", name, null, description)); + return this; + } + + /** Register a {@code key=true|false} option with both execution handler and help metadata. */ + OptionParser bool(String name, String description, BoolAction action) + { + bool(name, action); + helpEntries.add(new HelpEntry("bool", name, null, description)); + return this; + } + + // ── Choice options ──────────────────────────────────────────────────────── + + /** Register a {@code key=val} option where {@code val} must be one of a fixed set (action only). */ + OptionParser choice(String name, Choice c) + { + valueHandlers.put(name, c.toHandler()); + return this; + } + + /** Record a choice option for help output only; {@code validValues} are the displayed accepted values. */ + OptionParser choice(String name, String description, String... validValues) + { + helpEntries.add(new HelpEntry("choice", name, String.join("/", validValues), description)); + return this; + } + + /** + * Register a {@code key=val} choice option with both execution handler and help metadata. + * The displayed valid values are derived from the primary key of each {@link Choice#when} entry + * (the first argument when multiple keys are given as aliases). + */ + OptionParser choice(String name, String description, Choice c) + { + valueHandlers.put(name, c.toHandler()); + helpEntries.add(new HelpEntry("choice", name, String.join("/", c.primaryKeys()), description)); + return this; + } + + // ── Help output ─────────────────────────────────────────────────────────── + + /** + * Print the registered help entries as a human-readable option list. + * Only entries added via the description-only or combined overloads appear. + * Typical output: + * 

+	 *  * csv - Export results as comma-separated values
+	 *  * format (=explicit/matlab/dot) - model export format
+	 *  * precision (=<n>) - use n significant figures
+	 *  * rewards (=true/false) - whether to include rewards
+	 *
+ */ + void printOptions(PrismLog log) + { + for (HelpEntry e : helpEntries) { + StringBuilder sb = new StringBuilder(" * ").append(e.name); + switch (e.type) { + case "flag": /* nothing after name */ break; + case "bool": sb.append(" (=true/false)"); break; + case "string": // fall-through + case "choice": sb.append(" (=").append(e.argHint).append(")"); break; + } + sb.append(" - ").append(e.description); + log.println(sb.toString()); + } + } + + // ── Parsing ─────────────────────────────────────────────────────────────── + + /** + * Parse a comma-separated options string, dispatching each token to the registered handler. + * @param optionsString comma-separated options (may be empty or null) + * @param switchName CLI switch name used in error messages (without leading {@code -}) + */ + void parse(String optionsString, String switchName) throws PrismException + { + if (optionsString == null || optionsString.isEmpty()) return; + for (String rawOpt : optionsString.split(",")) { + String opt = rawOpt.trim(); + if (opt.isEmpty()) continue; + int eq = opt.indexOf('='); + if (eq == -1) { + FlagAction fa = flagHandlers.get(opt); + if (fa != null) { fa.run(); continue; } + if (valueHandlers.containsKey(opt)) + throw new PrismException("No value provided for \"" + opt + "\" option of -" + switchName); + throw new PrismException("Unknown option \"" + opt + "\" for -" + switchName + " switch"); + } else { + String key = opt.substring(0, eq).trim(); + String val = opt.substring(eq + 1).trim(); + ValueHandler vh = valueHandlers.get(key); + if (vh != null) { vh.accept(key, val, switchName); continue; } + if (flagHandlers.containsKey(key)) + throw new PrismException("Option \"" + key + "\" for -" + switchName + " does not take a value"); + throw new PrismException("Unknown option \"" + key + "\" for -" + switchName + " switch"); + } + } + } + + // ── Choice builder ──────────────────────────────────────────────────────── + + /** + * Builder for a fixed set of enumerated values for a {@link #choice} option. + * The first key in each {@code when()} call is the "primary" key shown in help output + * via {@link #primaryKeys()}; additional keys in the same call are accepted aliases + * but are not displayed. + */ + static class Choice + { + private final LinkedHashMap map = new LinkedHashMap<>(); + private final List primaryKeys = new ArrayList<>(); + + /** Register a single accepted value and its action. */ + Choice when(String key, FlagAction action) + { + primaryKeys.add(key); + map.put(key, action); + return this; + } + + /** Register a primary value and one alias; both trigger the same action. */ + Choice when(String primary, String alias, FlagAction action) + { + primaryKeys.add(primary); + map.put(primary, action); + map.put(alias, action); + return this; + } + + /** Register a primary value and two aliases; all three trigger the same action. */ + Choice when(String primary, String alias1, String alias2, FlagAction action) + { + primaryKeys.add(primary); + map.put(primary, action); + map.put(alias1, action); + map.put(alias2, action); + return this; + } + + /** Returns the primary key of each registered choice, in registration order. */ + List primaryKeys() { return primaryKeys; } + + /** Build the {@link ValueHandler} that dispatches on the registered values. */ + ValueHandler toHandler() + { + return (key, val, sw) -> { + FlagAction action = map.get(val); + if (action == null) + throw new PrismException("Unknown value \"" + val + "\" for \"" + key + "\" option of -" + sw + + " (options are: " + String.join(", ", map.keySet()) + ")"); + action.run(); + }; + } + } +} diff --git a/prism/src/prism/OptionsIntervalIteration.java b/prism/src/prism/OptionsIntervalIteration.java index 78d01a8d5..03b479cf4 100644 --- a/prism/src/prism/OptionsIntervalIteration.java +++ b/prism/src/prism/OptionsIntervalIteration.java @@ -26,9 +26,6 @@ package prism; -import java.util.ArrayList; -import java.util.List; -import java.util.Map.Entry; /** Option handling for interval iteration */ public class OptionsIntervalIteration @@ -78,6 +75,8 @@ public OptionsIntervalIteration(String options) throws PrismException fromOptionsString(options); } + private OptionsIntervalIteration() {} // use field defaults (for buildParser dummy target) + /** Static constructor from PrismComponent settings, throws PrismException on errors */ public static OptionsIntervalIteration from(PrismComponent parent) throws PrismException { @@ -90,12 +89,6 @@ public static OptionsIntervalIteration from(PrismSettings settings) throws Prism return new OptionsIntervalIteration(settings.getString(PrismSettings.PRISM_INTERVAL_ITER_OPTIONS)); } - /** Validate an options String, throws PrismException on errors */ - public static void validate(String optionsString) throws PrismException - { - new OptionsIntervalIteration(optionsString); - } - /** The method for computing upper bounds for reward computations */ public BoundMethod getBoundMethod() { @@ -156,7 +149,7 @@ public Double getManualUpperBound() return manualUpperBound; } - /** Get helper text for the options */ + /** Get helper text for the options (used by GUI settings tooltip). */ public static String getOptionsDescription() { StringBuffer sb = new StringBuffer(); @@ -170,109 +163,54 @@ public static String getOptionsDescription() sb.append(" [no]monotonicabove Enforce monotonicity in iteration from above (default = yes)\n"); sb.append(" [no]checkmonotonic Check monotonicity, for testing (default = no)\n"); sb.append("\nExample: boundmethod=default,upper=3.0,noselectmidpoint,checkmonotonic\n"); - return sb.toString(); } - /** Parse options string, throw on error */ - private void fromOptionsString(String options) throws PrismException + /** Print the options using {@link OptionParser} formatting (for CLI -help output). */ + public static void printOptions(PrismLog log) { - for (Entry entry : splitOptionsString(options)){ - String option = entry.getKey(); - String extra = entry.getValue(); - - boolean isBooleanOption = true; - switch (option) { - case "boundverbose": - case "noboundverbose": - boundComputationVerbose = !option.startsWith("no"); - break; - case "selectmidpoint": - case "noselectmidpoint": - resultSelectMidpoint = !option.startsWith("no"); - break; - case "checkmonotonic": - case "nocheckmonotonic": - checkMonotonicity = !option.startsWith("no"); - break; - case "monotonicbelow": - case "nomonotonicbelow": - enforceMonotonicityBelow = !option.startsWith("no"); - break; - case "monotonicabove": - case "nomonotonicabove": - enforceMonotonicityAbove = !option.startsWith("no"); - break; - case "lower": - case "upper": { - if (extra == null) - throw new PrismException("Missing argument to interval iteration option '" + option + "'"); - try { - Double value = Double.parseDouble(extra); - if (option.equals("lower")) { - manualLowerBound = value; - } else { - manualUpperBound = value; - } - } catch (NumberFormatException e) { - throw new PrismException("Illegal argument to interval iteration option '" + option + "': " + e.getMessage()); - } - isBooleanOption = false; - break; - } - case "boundmethod": { - if (extra == null) - throw new PrismException("Missing argument to interval iteration option '" + option + "'"); - switch (extra) { - case "default": - boundMethod = BoundMethod.DEFAULT; - break; - case "variant-1-coarse": - boundMethod = BoundMethod.VARIANT_1_COARSE; - break; - case "variant-1-fine": - boundMethod = BoundMethod.VARIANT_1_FINE; - break; - case "variant-2": - boundMethod = BoundMethod.VARIANT_2; - break; - case "dsmpi": - boundMethod = BoundMethod.DSMPI; - break; - default: - throw new PrismException("Unknown argument to interval iteration option '" + option + "', expected one of " - + boundMethodsList); - } - isBooleanOption = false; - break; - } - default: - throw new PrismException("Unknown interval iteration option '" + option + "'"); - } - - if (isBooleanOption) { - if (extra != null) { - throw new PrismException("Interval iteration option '" + option + "' has additional argument (" + extra + "), but is boolean option"); - } - } - } + parser().printOptions(log); + log.println("\nExample: boundmethod=default,upper=3.0,noselectmidpoint,checkmonotonic"); } - /** Split options string into list of pairs */ - private static List> splitOptionsString(String options) + /** + * An {@link OptionParser} for parsing/validating an interval-iteration options string + * (built with a throwaway dummy target; for CLI switch registration and -help output). + */ + static OptionParser parser() { - List> list = new ArrayList<>(); - if ("".equals(options)) - return list; + return buildParser(new OptionsIntervalIteration()); + } - for (String option : options.split(",")) { - int j = option.indexOf("="); - if (j == -1) { - list.add(new Pair<>(option.trim(), null)); - } else { - list.add(new Pair<>(option.substring(0,j).trim(), option.substring(j+1).trim())); - } - } - return list; + /** Parse options string, throw on error */ + private void fromOptionsString(String options) throws PrismException + { + buildParser(this).parse(options, "intervaliter"); + } + + /** Build an {@link OptionParser} whose actions set fields on {@code t}. */ + private static OptionParser buildParser(OptionsIntervalIteration t) + { + return new OptionParser() + .choice("boundmethod", "Select upper bound heuristic for reward computations", + new OptionParser.Choice() + .when("default", () -> t.boundMethod = BoundMethod.DEFAULT) + .when("variant-1-coarse", () -> t.boundMethod = BoundMethod.VARIANT_1_COARSE) + .when("variant-1-fine", () -> t.boundMethod = BoundMethod.VARIANT_1_FINE) + .when("variant-2", () -> t.boundMethod = BoundMethod.VARIANT_2) + .when("dsmpi", () -> t.boundMethod = BoundMethod.DSMPI)) + .string("lower", "", "Manually specify lower bound for reward computations", v -> { + try { t.manualLowerBound = Double.parseDouble(v); } + catch (NumberFormatException e) { throw new PrismException("Invalid value for 'lower' option: " + v); } + }) + .string("upper", "", "Manually specify upper bound for reward computations", v -> { + try { t.manualUpperBound = Double.parseDouble(v); } + catch (NumberFormatException e) { throw new PrismException("Invalid value for 'upper' option: " + v); } + }) + .toggle("boundverbose", "Verbose output for upper bound computations (default = no)", v -> t.boundComputationVerbose = v) + .toggle("selectmidpoint", "Select midpoint between upper and lower as the result (default = yes)", v -> t.resultSelectMidpoint = v) + .toggle("monotonicbelow", "Enforce monotonicity in iteration from below (default = yes)", v -> t.enforceMonotonicityBelow = v) + .toggle("monotonicabove", "Enforce monotonicity in iteration from above (default = yes)", v -> t.enforceMonotonicityAbove = v) + .toggle("checkmonotonic", "Check monotonicity, for testing (default = no)", v -> t.checkMonotonicity = v); } } diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index fd5744ea0..d25f9d8e1 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -2,7 +2,7 @@ // // Copyright (c) 2002- // Authors: -// * Dave Parker (University of Oxford, formerly University of Birmingham) +// * Dave Parker (University of Oxford) // //------------------------------------------------------------------------------ // @@ -36,8 +36,14 @@ import java.util.ArrayList; import java.util.Arrays; import java.util.Collections; +import java.util.HashSet; +import java.util.LinkedHashMap; import java.util.List; +import java.util.Map; import java.util.Map.Entry; +import java.util.Objects; +import java.util.Set; +import java.util.function.Consumer; import common.StackTraceHelper; import csv.CsvFormatException; @@ -144,6 +150,10 @@ public class PrismCL implements PrismModelListener private String exportStratFilename = null; private String simpathFilename = null; + // Unified CLI switch map (handler + help metadata), populated by initSwitchHandlers + private Map switchHandlers; + private SwitchRegistry registry; + // logs private PrismLog mainLog = null; @@ -195,7 +205,15 @@ public class PrismCL implements PrismModelListener // strategy export info private StrategyExportOptions exportStratOptions = null; - + + // transient state used during option parsing for complex switches + private ModelExportOptions pendingExportOptions; + private List pendingExportTasks; + + // option parsers for complex switches (initialised in initSwitchHandlers, capture 'this') + // switch stored as field so handleFilesOnly() can be called for the .all shorthand (line ~1563) + private StringPlusOptionsSwitch importModelSwitch; + // parametric analysis info private String[] paramLowerBounds = null; private String[] paramUpperBounds = null; @@ -1050,827 +1068,495 @@ public void notifyModelBuildFailed(PrismException e) */ private void parseArguments(String[] args) throws PrismException { - int i, j; - String sw, s; - PrismLog log; - constSwitch = ""; paramSwitch = ""; List filenameArgs = new ArrayList<>(); + initSwitchHandlers(); + + ArgConsumer consumer = new ArgConsumer(args); + while (consumer.hasNext()) { + String arg = consumer.advance(); + String sw = consumer.parseSwitch(arg); + if (sw != null) { + SwitchEntry entry = switchHandlers.get(sw); + if (entry != null) + entry.handler.handle(sw, consumer); + else + errorAndExit("Unknown switch -" + sw + " (type \"prism -help\" for full list)"); + } else { + // argument is assumed to be a (model/properties) filename + filenameArgs.add(arg); + } + } - for (i = 0; i < args.length; i++) { - - // if is a switch... - if (args[i].length() > 0 && args[i].charAt(0) == '-') { - - // Remove "-" - sw = args[i].substring(1); - if (sw.length() == 0) { - errorAndExit("Invalid empty switch"); - } - // Remove optional second "-" (i.e. we allow switches of the form --sw too) - if (sw.charAt(0) == '-') - sw = sw.substring(1); - - // Note: the order of these switches should match the -help output (just to help keep track of things). - // But: processing of "PRISM" options is done elsewhere in PrismSettings - // Any "hidden" options, i.e. not in -help text/manual, are indicated as such. - - // print help - if (sw.equals("help") || sw.equals("?")) { - // see if user requested help for a specific switch, e.g. -help simpath - // note: this is one of the few places where a second argument is optional, - // which is possible here because -help should usually be the only switch provided - if (i < args.length - 1) { - printHelpSwitch(args[++i]); - } else { - printHelp(); - } - exit(); - } - // java max mem & java stack size & java parameters - else if (sw.equals("javamaxmem") || sw.equals("javastack") || sw.equals("javaparams")) { - // ignore argument and subsequent value, this is dealt with before java is launched - i++; - } - // timeout - else if (sw.equals("timeout")) { - if (i < args.length - 1) { - int timeout = PrismUtils.convertTimeStringtoSeconds(args[++i]); - if (timeout < 0) { - errorAndExit("Negative timeout value \"" + timeout + "\" for -" + sw + " switch"); - } - if (timeout > 0) { - setTimeout(timeout); - } - // timeout == 0 -> no timeout - } else { - errorAndExit("Missing timeout value for -" + sw + " switch"); - } - } - // print version - else if (sw.equals("version")) { - printVersion(); - exit(); - } - // set working directory - else if (sw.equals("dir")) { - if (i < args.length - 1) { - Prism.setWorkingDirectory(args[++i]); - } else { - errorAndExit("No property specified for -" + sw + " switch"); - } - } - // load settings - else if (sw.equals("settings")) { - if (i < args.length - 1) { - settingsFilename = args[++i].trim(); - } else { - errorAndExit("Incomplete -" + sw + " switch"); - } - } - // print a list of all keywords (hidden option) - else if (sw.equals("keywords")) { - printListOfKeywords(); - exit(); - } - - // property/properties given in command line - else if (sw.equals("pf") || sw.equals("pctl") || sw.equals("csl")) { - if (i < args.length - 1) { - propertyString = args[++i]; - } else { - errorAndExit("No property specified for -" + sw + " switch"); - } - } - // which property to check (int index or string name) - else if (sw.equals("prop") || sw.equals("property")) { - if (i < args.length - 1) { - String[] props = args[++i].trim().split(","); - propertyIndices = new ArrayList(); - for (String p : props) { - if (!p.isEmpty()) { - try { - propertyIndices.add(Integer.parseInt(p)); - } catch (NumberFormatException e) { - propertyIndices.add(p); - } - } - } - } else { - errorAndExit("No value specified for -" + sw + " switch"); - } - } - // definition of undefined constants - else if (sw.equals("const")) { - if (i < args.length - 1) { - // store argument for later use (append if already partially specified) - if ("".equals(constSwitch)) - constSwitch = args[++i].trim(); - else - constSwitch += "," + args[++i].trim(); - } else { - errorAndExit("Incomplete -" + sw + " switch"); - } - } - // defining a parameter - else if (sw.equals("param")) { - param = true; - if (i < args.length - 1) { - // store argument for later use (append if already partially specified) - if ("".equals(paramSwitch)) { - paramSwitch = args[++i].trim(); - } else { - paramSwitch += "," + args[++i].trim(); - } - } else { - errorAndExit("Incomplete -" + sw + " switch"); - } - } - // do steady-state probability computation - else if (sw.equals("steadystate") || sw.equals("ss")) { - steadystate = true; - } - // do transient probability computation - else if (sw.equals("transient") || sw.equals("tr")) { - if (i < args.length - 1) { - dotransient = true; - transientTime = args[++i]; - } else { - errorAndExit("No value specified for -" + sw + " switch"); - } - } - // generate random path with simulator - else if (sw.equals("simpath")) { - if (i < args.length - 2) { - simpath = true; - simpathDetails = args[++i]; - simpathFilename = args[++i]; - } else { - errorAndExit("The -" + sw + " switch requires two arguments (path details, filename)"); - } - } - // disable model construction - else if (sw.equals("nobuild")) { - nobuild = true; - } - // enable "testing" mode - else if (sw.equals("test")) { - test = true; - } - // enable "test all" mode (don't stop on errors) - // (overrides -test switch) - else if (sw.equals("testall")) { - test = true; - testExitsOnFail = false; - } - // enable UMB test mode - else if (sw.equals("test:umb")) { - prism.setTestUMB(true); - } - - // DD Debugging options - else if (sw.equals("dddebug")) { - jdd.DebugJDD.enable(); - } - else if (sw.equals("ddtraceall")) { - jdd.DebugJDD.traceAll = true; - } - else if (sw.equals("ddtracefollowcopies")) { - jdd.DebugJDD.traceFollowCopies = true; - } - else if (sw.equals("dddebugwarnfatal")) { - jdd.DebugJDD.warningsAreFatal = true; - } - else if (sw.equals("dddebugwarnoff")) { - jdd.DebugJDD.warningsOff = true; - } - else if (sw.equals("ddtrace")) { - if (i < args.length - 1) { - String idString = args[++i]; - try { - int id = Integer.parseInt(idString); - jdd.DebugJDD.enableTracingForID(id); - } catch (NumberFormatException e) { - errorAndExit("The -" + sw + " switch requires an integer argument (JDDNode ID)"); - } - } else { - errorAndExit("The -" + sw + " switch requires an additional argument (JDDNode ID)"); - } - } - - // IMPORT OPTIONS: - - // change model type to pepa - else if (sw.equals("importpepa")) { - importpepa = true; - } - // Import model from PRISM preprocessor (hidden option) - else if (sw.equals("importprismpp")) { - if (i < args.length - 1) { - importprismpp = true; - prismppParams = args[++i]; - } else { - errorAndExit("No parameters specified for -" + sw + " switch"); - } - } - // import model from explicit file(s) - else if (sw.equals("importmodel")) { - if (i < args.length - 1) { - processImportModelSwitch(args[++i]); - } else { - errorAndExit("No file/options specified for -" + sw + " switch"); - } - } - // import transition matrix from explicit format - else if (sw.equals("importtrans")) { - if (i < args.length - 1) { - // Recall model name in case needed as basename for model exprts - modelFilename = args[++i]; - modelImportSources.add(new ModelImportSource(ModelExportTask.ModelExportEntity.MODEL, ModelExportFormat.EXPLICIT, new File(modelFilename))); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // import states for explicit model import - else if (sw.equals("importstates")) { - if (i < args.length - 1) { - modelImportSources.add(new ModelImportSource(ModelExportTask.ModelExportEntity.STATES, ModelExportFormat.EXPLICIT, new File(args[++i]))); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // import observations for explicit model import - else if (sw.equals("importobs")) { - if (i < args.length - 1) { - modelImportSources.add(new ModelImportSource(ModelExportTask.ModelExportEntity.OBSERVATIONS, ModelExportFormat.EXPLICIT, new File(args[++i]))); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // import labels for explicit model import - else if (sw.equals("importlabels")) { - if (i < args.length - 1) { - modelImportSources.add(new ModelImportSource(ModelExportTask.ModelExportEntity.LABELS, ModelExportFormat.EXPLICIT, new File(args[++i]))); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // import state rewards for explicit model import - else if (sw.equals("importstaterewards")) { - if (i < args.length - 1) { - modelImportSources.add(new ModelImportSource(ModelExportTask.ModelExportEntity.STATE_REWARDS, ModelExportFormat.EXPLICIT, new File(args[++i]))); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // import trans rewards for explicit model import - else if (sw.equals("importtransrewards")) { - if (i < args.length - 1) { - modelImportSources.add(new ModelImportSource(ModelExportTask.ModelExportEntity.TRANSITION_REWARDS, ModelExportFormat.EXPLICIT, new File(args[++i]))); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // import initial distribution e.g. for transient probability distribution - else if (sw.equals("importinitdist")) { - if (i < args.length - 1) { - importinitdist = true; - importInitDistFilename = args[++i]; - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // import results - else if (sw.equals("importresults")) { - if (i < args.length - 1) { - importresults = true; - modelFilename = "no-model-file.prism"; - importResultsFilename = args[++i]; - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // override model type to dtmc - else if (sw.equals("dtmc")) { - typeOverride = ModelType.DTMC; - } - // override model type to mdp - else if (sw.equals("mdp")) { - typeOverride = ModelType.MDP; - } - // override model type to ctmc - else if (sw.equals("ctmc")) { - typeOverride = ModelType.CTMC; - } - - // EXPORT OPTIONS: - - // export prism model to file - else if (sw.equals("exportprism")) { - if (i < args.length - 1) { - exportprism = true; - exportPrismFilename = args[++i]; - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // export prism model to file (with consts expanded) - else if (sw.equals("exportprismconst")) { - if (i < args.length - 1) { - exportprismconst = true; - exportPrismConstFilename = args[++i]; - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // export results - else if (sw.equals("exportresults")) { - if (i < args.length - 1) { - exportresults = true; - // Parse filename/options - s = args[++i]; - // Assume use of : to split filename/options but check for , if : not found - // (this was the old notation) - String halves[] = splitFilesAndOptions(s); - if (halves[1].length() == 0 && halves[0].indexOf(',') > -1) { - int comma = halves[0].indexOf(','); - halves[1] = halves[0].substring(comma + 1); - halves[0] = halves[0].substring(0, comma); - } - exportResultsFilename = halves[0]; - String ss[] = halves[1].split(","); - exportShape = ResultsExportShape.LIST_PLAIN; - for (j = 0; j < ss.length; j++) { - if (ss[j].equals("")) { - } else if (ss[j].equals("csv")) - exportShape = exportShape.isMatrix ? ResultsExportShape.MATRIX_CSV : ResultsExportShape.LIST_CSV; - else if (ss[j].equals("matrix")) - switch (exportShape) { - case LIST_PLAIN: - exportShape = ResultsExportShape.MATRIX_PLAIN; - break; - case LIST_CSV: - exportShape = ResultsExportShape.MATRIX_CSV; - break; - default: - // switch does not apply - } - else if (ss[j].equals("dataframe")) - exportShape = ResultsExportShape.DATA_FRAME; - else if (ss[j].equals("comment")) - exportShape = ResultsExportShape.COMMENT; - else - errorAndExit("Unknown option \"" + ss[j] + "\" for -" + sw + " switch"); - } - } else { - errorAndExit("No file/options specified for -" + sw + " switch"); - } - } - // export vector of results - else if (sw.equals("exportvector")) { - if (i < args.length - 1) { - exportvector = true; - exportVectorFilename = args[++i]; - prism.setStoreVector(true); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // export model to explicit file(s) - else if (sw.equals("exportmodel")) { - if (i < args.length - 1) { - processExportModelSwitch(args[++i]); - } else { - errorAndExit("No file/options specified for -" + sw + " switch"); - } - } - // process -exportmodelprecision in PrismSettings - // export transition matrix to file - else if (sw.equals("exporttrans")) { - if (i < args.length - 1) { - modelExportTasks.add(new ModelExportTask(ModelExportTask.ModelExportEntity.MODEL, args[++i])); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // export state rewards to file - else if (sw.equals("exportstaterewards")) { - if (i < args.length - 1) { - modelExportTasks.add(new ModelExportTask(ModelExportTask.ModelExportEntity.STATE_REWARDS, args[++i])); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // export transition rewards to file - else if (sw.equals("exporttransrewards")) { - if (i < args.length - 1) { - modelExportTasks.add(new ModelExportTask(ModelExportTask.ModelExportEntity.TRANSITION_REWARDS, args[++i])); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // export both state/transition rewards to file - else if (sw.equals("exportrewards")) { - if (i < args.length - 2) { - modelExportTasks.add(new ModelExportTask(ModelExportTask.ModelExportEntity.STATE_REWARDS, args[++i])); - modelExportTasks.add(new ModelExportTask(ModelExportTask.ModelExportEntity.TRANSITION_REWARDS, args[++i])); - } else { - errorAndExit("Two files must be specified for -" + sw + " switch"); - } - } - // export states - else if (sw.equals("exportstates")) { - if (i < args.length - 1) { - modelExportTasks.add(new ModelExportTask(ModelExportTask.ModelExportEntity.STATES, args[++i])); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // export observations - else if (sw.equals("exportobs")) { - if (i < args.length - 1) { - modelExportTasks.add(new ModelExportTask(ModelExportTask.ModelExportEntity.OBSERVATIONS, args[++i])); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // export labels/states - else if (sw.equals("exportlabels")) { - if (i < args.length - 1) { - processExportLabelsSwitch(args[++i]); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // export labels/states from properties file - else if (sw.equals("exportproplabels")) { - if (i < args.length - 1) { - processExportPropLabelsSwitch(args[++i]); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // switch export mode to "matlab" - else if (sw.equals("exportmatlab")) { - exportType = Prism.EXPORT_MATLAB; - modelExportOptionsGlobal.setFormat(ModelExportFormat.MATLAB); - } - // switch export mode to "mrmc" - else if (sw.equals("exportmrmc")) { - errorAndExit("Export to MRMC format no longer supported"); - } - // switch export mode to "rows" - else if (sw.equals("exportrows")) { - exportType = Prism.EXPORT_ROWS; - modelExportOptionsGlobal.setExplicitRows(true); - } - // exported matrix entries are ordered - else if (sw.equals("exportordered") || sw.equals("ordered")) { - // this is always done now, so ignore - } - // exported matrix entries are unordered - else if (sw.equals("exportunordered") || sw.equals("unordered")) { - errorAndExit("Switch -" + sw + " is no longer supported"); - } - // export transition matrix graph to dot file - else if (sw.equals("exporttransdot")) { - if (i < args.length - 1) { - ModelExportOptions exportOptions = new ModelExportOptions().setFormat(ModelExportFormat.DOT).setShowStates(false).setShowObservations(false); - modelExportTasks.add(new ModelExportTask(ModelExportTask.ModelExportEntity.MODEL, args[++i], exportOptions)); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // export transition matrix graph to dot file (with states) - else if (sw.equals("exporttransdotstates")) { - if (i < args.length - 1) { - ModelExportOptions exportOptions = new ModelExportOptions().setFormat(ModelExportFormat.DOT).setShowStates(true).setShowObservations(true); - modelExportTasks.add(new ModelExportTask(ModelExportTask.ModelExportEntity.MODEL, args[++i], exportOptions)); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // export transition matrix MTBDD to dot file - else if (sw.equals("exportdot")) { - if (i < args.length - 1) { - ModelExportOptions exportOptions = new ModelExportOptions().setFormat(ModelExportFormat.DD_DOT); - modelExportTasks.add(new ModelExportTask(ModelExportTask.ModelExportEntity.MODEL, args[++i], exportOptions)); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // export sccs to file - else if (sw.equals("exportsccs")) { - if (i < args.length - 1) { - exportsccs = true; - exportSCCsFilename = args[++i]; - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // export bsccs to file - else if (sw.equals("exportbsccs")) { - if (i < args.length - 1) { - exportbsccs = true; - exportBSCCsFilename = args[++i]; - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // export mecs to file - else if (sw.equals("exportmecs")) { - if (i < args.length - 1) { - exportmecs = true; - exportMECsFilename = args[++i]; - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // export steady-state probs (as opposed to displaying on screen) - else if (sw.equals("exportsteadystate") || sw.equals("exportss")) { - if (i < args.length - 1) { - exportSteadyStateFilename = args[++i]; - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - // if we are asked to export the steady-state probs, we should compute them - steadystate = true; - } - // export transient probs (as opposed to displaying on screen) - else if (sw.equals("exporttransient") || sw.equals("exporttr")) { - if (i < args.length - 1) { - exportTransientFilename = args[++i]; - } else { - 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 digital clocks translation prism model to file - else if (sw.equals("exportdigital")) { - if (i < args.length - 1) { - String filename = args[++i]; - File f = (filename.equals("stdout")) ? null : new File(filename); - prism.setExportDigital(true); - prism.setExportDigitalFile(f); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // export reachability target info to file (hidden option) - else if (sw.equals("exporttarget")) { - if (i < args.length - 1) { - prism.setExportTarget(true); - prism.setExportTargetFilename(args[++i]); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // export product transition matrix to file (hidden option) - else if (sw.equals("exportprodtrans")) { - if (i < args.length - 1) { - prism.setExportProductTrans(true); - prism.setExportProductTransFilename(args[++i]); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // export product states to file (hidden option) - else if (sw.equals("exportprodstates")) { - if (i < args.length - 1) { - prism.setExportProductStates(true); - prism.setExportProductStatesFilename(args[++i]); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // export product vector to file (hidden option) - else if (sw.equals("exportprodvector")) { - if (i < args.length - 1) { - prism.setExportProductVector(true); - prism.setExportProductVectorFilename(args[++i]); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - - // NB: Following the ordering of the -help text, more options go here, - // but these are processed in the PrismSettings class; see below - - // SIMULATION OPTIONS: - - // use simulator for approximate/statistical model checking - else if (sw.equals("sim")) { - simulate = true; - } - // simulation-based model checking methods - else if (sw.equals("simmethod")) { - if (i < args.length - 1) { - s = args[++i]; - if (s.equals("ci") || s.equals("aci") || s.equals("apmc") || s.equals("sprt")) - simMethodName = s; - else - errorAndExit("Unrecognised option for -" + sw + " switch (options are: ci, aci, apmc, sprt)"); - } else { - errorAndExit("No parameter specified for -" + sw + " switch"); - } - } - // simulation number of samples - else if (sw.equals("simsamples")) { - if (i < args.length - 1) { - try { - simNumSamples = Integer.parseInt(args[++i]); - if (simNumSamples <= 0) - throw new NumberFormatException(""); - simNumSamplesGiven = true; - } catch (NumberFormatException e) { - errorAndExit("Invalid value for -" + sw + " switch"); - } - } else { - errorAndExit("No value specified for -" + sw + " switch"); - } - } - // simulation confidence parameter - else if (sw.equals("simconf")) { - if (i < args.length - 1) { - try { - simConfidence = Double.parseDouble(args[++i]); - if (simConfidence <= 0 || simConfidence >= 1) - throw new NumberFormatException(""); - simConfidenceGiven = true; - } catch (NumberFormatException e) { - errorAndExit("Invalid value for -" + sw + " switch"); - } - } else { - errorAndExit("No value specified for -" + sw + " switch"); - } - } - // simulation confidence interval width - else if (sw.equals("simwidth")) { - if (i < args.length - 1) { - try { - simWidth = Double.parseDouble(args[++i]); - if (simWidth <= 0) - throw new NumberFormatException(""); - simWidthGiven = true; - } catch (NumberFormatException e) { - errorAndExit("Invalid value for -" + sw + " switch"); - } - } else { - errorAndExit("No value specified for -" + sw + " switch"); - } - } - // simulation approximation parameter - else if (sw.equals("simapprox")) { - if (i < args.length - 1) { - try { - simApprox = Double.parseDouble(args[++i]); - if (simApprox <= 0) - throw new NumberFormatException(""); - simApproxGiven = true; - } catch (NumberFormatException e) { - errorAndExit("Invalid value for -" + sw + " switch"); - } - } else { - errorAndExit("No value specified for -" + sw + " switch"); - } - } - // use the number of iterations given instead of automatically deciding whether the variance is null ot not - else if (sw.equals("simmanual")) { - simManual = true; - } - // simulation number of samples to conclude S^2=0 or not - else if (sw.equals("simvar")) { - if (i < args.length - 1) { - try { - reqIterToConclude = Integer.parseInt(args[++i]); - if (reqIterToConclude <= 0) - throw new NumberFormatException(""); - reqIterToConcludeGiven = true; - } catch (NumberFormatException e) { - errorAndExit("Invalid value for -" + sw + " switch"); - } - } else { - errorAndExit("No value specified for -" + sw + " switch"); - } - } - // maximum value of reward - else if (sw.equals("simmaxrwd")) { - if (i < args.length - 1) { - try { - simMaxReward = Double.parseDouble(args[++i]); - if (simMaxReward <= 0.0) - throw new NumberFormatException(""); - simMaxRewardGiven = true; - } catch (NumberFormatException e) { - errorAndExit("Invalid value for -" + sw + " switch"); - } - } else { - errorAndExit("No value specified for -" + sw + " switch"); - } - } - // simulation max path length - else if (sw.equals("simpathlen")) { - if (i < args.length - 1) { - try { - simMaxPath = Long.parseLong(args[++i]); - if (simMaxPath <= 0) - throw new NumberFormatException(""); - simMaxPathGiven = true; - } catch (NumberFormatException e) { - errorAndExit("Invalid value for -" + sw + " switch"); - } - } else { - errorAndExit("No value specified for -" + sw + " switch"); - } - } - - // FURTHER OPTIONS - NEED TIDYING/FIXING - - // zero-reward loops check on - else if (sw.equals("zerorewardcheck")) { - prism.setCheckZeroLoops(true); - } - // explicit-state model construction - else if (sw.equals("explicitbuild")) { - explicitbuild = true; - } - // (hidden) option for testing of prototypical explicit-state model construction - else if (sw.equals("explicitbuildtest")) { - explicitbuildtest = true; - } - - // MISCELLANEOUS UNDOCUMENTED/UNUSED OPTIONS: - - // specify main log (hidden option) - else if (sw.equals("mainlog")) { - if (i < args.length - 1) { - processMainLogSwitch(args[++i]); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } - // export transition matrix graph to dot file and view it (hidden option, for now) - else if (sw.equals("exportmodeldotview")) { - exportmodeldotview = true; - } - // mtbdd construction method (hidden option) - else if (sw.equals("c1")) { - prism.setConstruction(1); - } else if (sw.equals("c2")) { - prism.setConstruction(2); - } else if (sw.equals("c3")) { - prism.setConstruction(3); - } - // mtbdd variable ordering (hidden option) - else if (sw.equals("o1")) { - prism.setOrdering(1); - orderingOverride = true; - } else if (sw.equals("o2")) { - } else if (sw.equals("o2")) { - prism.setOrdering(2); - orderingOverride = true; - } else if (sw.equals("o2")) { - } - // reachability off (hidden option) - else if (sw.equals("noreach")) { - prism.setDoReach(false); - } - // no bscc computation (hidden option) - else if (sw.equals("nobscc")) { - prism.setBSCCComp(false); - } - // reachability options (hidden options) - else if (sw.equals("frontier")) { - prism.setReachMethod(Prism.REACH_FRONTIER); - } else if (sw.equals("bfs")) { - prism.setReachMethod(Prism.REACH_BFS); - } - // enable bisimulation minimisation before model checking (hidden option) - else if (sw.equals("bisim")) { - prism.setDoBisim(true); - } + processFileNames(filenameArgs); + } - // Other switches - pass to PrismSettings + /** + * Populate {@link #switchHandlers} with a handler and help metadata for every recognised switch. + * {@link PrismSettings#registerSwitchHandlers} contributes PrismSettings switches in the right + * position. Insertion order determines the {@code -help} output ordering. + */ + private void initSwitchHandlers() + { + switchHandlers = new LinkedHashMap<>(); + registry = new SwitchRegistry(switchHandlers); - else { - i = prism.getSettings().setFromCommandLineSwitch(args, i) - 1; - } - } - // otherwise argument is assumed to be a (model/properties) filename - else { - filenameArgs.add(args[i]); + // ── General (no section header) ────────────────────────────────────── + SwitchHandler helpHandler = (sw, a) -> { + // NB: -help [switch] is one of the few cases where the value arg is optional + if (a.hasNext()) printHelpSwitch(a.next(sw)); else printHelp(); + exit(); + }; + registry.addSwitch("help", helpHandler, "", "Display this help message"); + registry.addSwitch("?", helpHandler); // hidden alias + registry.addSwitch("version", new FlagSwitch(() -> { printVersion(); exit(); }), + "", "Display PRISM version info"); + registry.addSwitch("javaversion", new FlagSwitch(() -> {}), // handled by launch script + "", "Display Java version info"); + registry.addSwitch("dir", new StringSwitch(Prism::setWorkingDirectory), + "", "Set current working directory"); + registry.addSwitch("settings", new StringSwitch(s -> settingsFilename = s.trim()), + "", "Load settings from "); + boolean[] appendToLog = {false}; + registry.addSwitch("mainlog", new StringPlusOptionsSwitch( + new OptionParser().flag("append", "Append to the log file, rather than overwriting it", () -> appendToLog[0] = true), + (file, parse) -> { + appendToLog[0] = false; + parse.run(); + try { mainLog = new PrismFileLog(file, appendToLog[0]); prism.setMainLog(mainLog); } + + catch (PrismException e) { errorAndExit("Couldn't open log file \"" + file + "\""); } + }), + "[:]", "Write the log to instead of stdout"); + + registry.addBlankLine(); + + registry.addSwitch("pf", "pctl", "csl", new StringSwitch(s -> propertyString = s), + "", "Model check properties "); + SwitchHandler propHandler = (sw, a) -> { + String[] props = a.next(sw).trim().split(","); + propertyIndices = new ArrayList<>(); + for (String p : props) { + if (!p.isEmpty()) { + try { propertyIndices.add(Integer.parseInt(p)); } + catch (NumberFormatException e) { propertyIndices.add(p); } + } + } + }; + registry.addSwitch("property", "prop", propHandler, + "", "Only model check properties included in list of indices/names"); + registry.addSwitch("const", new StringSwitch(s -> { + String v = s.trim(); + if ("".equals(constSwitch)) constSwitch = v; else constSwitch += "," + v; + }), "", "Define constant values as (e.g. for experiments)", + log -> { + log.println(" is a comma-separated list of values or value ranges for undefined constants"); + log.println("in the model or properties (i.e. those declared without values, such as \"const int a;\")."); + log.println("You can either specify a single value (a=1), a range (a=1:10) or a range with a step (a=1:2:50)."); + log.println("For convenience, constant definutions can also be split across multiple -const switches."); + log.println("\nExamples:"); + log.println(" -const a=1,b=5.6,c=true"); + log.println(" -const a=1:10,b=5.6"); + log.println(" -const a=1:2:50,b=5.6"); + log.println(" -const a=1:2:50 -const b=5.6"); + }); + registry.addSwitch("steadystate", "ss", new FlagSwitch(() -> steadystate = true), + "", "Compute steady-state probabilities (D/CTMCs only)"); + registry.addSwitch("transient", "tr", new StringSwitch(s -> { dotransient = true; transientTime = s; }), + "", "Compute transient probabilities for time (or time range) (D/CTMCs only)"); + registry.addSwitch("simpath", (sw, a) -> { + simpath = true; + simpathDetails = a.next(sw); + simpathFilename = a.next(sw); + }, " ", "Generate a random path with the simulator", + log -> { + log.println("Generate a random path with the simulator and export it to (or to the screen if =\"stdout\")."); + log.println(" is a comma-separated list of options taken from:"); + GenerateSimulationPath.printOptions(log); + }); + registry.addSwitch("nobuild", new FlagSwitch(() -> nobuild = true), + "", "Skip model construction (just do parse/export)"); + registry.addSwitch("test", new OptionsOnlySwitch( + new OptionParser().flag("umb", "Enable UMB round trip test", () -> prism.setTestUMB(true)), + parse -> { test = true; parse.run(); }), + "[:]", "Enable \"test\" mode"); + registry.addSwitch("testall", new FlagSwitch(() -> { test = true; testExitsOnFail = false; }), + "", "Enable \"test\" mode, but don't exit on error"); + registry.addSwitch("javamaxmem", (sw, a) -> a.next(sw), // consumed before JVM launch + "", "Set the maximum heap size for Java, e.g. 500m, 4g [default: 1g]"); + registry.addSwitch("javastack", (sw, a) -> a.next(sw), // consumed before JVM launch + "", "Set the Java stack size [default: 4m]"); + registry.addSwitch("javaparams", (sw, a) -> a.next(sw), // consumed before JVM launch + "", "Pass additional command-line arguments to Java"); + registry.addSwitch("timeout", (sw, a) -> { + int t = PrismUtils.convertTimeStringtoSeconds(a.next(sw)); + if (t < 0) errorAndExit("Negative timeout value \"" + t + "\" for -" + sw + " switch"); + if (t > 0) setTimeout(t); + }, "", "Exit after a time-out of seconds if not already terminated"); + registry.addSwitch("ng", new FlagSwitch(() -> {}), // handled in main() before go() + "", "Run PRISM in Nailgun server mode; subsequent calls are then made via \"ngprism\""); + + // Hidden general switches + registry.addSwitch("keywords", new FlagSwitch(() -> { printListOfKeywords(); exit(); })); + registry.addSwitch("dddebug", new FlagSwitch(() -> jdd.DebugJDD.enable())); + registry.addSwitch("ddtraceall", new FlagSwitch(() -> jdd.DebugJDD.traceAll = true)); + registry.addSwitch("ddtracefollowcopies", new FlagSwitch(() -> jdd.DebugJDD.traceFollowCopies = true)); + registry.addSwitch("dddebugwarnfatal", new FlagSwitch(() -> jdd.DebugJDD.warningsAreFatal = true)); + registry.addSwitch("dddebugwarnoff", new FlagSwitch(() -> jdd.DebugJDD.warningsOff = true)); + registry.addSwitch("ddtrace", (sw, a) -> { + String idStr = a.next(sw); + try { + jdd.DebugJDD.enableTracingForID(Integer.parseInt(idStr)); + } catch (NumberFormatException e) { + errorAndExit("The -" + sw + " switch requires an integer argument (JDDNode ID)"); } - } + }); - processFileNames(filenameArgs); + // ── IMPORTS ────────────────────────────────────────────────────────── + registry.beginGroup("IMPORTS"); + registry.addSwitch("importpepa", new FlagSwitch(() -> importpepa = true), + "", "Model description is in PEPA, not the PRISM language"); + registry.addSwitch("importprismpp", (sw, a) -> { importprismpp = true; prismppParams = a.next(sw); }); // hidden + importModelSwitch = new StringPlusOptionsSwitch( + new OptionParser() + .choice("format", "model import format", new OptionParser.Choice() + .when("explicit", () -> { for (ModelImportSource s : modelImportSources) s.format = ModelExportFormat.EXPLICIT; }) + .when("umb", () -> { for (ModelImportSource s : modelImportSources) s.format = ModelExportFormat.UMB; })), + this::processImportModelSwitch); + registry.addSwitch("importmodel", importModelSwitch, + "[:]", "Import the model directly from file(s)", + log -> { + log.println("Import the model directly from one or more file(s)."); + log.println("Use a list of file extensions to indicate which files should be read, e.g.:"); + log.println("\n -importmodel in.tra,sta\n"); + log.println("Possible extensions are: .tra, .sta, .obs, .lab, .srew, .trew, .umb"); + log.println("Use extension .all to import all explicit files (.tra/sta/obs/lab/srew/trew), e.g.:"); + log.println("\n -importmodel in.all\n"); + log.println("If provided, is a comma-separated list of options taken from:"); + importModelSwitch.printOptions(log); + }); + registry.addSwitch("importtrans", new StringSwitch(s -> { + modelFilename = s; // recall for use as basename in model exports + modelImportSources.add(new ModelImportSource(ModelExportTask.ModelExportEntity.MODEL, ModelExportFormat.EXPLICIT, new File(s))); + }), "", "Import the transition matrix directly from a text file"); + registry.addSwitch("importstates", new StringSwitch(s -> modelImportSources.add( + new ModelImportSource(ModelExportTask.ModelExportEntity.STATES, ModelExportFormat.EXPLICIT, new File(s)))), + "", "Import the list of states directly from a text file"); + registry.addSwitch("importobs", new StringSwitch(s -> modelImportSources.add( + new ModelImportSource(ModelExportTask.ModelExportEntity.OBSERVATIONS, ModelExportFormat.EXPLICIT, new File(s)))), + "", "Import the list of observations directly from a text file"); + registry.addSwitch("importlabels", new StringSwitch(s -> modelImportSources.add( + new ModelImportSource(ModelExportTask.ModelExportEntity.LABELS, ModelExportFormat.EXPLICIT, new File(s)))), + "", "Import the list of labels directly from a text file"); + registry.addSwitch("importstaterewards", new StringSwitch(s -> modelImportSources.add( + new ModelImportSource(ModelExportTask.ModelExportEntity.STATE_REWARDS, ModelExportFormat.EXPLICIT, new File(s)))), + "", "Import the state rewards directly from a text file"); + registry.addSwitch("importtransrewards", new StringSwitch(s -> modelImportSources.add( + new ModelImportSource(ModelExportTask.ModelExportEntity.TRANSITION_REWARDS, ModelExportFormat.EXPLICIT, new File(s)))), + "", "Import the transition rewards directly from a text file"); + registry.addSwitch("importinitdist", new StringSwitch(s -> { importinitdist = true; importInitDistFilename = s; }), + "", "Specify initial probability distribution for transient/steady-state analysis"); + registry.addSwitch("dtmc", new FlagSwitch(() -> typeOverride = ModelType.DTMC), + "", "Force imported/built model to be a DTMC"); + registry.addSwitch("ctmc", new FlagSwitch(() -> typeOverride = ModelType.CTMC), + "", "Force imported/built model to be a CTMC"); + registry.addSwitch("mdp", new FlagSwitch(() -> typeOverride = ModelType.MDP), + "", "Force imported/built model to be an MDP"); + registry.addSwitch("importresults", new StringSwitch(s -> { + importresults = true; + modelFilename = "no-model-file.prism"; + importResultsFilename = s; + }), "", "Import results from a data frame stored in CSV file", + log -> { + log.println("Import results from a data frame stored as comma-separated values in ."); + }); + + // ── EXPORTS ────────────────────────────────────────────────────────── + registry.beginGroup("EXPORTS"); + boolean[] csv = {false}, matrix = {false}; + StringPlusOptionsSwitch exportResultsSwitch = new StringPlusOptionsSwitch( + new OptionParser() + .flag("csv", "Export results as comma-separated values", () -> csv[0] = true) + .flag("matrix", "Export results as one or more 2D matrices (e.g. for surface plots)", () -> matrix[0] = true) + .flag("dataframe", "Export results as dataframe in comma-separated values", () -> exportShape = ResultsExportShape.DATA_FRAME) + .flag("comment", "Export results in comment format for regression testing",() -> exportShape = ResultsExportShape.COMMENT), + (file, parse) -> { + exportresults = true; + exportResultsFilename = file; + exportShape = ResultsExportShape.LIST_PLAIN; + csv[0] = false; matrix[0] = false; + parse.run(); + if (exportShape == ResultsExportShape.LIST_PLAIN) + exportShape = csv[0] ? (matrix[0] ? ResultsExportShape.MATRIX_CSV : ResultsExportShape.LIST_CSV) + : (matrix[0] ? ResultsExportShape.MATRIX_PLAIN : ResultsExportShape.LIST_PLAIN); + }); + registry.addSwitch("exportresults", exportResultsSwitch, + "]>", "Export the results of model checking to a file", + log -> { + log.println("Exports the results of model checking to (or to the screen if =\"stdout\")."); + log.println("The default behaviour is to export a list of results in text form, using tabs to separate items."); + log.println("If provided, is a comma-separated list of options taken from:"); + exportResultsSwitch.printOptions(log); + }); + registry.addSwitch("exportvector", new StringSwitch(s -> { + exportvector = true; exportVectorFilename = s; prism.setStoreVector(true); + }), "", "Export results of model checking for all states to a file"); + StringPlusOptionsSwitch exportModelSwitch = new StringPlusOptionsSwitch( + new OptionParser() + .choice("format", "model export format", new OptionParser.Choice() + .when("explicit", () -> pendingExportOptions.setFormat(ModelExportFormat.EXPLICIT)) + .when("matlab", () -> pendingExportOptions.setFormat(ModelExportFormat.MATLAB)) + .when("dot", () -> pendingExportOptions.setFormat(ModelExportFormat.DOT)) + .when("drn", () -> pendingExportOptions.setFormat(ModelExportFormat.DRN)) + .when("umb", () -> pendingExportOptions.setFormat(ModelExportFormat.UMB))) + .bool("rewards", "whether to include rewards", v -> pendingExportOptions.setShowRewards(v)) + .bool("labels", "whether to include labels", v -> pendingExportOptions.setShowLabels(v)) + .bool("states", "whether to include state definitions", v -> pendingExportOptions.setShowStates(v)) + .bool("obs", "whether to include observation definitions", v -> pendingExportOptions.setShowObservations(v)) + .bool("actions", "whether to include actions on choices/transitions", v -> pendingExportOptions.setShowActions(v)) + .integer("precision", "", n -> RANGE_EXPORT_DOUBLE_PRECISION.contains(n), + "use significant figures for floating point values (in text)", + n -> pendingExportOptions.setModelPrecision(n)) + .choice("zip", "whether to zip UMB files", new OptionParser.Choice() + .when("true", () -> pendingExportOptions.setZipped(true)) + .when("false", () -> pendingExportOptions.setZipped(false)) + .when("gzip", "gz", () -> pendingExportOptions.setZipped(true).setCompressionFormat(ModelExportOptions.CompressionFormat.GZIP)) + .when("xz", () -> pendingExportOptions.setZipped(true).setCompressionFormat(ModelExportOptions.CompressionFormat.XZ))) + .flag("text", "show binary formats in textual form", () -> pendingExportOptions.setBinaryAsText(true)) + .flag("matlab", "same as format=matlab", () -> { pendingExportOptions.setFormat(ModelExportFormat.MATLAB); exportType = Prism.EXPORT_MATLAB; }) + .flag("rows", "export matrices with one row/distribution on each line", () -> { pendingExportOptions.setExplicitRows(true); exportType = Prism.EXPORT_ROWS; }) + .flag("proplabels", "also export labels from a properties file into the same file, too", () -> { + for (ModelExportTask t : pendingExportTasks) + if (t.getEntity() == ModelExportTask.ModelExportEntity.LABELS) + t.setLabelExportSet(ModelExportTask.LabelExportSet.ALL); + }) + .bool("headers", "include headers in explicit (reward) files", v -> pendingExportOptions.setPrintHeaders(v)), + this::processExportModelSwitch); + registry.addSwitch("exportmodel", exportModelSwitch, + "]>", "Export the built model to file(s)", + log -> { + log.println("Export the built model to file(s) (or to the screen if =\"stdout\")."); + log.println("Use a list of file extensions to indicate which files should be generated, e.g.:"); + log.println("\n -exportmodel out.tra,sta"); + log.println(" -exportmodel out.umb"); + log.println("\nPossible extensions are: .tra, .srew, .trew, .lab, .sta, .obs, .dot, .umb, .drn"); + log.println("Use extension .all to export all explicit files (.tra/srew/trew/lab/sta/obs), e.g.:"); + log.println("\n -exportmodel out.all"); + log.println("\nOmit the file basename to use the basename of the model file, e.g.:"); + log.println("\n -exportmodel .all"); + log.println("\nUse extension .rew to export both .srew/.trew files"); + log.println(); + log.println("If provided, is a comma-separated list of options taken from:"); + exportModelSwitch.printOptions(log); + }); + StringPlusOptionsSwitch exportTransSwitch = exportEntitySwitch(ModelExportTask.ModelExportEntity.MODEL); + registry.addSwitch("exporttrans", exportTransSwitch, + "[:]", "Export the transition matrix to a file"); + StringPlusOptionsSwitch exportStateRewardsSwitch = exportEntitySwitch(ModelExportTask.ModelExportEntity.STATE_REWARDS); + registry.addSwitch("exportstaterewards", exportStateRewardsSwitch, + "[:]", "Export the state rewards vector to a file"); + StringPlusOptionsSwitch exportTransRewardsSwitch = exportEntitySwitch(ModelExportTask.ModelExportEntity.TRANSITION_REWARDS); + registry.addSwitch("exporttransrewards", exportTransRewardsSwitch, + "[:]", "Export the transition rewards matrix to a file"); + OptionParser exportRewardsOptionsParser = exportTaskOptionsParser(); + registry.addSwitch("exportrewards", (sw, a) -> { + String[] file1 = StringPlusOptionsSwitch.splitFilesAndOptions(a.next(sw)); + pendingExportOptions = new ModelExportOptions(); + exportRewardsOptionsParser.parse(file1[1], sw); + ModelExportTask stateRewardsTask = new ModelExportTask(ModelExportTask.ModelExportEntity.STATE_REWARDS, file1[0]); + stateRewardsTask.getExportOptions().apply(pendingExportOptions); + modelExportTasks.add(stateRewardsTask); + + String[] file2 = StringPlusOptionsSwitch.splitFilesAndOptions(a.next(sw)); + pendingExportOptions = new ModelExportOptions(); + exportRewardsOptionsParser.parse(file2[1], sw); + ModelExportTask transRewardsTask = new ModelExportTask(ModelExportTask.ModelExportEntity.TRANSITION_REWARDS, file2[0]); + transRewardsTask.getExportOptions().apply(pendingExportOptions); + modelExportTasks.add(transRewardsTask); + }, "]> ]>", "Export state/transition rewards to files 1/2", + log -> { + log.println("Export state/transition rewards to files 1/2 (or to the screen if =\"stdout\")."); + log.println(); + log.println("If provided, is a comma-separated list of options (for either file) taken from:"); + exportRewardsOptionsParser.printOptions(log); + }); + StringPlusOptionsSwitch exportStatesSwitch = exportEntitySwitch(ModelExportTask.ModelExportEntity.STATES); + registry.addSwitch("exportstates", exportStatesSwitch, + "[:]", "Export the list of reachable states to a file"); + StringPlusOptionsSwitch exportObsSwitch = exportEntitySwitch(ModelExportTask.ModelExportEntity.OBSERVATIONS); + registry.addSwitch("exportobs", exportObsSwitch, + "[:]", "Export the list of observations to a file"); + ModelExportTask.LabelExportSet[] pendingLabelExportSet = {ModelExportTask.LabelExportSet.MODEL}; + StringPlusOptionsSwitch exportLabelsSwitch = exportEntitySwitch(ModelExportTask.ModelExportEntity.LABELS, + p -> p + .flag("matlab", "export data in Matlab format", () -> pendingExportOptions.setFormat(ModelExportFormat.MATLAB)) + .flag("proplabels", "export labels from a properties file into the same file, too", () -> pendingLabelExportSet[0] = ModelExportTask.LabelExportSet.ALL), + t -> { + t.setLabelExportSet(pendingLabelExportSet[0]); + pendingLabelExportSet[0] = ModelExportTask.LabelExportSet.MODEL; + }); + registry.addSwitch("exportlabels", exportLabelsSwitch, + "]>", "Export the list of labels and satisfying states to a file"); + StringPlusOptionsSwitch exportPropLabelsSwitch = exportEntitySwitch(ModelExportTask.ModelExportEntity.LABELS, + p -> p.flag("matlab", "export data in Matlab format", () -> pendingExportOptions.setFormat(ModelExportFormat.MATLAB)), + t -> t.setLabelExportSet(ModelExportTask.LabelExportSet.EXTRA)); + registry.addSwitch("exportproplabels", exportPropLabelsSwitch, + "]>", "Export the list of labels and satisfying states from the properties file to a file"); + StringPlusOptionsSwitch exportStratSwitch = new StringPlusOptionsSwitch( + new OptionParser() + .choice("type", "type of strategy export", new OptionParser.Choice() + .when("actions", () -> exportStratOptions.setType(StrategyExportOptions.StrategyExportType.ACTIONS)) + .when("indices", () -> exportStratOptions.setType(StrategyExportOptions.StrategyExportType.INDICES)) + .when("induced", "model", () -> exportStratOptions.setType(StrategyExportOptions.StrategyExportType.INDUCED_MODEL)) + .when("dot", () -> exportStratOptions.setType(StrategyExportOptions.StrategyExportType.DOT_FILE))) + .choice("mode", "mode to use for building induced model (or Dot file)", new OptionParser.Choice() + .when("restrict", () -> exportStratOptions.setMode(StrategyExportOptions.InducedModelMode.RESTRICT)) + .when("reduce", () -> exportStratOptions.setMode(StrategyExportOptions.InducedModelMode.REDUCE))) + .bool("reach", "whether to restrict the strategy to its reachable states", v -> exportStratOptions.setReachOnly(v)) + .bool("states", "whether to show states, rather than state indices, for actions lists or Dot files", v -> exportStratOptions.setShowStates(v)) + .bool("obs", "for partially observable models, whether to merge observationally equivalent states", v -> exportStratOptions.setMergeObservations(v)), + this::processExportStratSwitch); + registry.addSwitch("exportstrat", exportStratSwitch, + "]>", "Generate and export a strategy to a file", + log -> { + log.println("Generate and export a strategy to a file (or to the screen if =\"stdout\")."); + log.println("Use file extension .tra or .dot to export as an induced model or Dot file, respectively."); + log.println("If provided, is a comma-separated list of options taken from:"); + exportStratSwitch.printOptions(log); + }); + registry.addSwitch("exportmatlab", new FlagSwitch(() -> { + exportType = Prism.EXPORT_MATLAB; + modelExportOptionsGlobal.setFormat(ModelExportFormat.MATLAB); + }), "", "When exporting matrices/vectors/labels/etc., use Matlab format"); + registry.addSwitch("exportrows", new FlagSwitch(() -> { + exportType = Prism.EXPORT_ROWS; + modelExportOptionsGlobal.setExplicitRows(true); + }), "", "When exporting matrices, put a whole row on one line"); + registry.addSwitch("exporttransdot", new StringSwitch(s -> { + ModelExportOptions exportOptions = new ModelExportOptions().setFormat(ModelExportFormat.DOT).setShowStates(false).setShowObservations(false); + modelExportTasks.add(new ModelExportTask(ModelExportTask.ModelExportEntity.MODEL, s, exportOptions)); + }), "", "Export the transition matrix graph to a dot file"); + registry.addSwitch("exporttransdotstates", new StringSwitch(s -> { + ModelExportOptions exportOptions = new ModelExportOptions().setFormat(ModelExportFormat.DOT).setShowStates(true).setShowObservations(true); + modelExportTasks.add(new ModelExportTask(ModelExportTask.ModelExportEntity.MODEL, s, exportOptions)); + }), "", "Export the transition matrix graph to a dot file, with state info"); + registry.addSwitch("exportdot", new StringSwitch(s -> { + ModelExportOptions exportOptions = new ModelExportOptions().setFormat(ModelExportFormat.DD_DOT); + modelExportTasks.add(new ModelExportTask(ModelExportTask.ModelExportEntity.MODEL, s, exportOptions)); + }), "", "Export the transition matrix MTBDD to a dot file"); + registry.addSwitch("exportsccs", new StringSwitch(s -> { exportsccs = true; exportSCCsFilename = s; }), + "", "Compute and export all SCCs of the model"); + registry.addSwitch("exportbsccs", new StringSwitch(s -> { exportbsccs = true; exportBSCCsFilename = s; }), + "", "Compute and export all BSCCs of the model"); + registry.addSwitch("exportmecs", new StringSwitch(s -> { exportmecs = true; exportMECsFilename = s; }), + "", "Compute and export all maximal end components (MDPs only)"); + SwitchHandler exportSteadyStateHandler = new StringSwitch(s -> { exportSteadyStateFilename = s; steadystate = true; }); + registry.addSwitch("exportsteadystate", exportSteadyStateHandler, + "", "Export steady-state probabilities to a file"); + registry.addSwitch("exportss", exportSteadyStateHandler); // hidden alias + SwitchHandler exportTransientHandler = new StringSwitch(s -> exportTransientFilename = s); + registry.addSwitch("exporttransient", exportTransientHandler, + "", "Export transient probabilities to a file"); + registry.addSwitch("exporttr", exportTransientHandler); // hidden alias + registry.addSwitch("exportprism", new StringSwitch(s -> { exportprism = true; exportPrismFilename = s; }), + "", "Export final PRISM model to a file"); + registry.addSwitch("exportprismconst", new StringSwitch(s -> { exportprismconst = true; exportPrismConstFilename = s; }), + "", "Export final PRISM model with expanded constants to a file"); + + // Hidden export switches + registry.addSwitch("exportmrmc", new FlagSwitch(() -> errorAndExit("Export to MRMC format no longer supported"))); + registry.addSwitch("exportordered", "ordered", new FlagSwitch(() -> {})); // always done now, no-op + registry.addSwitch("exportunordered", "unordered", new FlagSwitch(() -> errorAndExit("Switch -exportunordered is no longer supported"))); + registry.addSwitch("exportdigital", new StringSwitch(s -> { + File f = s.equals("stdout") ? null : new File(s); + prism.setExportDigital(true); + prism.setExportDigitalFile(f); + })); + registry.addSwitch("exporttarget", new StringSwitch(s -> { + prism.setExportTarget(true); prism.setExportTargetFilename(s); + })); + registry.addSwitch("exportprodtrans", new StringSwitch(s -> { + prism.setExportProductTrans(true); prism.setExportProductTransFilename(s); + })); + registry.addSwitch("exportprodstates", new StringSwitch(s -> { + prism.setExportProductStates(true); prism.setExportProductStatesFilename(s); + })); + registry.addSwitch("exportprodvector", new StringSwitch(s -> { + prism.setExportProductVector(true); prism.setExportProductVectorFilename(s); + })); + + // ── PrismSettings sections (EXPORT OPTIONS through FAU OPTIONS) ─────── + // The -param handler captures PrismCL state so is passed in explicitly. + SwitchHandler paramHandler = (sw, a) -> { + param = true; + String v = a.next(sw).trim(); + if ("".equals(paramSwitch)) paramSwitch = v; else paramSwitch += "," + v; + }; + prism.getSettings().registerSwitchHandlers(registry, prism, paramHandler); + + // ── SIMULATION OPTIONS ──────────────────────────────────────────────── + registry.beginGroup("SIMULATION OPTIONS"); + registry.addSwitch("sim", new FlagSwitch(() -> simulate = true), + "", "Use the PRISM simulator to approximate results of model checking"); + registry.addSwitch("simmethod", new EnumSwitch() + .when("ci", () -> simMethodName = "ci") + .when("aci", () -> simMethodName = "aci") + .when("apmc", () -> simMethodName = "apmc") + .when("sprt", () -> simMethodName = "sprt"), + "", "Specify the method for approximate model checking (ci, aci, apmc, sprt)"); + registry.addSwitch("simsamples", (sw, a) -> { + int n = a.nextInt(sw); + if (n <= 0) errorAndExit("Invalid value for -" + sw + " switch"); + simNumSamples = n; simNumSamplesGiven = true; + }, "", "Set the number of samples for the simulator (CI/ACI/APMC methods)"); + registry.addSwitch("simconf", (sw, a) -> { + double d = a.nextDouble(sw); + if (d <= 0 || d >= 1) errorAndExit("Invalid value for -" + sw + " switch"); + simConfidence = d; simConfidenceGiven = true; + }, "", "Set the confidence parameter for the simulator (CI/ACI/APMC methods)"); + registry.addSwitch("simwidth", (sw, a) -> { + double d = a.nextDouble(sw); + if (d <= 0) errorAndExit("Invalid value for -" + sw + " switch"); + simWidth = d; simWidthGiven = true; + }, "", "Set the interval width for the simulator (CI/ACI methods)"); + registry.addSwitch("simapprox", (sw, a) -> { + double d = a.nextDouble(sw); + if (d <= 0) errorAndExit("Invalid value for -" + sw + " switch"); + simApprox = d; simApproxGiven = true; + }, "", "Set the approximation parameter for the simulator (APMC method)"); + registry.addSwitch("simmanual", new FlagSwitch(() -> simManual = true), + "", "Do not use the automated way of deciding whether the variance is null or not"); + registry.addSwitch("simvar", (sw, a) -> { + int n = a.nextInt(sw); + if (n <= 0) errorAndExit("Invalid value for -" + sw + " switch"); + reqIterToConclude = n; reqIterToConcludeGiven = true; + }, "", "Set the minimum number of samples to know the variance is null or not"); + registry.addSwitch("simmaxrwd", (sw, a) -> { + double d = a.nextDouble(sw); + if (d <= 0.0) errorAndExit("Invalid value for -" + sw + " switch"); + simMaxReward = d; simMaxRewardGiven = true; + }, "", "Set the maximum reward -- useful to display the CI/ACI methods progress"); + registry.addSwitch("simpathlen", (sw, a) -> { + long n = a.nextLong(sw); + if (n <= 0) errorAndExit("Invalid value for -" + sw + " switch"); + simMaxPath = n; simMaxPathGiven = true; + }, "", "Set the maximum path length for the simulator"); + + // Hidden miscellaneous switches + registry.addSwitch("explicitbuild", new FlagSwitch(() -> explicitbuild = true)); + registry.addSwitch("explicitbuildtest", new FlagSwitch(() -> explicitbuildtest = true)); + registry.addSwitch("exportmodeldotview", new FlagSwitch(() -> exportmodeldotview = true)); + registry.addSwitch("c1", new FlagSwitch(() -> prism.setConstruction(1))); + registry.addSwitch("c2", new FlagSwitch(() -> prism.setConstruction(2))); + registry.addSwitch("c3", new FlagSwitch(() -> prism.setConstruction(3))); + registry.addSwitch("o1", new FlagSwitch(() -> { prism.setOrdering(1); orderingOverride = true; })); + registry.addSwitch("o2", new FlagSwitch(() -> { prism.setOrdering(2); orderingOverride = true; })); + registry.addSwitch("noreach", new FlagSwitch(() -> prism.setDoReach(false))); + registry.addSwitch("nobscc", new FlagSwitch(() -> prism.setBSCCComp(false))); + registry.addSwitch("frontier", new FlagSwitch(() -> prism.setReachMethod(Prism.REACH_FRONTIER))); + registry.addSwitch("bfs", new FlagSwitch(() -> prism.setReachMethod(Prism.REACH_BFS))); + registry.addSwitch("bisim", new FlagSwitch(() -> prism.setDoBisim(true))); } /** @@ -1892,7 +1578,7 @@ private void processFileNames(List filenameArgs) throws PrismException if (filenameArgs.size() > 0) { modelFilename = filenameArgs.get(0); if (modelFilename.endsWith(".all")) { - processImportModelSwitch(modelFilename); + importModelSwitch.handleFilesOnly("importmodel", modelFilename); } } if (filenameArgs.size() > 1) { @@ -1907,12 +1593,8 @@ private void processFileNames(List filenameArgs) throws PrismException * because other individual switches (e.g. -importXXX) can later override * parts of the configurations set up here. */ - private void processImportModelSwitch(String filesOptionsString) throws PrismException + private void processImportModelSwitch(String filesString, StringPlusOptionsSwitch.ParseCallback parse) throws PrismException { - // Split into files/options (on :) - String halves[] = splitFilesAndOptions(filesOptionsString); - String filesString = halves[0]; - String optionsString = halves[1]; // Split files into basename/extensions int i = filesString.lastIndexOf('.'); String basename = i == -1 ? filesString : filesString.substring(0, i); @@ -1954,38 +1636,7 @@ private void processImportModelSwitch(String filesOptionsString) throws PrismExc } } // Process options - String options[] = optionsString.split(","); - for (String opt : options) { - // Ignore "" - if (opt.equals("")) { - } - // Import format - else if (opt.startsWith("format")) { - if (!opt.startsWith("format=")) { - throw new PrismException("No value provided for \"format\" option of -importmodel"); - } - String optVal = opt.substring(7); - ModelExportFormat importFormat = null; - switch (optVal) { - case "explicit": - importFormat = ModelExportFormat.EXPLICIT; - break; - case "umb": - importFormat = ModelExportFormat.UMB; - break; - default: - throw new PrismException("Unknown value \"" + optVal + "\" provided for \"format\" option of -importmodel"); - } - // Apply format to the import sources - for (ModelImportSource source : modelImportSources) { - source.format = importFormat; - } - } - // Unknown option - else { - throw new PrismException("Unknown option \"" + opt + "\" for -importmodel switch"); - } - } + parse.run(); } /** @@ -2066,56 +1717,49 @@ private void addTransitionRewardImports(String basename, boolean assumeExists) } /** - * Process the arguments (file, options) to the -exportlabels switch. + * Build an {@link OptionParser} for the {@code precision}/{@code headers} sub-options shared + * by the simple per-entity export switches ({@code -exporttrans}, {@code -exportstates}, etc., + * as opposed to the full option set of {@code -exportmodel}). Actions target + * {@link #pendingExportOptions}, which the caller must reset before parsing and apply to the + * resulting {@link ModelExportTask}(s) afterwards. */ - private void processExportLabelsSwitch(String filesOptionsString) throws PrismException + private OptionParser exportTaskOptionsParser() { - // Split into files/options (on :) - String pair[] = splitFilesAndOptions(filesOptionsString); - ModelExportTask newExportTask = new ModelExportTask(ModelExportTask.ModelExportEntity.LABELS, pair[0]); - String options[] = pair[1].split(","); - for (String opt : options) { - // Ignore "" - if (opt.equals("")) { - } - // Export type - else if (opt.equals("matlab")) { - newExportTask.getExportOptions().setFormat(ModelExportFormat.MATLAB); - } else if (opt.equals("proplabels")) { - newExportTask.setLabelExportSet(ModelExportTask.LabelExportSet.ALL); - } - // Unknown option - else { - throw new PrismException("Unknown option \"" + opt + "\" for -exportlabels switch"); - } - } - modelExportTasks.add(newExportTask); + return new OptionParser() + .integer("precision", "", n -> RANGE_EXPORT_DOUBLE_PRECISION.contains(n), + "use significant figures for floating point values (in text)", + n -> pendingExportOptions.setModelPrecision(n)); } /** - * Process the arguments (file, options) to the -exportproplabels switch. + * Build a {@link StringPlusOptionsSwitch} that put a single {@link ModelExportTask} of the + * given entity into {@link #modelExportTasks}, adding common options for exporting + * model entities (see {@link #exportTaskOptionsParser}). */ - private void processExportPropLabelsSwitch(String filesOptionsString) throws PrismException + private StringPlusOptionsSwitch exportEntitySwitch(ModelExportTask.ModelExportEntity entity) { - // Split into files/options (on :) - String pair[] = splitFilesAndOptions(filesOptionsString); - ModelExportTask newExportTask = new ModelExportTask(ModelExportTask.ModelExportEntity.LABELS, pair[0]); - newExportTask.setLabelExportSet(ModelExportTask.LabelExportSet.EXTRA); - String options[] = pair[1].split(","); - for (String opt : options) { - // Ignore "" - if (opt.equals("")) { - } - // Export type - else if (opt.equals("matlab")) { - newExportTask.getExportOptions().setFormat(ModelExportFormat.MATLAB); - } - // Unknown option - else { - throw new PrismException("Unknown option \"" + opt + "\" for -exportproplabels switch"); - } - } - modelExportTasks.add(newExportTask); + return exportEntitySwitch(entity, p -> {}, t -> {}); + } + + /** + * As {@link #exportEntitySwitch(ModelExportTask.ModelExportEntity)}, but additionally lets the + * caller register extra sub-options on the parser ({@code extraOptions}, applied once at + * registration time) and post-process the created task ({@code postProcess}, run on every + * invocation after the {@code precision}/{@code headers} options have been applied). + */ + private StringPlusOptionsSwitch exportEntitySwitch(ModelExportTask.ModelExportEntity entity, + Consumer extraOptions, Consumer postProcess) + { + OptionParser parser = exportTaskOptionsParser(); + extraOptions.accept(parser); + return new StringPlusOptionsSwitch(parser, (file, parse) -> { + pendingExportOptions = new ModelExportOptions(); + parse.run(); + ModelExportTask task = new ModelExportTask(entity, file); + task.getExportOptions().apply(pendingExportOptions); + postProcess.accept(task); + modelExportTasks.add(task); + }); } /** @@ -2124,12 +1768,8 @@ else if (opt.equals("matlab")) { * because other individual switches (e.g. -exportmatlab) can later override * parts of the configurations set up here. */ - private void processExportModelSwitch(String filesOptionsString) throws PrismException + private void processExportModelSwitch(String filesString, StringPlusOptionsSwitch.ParseCallback parse) throws PrismException { - // Split into files/options (on :) - String halves[] = splitFilesAndOptions(filesOptionsString); - String filesString = halves[0]; - String optionsString = halves[1]; // Split files into basename/extensions int i = filesString.lastIndexOf('.'); String basename = i == -1 ? filesString : filesString.substring(0, i); @@ -2156,165 +1796,12 @@ private void processExportModelSwitch(String filesOptionsString) throws PrismExc } } // Process options - ModelExportOptions exportOptions = new ModelExportOptions(); - String options[] = optionsString.split(","); - for (String opt : options) { - String sOpt; - // Ignore "" - if (opt.equals("")) { - } - // Export format - else if (opt.startsWith("format")) { - if (!opt.startsWith("format=")) { - throw new PrismException("No value provided for \"format\" option of -exportmodel"); - } - String optVal = opt.substring(7); - switch (optVal) { - case "explicit": - exportOptions.setFormat(ModelExportFormat.EXPLICIT); - break; - case "matlab": - exportOptions.setFormat(ModelExportFormat.MATLAB); - break; - case "dot": - exportOptions.setFormat(ModelExportFormat.DOT); - break; - case "drn": - exportOptions.setFormat(ModelExportFormat.DRN); - break; - case "umb": - exportOptions.setFormat(ModelExportFormat.UMB); - break; - default: - throw new PrismException("Unknown value \"" + optVal + "\" provided for \"format\" option of -exportmodel"); - } - } - // Export type - else if (opt.equals("matlab")) { - exportOptions.setFormat(ModelExportFormat.MATLAB); - exportType = Prism.EXPORT_MATLAB; - } else if (opt.equals("rows")) { - exportOptions.setExplicitRows(true); - exportType = Prism.EXPORT_ROWS; - } else if (opt.equals("text")) { - exportOptions.setBinaryAsText(true); - } - else if (opt.equals("proplabels")) { - for (ModelExportTask exportTask : newModelExportTasks) { - if (exportTask.getEntity() == ModelExportTask.ModelExportEntity.LABELS) { - exportTask.setLabelExportSet(ModelExportTask.LabelExportSet.ALL); - } - } - } - else if (opt.startsWith(sOpt = "labels")) { - if (!opt.startsWith(sOpt + "=")) - throw new PrismException("No value provided for \"" + sOpt + "\" option of -exportmodel"); - String optVal = opt.substring(sOpt.length() + 1); - if (optVal.equals("true")) - exportOptions.setShowLabels(true); - else if (optVal.equals("false")) - exportOptions.setShowLabels(false); - else - throw new PrismException("Unknown value \"" + optVal + "\" provided for \"" + sOpt + "\" option of -exportmodel"); - } - else if (opt.startsWith(sOpt = "rewards")) { - if (!opt.startsWith(sOpt + "=")) - throw new PrismException("No value provided for \"" + sOpt + "\" option of -exportmodel"); - String optVal = opt.substring(sOpt.length() + 1); - if (optVal.equals("true")) - exportOptions.setShowRewards(true); - else if (optVal.equals("false")) - exportOptions.setShowRewards(false); - else - throw new PrismException("Unknown value \"" + optVal + "\" provided for \"" + sOpt + "\" option of -exportmodel"); - } - else if (opt.startsWith(sOpt = "states")) { - if (!opt.startsWith(sOpt + "=")) - throw new PrismException("No value provided for \"" + sOpt + "\" option of -exportmodel"); - String optVal = opt.substring(sOpt.length() + 1); - if (optVal.equals("true")) - exportOptions.setShowStates(true); - else if (optVal.equals("false")) - exportOptions.setShowStates(false); - else - throw new PrismException("Unknown value \"" + optVal + "\" provided for \"" + sOpt + "\" option of -exportmodel"); - } - else if (opt.startsWith(sOpt = "obs")) { - if (!opt.startsWith(sOpt + "=")) - throw new PrismException("No value provided for \"" + sOpt + "\" option of -exportmodel"); - String optVal = opt.substring(sOpt.length() + 1); - if (optVal.equals("true")) - exportOptions.setShowObservations(true); - else if (optVal.equals("false")) - exportOptions.setShowObservations(false); - else - throw new PrismException("Unknown value \"" + optVal + "\" provided for \"" + sOpt + "\" option of -exportmodel"); - } - else if (opt.startsWith(sOpt = "actions")) { - if (!opt.startsWith(sOpt + "=")) - throw new PrismException("No value provided for \"" + sOpt + "\" option of -exportmodel"); - String optVal = opt.substring(sOpt.length() + 1); - if (optVal.equals("true")) { - exportOptions.setShowActions(true); - } else if (optVal.equals("false")) { - exportOptions.setShowActions(false); - } - else { - throw new PrismException("Unknown value \"" + optVal + "\" provided for \"" + sOpt + "\" option of -exportmodel"); - } - } - else if (opt.startsWith(sOpt = "headers")) { - if (!opt.startsWith(sOpt + "=")) - throw new PrismException("No value provided for \"" + sOpt + "\" option of -exportmodel"); - String optVal = opt.substring(sOpt.length() + 1); - if (optVal.equals("true")) { - exportOptions.setPrintHeaders(true); - } else if (optVal.equals("false")) { - exportOptions.setPrintHeaders(false); - } - else { - throw new PrismException("Unknown value \"" + optVal + "\" provided for \"" + sOpt + "\" option of -exportmodel"); - } - } - else if (opt.startsWith(sOpt = "precision")) { - if (!opt.startsWith(sOpt + "=")) - throw new PrismException("No value provided for \"" + sOpt + "\" option of -exportmodel"); - String optVal = opt.substring(sOpt.length() + 1); - try { - int precision = Integer.parseInt(optVal); - if (!RANGE_EXPORT_DOUBLE_PRECISION.contains(precision)) { - throw new NumberFormatException(""); - } - exportOptions.setModelPrecision(precision); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value \"" + optVal + "\" provided for \"" + sOpt + "\" option of -exportmodel"); - } - } - else if (opt.startsWith(sOpt = "zip")) { - if (!opt.startsWith(sOpt + "=")) - throw new PrismException("No value provided for \"" + sOpt + "\" option of -exportmodel"); - String optVal = opt.substring(sOpt.length() + 1); - if (optVal.equals("true")) { - exportOptions.setZipped(true); - } else if (optVal.equals("false")) { - exportOptions.setZipped(false); - } else if (optVal.equals("gzip") || optVal.equals("gz")) { - exportOptions.setZipped(true).setCompressionFormat(ModelExportOptions.CompressionFormat.GZIP); - } else if (optVal.equals("xz")) { - exportOptions.setZipped(true).setCompressionFormat(ModelExportOptions.CompressionFormat.XZ); - } - else { - throw new PrismException("Unknown value \"" + optVal + "\" provided for \"" + sOpt + "\" option of -exportmodel"); - } - } - // Unknown option - else { - throw new PrismException("Unknown option \"" + opt + "\" for -exportmodel switch"); - } - } + pendingExportOptions = new ModelExportOptions(); + pendingExportTasks = newModelExportTasks; + parse.run(); // Apply options from this switch to each export task for (ModelExportTask exportTask : newModelExportTasks) { - exportTask.getExportOptions().apply(exportOptions); + exportTask.getExportOptions().apply(pendingExportOptions); } // Add export tasks to the main list modelExportTasks.addAll(newModelExportTasks); @@ -2323,12 +1810,8 @@ else if (opt.startsWith(sOpt = "zip")) { /** * Process the arguments (files, options) to the -exportstrat switch */ - private void processExportStratSwitch(String filesOptionsString) throws PrismException + private void processExportStratSwitch(String fileString, StringPlusOptionsSwitch.ParseCallback parse) throws PrismException { - // Split into files/options (on :) - String halves[] = splitFilesAndOptions(filesOptionsString); - String fileString = halves[0]; - String optionsString = halves[1]; // Split file into basename/extension int i = fileString.lastIndexOf('.'); String basename = i == -1 ? fileString : fileString.substring(0, i); @@ -2347,128 +1830,7 @@ private void processExportStratSwitch(String filesOptionsString) throws PrismExc exportStratOptions.setType(StrategyExportOptions.StrategyExportType.ACTIONS); } // Process options - String options[] = optionsString.split(","); - for (String opt : options) { - // Ignore "" - if (opt.equals("")) { - } - else if (opt.startsWith("type")) { - if (!opt.startsWith("type=")) - throw new PrismException("No value provided for \"type\" option of -exportstrat"); - String optVal = opt.substring(5); - if (optVal.equals("actions")) - exportStratOptions.setType(StrategyExportOptions.StrategyExportType.ACTIONS); - else if (optVal.equals("indices")) - exportStratOptions.setType(StrategyExportOptions.StrategyExportType.INDICES); - else if (optVal.equals("model") || optVal.equals("induced")) - exportStratOptions.setType(StrategyExportOptions.StrategyExportType.INDUCED_MODEL); - else if (optVal.equals("dot")) - exportStratOptions.setType(StrategyExportOptions.StrategyExportType.DOT_FILE); - else - throw new PrismException("Unknown value \"" + optVal + "\" provided for \"type\" option of -exportstrat"); - } - else if (opt.startsWith("mode")) { - if (!opt.startsWith("mode=")) - throw new PrismException("No value provided for \"mode\" option of -exportstrat"); - String optVal = opt.substring(5); - if (optVal.equals("restrict")) - exportStratOptions.setMode(StrategyExportOptions.InducedModelMode.RESTRICT); - else if (optVal.equals("reduce")) - exportStratOptions.setMode(StrategyExportOptions.InducedModelMode.REDUCE); - else - throw new PrismException("Unknown value \"" + optVal + "\" provided for \"mode\" option of -exportstrat"); - } - else if (opt.startsWith("reach")) { - if (!opt.startsWith("reach=")) - throw new PrismException("No value provided for \"reach\" option of -exportstrat"); - String optVal = opt.substring(6); - if (optVal.equals("true")) - exportStratOptions.setReachOnly(true); - else if (optVal.equals("false")) - exportStratOptions.setReachOnly(false); - else - throw new PrismException("Unknown value \"" + optVal + "\" provided for \"reach\" option of -exportstrat"); - } - else if (opt.startsWith("states")) { - if (!opt.startsWith("states=")) - throw new PrismException("No value provided for \"states\" option of -exportstrat"); - String optVal = opt.substring(7); - if (optVal.equals("true")) - exportStratOptions.setShowStates(true); - else if (optVal.equals("false")) - exportStratOptions.setShowStates(false); - else - throw new PrismException("Unknown value \"" + optVal + "\" provided for \"reach\" option of -exportstrat"); - } - else if (opt.startsWith("obs")) { - if (!opt.startsWith("obs=")) - throw new PrismException("No value provided for \"obs\" option of -exportstrat"); - String optVal = opt.substring(4); - if (optVal.equals("true")) - exportStratOptions.setMergeObservations(true); - else if (optVal.equals("false")) - exportStratOptions.setMergeObservations(false); - else - throw new PrismException("Unknown value \"" + optVal + "\" provided for \"reach\" option of -exportstrat"); - } - // Unknown option - else { - throw new PrismException("Unknown option \"" + opt + "\" for -exportstrat switch"); - } - } - } - - /** - * Process the arguments (file, options) to the -mainlog switch - */ - private void processMainLogSwitch(String filesOptionsString) throws PrismException - { - // Split into file/options (on :) - String halves[] = splitFilesAndOptions(filesOptionsString); - String filename = halves[0]; - String optionsString = halves[1]; - // Process options - boolean append = false; - for (String opt : optionsString.split(",")) { - if (opt.equals("")) { - // ignore empty - } else if (opt.equals("append")) { - append = true; - } else { - throw new PrismException("Unknown option \"" + opt + "\" for -mainlog switch"); - } - } - // Open the log - try { - mainLog = new PrismFileLog(filename, append); - prism.setMainLog(mainLog); - } catch (PrismException e) { - errorAndExit("Couldn't open log file \"" + filename + "\""); - } - } - - /** - * Split a string of the form : into its two parts. - * The latter can be empty, in which case the : is optional. - * Instances of :\ are ignored (not treated as :) in case there is a Windows filename. - * @return the two parts as an array of two strings. - */ - private static String[] splitFilesAndOptions(String filesOptionsString) - { - String res[] = new String[2]; - // Split into files/options (on :) - int i = filesOptionsString.indexOf(':'); - while (filesOptionsString.length() > i + 1 && filesOptionsString.charAt(i + 1) == '\\') { - i = filesOptionsString.indexOf(':', i + 1); - } - if (i != -1) { - res[0] = filesOptionsString.substring(0, i); - res[1] = filesOptionsString.substring(i + 1); - } else { - res[0] = filesOptionsString; - res[1] = ""; - } - return res; + parse.run(); } // print command line arguments @@ -2723,6 +2085,22 @@ else if (simMethodName.equals("sprt")) { /** * Print a -help message, i.e. a list of the command-line switches. */ + /** Build the left column of a {@code -help} line: {@code -name (or -alias, ...)}. */ + private static String buildHelpLeft(SwitchEntry entry) + { + StringBuilder left = new StringBuilder("-").append(entry.primaryName); + left.append(entry.formattedArgHint()); + if (entry.shownAliases.length > 0) { + left.append(" (or "); + for (int i = 0; i < entry.shownAliases.length; i++) { + if (i > 0) left.append(", "); + left.append("-").append(entry.shownAliases[i]); + } + left.append(")"); + } + return left.toString(); + } + private void printHelp() { mainLog.println("Usage: " + Prism.getCommandLineName() + " [options] [] [more-options]"); @@ -2730,211 +2108,46 @@ private void printHelp() mainLog.println("Options:"); mainLog.println("========"); mainLog.println(); - mainLog.println("-help .......................... Display this help message"); - mainLog.println("-version ....................... Display PRISM version info"); - mainLog.println("-javaversion ................... Display Java version info"); - mainLog.println("-dir ..................... Set current working directory"); - mainLog.println("-settings ................ Load settings from "); - mainLog.println(); - mainLog.println("-pf (or -pctl or -csl) . Model check properties "); - mainLog.println("-property (or -prop) .... Only model check properties included in list of indices/names"); - mainLog.println("-const .................. Define constant values as (e.g. for experiments)"); - mainLog.println("-steadystate (or -ss) .......... Compute steady-state probabilities (D/CTMCs only)"); - mainLog.println("-transient (or -tr ) .... Compute transient probabilities for time (or time range) (D/CTMCs only)"); - mainLog.println("-simpath ....... Generate a random path with the simulator"); - mainLog.println("-nobuild ....................... Skip model construction (just do parse/export)"); - mainLog.println("-test .......................... Enable \"test\" mode"); - mainLog.println("-testall ....................... Enable \"test\" mode, but don't exit on error"); - mainLog.println("-javamaxmem ................. Set the maximum heap size for Java, e.g. 500m, 4g [default: 1g]"); - mainLog.println("-javastack ................. Set the Java stack size [default: 4m]"); - mainLog.println("-javaparams ................. Pass additional command-line arguments to Java"); - mainLog.println("-timeout ................... Exit after a time-out of seconds if not already terminated"); - mainLog.println("-ng ............................ Run PRISM in Nailgun server mode; subsequent calls are then made via \"ngprism\""); - mainLog.println(); - mainLog.println("IMPORTS:"); - mainLog.println("-importpepa .................... Model description is in PEPA, not the PRISM language"); - mainLog.println("-importmodel ........... Import the model directly from text file(s)"); - mainLog.println("-importtrans ............ Import the transition matrix directly from a text file"); - mainLog.println("-importstates ............ Import the list of states directly from a text file"); - mainLog.println("-importobs ............... Import the list of observations directly from a text file"); - mainLog.println("-importlabels ............ Import the list of labels directly from a text file"); - mainLog.println("-importstaterewards ...... Import the state rewards directly from a text file"); - mainLog.println("-importtransrewards ...... Import the transition rewards directly from a text file"); - mainLog.println("-importinitdist .......... Specify initial probability distribution for transient/steady-state analysis"); - mainLog.println("-dtmc .......................... Force imported/built model to be a DTMC"); - mainLog.println("-ctmc .......................... Force imported/built model to be a CTMC"); - mainLog.println("-mdp ........................... Force imported/built model to be an MDP"); - mainLog.println("-importresults .......... Import results from a data frame stored in CSV file"); - mainLog.println(); - mainLog.println("EXPORTS:"); - mainLog.println("-exportresults Export the results of model checking to a file"); - mainLog.println("-exportvector .......... Export results of model checking for all states to a file"); - mainLog.println("-exportmodel . Export the built model to file(s)"); - mainLog.println("-exporttrans ............ Export the transition matrix to a file"); - mainLog.println("-exportstaterewards ..... Export the state rewards vector to a file"); - mainLog.println("-exporttransrewards ..... Export the transition rewards matrix to a file"); - mainLog.println("-exportrewards .. Export state/transition rewards to files 1/2"); - mainLog.println("-exportstates ........... Export the list of reachable states to a file"); - mainLog.println("-exportobs .............. Export the list of observations to a file"); - mainLog.println("-exportlabels . Export the list of labels and satisfying states to a file"); - mainLog.println("-exportproplabels . Export the list of labels and satisfying states from the properties file to a file"); - mainLog.println("-exportstrat .. Generate and export a strategy to a file"); - mainLog.println("-exportmatlab .................. When exporting matrices/vectors/labels/etc., use Matlab format"); - mainLog.println("-exportrows .................... When exporting matrices, put a whole row on one line"); - mainLog.println("-exporttransdot ......... Export the transition matrix graph to a dot file"); - mainLog.println("-exporttransdotstates ... Export the transition matrix graph to a dot file, with state info"); - mainLog.println("-exportdot .............. Export the transition matrix MTBDD to a dot file"); - mainLog.println("-exportsccs ............. Compute and export all SCCs of the model"); - mainLog.println("-exportbsccs ............ Compute and export all BSCCs of the model"); - mainLog.println("-exportmecs ............. Compute and export all maximal end components (MDPs only)"); - mainLog.println("-exportsteadystate ...... Export steady-state probabilities to a file"); - mainLog.println("-exporttransient ........ Export transient probabilities to a file"); - mainLog.println("-exportprism ............ Export final PRISM model to a file"); - mainLog.println("-exportprismconst ....... Export final PRISM model with expanded constants to a file"); - - PrismSettings.printHelp(mainLog); - - mainLog.println(); - mainLog.println("SIMULATION OPTIONS:"); - mainLog.println("-sim ........................... Use the PRISM simulator to approximate results of model checking"); - mainLog.println("-simmethod .............. Specify the method for approximate model checking (ci, aci, apmc, sprt)"); - mainLog.println("-simsamples ................ Set the number of samples for the simulator (CI/ACI/APMC methods)"); - mainLog.println("-simconf ................... Set the confidence parameter for the simulator (CI/ACI/APMC methods)"); - mainLog.println("-simwidth .................. Set the interval width for the simulator (CI/ACI methods)"); - mainLog.println("-simapprox ................. Set the approximation parameter for the simulator (APMC method)"); - mainLog.println("-simmanual ..................... Do not use the automated way of deciding whether the variance is null or not"); - mainLog.println("-simvar .................... Set the minimum number of samples to know the variance is null or not"); - mainLog.println("-simmaxrwd ................. Set the maximum reward -- useful to display the CI/ACI methods progress"); - mainLog.println("-simpathlen ................ Set the maximum path length for the simulator"); - + // First pass: find the longest left column across all visible entries. + int maxLeft = 0; + Set counted = new HashSet<>(); + for (SwitchEntry entry : switchHandlers.values()) { + if (!counted.add(entry)) continue; + if (entry.primaryName == null || entry.argHint == null) continue; + maxLeft = Math.max(maxLeft, buildHelpLeft(entry).length()); + } + // Second pass: print with dot-padding aligned to the longest entry (minimum 1 dot). + String lastGroup = ""; // sentinel: different from null so first group change fires + Set seen = new HashSet<>(); + for (Map.Entry e : switchHandlers.entrySet()) { + SwitchEntry entry = e.getValue(); + if (!seen.add(entry)) continue; + if (entry.primaryName == null) { mainLog.println(); continue; } // blank-line sentinel + if (entry.argHint == null) continue; // hidden + if (!Objects.equals(entry.group, lastGroup)) { + if (entry.group != null) { + mainLog.println(); + mainLog.println(entry.group + ":"); + } + lastGroup = entry.group; + } + String left = buildHelpLeft(entry); + mainLog.println(left + " " + ".".repeat(maxLeft - left.length() + 1) + " " + entry.shortText); + } mainLog.println(); mainLog.println("You can also use \"prism -help xxx\" for help on some switches -xxx with non-obvious syntax."); } - /** - * Print a -help xxx message, i.e. display help on a specific switch - */ + /** Print a {@code -help } message: display detailed help on a specific switch. */ private void printHelpSwitch(String sw) { - // Remove "-" from start of switch, in case present (it shouldn't be really) if (sw.charAt(0) == '-') sw = sw.substring(1); - - // -const - if (sw.equals("const")) { - mainLog.println("Switch: -const \n"); - mainLog.println(" is a comma-separated list of values or value ranges for undefined constants"); - mainLog.println("in the model or properties (i.e. those declared without values, such as \"const int a;\")."); - mainLog.println("You can either specify a single value (a=1), a range (a=1:10) or a range with a step (a=1:2:50)."); - mainLog.println("For convenience, constant definutions can also be split across multiple -const switches."); - mainLog.println("\nExamples:"); - mainLog.println(" -const a=1,b=5.6,c=true"); - mainLog.println(" -const a=1:10,b=5.6"); - mainLog.println(" -const a=1:2:50,b=5.6"); - mainLog.println(" -const a=1:2:50 -const b=5.6"); - } - // -simpath - else if (sw.equals("simpath")) { - mainLog.println("Switch: -simpath \n"); - mainLog.println("Generate a random path with the simulator and export it to (or to the screen if =\"stdout\")."); - mainLog.println(" is a comma-separated list of options taken from:"); - GenerateSimulationPath.printOptions(mainLog); - } - // -importmodel - else if (sw.equals("importmodel")) { - mainLog.println("Switch: -importmodel [:options]\n"); - mainLog.println("Import the model directly from one or more file(s)."); - mainLog.println("Use a list of file extensions to indicate which files should be read, e.g.:"); - mainLog.println("\n -importmodel in.tra,sta\n"); - mainLog.println("Possible extensions are: .tra, .sta, .obs, .lab, .srew, .trew, .umb"); - mainLog.println("Use extension .all to import all explicit files (.tra/sta/obs/lab/srew/trew), e.g.:"); - mainLog.println("\n -importmodel in.all\n"); - mainLog.println("If provided, is a comma-separated list of options taken from:"); - mainLog.println(" * format (=explicit/umb) - model import format"); - } - // -importresults - else if (sw.equals("importresults")) { - mainLog.println("Switch: -importresults \n"); - mainLog.println("Import results from a data frame stored as comma-separated values in ."); - } - // -exportresults - else if (sw.equals("exportresults")) { - mainLog.println("Switch: -exportresults \n"); - mainLog.println("Exports the results of model checking to (or to the screen if =\"stdout\")."); - mainLog.println("The default behaviour is to export a list of results in text form, using tabs to separate items."); - mainLog.println("If provided, is a comma-separated list of options taken from:"); - mainLog.println(" * csv - Export results as comma-separated values"); - mainLog.println(" * matrix - Export results as one or more 2D matrices (e.g. for surface plots)"); - mainLog.println(" * dataframe - Export results as dataframe in comma-separated values)"); - mainLog.println(" * comment - Export results in comment format for regression testing)"); - } - // -exportlabels - else if (sw.equals("exportlabels")) { - mainLog.println("Switch: -exportlabels \n"); - mainLog.println("Export the list of labels and satisfying states to a file (or to the screen if =\"stdout\")."); - mainLog.println(); - mainLog.println("If provided, is a comma-separated list of options taken from:"); - mainLog.println(" * matlab - export data in Matlab format"); - mainLog.println(" * proplabels - export labels from a properties file into the same file, too"); - } - // -exportproplabels - else if (sw.equals("exportproplabels")) { - mainLog.println("Switch: -exportproplabels \n"); - mainLog.println("Export the list of labels and satisfying states from the properties file to a file (or to the screen if =\"stdout\")."); - mainLog.println(); - mainLog.println("If provided, is a comma-separated list of options taken from:"); - mainLog.println(" * matlab - export data in Matlab format"); - } - // -exportmodel - else if (sw.equals("exportmodel")) { - mainLog.println("Switch: -exportmodel \n"); - mainLog.println("Export the built model to file(s) (or to the screen if =\"stdout\")."); - mainLog.println("Use a list of file extensions to indicate which files should be generated, e.g.:"); - mainLog.println("\n -exportmodel out.tra,sta\n"); - mainLog.println("\n -exportmodel out.umb\n"); - mainLog.println("Possible extensions are: .tra, .srew, .trew, .lab, .sta, .obs, .dot, .umb, .drn"); - mainLog.println("Use extension .all to export all explicit files (.tra/srew/trew/lab/sta/obs), e.g.:"); - mainLog.println("\n -exportmodel out.all\n"); - mainLog.println("Omit the file basename to use the basename of the model file, e.g.:"); - mainLog.println("\n -exportmodel .all\n"); - mainLog.println("Use extension .rew to export both .srew/.trew files"); - mainLog.println(); - mainLog.println("If provided, is a comma-separated list of options taken from:"); - mainLog.println(" * format (=explicit/matlab/dot/drn/umb) - model export format"); - mainLog.println(" * rewards (=true/false) - whether to include rewards"); - mainLog.println(" * labels (=true/false) - whether to include labels"); - mainLog.println(" * states (=true/false) - whether to include state definitions"); - mainLog.println(" * obs (=true/false) - whether to include observation definitions"); - mainLog.println(" * actions (=true/false) - whether to include actions on choices/transitions"); - mainLog.println(" * precision (=) - use significant figures for floating point values (in text)"); - mainLog.println(" * zip (=true/false) - whether to zip UMB files"); - mainLog.println(" * text - show binary formats in textual form "); - mainLog.println(" * matlab - same as format=matlab"); - mainLog.println("For the explicit files format:"); - mainLog.println(" * rows - export matrices with one row/distribution on each line"); - mainLog.println(" * proplabels - also export labels from a properties file into the same file, too"); - mainLog.println(" * headers (=true/false) - include headers in explicit (reward) files"); - } - // -exportstrat - else if (sw.equals("exportstrat")) { - mainLog.println("Switch: -exportstrat \n"); - mainLog.println("Generate and export a strategy to a file (or to the screen if =\"stdout\")."); - mainLog.println("Use file extension .tra or .dot to export as an induced model or Dot file, respectively."); - mainLog.println("If provided, is a comma-separated list of options taken from:"); - mainLog.println(" * type (=actions/induced/dot) - type of strategy export"); - mainLog.println(" * mode (=restrict/reduce) - mode to use for building induced model (or Dot file)"); - mainLog.println(" * reach (=true/false) - whether to restrict the strategy to its reachable states"); - mainLog.println(" * states (=true/false) - whether to show states, rather than state indices, for actions lists or Dot files"); - mainLog.println(" * obs (=true/false) - for partially observable models, whether to merge observationally equivalent states"); - } - // Try PrismSettings - else if (PrismSettings.printHelpSwitch(mainLog, sw)) { - return; - } - // Unknown - else { + SwitchEntry entry = switchHandlers.get(sw); + if (entry != null && entry.argHint != null) + entry.printLongDesc(mainLog); + else mainLog.println("Sorry - no help available for switch -" + sw); - } } // print version diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index d3f099f00..8cd673afa 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -2,10 +2,8 @@ // // Copyright (c) 2002- // Authors: -// * Dave Parker (University of Oxford, formerly University of Birmingham) -// * Andrew Hinton (University of Birmingham) -// * Vincent Nimal (University of Oxford) -// +// * Dave Parker (University of Oxford) +// //------------------------------------------------------------------------------ // // This file is part of PRISM. @@ -949,7 +947,7 @@ public synchronized void loadDefaults() protected boolean exportPropAut = false; protected String exportPropAutType = "txt"; protected String exportPropAutFilename = "da.txt"; - + public void setExportPropAut(boolean b) throws PrismException { exportPropAut = b; @@ -981,795 +979,374 @@ public String getExportPropAutFilename() } /** - * Set an option by parsing one or more command-line arguments. - * Reads the ith argument (assumed to be in the form "-switch") - * and also any subsequent arguments required as parameters. - * Return the index of the next argument to be read. - * @param args Full list of arguments - * @param i Index of first argument to read + * Register all PrismSettings switch handlers with the unified CLI switch registry. + * Called from {@link PrismCL#initSwitchHandlers()} to contribute PrismSettings switches + * in the correct help-output position (between EXPORTS and SIMULATION OPTIONS). + * + * @param reg the shared switch registry + * @param prism the Prism instance (for switches that set Prism-level state) + * @param paramHandler PrismCL-owned handler for {@code -param}; registered here so that + * {@code -param} appears in the PARAMETRIC section of {@code -help} */ - public synchronized int setFromCommandLineSwitch(String args[], int i) throws PrismException + void registerSwitchHandlers(SwitchRegistry reg, Prism prism, SwitchHandler paramHandler) { - String s; - int j; - double d; - - // Process string (remove - and extract any options) - Pair pair = splitSwitch(args[i]); - String sw = pair.first; - String optionsString = pair.second; - Map options = splitOptionsString(optionsString); - - // Note: the order of these switches should match the -help output (just to help keep track of things). - - // ENGINES/METHODS: - - // Main model checking engine - if (sw.equals("mtbdd") || sw.equals("m")) { - set(PRISM_ENGINE, "MTBDD"); - } - else if (sw.equals("sparse") || sw.equals("s")) { - set(PRISM_ENGINE, "Sparse"); - } - else if (sw.equals("hybrid") || sw.equals("h")) { - set(PRISM_ENGINE, "Hybrid"); - } - else if (sw.equals("explicit") || sw.equals("ex")) { - set(PRISM_ENGINE, "Explicit"); - } - // Exact model checking - else if (sw.equals("exact")) { - set(PRISM_EXACT_ENABLED, true); - } - // PTA model checking methods - else if (sw.equals("ptamethod")) { - if (i < args.length - 1) { - s = args[++i]; - if (s.equals("digital")) - set(PRISM_PTA_METHOD, "Digital clocks"); - else if (s.equals("games")) - set(PRISM_PTA_METHOD, "Stochastic games"); - else if (s.equals("backwards") || s.equals("bw")) - set(PRISM_PTA_METHOD, "Backwards reachability"); - else - throw new PrismException("Unrecognised option for -" + sw + " switch (options are: digital, games, backwards)"); - } else { - throw new PrismException("No parameter specified for -" + sw + " switch"); - } - } - // Transient methods - else if (sw.equals("transientmethod")) { - if (i < args.length - 1) { - s = args[++i]; - if (s.equals("unif")) - set(PRISM_TRANSIENT_METHOD, "Uniformisation"); - else if (s.equals("fau")) - set(PRISM_TRANSIENT_METHOD, "Fast adaptive uniformisation"); - else - throw new PrismException("Unrecognised option for -" + sw + " switch (options are: unif, fau)"); - } else { - throw new PrismException("No parameter specified for -" + sw + " switch"); - } - } - // Heuristic modes - else if (sw.equals("heuristic")) { - if (i < args.length - 1) { - s = args[++i]; - if (s.equals("none")) - set(PRISM_HEURISTIC, "None"); - else if (s.equals("speed")) - set(PRISM_HEURISTIC, "Speed"); - else if (s.equals("memory")) - set(PRISM_HEURISTIC, "Memory"); - else - throw new PrismException("Unrecognised option for -" + sw + " switch (options are: none, speed, memory)"); - } else { - throw new PrismException("No parameter specified for -" + sw + " switch"); - } - } + // ── EXPORT OPTIONS ─────────────────────────────────────────────────── + reg.beginGroup("EXPORT OPTIONS"); + reg.addSwitch("exportmodelprecision", (sw, a) -> { + int n = a.nextInt(sw); + if (!RANGE_EXPORT_DOUBLE_PRECISION.contains(n)) + throw new PrismException("Invalid value for -" + sw + " switch"); + set(PRISM_EXPORT_MODEL_PRECISION, n); + }, "", "Export probabilities/rewards with n significant decimal places"); + reg.addSwitch("noexportheaders", new FlagSwitch(() -> set(PRISM_EXPORT_MODEL_HEADERS, false)), + "", "Don't include headers when exporting rewards"); - // NUMERICAL SOLUTION OPTIONS: - - // Linear equation solver + MDP soln method - else if (sw.equals("power") || sw.equals("pow") || sw.equals("pwr")) { - set(PRISM_LIN_EQ_METHOD, "Power"); - } else if (sw.equals("jacobi") || sw.equals("jac")) { - set(PRISM_LIN_EQ_METHOD, "Jacobi"); - } else if (sw.equals("gaussseidel") || sw.equals("gs")) { + // ── ENGINES/METHODS ────────────────────────────────────────────────── + reg.beginGroup("ENGINES/METHODS"); + reg.addSwitch("mtbdd", "m", new FlagSwitch(() -> set(PRISM_ENGINE, "MTBDD")), + "", "Use the MTBDD engine"); + reg.addSwitch("sparse", "s", new FlagSwitch(() -> set(PRISM_ENGINE, "Sparse")), + "", "Use the Sparse engine"); + reg.addSwitch("hybrid", "h", new FlagSwitch(() -> set(PRISM_ENGINE, "Hybrid")), + "", "Use the Hybrid engine [default]"); + reg.addSwitch("explicit", "ex", new FlagSwitch(() -> set(PRISM_ENGINE, "Explicit")), + "", "Use the explicit engine"); + reg.addSwitch("exact", new FlagSwitch(() -> set(PRISM_EXACT_ENABLED, true)), + "", "Perform exact (arbitrary precision) model checking"); + reg.addSwitch("ptamethod", new EnumSwitch() + .when("digital", () -> set(PRISM_PTA_METHOD, "Digital clocks")) + .when("games", () -> set(PRISM_PTA_METHOD, "Stochastic games")) + .when("backwards", "bw", () -> set(PRISM_PTA_METHOD, "Backwards reachability")), + "", "Specify PTA engine (games, digital, backwards) [default: games]"); + reg.addSwitch("transientmethod", new EnumSwitch() + .when("unif", () -> set(PRISM_TRANSIENT_METHOD, "Uniformisation")) + .when("fau", () -> set(PRISM_TRANSIENT_METHOD, "Fast adaptive uniformisation")), + "", "CTMC transient analysis method (unif, fau) [default: unif]"); + reg.addSwitch("heuristic", new EnumSwitch() + .when("none", () -> set(PRISM_HEURISTIC, "None")) + .when("speed", () -> set(PRISM_HEURISTIC, "Speed")) + .when("memory", () -> set(PRISM_HEURISTIC, "Memory")), + "", "Automatic choice of engines/settings (none, speed, memory) [default: none]"); + + // ── SOLUTION METHODS (LINEAR EQUATIONS) ────────────────────────────── + reg.beginGroup("SOLUTION METHODS (LINEAR EQUATIONS)"); + reg.addSwitch("power", "pow", "pwr", new FlagSwitch(() -> set(PRISM_LIN_EQ_METHOD, "Power")), + "", "Use the Power method for numerical computation"); + reg.addSwitch("jacobi", "jac", new FlagSwitch(() -> set(PRISM_LIN_EQ_METHOD, "Jacobi")), + "", "Use Jacobi for numerical computation [default]"); + reg.addSwitch("gaussseidel", "gs", new FlagSwitch(() -> { set(PRISM_LIN_EQ_METHOD, "Gauss-Seidel"); set(PRISM_MDP_SOLN_METHOD, "Gauss-Seidel"); set(PRISM_MDP_MULTI_SOLN_METHOD, "Gauss-Seidel"); set(PRISM_IMDP_SOLN_METHOD, "Gauss-Seidel"); - } else if (sw.equals("bgaussseidel") || sw.equals("bgs")) { - set(PRISM_LIN_EQ_METHOD, "Backwards Gauss-Seidel"); - } else if (sw.equals("pgaussseidel") || sw.equals("pgs")) { - set(PRISM_LIN_EQ_METHOD, "Pseudo-Gauss-Seidel"); - } else if (sw.equals("bpgaussseidel") || sw.equals("bpgs")) { - set(PRISM_LIN_EQ_METHOD, "Backwards Pseudo-Gauss-Seidel"); - } else if (sw.equals("jor")) { - set(PRISM_LIN_EQ_METHOD, "JOR"); - } else if (sw.equals("sor")) { - set(PRISM_LIN_EQ_METHOD, "SOR"); - } else if (sw.equals("bsor")) { - set(PRISM_LIN_EQ_METHOD, "Backwards SOR"); - } else if (sw.equals("psor")) { - set(PRISM_LIN_EQ_METHOD, "Pseudo-SOR"); - } else if (sw.equals("bpsor")) { - set(PRISM_LIN_EQ_METHOD, "Backwards Pseudo-SOR"); - } else if (sw.equals("valiter")) { + }), "", "Use Gauss-Seidel for numerical computation"); + reg.addSwitch("bgaussseidel", "bgs", new FlagSwitch(() -> set(PRISM_LIN_EQ_METHOD, "Backwards Gauss-Seidel")), + "", "Use Backwards Gauss-Seidel for numerical computation"); + reg.addSwitch("pgaussseidel", "pgs", new FlagSwitch(() -> set(PRISM_LIN_EQ_METHOD, "Pseudo-Gauss-Seidel")), + "", "Use Pseudo Gauss-Seidel for numerical computation"); + reg.addSwitch("bpgaussseidel", "bpgs", new FlagSwitch(() -> set(PRISM_LIN_EQ_METHOD, "Backwards Pseudo-Gauss-Seidel")), + "", "Use Backwards Pseudo Gauss-Seidel for numerical computation"); + reg.addSwitch("jor", new FlagSwitch(() -> set(PRISM_LIN_EQ_METHOD, "JOR")), + "", "Use JOR for numerical computation"); + reg.addSwitch("sor", new FlagSwitch(() -> set(PRISM_LIN_EQ_METHOD, "SOR")), + "", "Use SOR for numerical computation"); + reg.addSwitch("bsor", new FlagSwitch(() -> set(PRISM_LIN_EQ_METHOD, "Backwards SOR")), + "", "Use Backwards SOR for numerical computation"); + reg.addSwitch("psor", new FlagSwitch(() -> set(PRISM_LIN_EQ_METHOD, "Pseudo-SOR")), + "", "Use Pseudo SOR for numerical computation"); + reg.addSwitch("bpsor", new FlagSwitch(() -> set(PRISM_LIN_EQ_METHOD, "Backwards Pseudo-SOR")), + "", "Use Backwards Pseudo SOR for numerical computation"); + reg.addSwitch("omega", new DoubleSwitch(d -> set(PRISM_LIN_EQ_METHOD_PARAM, d)), + "", "Set over-relaxation parameter (for JOR/SOR/...) [default: 0.9]"); + + // ── SOLUTION METHODS (MDPS) ─────────────────────────────────────────── + reg.beginGroup("SOLUTION METHODS (MDPS)"); + reg.addSwitch("valiter", new FlagSwitch(() -> { set(PRISM_MDP_SOLN_METHOD, "Value iteration"); set(PRISM_MDP_MULTI_SOLN_METHOD, "Value iteration"); set(PRISM_IMDP_SOLN_METHOD, "Value iteration"); - } else if (sw.equals("politer")) { - set(PRISM_MDP_SOLN_METHOD, "Policy iteration"); - } else if (sw.equals("modpoliter")) { - set(PRISM_MDP_SOLN_METHOD, "Modified policy iteration"); - } else if (sw.equals("linprog") || sw.equals("lp")) { - set(PRISM_MDP_SOLN_METHOD, "Linear programming"); - set(PRISM_MDP_MULTI_SOLN_METHOD, "Linear programming"); - } - - // Interval iterations - else if (sw.equals("intervaliter") || - sw.equals("ii")) { + }), "", "Use value iteration for solving MDPs [default]"); + reg.addSwitchAlias("gaussseidel", new String[]{"gs"}, "Use Gauss-Seidel value iteration for solving MDPs"); + reg.addSwitch("politer", new FlagSwitch(() -> set(PRISM_MDP_SOLN_METHOD, "Policy iteration")), + "", "Use policy iteration for solving MDPs"); + reg.addSwitch("modpoliter", new FlagSwitch(() -> set(PRISM_MDP_SOLN_METHOD, "Modified policy iteration")), + "", "Use modified policy iteration for solving MDPs"); + reg.addSwitch("intervaliter", "ii", new OptionsOnlySwitch(OptionsIntervalIteration.parser(), parse -> { set(PRISM_INTERVAL_ITER, true); - - if (optionsString != null) { - optionsString = optionsString.trim(); - try { - OptionsIntervalIteration.validate(optionsString); - } catch (PrismException e) { - throw new PrismException("In options for -" + sw + " switch: " + e.getMessage()); - } - - // append options to existing ones - String iiOptions = getString(PRISM_INTERVAL_ITER_OPTIONS); - if ("".equals(iiOptions)) - iiOptions = optionsString; - else - iiOptions += "," + optionsString; - set(PRISM_INTERVAL_ITER_OPTIONS, iiOptions); + String opts = parse.options().trim(); + if (!opts.isEmpty()) { + // Parse options just to make sure they are valid + parse.run(opts); + // Then concatenate with any other -intervaliter options, and process later + String existing = getString(PRISM_INTERVAL_ITER_OPTIONS); + set(PRISM_INTERVAL_ITER_OPTIONS, "".equals(existing) ? opts : existing + "," + opts); } - } + }), "[:]", "Use interval iteration to solve MDPs/MCs (see -help -ii)", + log -> { + log.println("Use interval iteration to solve MDPs/MCs."); + log.println(); + log.println("If provided, is a comma-separated list of options taken from:"); + OptionsIntervalIteration.printOptions(log); + }); + reg.addSwitch("topological", new FlagSwitch(() -> set(PRISM_TOPOLOGICAL_VI, true)), + "", "Use topological value iteration"); - // Pmax quotient - else if (sw.equals("pmaxquotient")) { - set(PRISM_PMAX_QUOTIENT, true); - } + // ── SOLUTION METHOD SETTINGS ────────────────────────────────────────── + reg.beginGroup("SOLUTION METHOD SETTINGS"); + reg.addSwitch("relative", "rel", new FlagSwitch(() -> set(PRISM_TERM_CRIT, "Relative")), + "", "Use relative error for detecting convergence [default]"); + reg.addSwitch("absolute", "abs", new FlagSwitch(() -> set(PRISM_TERM_CRIT, "Absolute")), + "", "Use absolute error for detecting convergence"); + reg.addSwitch("epsilon", "e", (sw, a) -> { + double d = a.nextDouble(sw); + if (d < 0) throw new PrismException("Invalid value for -" + sw + " switch"); + set(PRISM_TERM_CRIT_PARAM, d); + }, "", "Set value of epsilon (for convergence check) [default: 1e-6]"); + reg.addSwitch("maxiters", (sw, a) -> { + int n = a.nextInt(sw); + if (n < 0) throw new PrismException("Invalid value for -" + sw + " switch"); + set(PRISM_MAX_ITERS, n); + }, "", "Set max number of iterations [default: 10000]"); + reg.addSwitch("gridresolution", (sw, a) -> { + int n = a.nextInt(sw); + if (n < 0) throw new PrismException("Invalid value for -" + sw + " switch"); + set(PRISM_GRID_RESOLUTION, n); + }, "", "Set resolution for fixed grid approximation (POMDP) [default: 10]"); - // Topological VI - else if (sw.equals("topological")) { - set(PRISM_TOPOLOGICAL_VI, true); - } + // ── MODEL CHECKING OPTIONS ──────────────────────────────────────────── + reg.beginGroup("MODEL CHECKING OPTIONS"); + reg.addSwitch("nopre", new FlagSwitch(() -> set(PRISM_PRECOMPUTATION, false)), + "", "Skip precomputation algorithms (where optional)"); + reg.addSwitch("noprob0", new FlagSwitch(() -> set(PRISM_PROB0, false)), + "", "Skip precomputation algorithm Prob0 (where optional)"); + reg.addSwitch("noprob1", new FlagSwitch(() -> set(PRISM_PROB1, false)), + "", "Skip precomputation algorithm Prob1 (where optional)"); + reg.addSwitch("noprerel", new FlagSwitch(() -> set(PRISM_PRE_REL, false)), + "", "Do not pre-compute/use predecessor relation, e.g. for precomputation"); + reg.addSwitch("fair", new FlagSwitch(() -> set(PRISM_FAIRNESS, true)), + "", "Use fairness (for model checking of MDPs)"); + reg.addSwitch("nofair", new FlagSwitch(() -> set(PRISM_FAIRNESS, false)), + "", "Don't use fairness (for model checking of MDPs) [default]"); + reg.addSwitch("fixdl", new FlagSwitch(() -> set(PRISM_FIX_DEADLOCKS, true)), + "", "Automatically put self-loops in deadlock states [default]"); + reg.addSwitch("nofixdl", new FlagSwitch(() -> set(PRISM_FIX_DEADLOCKS, false)), + "", "Do not automatically put self-loops in deadlock states"); + reg.addSwitch("noprobchecks", new FlagSwitch(() -> set(PRISM_DO_PROB_CHECKS, false)), + "", "Disable checks on model probabilities/rates"); + reg.addSwitch("sumroundoff", (sw, a) -> { + double d = a.nextDouble(sw); + if (d < 0) throw new PrismException("Invalid value for -" + sw + " switch"); + set(PRISM_SUM_ROUND_OFF, d); + }, "", "Set probability sum threshold [default: 1-e5]"); + reg.addSwitch("zerorewardcheck", new FlagSwitch(() -> prism.setCheckZeroLoops(true)), + "", "Check for absence of zero-reward loops"); + reg.addSwitch("nossdetect", new FlagSwitch(() -> set(PRISM_DO_SS_DETECTION, false)), + "", "Disable steady-state detection for CTMC transient computations"); + SwitchHandler sccMethodHandler = new EnumSwitch() + .when("xiebeerel", () -> set(PRISM_SCC_METHOD, "Xie-Beerel")) + .when("lockstep", () -> set(PRISM_SCC_METHOD, "Lockstep")) + .when("sccfind", () -> set(PRISM_SCC_METHOD, "SCC-Find")); + reg.addSwitch("sccmethod", sccMethodHandler, + "", "Specify (symbolic) SCC computation method (xiebeerel, lockstep, sccfind)"); + reg.addSwitch("bsccmethod", sccMethodHandler); // hidden alias + reg.addSwitch("symm", (sw, a) -> { + String p1 = a.next(sw); + String p2 = a.next(sw); + set(PRISM_SYMM_RED_PARAMS, p1 + " " + p2); + }, "", "Symmetry reduction options string"); + reg.addSwitch("aroptions", (sw, a) -> { + String v = a.next(sw).trim(); + String existing = getString(PRISM_AR_OPTIONS); + set(PRISM_AR_OPTIONS, "".equals(existing) ? v : existing + "," + v); + }, "", "Abstraction-refinement engine options string", + log -> { + log.println(" is a comma-separated list of options regarding abstraction-refinement:"); + QuantAbstractRefine.printOptions(log); + }); + reg.addSwitch("pathviaautomata", new FlagSwitch(() -> set(PRISM_PATH_VIA_AUTOMATA, true)), + "", "Handle all path formulas via automata constructions"); + reg.addSwitch("nodasimplify", new FlagSwitch(() -> set(PRISM_NO_DA_SIMPLIFY, true)), + "", "Do not attempt to simplify deterministic automata, acceptance conditions"); + reg.addSwitch("exportadv", (sw, a) -> { + set(PRISM_EXPORT_ADV, "DTMC"); + set(PRISM_EXPORT_ADV_FILENAME, a.next(sw)); + }, "", "Export an adversary from MDP model checking (as a DTMC)"); + reg.addSwitch("exportadvmdp", (sw, a) -> { + set(PRISM_EXPORT_ADV, "MDP"); + set(PRISM_EXPORT_ADV_FILENAME, a.next(sw)); + }, "", "Export an adversary from MDP model checking (as an MDP)"); + reg.addSwitch("ltl2datool", new StringSwitch(s -> set(PRISM_LTL2DA_TOOL, s)), + "", "Run executable to convert LTL formulas to deterministic automata"); + reg.addSwitch("ltl2dasyntax", new EnumSwitch() + .when("lbt", () -> set(PRISM_LTL2DA_SYNTAX, "LBT")) + .when("spin", () -> set(PRISM_LTL2DA_SYNTAX, "Spin")) + .when("spot", () -> set(PRISM_LTL2DA_SYNTAX, "Spot")) + .when("rabinizer", () -> set(PRISM_LTL2DA_SYNTAX, "Rabinizer")), + "", "Specify output format for -ltl2datool switch (lbt, spin, spot, rabinizer)"); + reg.addSwitch("exportiterations", new FlagSwitch(() -> set(PRISM_EXPORT_ITERATIONS, true)), + "", "Export vectors for iteration algorithms to file"); + reg.addSwitch("pmaxquotient", new FlagSwitch(() -> set(PRISM_PMAX_QUOTIENT, true)), + "", "For Pmax computations in MDPs, compute in the MEC quotient"); - // Linear equation solver over-relaxation parameter - else if (sw.equals("omega")) { - if (i < args.length - 1) { - try { - d = Double.parseDouble(args[++i]); - set(PRISM_LIN_EQ_METHOD_PARAM, d); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - // Termination criterion (iterative methods) - else if (sw.equals("relative") || sw.equals("rel")) { - set(PRISM_TERM_CRIT, "Relative"); - } - else if (sw.equals("absolute") || sw.equals("abs")) { - set(PRISM_TERM_CRIT, "Absolute"); - } - // Termination criterion parameter - else if (sw.equals("epsilon") || sw.equals("e")) { - if (i < args.length - 1) { - try { - d = Double.parseDouble(args[++i]); - if (d < 0) - throw new NumberFormatException(""); - set(PRISM_TERM_CRIT_PARAM, d); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - // Max iters - else if (sw.equals("maxiters")) { - if (i < args.length - 1) { - try { - j = Integer.parseInt(args[++i]); - if (j < 0) - throw new NumberFormatException(""); - set(PRISM_MAX_ITERS, j); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - // export iterations - else if (sw.equals("exportiterations")) { - set(PRISM_EXPORT_ITERATIONS, true); - } - // fixed grid resolution - else if (sw.equals("gridresolution")) { - if (i < args.length - 1) { - try { - j = Integer.parseInt(args[++i]); - if (j < 0) - throw new NumberFormatException(""); - set(PRISM_GRID_RESOLUTION, j); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - // export probabilities/rewards with up to n significant decimal places - else if (sw.equals("exportmodelprecision")) { - if (i < args.length - 1) { - try { - int precision = Integer.parseInt(args[++i]); - if (!RANGE_EXPORT_DOUBLE_PRECISION.contains(precision)) - throw new NumberFormatException(""); - set(PRISM_EXPORT_MODEL_PRECISION, precision); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - // export headers off - else if (sw.equals("noexportheaders")) { - set(PRISM_EXPORT_MODEL_HEADERS, false); - } + // ── MULTI-OBJECTIVE MODEL CHECKING ─────────────────────────────────── + reg.beginGroup("MULTI-OBJECTIVE MODEL CHECKING"); + reg.addSwitch("linprog", "lp", new FlagSwitch(() -> { + set(PRISM_MDP_SOLN_METHOD, "Linear programming"); + set(PRISM_MDP_MULTI_SOLN_METHOD, "Linear programming"); + }), "", "Use linear programming for multi-objective model checking"); + reg.addSwitch("multimaxpoints", (sw, a) -> { + int n = a.nextInt(sw); + if (n < 0) throw new PrismException("Invalid value for -" + sw + " switch"); + set(PRISM_MULTI_MAX_POINTS, n); + }, "", "Maximal number of corner points for (valiter-based) multi-objective"); + reg.addSwitch("paretoepsilon", (sw, a) -> { + double d = a.nextDouble(sw); + if (d < 0) throw new PrismException("Value for -" + sw + " switch must be non-negative"); + set(PRISM_PARETO_EPSILON, d); + }, "", "Threshold for Pareto curve approximation"); + reg.addSwitch("exportpareto", new StringSwitch(s -> set(PRISM_EXPORT_PARETO_FILENAME, s)), + "", "When computing Pareto curves, export points to a file"); - // MODEL CHECKING OPTIONS: - - // Precomputation algs off - else if (sw.equals("nopre")) { - set(PRISM_PRECOMPUTATION, false); - } - else if (sw.equals("noprob0")) { - set(PRISM_PROB0, false); - } - else if (sw.equals("noprob1")) { - set(PRISM_PROB1, false); - } - // Use predecessor relation? (e.g. for precomputation) - else if (sw.equals("noprerel")) { - set(PRISM_PRE_REL, false); - } - // Fix deadlocks on/off - else if (sw.equals("fixdl")) { - set(PRISM_FIX_DEADLOCKS, true); - } - else if (sw.equals("nofixdl")) { - set(PRISM_FIX_DEADLOCKS, false); - } - // Fairness on/off - else if (sw.equals("fair")) { - set(PRISM_FAIRNESS, true); - } - else if (sw.equals("nofair")) { - set(PRISM_FAIRNESS, false); - } - // Prob/rate checks off - else if (sw.equals("noprobchecks")) { - set(PRISM_DO_PROB_CHECKS, false); - } - // Sum round-off threshold - else if (sw.equals("sumroundoff")) { - if (i < args.length - 1) { - try { - d = Double.parseDouble(args[++i]); - if (d < 0) - throw new NumberFormatException(""); - set(PRISM_SUM_ROUND_OFF, d); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - // No steady-state detection - else if (sw.equals("nossdetect")) { - set(PRISM_DO_SS_DETECTION, false); - } - // SCC computation algorithm - else if (sw.equals("sccmethod") || sw.equals("bsccmethod")) { - if (i < args.length - 1) { - s = args[++i]; - if (s.equals("xiebeerel")) - set(PRISM_SCC_METHOD, "Xie-Beerel"); - else if (s.equals("lockstep")) - set(PRISM_SCC_METHOD, "Lockstep"); - else if (s.equals("sccfind")) - set(PRISM_SCC_METHOD, "SCC-Find"); - else - throw new PrismException("Unrecognised option for -" + sw + " switch (options are: xiebeerel, lockstep, sccfind)"); - } else { - throw new PrismException("No parameter specified for -" + sw + " switch"); - } - } - // Enable symmetry reduction - else if (sw.equals("symm")) { - if (i < args.length - 2) { - set(PRISM_SYMM_RED_PARAMS, args[++i] + " " + args[++i]); - } else { - throw new PrismException("-symm switch requires two parameters (num. modules before/after symmetric ones)"); - } - } - // Abstraction-refinement engine options string (append if already partially specified) - else if (sw.equals("aroptions")) { - if (i < args.length - 1) { - String arOptions = getString(PRISM_AR_OPTIONS); - if ("".equals(arOptions)) - arOptions = args[++i].trim(); - else - arOptions += "," + args[++i].trim(); - set(PRISM_AR_OPTIONS, arOptions); - } else { - throw new PrismException("No parameter specified for -" + sw + " switch"); - } - } - // Handle all path formulas via automata constructions - else if (sw.equals("pathviaautomata")) { - set(PRISM_PATH_VIA_AUTOMATA, true); - } - // Don't simplify deterministic automata - else if (sw.equals("nodasimplify")) { - set(PRISM_NO_DA_SIMPLIFY, true); - } + // ── OUTPUT OPTIONS ──────────────────────────────────────────────────── + reg.beginGroup("OUTPUT OPTIONS"); + reg.addSwitch("verbose", "v", new FlagSwitch(() -> set(PRISM_VERBOSE, true)), + "", "Verbose mode: print out state lists and probability vectors"); + reg.addSwitch("extraddinfo", new FlagSwitch(() -> set(PRISM_EXTRA_DD_INFO, true)), + "", "Display extra info about some (MT)BDDs"); + reg.addSwitch("extrareachinfo", new FlagSwitch(() -> set(PRISM_EXTRA_REACH_INFO, true)), + "", "Display extra info about progress of reachability"); - - // MULTI-OBJECTIVE MODEL CHECKING OPTIONS: - - // Max different corner points that will be generated when performing - // target driven multi-obj verification. - else if (sw.equals("multimaxpoints")) { - if (i < args.length - 1) { - try { - j = Integer.parseInt(args[++i]); - if (j < 0) - throw new NumberFormatException(""); - set(PRISM_MULTI_MAX_POINTS, j); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - // Threshold for approximate Pareto curve generation - else if (sw.equals("paretoepsilon")) { - if (i < args.length - 1) { - try { - d = Double.parseDouble(args[++i]); - if (d < 0) - throw new PrismException("Value for -" + sw + " switch must be non-negative"); - set(PRISM_PARETO_EPSILON, d); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - else if (sw.equals("exportpareto")) { - if (i < args.length - 1) { - set(PRISM_EXPORT_PARETO_FILENAME, args[++i]); - } else { - throw new PrismException("No file specified for -" + sw + " switch"); - } - } - - // OUTPUT OPTIONS: - - // Verbosity - else if (sw.equals("verbose") || sw.equals("v")) { - set(PRISM_VERBOSE, true); - } - // Extra dd info on - else if (sw.equals("extraddinfo")) { - set(PRISM_EXTRA_DD_INFO, true); - } - // Extra reach info on - else if (sw.equals("extrareachinfo")) { - set(PRISM_EXTRA_REACH_INFO, true); - } - - // SPARSE/HYBRID/MTBDD OPTIONS: - - // Turn off compact option for sparse matrix storage - else if (sw.equals("nocompact")) { - set(PRISM_COMPACT, false); - } - // Sparse bits info - else if (sw.equals("sbl")) { - if (i < args.length - 1) { - try { - j = Integer.parseInt(args[++i]); - if (j < -1) - throw new NumberFormatException(); - set(PRISM_NUM_SB_LEVELS, j); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - else if (sw.equals("sbmax")) { - if (i < args.length - 1) { - try { - j = Integer.parseInt(args[++i]); - if (j < 0) - throw new NumberFormatException(); - set(PRISM_SB_MAX_MEM, j); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - // Hybrid SOR info - else if (sw.equals("sorl") || sw.equals("gsl")) { - if (i < args.length - 1) { - try { - j = Integer.parseInt(args[++i]); - if (j < -1) - throw new NumberFormatException(); - set(PRISM_NUM_SOR_LEVELS, j); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - else if (sw.equals("sormax") || sw.equals("gsmax")) { - if (i < args.length - 1) { - try { - j = Integer.parseInt(args[++i]); - if (j < 0) - throw new NumberFormatException(); - set(PRISM_SOR_MAX_MEM, j); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - // CUDD settings - else if (sw.equals("cuddmaxmem")) { - if (i < args.length - 1) { - set(PRISM_CUDD_MAX_MEM, args[++i]); - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - else if (sw.equals("cuddepsilon")) { - if (i < args.length - 1) { - try { - d = Double.parseDouble(args[++i]); - if (d < 0) - throw new NumberFormatException(""); - set(PRISM_CUDD_EPSILON, d); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } else if (sw.equals("ddextrastatevars")) { - if (i < args.length - 1) { - try { - int v = Integer.parseInt(args[++i]); - if (v < 0) - throw new NumberFormatException(""); - set(PRISM_DD_EXTRA_STATE_VARS, v); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } else if (sw.equals("ddextraactionvars")) { - if (i < args.length - 1) { - try { - int v = Integer.parseInt(args[++i]); - if (v < 0) - throw new NumberFormatException(""); - set(PRISM_DD_EXTRA_ACTION_VARS, v); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - - // ADVERSARIES/COUNTEREXAMPLES: - - // Export adversary to file - else if (sw.equals("exportadv")) { - if (i < args.length - 1) { - set(PRISM_EXPORT_ADV, "DTMC"); - set(PRISM_EXPORT_ADV_FILENAME, args[++i]); - } else { - throw new PrismException("No file specified for -" + sw + " switch"); - } - } - // Export adversary to file, as an MDP - else if (sw.equals("exportadvmdp")) { - if (i < args.length - 1) { - set(PRISM_EXPORT_ADV, "MDP"); - set(PRISM_EXPORT_ADV_FILENAME, args[++i]); - } else { - throw new PrismException("No file specified for -" + sw + " switch"); - } - } - - // LTL2DA TOOLS - - else if (sw.equals("ltl2datool")) { - if (i < args.length - 1) { - String filename = args[++i]; - set(PRISM_LTL2DA_TOOL, filename); - } else { - throw new PrismException("The -" + sw + " switch requires one argument (path to the executable)"); - } - } - else if (sw.equals("ltl2dasyntax")) { - if (i < args.length - 1) { - String syntax = args[++i]; - switch (syntax) { - case "lbt": - set(PRISM_LTL2DA_SYNTAX, "LBT"); - break; - case "spin": - set(PRISM_LTL2DA_SYNTAX, "Spin"); - break; - case "spot": - set(PRISM_LTL2DA_SYNTAX, "Spot"); - break; - case "rabinizer": - set(PRISM_LTL2DA_SYNTAX, "Rabinizer"); - break; - default: - throw new PrismException("Unrecognised option for -" + sw + " switch (options are: lbt, spin, spot, rabinizer)"); - } - } else { - throw new PrismException("The -" + sw + " switch requires one argument (options are: lbt, spin, spot, rabinizer)"); - } - } + // ── SPARSE/HYBRID/MTBDD OPTIONS ────────────────────────────────────── + reg.beginGroup("SPARSE/HYBRID/MTBDD OPTIONS"); + reg.addSwitch("nocompact", new FlagSwitch(() -> set(PRISM_COMPACT, false)), + "", "Switch off \"compact\" sparse storage schemes"); + reg.addSwitch("sbl", (sw, a) -> { + int n = a.nextInt(sw); + if (n < -1) throw new PrismException("Invalid value for -" + sw + " switch"); + set(PRISM_NUM_SB_LEVELS, n); + }, "", "Set number of levels (for hybrid engine) [default: -1]"); + reg.addSwitch("sbmax", (sw, a) -> { + int n = a.nextInt(sw); + if (n < 0) throw new PrismException("Invalid value for -" + sw + " switch"); + set(PRISM_SB_MAX_MEM, n); + }, "", "Set memory limit (KB) (for hybrid engine) [default: 1024]"); + reg.addSwitch("gsl", "sorl", (sw, a) -> { + int n = a.nextInt(sw); + if (n < -1) throw new PrismException("Invalid value for -" + sw + " switch"); + set(PRISM_NUM_SOR_LEVELS, n); + }, "", "Set number of levels for hybrid GS/SOR [default: -1]"); + reg.addSwitch("gsmax", "sormax", (sw, a) -> { + int n = a.nextInt(sw); + if (n < 0) throw new PrismException("Invalid value for -" + sw + " switch"); + set(PRISM_SOR_MAX_MEM, n); + }, "", "Set memory limit (KB) for hybrid GS/SOR [default: 1024]"); + reg.addSwitch("cuddmaxmem", new StringSwitch(s -> set(PRISM_CUDD_MAX_MEM, s)), + "", "Set max memory for CUDD package, e.g. 125k, 50m, 4g [default: 1g]"); + reg.addSwitch("cuddepsilon", (sw, a) -> { + double d = a.nextDouble(sw); + if (d < 0) throw new PrismException("Invalid value for -" + sw + " switch"); + set(PRISM_CUDD_EPSILON, d); + }, "", "Set epsilon value for CUDD package [default: 1e-15]"); + reg.addSwitch("ddsanity", new FlagSwitch(() -> set(PRISM_JDD_SANITY_CHECKS, true)), + "", "Enable internal sanity checks (causes slow-down)"); + reg.addSwitch("ddextrastatevars", (sw, a) -> { + int n = a.nextInt(sw); + if (n < 0) throw new PrismException("Invalid value for -" + sw + " switch"); + set(PRISM_DD_EXTRA_STATE_VARS, n); + }, "", "Set the number of preallocated state vars [default: 20]"); + reg.addSwitch("ddextraactionvars", (sw, a) -> { + int n = a.nextInt(sw); + if (n < 0) throw new PrismException("Invalid value for -" + sw + " switch"); + set(PRISM_DD_EXTRA_ACTION_VARS, n); + }, "", "Set the number of preallocated action vars [default: 20]"); - // DEBUGGING / SANITY CHECKS - else if (sw.equals("ddsanity")) { - set(PRISM_JDD_SANITY_CHECKS, true); - } + // ── PARAMETRIC MODEL CHECKING OPTIONS ──────────────────────────────── + reg.beginGroup("PARAMETRIC MODEL CHECKING OPTIONS"); + reg.addSwitch("param", paramHandler, + "", "Do parametric model checking with parameters (and ranges) "); + reg.addSwitch("paramprecision", new StringSwitch(s -> set(PRISM_PARAM_PRECISION, s)), + "", "Set max undecided region for parameter synthesis [default: 5/100]"); + reg.addSwitch("paramsplit", new EnumSwitch() + .when("longest", () -> set(PRISM_PARAM_SPLIT, "Longest")) + .when("all", () -> set(PRISM_PARAM_SPLIT, "All")), + "", "Set method to split parameter regions (longest,all) [default: longest]"); + reg.addSwitch("parambisim", new EnumSwitch() + .when("strong", () -> set(PRISM_PARAM_BISIM, "Strong")) + .when("weak", () -> set(PRISM_PARAM_BISIM, "Weak")) + .when("none", () -> set(PRISM_PARAM_BISIM, "None")), + "", "Set bisimulation minimisation for parameter synthesis (weak,strong,none) [default: weak]"); + reg.addSwitch("paramfunction", new EnumSwitch() + .when("jascached", () -> set(PRISM_PARAM_FUNCTION, "JAS-cached")) + .when("jas", () -> set(PRISM_PARAM_FUNCTION, "JAS")) + .when("dag", () -> set(PRISM_PARAM_FUNCTION, "DAG")), + "", "Set function representation for parameter synthesis (jascached,jas) [default: jascached]"); + reg.addSwitch("paramelimorder", new EnumSwitch() + .when("arb", () -> set(PRISM_PARAM_ELIM_ORDER, "Arbitrary")) + .when("fw", () -> set(PRISM_PARAM_ELIM_ORDER, "Forward")) + .when("fwrev", () -> set(PRISM_PARAM_ELIM_ORDER, "Forward-reversed")) + .when("bw", () -> set(PRISM_PARAM_ELIM_ORDER, "Backward")) + .when("bwrev", () -> set(PRISM_PARAM_ELIM_ORDER, "Backward-reversed")) + .when("rand", () -> set(PRISM_PARAM_ELIM_ORDER, "Random")), + "", "Set elimination order for parameter synthesis (arb,fw,fwrev,bw,bwrev,rand) [default: bw]"); + reg.addSwitch("paramrandompoints", (sw, a) -> { + int n = a.nextInt(sw); + if (n < 0) throw new PrismException("Invalid value for -" + sw + " switch"); + set(PRISM_PARAM_RANDOM_POINTS, n); + }, "", "Set number of random points to evaluate per region [default: 5]"); + reg.addSwitch("paramsubsumeregions", (sw, a) -> { + set(PRISM_PARAM_SUBSUME_REGIONS, Boolean.parseBoolean(a.next(sw))); + }, "", "Subsume adjacent regions during analysis [default: true]"); + reg.addSwitch("paramdagmaxerror", (sw, a) -> { + double d = a.nextDouble(sw); + if (d < 0) throw new PrismException("Invalid value for -" + sw + " switch"); + set(PRISM_PARAM_DAG_MAX_ERROR, d); + }, "", "Maximal error probability allowed for DAG function representation [default: 1E-100]"); - // PARAMETRIC MODEL CHECKING: - - else if (sw.equals("param")) { - set(PRISM_PARAM_ENABLED, true); - } - else if (sw.equals("paramprecision")) { - if (i < args.length - 1) { - set(PRISM_PARAM_PRECISION, args[++i]); - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - else if (sw.equals("paramsplit")) { - if (i < args.length - 1) { - s = args[++i]; - if (s.equals("longest")) - set(PRISM_PARAM_SPLIT, "Longest"); - else if (s.equals("all")) - set(PRISM_PARAM_SPLIT, "All"); - else - throw new PrismException("Unrecognised option for -" + sw + " switch (options are: longest, all)"); - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - else if (sw.equals("parambisim")) { - if (i < args.length - 1) { - s = args[++i]; - if (s.equals("strong")) - set(PRISM_PARAM_BISIM, "Strong"); - else if (s.equals("weak")) - set(PRISM_PARAM_BISIM, "Weak"); - else if (s.equals("none")) - set(PRISM_PARAM_BISIM, "None"); - else - throw new PrismException("Unrecognised option for -" + sw + " switch (options are: strong, weak, none)"); - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - else if (sw.equals("paramfunction")) { - if (i < args.length - 1) { - s = args[++i]; - if (s.equals("jascached")) - set(PRISM_PARAM_FUNCTION, "JAS-cached"); - else if (s.equals("jas")) - set(PRISM_PARAM_FUNCTION, "JAS"); - else if (s.equals("dag")) - set(PRISM_PARAM_FUNCTION, "DAG"); - else - throw new PrismException("Unrecognised option for -" + sw + " switch (options are: jascached, jas, dag)"); - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - else if (sw.equals("paramelimorder")) { - if (i < args.length - 1) { - s = args[++i]; - if (s.equals("arb")) - set(PRISM_PARAM_ELIM_ORDER, "Arbitrary"); - else if (s.equals("fw")) - set(PRISM_PARAM_ELIM_ORDER, "Forward"); - else if (s.equals("fwrev")) - set(PRISM_PARAM_ELIM_ORDER, "Forward-reversed"); - else if (s.equals("bw")) - set(PRISM_PARAM_ELIM_ORDER, "Backward"); - else if (s.equals("bwrev")) - set(PRISM_PARAM_ELIM_ORDER, "Backward-reversed"); - else if (s.equals("rand")) - set(PRISM_PARAM_ELIM_ORDER, "Random"); - else - throw new PrismException("Unrecognised option for -" + sw + " switch (options are: arb,fw,fwrev,bw,bwrev,rand)"); - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - else if (sw.equals("paramrandompoints")) { - try { - j = Integer.parseInt(args[++i]); - if (j < 0) - throw new NumberFormatException(); - set(PRISM_PARAM_RANDOM_POINTS, j); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } - else if (sw.equals("paramsubsumeregions")) { - boolean b = Boolean.parseBoolean(args[++i]); - set(PRISM_PARAM_SUBSUME_REGIONS, b); - } - else if (sw.equals("paramdagmaxerror")) { - try { - d = Double.parseDouble(args[++i]); - if (d < 0) - throw new NumberFormatException(); - set(PRISM_PARAM_DAG_MAX_ERROR, d); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } - - // FAST ADAPTIVE UNIFORMISATION - - // Epsilon for fast adaptive uniformisation - else if (sw.equals("fauepsilon")) { - if (i < args.length - 1) { - try { - d = Double.parseDouble(args[++i]); - if (d < 0) - throw new NumberFormatException(""); - set(PRISM_FAU_EPSILON, d); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - // Delta for fast adaptive uniformisation - else if (sw.equals("faudelta")) { - if (i < args.length - 1) { - try { - d = Double.parseDouble(args[++i]); - if (d < 0) - throw new NumberFormatException(""); - set(PRISM_FAU_DELTA, d); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - // Array threshold for fast adaptive uniformisation - else if (sw.equals("fauarraythreshold")) { - if (i < args.length - 1) { - try { - j = Integer.parseInt(args[++i]); - if (j < 0) - throw new NumberFormatException(""); - set(PRISM_FAU_ARRAYTHRESHOLD, j); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - // Number of intervals for fast adaptive uniformisation - else if (sw.equals("fauintervals")) { - if (i < args.length - 1) { - try { - j = Integer.parseInt(args[++i]); - if (j < 0) - throw new NumberFormatException(""); - set(PRISM_FAU_INTERVALS, j); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - else if (sw.equals("fauinitival")) { - if (i < args.length - 1) { - try { - d = Double.parseDouble(args[++i]); - if (d < 0.0) - throw new NumberFormatException(""); - set(PRISM_FAU_INITIVAL, d); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } + // ── FAST ADAPTIVE UNIFORMISATION (FAU) OPTIONS ─────────────────────── + reg.beginGroup("FAST ADAPTIVE UNIFORMISATION (FAU) OPTIONS"); + reg.addSwitch("fauepsilon", (sw, a) -> { + double d = a.nextDouble(sw); + if (d < 0) throw new PrismException("Invalid value for -" + sw + " switch"); + set(PRISM_FAU_EPSILON, d); + }, "", "Set probability threshold of birth process in FAU [default: 1e-6]"); + reg.addSwitch("faudelta", (sw, a) -> { + double d = a.nextDouble(sw); + if (d < 0) throw new PrismException("Invalid value for -" + sw + " switch"); + set(PRISM_FAU_DELTA, d); + }, "", "Set probability threshold for irrelevant states in FAU [default: 1e-12]"); + reg.addSwitch("fauarraythreshold", (sw, a) -> { + int n = a.nextInt(sw); + if (n < 0) throw new PrismException("Invalid value for -" + sw + " switch"); + set(PRISM_FAU_ARRAYTHRESHOLD, n); + }, "", "Set threshold when to switch to sparse matrix in FAU [default: 100]"); + reg.addSwitch("fauintervals", (sw, a) -> { + int n = a.nextInt(sw); + if (n < 0) throw new PrismException("Invalid value for -" + sw + " switch"); + set(PRISM_FAU_INTERVALS, n); + }, "", "Set number of intervals to divide time intervals into for FAU [default: 1]"); + reg.addSwitch("fauinitival", (sw, a) -> { + double d = a.nextDouble(sw); + if (d < 0.0) throw new PrismException("Invalid value for -" + sw + " switch"); + set(PRISM_FAU_INITIVAL, d); + }, "", "Set length of additional initial time interval for FAU [default: 1.0]"); - // HIDDEN OPTIONS - - // export property automaton to file (hidden option) - else if (sw.equals("exportpropaut")) { - if (i < args.length - 1) { - setExportPropAut(true); - setExportPropAutFilename(args[++i]); - setExportPropAutType("txt"); // default - for (Map.Entry option : options.entrySet()) { - if (option.getKey().equals("txt")) { - setExportPropAutType("txt"); - } else if (option.getKey().equals("dot")) { - setExportPropAutType("dot"); - } else if (option.getKey().equals("hoa")) { - setExportPropAutType("hoa"); - } else { - throw new PrismException("Unknown option \"" + option.getKey() + "\" for -" + sw + " switch"); - } + // Hidden switch + reg.addSwitch("exportpropaut", (sw, a) -> { + Map options = splitOptionsString(a.optionsString()); + setExportPropAut(true); + setExportPropAutFilename(a.next(sw)); + setExportPropAutType("txt"); // default + for (Map.Entry option : options.entrySet()) { + switch (option.getKey()) { + case "txt": setExportPropAutType("txt"); break; + case "dot": setExportPropAutType("dot"); break; + case "hoa": setExportPropAutType("hoa"); break; + default: throw new PrismException("Unknown option \"" + option.getKey() + "\" for -" + sw + " switch"); } - } else { - throw new PrismException("No file specified for -" + sw + " switch"); } - } - - // unknown switch - error - else { - throw new PrismException("Invalid switch -" + sw + " (type \"prism -help\" for full list)"); - } - - return i + 1; + }); } - + /** * Split a switch of the form -switch:options into parts. * The latter can be empty, in which case the : is optional. @@ -1823,149 +1400,6 @@ private static Map splitOptionsString(String optionsString) return map; } - /** - * Print a fragment of the -help message, - * i.e. a list of the command-line switches handled by this class. - */ - public static void printHelp(PrismLog mainLog) - { - mainLog.println(); - mainLog.println("EXPORT OPTIONS:"); - mainLog.println("-exportmodelprecision ....... Export probabilities/rewards with n significant decimal places"); - mainLog.println("-noexportheaders ............... Don't include headers when exporting rewards"); - mainLog.println(); - mainLog.println("ENGINES/METHODS:"); - mainLog.println("-mtbdd (or -m) ................. Use the MTBDD engine"); - mainLog.println("-sparse (or -s) ................ Use the Sparse engine"); - mainLog.println("-hybrid (or -h) ................ Use the Hybrid engine [default]"); - mainLog.println("-explicit (or -ex) ............. Use the explicit engine"); - mainLog.println("-exact ......................... Perform exact (arbitrary precision) model checking"); - mainLog.println("-ptamethod .............. Specify PTA engine (games, digital, backwards) [default: games]"); - mainLog.println("-transientmethod ........ CTMC transient analysis method (unif, fau) [default: unif]"); - mainLog.println("-heuristic .............. Automatic choice of engines/settings (none, speed, memory) [default: none]"); - mainLog.println(); - mainLog.println("SOLUTION METHODS (LINEAR EQUATIONS):"); - mainLog.println("-power (or -pow, -pwr) ......... Use the Power method for numerical computation"); - mainLog.println("-jacobi (or -jac) .............. Use Jacobi for numerical computation [default]"); - mainLog.println("-gaussseidel (or -gs) .......... Use Gauss-Seidel for numerical computation"); - mainLog.println("-bgaussseidel (or -bgs) ........ Use Backwards Gauss-Seidel for numerical computation"); - mainLog.println("-pgaussseidel (or -pgs) ........ Use Pseudo Gauss-Seidel for numerical computation"); - mainLog.println("-bpgaussseidel (or -bpgs) ...... Use Backwards Pseudo Gauss-Seidel for numerical computation"); - mainLog.println("-jor ........................... Use JOR for numerical computation"); - mainLog.println("-sor ........................... Use SOR for numerical computation"); - mainLog.println("-bsor .......................... Use Backwards SOR for numerical computation"); - mainLog.println("-psor .......................... Use Pseudo SOR for numerical computation"); - mainLog.println("-bpsor ......................... Use Backwards Pseudo SOR for numerical computation"); - mainLog.println("-omega ..................... Set over-relaxation parameter (for JOR/SOR/...) [default: 0.9]"); - mainLog.println(); - mainLog.println("SOLUTION METHODS (MDPS):"); - mainLog.println("-valiter ....................... Use value iteration for solving MDPs [default]"); - mainLog.println("-gaussseidel (or -gs) .......... Use Gauss-Seidel value iteration for solving MDPs"); - mainLog.println("-politer ....................... Use policy iteration for solving MDPs"); - mainLog.println("-modpoliter .................... Use modified policy iteration for solving MDPs"); - mainLog.println("-intervaliter (or -ii) ......... Use interval iteration to solve MDPs/MCs (see -help -ii)"); - mainLog.println("-topological ................... Use topological value iteration"); - mainLog.println(); - mainLog.println("SOLUTION METHOD SETTINGS"); - mainLog.println("-relative (or -rel) ............ Use relative error for detecting convergence [default]"); - mainLog.println("-absolute (or -abs) ............ Use absolute error for detecting convergence"); - mainLog.println("-epsilon (or -e ) ....... Set value of epsilon (for convergence check) [default: 1e-6]"); - mainLog.println("-maxiters .................. Set max number of iterations [default: 10000]"); - mainLog.println("-gridresolution .............Set resolution for fixed grid approximation (POMDP) [default: 10]"); - - mainLog.println(); - mainLog.println("MODEL CHECKING OPTIONS:"); - mainLog.println("-nopre ......................... Skip precomputation algorithms (where optional)"); - mainLog.println("-noprob0 ....................... Skip precomputation algorithm Prob0 (where optional)"); - mainLog.println("-noprob1 ....................... Skip precomputation algorithm Prob1 (where optional)"); - mainLog.println("-noprerel ...................... Do not pre-compute/use predecessor relation, e.g. for precomputation"); - mainLog.println("-fair .......................... Use fairness (for model checking of MDPs)"); - mainLog.println("-nofair ........................ Don't use fairness (for model checking of MDPs) [default]"); - mainLog.println("-fixdl ......................... Automatically put self-loops in deadlock states [default]"); - mainLog.println("-nofixdl ....................... Do not automatically put self-loops in deadlock states"); - mainLog.println("-noprobchecks .................. Disable checks on model probabilities/rates"); - mainLog.println("-sumroundoff ............... Set probability sum threshold [default: 1-e5]"); - mainLog.println("-zerorewardcheck ............... Check for absence of zero-reward loops"); - mainLog.println("-nossdetect .................... Disable steady-state detection for CTMC transient computations"); - mainLog.println("-sccmethod .............. Specify (symbolic) SCC computation method (xiebeerel, lockstep, sccfind)"); - mainLog.println("-symm ................. Symmetry reduction options string"); - mainLog.println("-aroptions ............ Abstraction-refinement engine options string"); - mainLog.println("-pathviaautomata ............... Handle all path formulas via automata constructions"); - mainLog.println("-nodasimplify .................. Do not attempt to simplify deterministic automata, acceptance conditions"); - mainLog.println("-exportadv .............. Export an adversary from MDP model checking (as a DTMC)"); - mainLog.println("-exportadvmdp ........... Export an adversary from MDP model checking (as an MDP)"); - mainLog.println("-ltl2datool ............. Run executable to convert LTL formulas to deterministic automata"); - mainLog.println("-ltl2dasyntax .............. Specify output format for -ltl2datool switch (lbt, spin, spot, rabinizer)"); - mainLog.println("-exportiterations .............. Export vectors for iteration algorithms to file"); - mainLog.println("-pmaxquotient .................. For Pmax computations in MDPs, compute in the MEC quotient"); - - mainLog.println(); - mainLog.println("MULTI-OBJECTIVE MODEL CHECKING:"); - mainLog.println("-linprog (or -lp) .............. Use linear programming for multi-objective model checking"); - mainLog.println("-multimaxpoints ............ Maximal number of corner points for (valiter-based) multi-objective"); - mainLog.println("-paretoepsilon ............. Threshold for Pareto curve approximation"); - mainLog.println("-exportpareto ........... When computing Pareto curves, export points to a file"); - mainLog.println(); - mainLog.println("OUTPUT OPTIONS:"); - mainLog.println("-verbose (or -v) ............... Verbose mode: print out state lists and probability vectors"); - mainLog.println("-extraddinfo ................... Display extra info about some (MT)BDDs"); - mainLog.println("-extrareachinfo ................ Display extra info about progress of reachability"); - mainLog.println(); - mainLog.println("SPARSE/HYBRID/MTBDD OPTIONS:"); - mainLog.println("-nocompact ..................... Switch off \"compact\" sparse storage schemes"); - mainLog.println("-sbl ....................... Set number of levels (for hybrid engine) [default: -1]"); - mainLog.println("-sbmax ..................... Set memory limit (KB) (for hybrid engine) [default: 1024]"); - mainLog.println("-gsl (or sorl ) ......... Set number of levels for hybrid GS/SOR [default: -1]"); - mainLog.println("-gsmax (or sormax ) ..... Set memory limit (KB) for hybrid GS/SOR [default: 1024]"); - mainLog.println("-cuddmaxmem ................ Set max memory for CUDD package, e.g. 125k, 50m, 4g [default: 1g]"); - mainLog.println("-cuddepsilon ............... Set epsilon value for CUDD package [default: 1e-15]"); - mainLog.println("-ddsanity ...................... Enable internal sanity checks (causes slow-down)"); - mainLog.println("-ddextrastatevars .......... Set the number of preallocated state vars [default: 20]"); - mainLog.println("-ddextraactionvars ......... Set the number of preallocated action vars [default: 20]"); - mainLog.println(); - mainLog.println("PARAMETRIC MODEL CHECKING OPTIONS:"); - mainLog.println("-param .................. Do parametric model checking with parameters (and ranges) "); - mainLog.println("-paramprecision ............ Set max undecided region for parameter synthesis [default: 5/100]"); - mainLog.println("-paramsplit ............. Set method to split parameter regions (longest,all) [default: longest]"); - mainLog.println("-parambisim ............. Set bisimulation minimisation for parameter synthesis (weak,strong,none) [default: weak]"); - mainLog.println("-paramfunction .......... Set function representation for parameter synthesis (jascached,jas) [default: jascached]"); - mainLog.println("-paramelimorder ......... Set elimination order for parameter synthesis (arb,fw,fwrev,bw,bwrev,rand) [default: bw]"); - mainLog.println("-paramrandompoints ......... Set number of random points to evaluate per region [default: 5]"); - mainLog.println("-paramsubsumeregions ....... Subsume adjacent regions during analysis [default: true]"); - mainLog.println("-paramdagmaxerror .......... Maximal error probability allowed for DAG function representation [default: 1E-100]"); - mainLog.println(); - mainLog.println("FAST ADAPTIVE UNIFORMISATION (FAU) OPTIONS:"); - mainLog.println("-fauepsilon ................ Set probability threshold of birth process in FAU [default: 1e-6]"); - mainLog.println("-faudelta .................. Set probability threshold for irrelevant states in FAU [default: 1e-12]"); - mainLog.println("-fauarraythreshold ......... Set threshold when to switch to sparse matrix in FAU [default: 100]"); - mainLog.println("-fauintervals .............. Set number of intervals to divide time intervals into for FAU [default: 1]"); - mainLog.println("-fauinitival ............... Set length of additional initial time interval for FAU [default: 1.0]"); - } - - /** - * Print a -help xxx message, i.e. display help on a specific switch {@code sw}. - * Return true iff help was available for this switch. - */ - public static boolean printHelpSwitch(PrismLog mainLog, String sw) - { - // -aroptions - if (sw.equals("aroptions")) { - mainLog.println("Switch: -aroptions \n"); - mainLog.println(" is a comma-separated list of options regarding abstraction-refinement:"); - QuantAbstractRefine.printOptions(mainLog); - return true; - } - else if (sw.equals("ii") || sw.equals("intervaliter")) { - mainLog.println("Switch: -intervaliter (or -ii) optionally takes a comma-separated list of options:\n"); - mainLog.println(" -intervaliter:option1,option2,...\n"); - mainLog.println("where the options are one of the following:\n"); - mainLog.println(OptionsIntervalIteration.getOptionsDescription()); - return true; - } - - return false; - } - /** * Set the value for an option, with the option key given as a String, * and the value as an Object of appropriate type or a String to be parsed. diff --git a/prism/src/prism/SwitchHandler.java b/prism/src/prism/SwitchHandler.java new file mode 100644 index 000000000..93b0c698b --- /dev/null +++ b/prism/src/prism/SwitchHandler.java @@ -0,0 +1,324 @@ +//============================================================================== +// +// Copyright (c) 2026- +// Authors: +// * Dave Parker (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package prism; + +import java.util.LinkedHashMap; +import java.util.function.Consumer; + +/** + * Handler for a single CLI switch. + * Can be implemented as a lambda or via one of the typed concrete classes + * ({@link FlagSwitch}, {@link StringSwitch}, {@link IntSwitch}, + * {@link DoubleSwitch}, {@link EnumSwitch}) that encapsulate common + * argument-consumption patterns. + */ +@FunctionalInterface +interface SwitchHandler +{ + void handle(String sw, ArgConsumer args) throws PrismException; +} + +// ── Concrete implementations ───────────────────────────────────────────────── + +/** Switch with no argument: just runs an action when the switch is seen. */ +class FlagSwitch implements SwitchHandler +{ + @FunctionalInterface + interface Action { void run() throws PrismException; } + + private final Action action; + + FlagSwitch(Action action) { this.action = action; } + + @Override + public void handle(String sw, ArgConsumer a) throws PrismException { action.run(); } +} + +/** Switch that consumes the next argument as a raw string and passes it to an action. */ +class StringSwitch implements SwitchHandler +{ + @FunctionalInterface + interface Action { void accept(String s) throws PrismException; } + + private final Action action; + + StringSwitch(Action action) { this.action = action; } + + @Override + public void handle(String sw, ArgConsumer a) throws PrismException { action.accept(a.next(sw)); } +} + +/** Switch that consumes the next argument, parses it as an {@code int}, and passes it to an action. */ +class IntSwitch implements SwitchHandler +{ + @FunctionalInterface + interface Action { void accept(int n) throws PrismException; } + + private final Action action; + + IntSwitch(Action action) { this.action = action; } + + @Override + public void handle(String sw, ArgConsumer a) throws PrismException { action.accept(a.nextInt(sw)); } +} + +/** Switch that consumes the next argument, parses it as a {@code double}, and passes it to an action. */ +class DoubleSwitch implements SwitchHandler +{ + @FunctionalInterface + interface Action { void accept(double d) throws PrismException; } + + private final Action action; + + DoubleSwitch(Action action) { this.action = action; } + + @Override + public void handle(String sw, ArgConsumer a) throws PrismException { action.accept(a.nextDouble(sw)); } +} + +/** + * Switch that consumes the next argument, splits it into {@code :}, + * then calls an {@link Action} with the files portion and a {@link ParseCallback} that + * triggers the stored {@link OptionParser} at whatever point in the action is appropriate. + * The split respects Windows path separators ({@code :\}) by skipping them. + * + *

Call {@link #printOptions} to print sub-option help from the stored parser. + * Call {@link #handleFilesOnly} to process a files-only argument (no options suffix). + */ +class StringPlusOptionsSwitch implements SwitchHandler +{ + @FunctionalInterface + interface Action { void accept(String files, ParseCallback parse) throws PrismException; } + + /** + * Token passed to an {@link Action} so it can trigger options parsing at the right moment. + * The options string is the text after the first {@code :} in the switch argument (empty if none). + */ + static final class ParseCallback + { + private final OptionParser parser; + private final String sw; + private final String options; + + ParseCallback(OptionParser parser, String sw, String options) + { + this.parser = parser; this.sw = sw; this.options = options; + } + + /** The options string as split from the switch argument (may be empty). */ + String options() { return options; } + + /** Parse the options with the stored parser under the switch name. */ + void run() throws PrismException { parser.parse(options, sw); } + + /** Parse an alternative options string (e.g. for legacy separator handling). */ + void run(String overrideOptions) throws PrismException { parser.parse(overrideOptions, sw); } + } + + private final OptionParser parser; + private final Action action; + + StringPlusOptionsSwitch(OptionParser parser, Action action) + { + this.parser = parser; this.action = action; + } + + @Override + public void handle(String sw, ArgConsumer a) throws PrismException + { + String[] parts = splitFilesAndOptions(a.next(sw)); + action.accept(parts[0], new ParseCallback(parser, sw, parts[1])); + } + + /** Process a files-only argument (empty options). Equivalent to handle with no {@code :options} suffix. */ + void handleFilesOnly(String sw, String files) throws PrismException + { + action.accept(files, new ParseCallback(parser, sw, "")); + } + + /** Print the sub-options registered in the stored parser (for use in help blocks). */ + void printOptions(PrismLog log) { parser.printOptions(log); } + + /** + * Split a {@code :} argument on the first {@code :} that is not a + * Windows path separator ({@code :\}). Returns {@code {files, options}}; options is + * empty if no {@code :} is found. + */ + static String[] splitFilesAndOptions(String arg) + { + int i = arg.indexOf(':'); + while (i != -1 && arg.length() > i + 1 && arg.charAt(i + 1) == '\\') + i = arg.indexOf(':', i + 1); + if (i != -1) + return new String[]{arg.substring(0, i), arg.substring(i + 1)}; + else + return new String[]{arg, ""}; + } +} + +/** + * Switch with no leading file/string argument: only an optional {@code :} suffix on the + * switch token itself (PrismSettings-style, where {@code splitSwitch} performs the colon split + * before dispatch and the result is exposed via {@link ArgConsumer#optionsString()}). Unlike + * {@link StringPlusOptionsSwitch}, there is no separate leading "files" portion to split off -- + * the switch token's own colon suffix is itself the options string. + * + *

Reuses {@link StringPlusOptionsSwitch.ParseCallback} so an {@link Action} can call + * {@code parse.run()} to dispatch immediately via the stored {@link OptionParser}, or + * {@code parse.options()} to read the raw string (e.g. for deferred/two-phase parsing). + */ +class OptionsOnlySwitch implements SwitchHandler +{ + @FunctionalInterface + interface Action { void accept(StringPlusOptionsSwitch.ParseCallback parse) throws PrismException; } + + private final OptionParser parser; + private final Action action; + + OptionsOnlySwitch(OptionParser parser, Action action) + { + this.parser = parser; this.action = action; + } + + @Override + public void handle(String sw, ArgConsumer a) throws PrismException + { + String opts = a.optionsString(); + action.accept(new StringPlusOptionsSwitch.ParseCallback(parser, sw, opts == null ? "" : opts)); + } + + /** Print the sub-options registered in the stored parser (for use in help blocks). */ + void printOptions(PrismLog log) { parser.printOptions(log); } +} + +/** + * Bundles a {@link SwitchHandler} with its help metadata for the unified CLI switch map. + * Visible entries have a non-null {@code argHint}; hidden entries have {@code argHint == null}; + * blank-line sentinels have {@code primaryName == null}. {@code group} is the section header + * printed above the first entry in a group. {@code longDesc} is invoked by {@code -help }. + */ +class SwitchEntry +{ + final SwitchHandler handler; + final String group; + final String primaryName; // null = blank-line sentinel + final String[] shownAliases; // aliases displayed in -help output (subset of all registered names) + final String argHint; // null = hidden; "" = flag switch; e.g. "", ""; "[:options]" for a colon suffix on the switch token itself + final String shortText; // description text; null for hidden/blank-line sentinels + final Consumer longDesc; + + SwitchEntry(SwitchHandler handler, String group, String primaryName, + String[] shownAliases, String argHint, String shortText, + Consumer longDesc) + { + this.handler = handler; + this.group = group; + this.primaryName = primaryName; + this.shownAliases = shownAliases; + this.argHint = argHint; + this.shortText = shortText; + this.longDesc = longDesc; + } + + /** + * The arg hint formatted for display directly after the switch name: glued with no space + * for a colon-suffix hint like {@code "[:options]"} (it attaches to the switch token itself, + * not a separate argument), space-separated otherwise (e.g. {@code ""}). Empty/null hints + * (flag switches / hidden entries) yield {@code ""}. + */ + String formattedArgHint() + { + if (argHint == null || argHint.isEmpty()) return ""; + return argHint.startsWith("[:") ? argHint : " " + argHint; + } + + /** Print detailed help: auto-generates the "Switch: -name [argHint] [aliases]" header, then the body. */ + void printLongDesc(PrismLog log) + { + StringBuilder header = new StringBuilder("Switch: -").append(primaryName); + header.append(formattedArgHint()); + if (shownAliases != null && shownAliases.length > 0) { + header.append(" (or"); + for (String alias : shownAliases) header.append(" -").append(alias); + header.append(")"); + } + log.println(header + "\n"); + if (longDesc != null) { + longDesc.accept(log); + } else { + if (shortText != null && !shortText.isEmpty()) + log.println(shortText); + if (handler instanceof EnumSwitch) { + ((EnumSwitch) handler).printOptions(log); + } else if (handler instanceof StringPlusOptionsSwitch || handler instanceof OptionsOnlySwitch) { + log.println(); + log.println("If provided, is a comma-separated list of options taken from:"); + if (handler instanceof StringPlusOptionsSwitch) + ((StringPlusOptionsSwitch) handler).printOptions(log); + else + ((OptionsOnlySwitch) handler).printOptions(log); + } + } + } +} + +/** + * Switch that consumes the next argument and dispatches to one of a fixed set of named choices. + * Throws a descriptive error listing valid options on unknown input. + * Choices are registered via {@link #when(String, FlagSwitch.Action)} which supports chaining. + * Aliases (multiple keys for the same action) are supported by calling {@code when()} multiple times. + */ +class EnumSwitch implements SwitchHandler +{ + private final LinkedHashMap choices = new LinkedHashMap<>(); + + EnumSwitch when(String key, FlagSwitch.Action action) + { + choices.put(key, action); + return this; + } + + EnumSwitch when(String key1, String key2, FlagSwitch.Action action) + { + choices.put(key1, action); + choices.put(key2, action); + return this; + } + + @Override + public void handle(String sw, ArgConsumer a) throws PrismException + { + String v = a.next(sw); + FlagSwitch.Action action = choices.get(v); + if (action == null) + throw new PrismException("Unrecognised option \"" + v + "\" for -" + sw + + " (options are: " + String.join(", ", choices.keySet()) + ")"); + action.run(); + } + + void printOptions(PrismLog log) { log.println("Valid options: " + String.join(", ", choices.keySet())); } +} diff --git a/prism/src/prism/SwitchRegistry.java b/prism/src/prism/SwitchRegistry.java new file mode 100644 index 000000000..69b4573d0 --- /dev/null +++ b/prism/src/prism/SwitchRegistry.java @@ -0,0 +1,153 @@ +//============================================================================== +// +// Copyright (c) 2026- +// Authors: +// * Dave Parker (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package prism; + +import java.util.Map; +import java.util.function.Consumer; + +/** + * Accumulator for the unified CLI switch map, shared between {@link PrismCL} and + * {@link PrismSettings} during one-time initialisation of the switch registry. + * Tracks the current help section so callers need only call {@link #beginGroup} + * when the section changes. + * + *

The visible {@code addSwitch} overloads separate the argument hint (e.g. {@code ""}, + * {@code ""} for flags) from the description text. The primary name and any shown aliases are + * recorded in the {@link SwitchEntry} so {@code printHelp()} can generate the left column and + * dot-padding automatically. + */ +class SwitchRegistry +{ + private static final String[] NO_ALIASES = new String[0]; + + private final Map map; + private String currentGroup = null; + + SwitchRegistry(Map map) { this.map = map; } + + /** Begin a new help section. Subsequent visible entries are listed under this header. */ + void beginGroup(String group) { currentGroup = group; } + + // ── Hidden (not listed in -help) ───────────────────────────────────────── + + void addSwitch(String name, SwitchHandler h) + { + map.put(name, new SwitchEntry(h, currentGroup, name, NO_ALIASES, null, null, null)); + } + + void addSwitch(String n1, String n2, SwitchHandler h) + { + SwitchEntry e = new SwitchEntry(h, currentGroup, n1, NO_ALIASES, null, null, null); + map.put(n1, e); map.put(n2, e); + } + + void addSwitch(String n1, String n2, String n3, SwitchHandler h) + { + SwitchEntry e = new SwitchEntry(h, currentGroup, n1, NO_ALIASES, null, null, null); + map.put(n1, e); map.put(n2, e); map.put(n3, e); + } + + // ── Visible flag switch (argHint = "", no argument) ────────────────────── + + void addSwitch(String name, SwitchHandler h, String shortText) + { + map.put(name, new SwitchEntry(h, currentGroup, name, NO_ALIASES, "", shortText, null)); + } + + void addSwitch(String n1, String n2, SwitchHandler h, String shortText) + { + SwitchEntry e = new SwitchEntry(h, currentGroup, n1, new String[]{n2}, "", shortText, null); + map.put(n1, e); map.put(n2, e); + } + + void addSwitch(String n1, String n2, String n3, SwitchHandler h, String shortText) + { + SwitchEntry e = new SwitchEntry(h, currentGroup, n1, new String[]{n2, n3}, "", shortText, null); + map.put(n1, e); map.put(n2, e); map.put(n3, e); + } + + // ── Visible switch with argument ────────────────────────────────────────── + + void addSwitch(String name, SwitchHandler h, String argHint, String shortText) + { + map.put(name, new SwitchEntry(h, currentGroup, name, NO_ALIASES, argHint, shortText, null)); + } + + void addSwitch(String n1, String n2, SwitchHandler h, String argHint, String shortText) + { + SwitchEntry e = new SwitchEntry(h, currentGroup, n1, new String[]{n2}, argHint, shortText, null); + map.put(n1, e); map.put(n2, e); + } + + void addSwitch(String n1, String n2, String n3, SwitchHandler h, String argHint, String shortText) + { + SwitchEntry e = new SwitchEntry(h, currentGroup, n1, new String[]{n2, n3}, argHint, shortText, null); + map.put(n1, e); map.put(n2, e); map.put(n3, e); + } + + // ── Visible flag with detailed help ────────────────────────────────────── + + void addSwitch(String name, SwitchHandler h, String shortText, Consumer longDesc) + { + map.put(name, new SwitchEntry(h, currentGroup, name, NO_ALIASES, "", shortText, longDesc)); + } + + void addSwitch(String n1, String n2, SwitchHandler h, String shortText, Consumer longDesc) + { + SwitchEntry e = new SwitchEntry(h, currentGroup, n1, new String[]{n2}, "", shortText, longDesc); + map.put(n1, e); map.put(n2, e); + } + + // ── Visible switch with argument and detailed help ──────────────────────── + + void addSwitch(String name, SwitchHandler h, String argHint, String shortText, Consumer longDesc) + { + map.put(name, new SwitchEntry(h, currentGroup, name, NO_ALIASES, argHint, shortText, longDesc)); + } + + void addSwitch(String n1, String n2, SwitchHandler h, String argHint, String shortText, Consumer longDesc) + { + SwitchEntry e = new SwitchEntry(h, currentGroup, n1, new String[]{n2}, argHint, shortText, longDesc); + map.put(n1, e); map.put(n2, e); + } + + /** Insert a blank line in the {@code -help} output at this position. */ + void addBlankLine() + { + map.put("__blank_" + map.size(), new SwitchEntry(null, null, null, NO_ALIASES, null, null, null)); + } + + /** + * Add a second, doc-only listing of an already-registered flag switch under the current group + * (e.g. a switch relevant to two different sections). Purely for {@code -help} output; + * does not affect dispatch since it is stored under a synthetic key. + */ + void addSwitchAlias(String name, String[] shownAliases, String shortText) + { + map.put("__alias_" + map.size(), new SwitchEntry(null, currentGroup, name, shownAliases, "", shortText, null)); + } +}