-exportstrat can export full induced model, including states/labels/rewards (to .pexp, .umb) - #294
Merged
Conversation
Contributor
There was a problem hiding this comment.
Pull request overview
Extends -exportstrat so that strategy export can emit the full induced model (including states/labels/rewards) using the same explicit/combined formats as -exportmodel (e.g. .pexp, .umb), and aligns the CLI option set accordingly (including renaming the old obs behavior to mergeobs).
Changes:
- Add induced-model
ModelExportOptionsplumbing to strategy export (format/states/labels/rewards/actions/precision/zip/text/headers) and update the-exportstratCLI parsing/defaults. - Refactor explicit strategy induced-model construction/export to delegate to
Model.export(...), and treat DOT export as an induced-model export when configured as DOT format. - Copy/lift labels and rewards during induced/product model construction, and attach rewards eagerly when strategy generation/export is requested.
Reviewed changes
Copilot reviewed 22 out of 22 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
| prism/src/strat/StrategyExportOptions.java | Replaces legacy precision handling with an optional ModelExportOptions for induced-model export; changes reachability default behavior. |
| prism/src/strat/StrategyExplicit.java | Centralizes induced-model export via Model.export(...) and conditionally routes DOT export through induced-model export options. |
| prism/src/strat/Strategy.java | Updates API documentation around induced-model construction. |
| prism/src/strat/MRStrategy.java | Switches induced-model construction to use ConstructInducedModel(options) and drops bespoke export code. |
| prism/src/strat/MDStrategyArray.java | Switches induced-model construction to use ConstructInducedModel(options) and drops bespoke export code. |
| prism/src/strat/FMDStrategyStep.java | Switches product construction to use ConstructStrategyProduct(options) and drops bespoke export code. |
| prism/src/strat/FMDStrategyProduct.java | Switches product construction to use ConstructStrategyProduct(options) and reuses superclass induced-model export when rebuilding for reachability. |
| prism/src/strat/FMDObsStrategyBeliefs.java | Switches product construction to use ConstructStrategyProduct(options); updates induced-model export path to use ModelExportOptions. |
| prism/src/prism/PrismCL.java | Extends -exportstrat options to mirror -exportmodel options; renames obs→mergeobs and redefines obs as “show observations”. |
| prism/src/prism/Prism.java | Merges induced-model export options with settings at export time; attaches rewards when strategies are generated/exported. |
| prism/src/explicit/StateModelChecker.java | Makes getAllRewards(...) public and adds attachRewards(...) to materialize rewards onto mutable explicit models. |
| prism/src/explicit/ConstructStrategyProduct.java | Adds optional copying of labels/rewards into strategy product models, controlled by induced-model export options. |
| prism/src/explicit/ConstructInducedModel.java | Adds optional copying of labels/rewards into induced models, controlled by induced-model export options. |
| prism-tests/functionality/export/strat/exportstratinduced.nm | New test model for induced-model strategy export behavior (reach/mode/format). |
| prism-tests/functionality/export/strat/exportstratinduced.nm.props | New properties file driving strategy generation for the test. |
| prism-tests/functionality/export/strat/exportstratinduced.nm.props.args | New test runner args covering .tra/.pexp outputs and options. |
| prism-tests/functionality/export/strat/exportstratinduced.nm.props.tra | Expected induced-model transition export for default .tra case. |
| prism-tests/functionality/export/strat/exportstratinduced.nm.props.reach.tra | Expected induced-model transition export with reach=true. |
| prism-tests/functionality/export/strat/exportstratinduced.nm.props.reach.sta | Expected state export corresponding to the reachable induced model. |
| prism-tests/functionality/export/strat/exportstratinduced.nm.props.reach.lab | Expected label export corresponding to the reachable induced model. |
| prism-tests/functionality/export/strat/exportstratinduced.nm.props.restrict.pexp | Expected combined explicit induced-model export in restrict mode. |
| prism-tests/functionality/export/strat/exportstratinduced.nm.props.reduce.pexp | Expected combined explicit induced-model export in reduce mode. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+3825
to
+3827
| if (exportOptions.getType() == StrategyExportType.INDUCED_MODEL && strat instanceof strat.StrategyExplicit) { | ||
| attachRewardsToModel(((strat.StrategyExplicit<?>) strat).getModel()); | ||
| } |
Comment on lines
+196
to
+200
| // Create empty reward structures for the induced model, if needed | ||
| List<Rewards<Value>> origRewardsList = null; | ||
| List<RewardsSimple<Value>> inducedRewardsList = null; | ||
| if (copyRewards) { | ||
| int numRewardStructs = model.getNumRewards(); |
…ewards. This is done using (combined) explicit format or UMB. 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). By default, the induced model is restricted to reachable states when exporting the full model. This can be disabled with option reach=false. For .tra export, reach=false remains the default (because there is not state information and so new (reahcable) state indices are hard to interpret. 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) * Strategy export in Dot format is by default just treated as an induced model, making it easier to pass the same formatting options.
…ported Guard the (potentially expensive) reward attachment in exportStrategy() with getShowRewards(), and check mergedExportOptions rather than exportOptions since that's what's actually used for the export.
Add a reward structure (with both state and transition rewards) to the exportstratinduced.nm test model, so the existing reduce/restrict .pexp tests exercise reward copying into the induced model, including folding of transition rewards into state rewards for the reduce (DTMC) case. Also add a mode=reduce,rewards=false test case to check that disabling reward export is respected.
davexparker
force-pushed
the
exportstrat
branch
from
August 12, 2026 08:01
4ed1609 to
1eee022
Compare
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.
This is done using (combined) explicit format or UMB. 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).
By default, the induced model is restricted to reachable states when exporting the full model. This can be disabled with option reach=false. For .tra export, reach=false remains the default (because there is not state information and so new (reahcable) state indices are hard to interpret.
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)
Strategy export in Dot format is by default just treated as an induced model, making it easier to pass the same formatting options.