Skip to content

Refactor PrismCL switch definitions and -help text generation#289

Merged
davexparker merged 15 commits into
prismmodelchecker:masterfrom
davexparker:cl-switch-refactor
Jun 30, 2026
Merged

Refactor PrismCL switch definitions and -help text generation#289
davexparker merged 15 commits into
prismmodelchecker:masterfrom
davexparker:cl-switch-refactor

Conversation

@davexparker

Copy link
Copy Markdown
Member

No description provided.

Code to process switches in PrismCL cleaned/refactored.

ArgConsumer: handles iteration through argument list.

SwitchHandler: interface for code to deal with a switch,
plus instantiations for switches that are flags or that
take strings, ints, doubles, enums.

OptionParser: parses an option list opt1,key=val,...

Switch definitions in PrismCL become calls rto addSwitch
methods that populate a switchHandlers map. Complex
switches (e.g. -exportmodel) now use OptionsParser.
The same idea is applied in PrismSettings, where switches
that set values in the settings object are defined.
Each switch's short description (for -help) and detailed description
(for -help <switch>) are now declared at the addSwitch call site rather
than maintained separately in printHelp/printHelpSwitch methods. Help
output is generated from the ordered switch registry, so adding a switch
requires only one place to edit.

Key additions in SwitchHandler.java:
- SwitchEntry bundles handler + short text + argHint + longDesc lambda
- SwitchRegistry wraps the ordered map and tracks the current group header
- StringPlusOptionsSwitch stores an OptionParser alongside its handler,
  splits <files>:<options>, and calls the action with (files, ParseCallback)
  so the process method triggers options parsing at the right moment;
  printOptions() on the switch lets the longDesc lambda list sub-options
  without referencing a separate field

Key changes in PrismCL.java:
- initSwitchHandlers() registers all ~110 switches with their descriptions
  using beginGroup()/addSwitch() overloads; short -help is derived from
  the registry, detailed -help <sw> from the longDesc lambdas
- Six OptionParser fields replaced by local StringPlusOptionsSwitch
  variables; process methods receive (String files, ParseCallback parse)
  and call parse.run() instead of naming the parser explicitly
- OptionParser combined overloads (flag/bool/string/choice with description
  + action) and printOptions() let sub-option help live alongside the
  handlers in each switch's OptionParser definition
* Replace some raw (sw, a) -> a.next(sw) lambdas with StringSwitch
* Inline small switch actions, removing some transient fields
* Generate the "Switch: -xx ..." automatically for prism -help -xx

Note: drop the legacy comma separator for -exportresults (now only colon).
Previously -help <sw> only produced detailed output for the ~11 switches
that had an explicit longDesc lambda; all others said "Sorry - no help
available".

Now SwitchEntry.printLongDesc generates useful output unconditionally for
any visible switch (argHint != null):
 - header line "Switch: -name [aliases] [argHint]" (already auto-generated)
 - when longDesc is set: delegates to it as before
 - when longDesc is absent: prints the short description; and for EnumSwitch
   additionally prints "Valid options: ..." listing all accepted keys

EnumSwitch gains a printOptions() method for this purpose.
When an argHint starts with [:, it's a colon-suffix on the switch token itself
(no separate argument), so it's glued directly to the switch name with no space,
rather than space-separated like normal hints (<x>, <files>[:<options>]).
For now, just precision=x is supported.

The code to generate switches for exporting individual model entities
is refactored to avoid repetition.

To support this, we also add an int option for OptionalParser, with an
optional validity predicate, and a default long text description.
(got lost in refactor because was duplicated across sections)

Copilot AI left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

This PR refactors PrismCL/PrismSettings command-line switch handling into a unified registry that centralizes switch dispatch and auto-generates -help output from stored metadata, reducing duplicated parsing/help formatting logic across classes.

Changes:

  • Introduces a unified switch registry (SwitchRegistry + SwitchEntry) shared by PrismCL and PrismSettings for one-time handler registration and ordered help output.
  • Replaces large manual switch/option parsing blocks with typed SwitchHandler implementations, ArgConsumer for argument consumption, and OptionParser for comma-separated sub-options.
  • Refactors interval-iteration option handling to use OptionParser and supports detailed per-switch help via -help <switch>.

Reviewed changes

Copilot reviewed 7 out of 7 changed files in this pull request and generated 3 comments.

Show a summary per file
File Description
prism/src/prism/SwitchRegistry.java Adds a registry API for accumulating switch handlers + help metadata with grouping and blank-line support.
prism/src/prism/SwitchHandler.java Adds the SwitchHandler interface plus reusable handler implementations and SwitchEntry help metadata/printing.
prism/src/prism/PrismSettings.java Moves PrismSettings CLI switch wiring into registerSwitchHandlers() and removes legacy printHelp* methods.
prism/src/prism/PrismCL.java Replaces manual argument parsing and help printing with the unified switch map, registry-driven help, and option parsers.
prism/src/prism/OptionsIntervalIteration.java Rebuilds interval-iteration options parsing/help on top of OptionParser.
prism/src/prism/OptionParser.java Introduces a reusable parser/builder for comma-separated sub-options with help metadata output.
prism/src/prism/ArgConsumer.java Introduces a typed argument consumer to support cleaner, consistent switch handler implementations.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Comment thread prism/src/prism/PrismCL.java Outdated
Comment on lines +1169 to +1189
registry.addSwitch("test", new FlagSwitch(() -> test = true),
"", "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
"<x>", "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
"<x>", "Set the Java stack size [default: 4m]");
registry.addSwitch("javaparams", (sw, a) -> a.next(sw), // consumed before JVM launch
"<x>", "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);
}, "<n>", "Exit after a time-out of <n> 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("test:umb", new FlagSwitch(() -> prism.setTestUMB(true)));
Comment on lines +173 to +175
int i = arg.indexOf(':');
while (arg.length() > i + 1 && arg.charAt(i + 1) == '\\')
i = arg.indexOf(':', i + 1);
Comment thread prism/src/prism/OptionParser.java Outdated
Comment on lines +294 to +312
for (String opt : optionsString.split(",")) {
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);
String val = opt.substring(eq + 1);
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");
}
}
@davexparker davexparker merged commit a2b1a81 into prismmodelchecker:master Jun 30, 2026
6 checks passed
@davexparker davexparker deleted the cl-switch-refactor branch June 30, 2026 10:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants