-exportstrat can export full induced model, including states/labels/rewards#292
Open
davexparker wants to merge 1 commit into
Open
-exportstrat can export full induced model, including states/labels/rewards#292davexparker wants to merge 1 commit into
davexparker wants to merge 1 commit into
Conversation
…ewards. For example: prism ... -exportstrat strat.pexp prism ... -exportstrat strat.umb The -exportstrat switch also gains many of -exportmodel's options: format, states, rewards, labels, actions, precision, zip, text, headers. To avoid an option clash, "obs" now means "show observations", like for -exportmodel, and the existing "obs" option for -exportstrat is now renamed to "mergeobs" (merge observationally equivalent states). We also make reach=true the default. Implementation details: * StrategyExportOptions gains an inducedModelExportOptions field. * Tidy up constructInducedModel and exportInducedModel in Strategy classes for explicit models to respect inducedModelExportOptions and to use new Model.export method, allow full model export to .pexp/.umb. * Induced model construction in both ConstructInducedModel and ConstructStrategyProduct copies/lifts (by default, but optionally) any labels and rewards attached to the original model. * Rewards are pre-emptively built and attached to built models when it is known that strategies are generated (via StateModelChecker.attachRewards)
Contributor
There was a problem hiding this comment.
Pull request overview
This PR extends -exportstrat so it can export the full induced model (including states/labels/rewards, and additional export options) in the same formats supported by -exportmodel (e.g., .pexp, .umb), and updates induced-model construction to carry annotations (labels/rewards) over by default.
Changes:
- Add induced-model
ModelExportOptionsplumbing to strategy export (format/states/labels/rewards/actions/obs/precision/zip/text/headers) and update-exportstratCLI parsing/help. - Update explicit-strategy induced-model export to use
Model.export(...)with export options rather than legacy.tra-only export. - Copy/lift labels and rewards onto induced models (including strategy products), and eagerly attach rewards when strategy generation/export is requested; add functionality tests for induced-model export outputs.
Reviewed changes
Copilot reviewed 25 out of 25 changed files in this pull request and generated 7 comments.
Show a summary per file
| File | Description |
|---|---|
| prism/src/strat/StrategyExportOptions.java | Adds inducedModelExportOptions to carry ModelExportOptions for induced-model export. |
| prism/src/strat/StrategyExplicit.java | Switches induced-model export to Model.export(...) using induced-model export options. |
| prism/src/strat/Strategy.java | Updates/clarifies the induced-model construction Javadoc. |
| prism/src/strat/MRStrategy.java | Removes legacy induced-model export override (now handled by base implementation). |
| prism/src/strat/MDStrategyArray.java | Removes legacy induced-model export override (now handled by base implementation). |
| prism/src/strat/FMDStrategyStep.java | Removes legacy induced-model export override (now handled by base implementation). |
| prism/src/strat/FMDStrategyProduct.java | Delegates reachable-only induced-model export to the base implementation. |
| prism/src/strat/FMDObsStrategyBeliefs.java | Updates induced-model export path for merged-observation strategies to use Model.export(...). |
| prism/src/prism/PrismCL.java | Extends -exportstrat sub-options to mirror -exportmodel options; renames obs→mergeobs and makes obs mean “show observations”. |
| prism/src/prism/Prism.java | Attaches rewards earlier when strategy generation is enabled; adds reward attachment during strategy export; adds merging helper for model export options. |
| prism/src/explicit/StateModelChecker.java | Exposes reward collection and adds a helper to attach rewards to mutable explicit models. |
| prism/src/explicit/ConstructStrategyProduct.java | Copies/lifts labels and rewards from the original model into strategy product models. |
| prism/src/explicit/ConstructInducedModel.java | Copies/lifts labels and rewards from the original model into induced models. |
| prism-tests/functionality/export/strat/exportstratinduced.nm.props.tra | New expected output for induced-model export in .tra form. |
| prism-tests/functionality/export/strat/exportstratinduced.nm.props.restrict.pexp | New expected combined explicit export output for induced-model export (restrict mode). |
| prism-tests/functionality/export/strat/exportstratinduced.nm.props.reduce.pexp | New expected combined explicit export output for induced-model export (reduce mode). |
| prism-tests/functionality/export/strat/exportstratinduced.nm.props.reach.tra | New expected output exercising reach=true reindexing for induced export. |
| prism-tests/functionality/export/strat/exportstratinduced.nm.props.reach.sta | New expected states output file for reachable induced export. |
| prism-tests/functionality/export/strat/exportstratinduced.nm.props.reach.lab | New expected labels output file for reachable induced export. |
| prism-tests/functionality/export/strat/exportstratinduced.nm.props.multi.tra | New expected output for a multi-initial-state induced export. |
| prism-tests/functionality/export/strat/exportstratinduced.nm.props.multi.sta | New expected states output file for multi-state induced export. |
| prism-tests/functionality/export/strat/exportstratinduced.nm.props.multi.lab | New expected labels output file for multi-state induced export. |
| prism-tests/functionality/export/strat/exportstratinduced.nm.props.args | New test invocation arguments covering the new export variants. |
| prism-tests/functionality/export/strat/exportstratinduced.nm.props | New properties file for the export-strategy induced-model tests. |
| prism-tests/functionality/export/strat/exportstratinduced.nm | New model used by the induced-model export tests. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+3816
to
+3820
| // Merge export options with PRISM settings and do export | ||
| StrategyExportOptions mergedExportOptions = exportOptions.clone(); | ||
| mergedExportOptions.setInducedModelExportOptions(newMergedModelExportOptions(mergedExportOptions.getInducedModelExportOptions())); | ||
| // For induced model export, attach reward structures to the strategy's model | ||
| // directly (if not already done, e.g. at model-build time), so that they get |
Comment on lines
+1966
to
1973
| ModelExportTask inducedModelTask = null; | ||
| ModelExportOptions inducedModelOptions = new ModelExportOptions(); | ||
| // Default strategy export type is based on filename extension | ||
| if (ext.equals("tra")) { | ||
| if (ext.equals("tra") || ext.equals("pexp") || ext.equals("umb")) { | ||
| exportStratOptions.setType(StrategyExportOptions.StrategyExportType.INDUCED_MODEL); | ||
| inducedModelOptions = ModelExportTask.fromFilename(basename, ext).getExportOptions(); | ||
| } else if (ext.equals("dot")) { | ||
| exportStratOptions.setType(StrategyExportOptions.StrategyExportType.DOT_FILE); |
Comment on lines
+1487
to
+1489
| log.println("Use file extension .tra, .pexp, .umb or .dot to export as an induced model."); | ||
| log.println("The default (e.g. for file extension .txt) is a list of stat-action choices."); | ||
| log.println("\nIf provided, <options> is a comma-separated list of options taken from:"); |
Comment on lines
+31
to
37
| import io.ModelExportFormat; | ||
| import io.ModelExportOptions; | ||
| import io.ModelExportTask; | ||
|
|
||
| import java.io.File; | ||
| import java.util.List; | ||
| import java.util.Optional; |
| /** | ||
| * For induced model export, the model export options. | ||
| */ | ||
| private Optional<ModelExportOptions> inducedModelExportOptions = Optional.empty();; |
Comment on lines
+197
to
+199
| /** | ||
| * Set the model export tasks specifying details for induced model export. | ||
| */ |
Comment on lines
+60
to
+68
| /** | ||
| * Whether to copy labels from the original model to the induced model | ||
| */ | ||
| private boolean copyLabels = true; | ||
|
|
||
| /** | ||
| * Whether to copy rewards from the original model to the induced model | ||
| */ | ||
| private boolean copyRewards = true; |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
For example:
prism ... -exportstrat strat.pexp
prism ... -exportstrat strat.umb
The -exportstrat switch also gains many of -exportmodel's options: format, states, rewards, labels, actions, precision, zip, text, headers.
To avoid an option clash, "obs" now means "show observations", like for -exportmodel, and the existing "obs" option for -exportstrat is now renamed to "mergeobs" (merge observationally equivalent states).
We also make reach=true the default.
Implementation details:
StrategyExportOptions gains an inducedModelExportOptions field.
Tidy up constructInducedModel and exportInducedModel in Strategy classes for explicit models to respect inducedModelExportOptions and to use new Model.export method, allow full model export to .pexp/.umb.
Induced model construction in both ConstructInducedModel and ConstructStrategyProduct copies/lifts (by default, but optionally) any labels and rewards attached to the original model.
Rewards are pre-emptively built and attached to built models when it is known that strategies are generated (via StateModelChecker.attachRewards)