Rewards (and labels) attach-able to explicit.Model#291
Merged
Conversation
(in a similar way to what is already done for labels, but also allowing reference by integer position as well as name) These are checked first when model checking reward properties. Read access, on explicit.Model: getNumRewards()/getRewards(i)/ getRewardName(i)/getRewardPosition(i) to enumerate attached reward structures by storage index (dense, 0-indexed, no gaps), plus getRewardsByName(name)/getRewardsByPosition(r) to look one up by its (optional) name or by its (optional) position, i.e. the index of the corresponding reward structure in its original source (e.g. a properties file), which need not match its storage index. Write access, on explicit.ModelSimple (and implemented in ModelExplicit): addRewards(name, position, rews) attaches a reward structure, overwriting any existing one with the same name or position (name/position must otherwise be unique); addRewards(name, rews) is a convenience form with no position. copyRewards(model) / copyRewardsMapped(model, map) copy all reward structures from another model, optionally transforming them.
Previously, exportModel (and the single-reward-structure export methods) only considered rewards from the (stored) RewardGenerator, and labels only from the (stored) ModelInfo, ignoring anything attached directly to the explicit.Model itself. This didn't match model checking, which already checks model-attached rewards/labels first. The same gap existed in doExportBuiltModelLabels (used by -exportlabels/-exportproplabels and the GUI "Export Labels" menu), which could therefore produce a smaller label set than embedding labels in a .pexp/.tra export. Add getRewards/getRewardStructName/getAllRewards to look up reward structures (by position and/or name, preferring the model's own copy over one built from the generator, erroring if a position and name match refer to different reward structures) and enumerate all of them (generator-provided ones, plus any extra named ones only attached to the model). Add getAllLabelNames similarly for labels (simpler, since labels have no positional info and ModelInfo, unlike the reward generator, is always present), and use it both in exportModel and in doExportBuiltModelLabels.
Rewards resolved directly from a model (rather than freshly built via a RewardGenerator) were not being converted from (Markov chain) transition rewards to expected state rewards before reaching the solution methods, which only ever read state rewards. Route all paths through a shared, cached conversion in ConstructRewards.getExpectedRewards, which also avoids redundant re-validation/re-conversion of the same rewards object on repeated property checks.
…ched labels/rewards.
Contributor
There was a problem hiding this comment.
Pull request overview
This PR extends the explicit-state model hierarchy so that reward structures (and similarly labels) can be attached directly to explicit.Model instances, then discovered/used consistently across model checking, copying, and export. It also updates model-checking/export paths to prefer model-attached rewards/labels when available, improving reuse of pre-built/derived models.
Changes:
- Adds a model-level rewards API (
getRewardsByName/getRewardsByPosition/ enumeration accessors) and wires reward copying intoModelExplicit.copyFrom(). - Updates explicit model checking and export to resolve rewards/labels from the model when possible, falling back to the stored
RewardGenerator. - Introduces caching for reward legality-checking / expected-reward conversion to avoid repeated O(|S|+|T|) passes.
Reviewed changes
Copilot reviewed 19 out of 19 changed files in this pull request and generated 4 comments.
Show a summary per file
| File | Description |
|---|---|
| prism/src/prism/PrismFileLog.java | Adds isStdout() to distinguish stdout-backed logs from file-backed logs. |
| prism/src/prism/Prism.java | Ensures label export also includes labels attached directly to the built model. |
| prism/src/parser/ast/ExpressionReward.java | Adds optional “error if absent” reward-structure index resolution overloads. |
| prism/src/explicit/SubNondetModel.java | Implements newly required rewards-access methods (currently unsupported in this view). |
| prism/src/explicit/StateModelChecker.java | Prefers model-attached rewards/labels for export and adds helper resolution utilities. |
| prism/src/explicit/rewards/ConstructRewards.java | Adds cached legality-checking and expected-reward conversion for externally supplied rewards. |
| prism/src/explicit/ProbModelChecker.java | Resolves R-operator rewards directly from the model when present, else builds via generator. |
| prism/src/explicit/modelviews/MDPFromDTMC.java | Delegates new rewards-access methods through the view to the wrapped model. |
| prism/src/explicit/modelviews/MDPEquiv.java | Delegates new rewards-access methods through the view to the wrapped model. |
| prism/src/explicit/modelviews/MDPDroppedChoicesCached.java | Delegates new rewards-access methods through the view to the wrapped model. |
| prism/src/explicit/modelviews/MDPDroppedAllChoices.java | Delegates new rewards-access methods through the view to the wrapped model. |
| prism/src/explicit/modelviews/MDPAdditionalChoices.java | Delegates new rewards-access methods through the view to the wrapped model. |
| prism/src/explicit/modelviews/DTMCAlteredDistributions.java | Delegates new rewards-access methods through the view to the wrapped model. |
| prism/src/explicit/ModelSimple.java | Adds mutation/copy APIs for attaching and copying rewards in simple explicit models. |
| prism/src/explicit/ModelExplicit.java | Stores attached rewards (name/position) and copies them during model cloning/copying. |
| prism/src/explicit/Model.java | Adds rewards accessor API to the core explicit model interface + convenience export methods. |
| prism/src/explicit/MDPSparse.java | Simplifies constructor copying using copyFrom() (now includes rewards). |
| prism/src/explicit/LTLModelChecker.java | Lifts rewards into the product model during LTL product construction. |
| prism/src/explicit/DTMCSparse.java | Simplifies constructor copying using copyFrom() (now includes rewards). |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+567
to
+602
| private static final Map<Rewards<?>, Rewards<?>> expectedRewardsCacheFF = Collections.synchronizedMap(new WeakHashMap<>()); | ||
| private static final Map<Rewards<?>, Rewards<?>> expectedRewardsCacheFT = Collections.synchronizedMap(new WeakHashMap<>()); | ||
| private static final Map<Rewards<?>, Rewards<?>> expectedRewardsCacheTF = Collections.synchronizedMap(new WeakHashMap<>()); | ||
| private static final Map<Rewards<?>, Rewards<?>> expectedRewardsCacheTT = Collections.synchronizedMap(new WeakHashMap<>()); | ||
|
|
||
| /** | ||
| * Get a version of {@code rewards} that is safe to pass to the (explicit engine) | ||
| * solution methods, i.e., with all state/transition rewards checked for legality | ||
| * and, if {@code expectedRewards} is true, with any (Markov chain) transition | ||
| * rewards converted to expected state rewards (since solution methods for | ||
| * Markov chains do not read transition rewards directly). | ||
| * <br> | ||
| * Use this (rather than constructing rewards afresh) for any {@link Rewards} object | ||
| * that was not just built by this class, e.g., one obtained directly from a model | ||
| * (see {@link Model#getRewards}) or from a {@link RewardGenerator} that supplies | ||
| * rewards objects directly (see {@link RewardGenerator.RewardLookup#BY_REWARD_OBJECT}). | ||
| * The result is cached against the identity of {@code rewards}. | ||
| * @param rewards The rewards to check/convert | ||
| * @param model The model that the rewards are for | ||
| * @param eval Evaluator matching the type {@code Value} of the reward value | ||
| * @param expectedRewards Whether to convert (Markov chain) transition rewards to expected state rewards | ||
| * @param allowNegative Whether negative rewards (i.e., weights) are allowed | ||
| */ | ||
| @SuppressWarnings("unchecked") | ||
| public static <Value> Rewards<Value> getExpectedRewards(Rewards<Value> rewards, Model<Value> model, Evaluator<Value> eval, boolean expectedRewards, boolean allowNegative) throws PrismException | ||
| { | ||
| Map<Rewards<?>, Rewards<?>> cache = expectedRewards | ||
| ? (allowNegative ? expectedRewardsCacheTT : expectedRewardsCacheTF) | ||
| : (allowNegative ? expectedRewardsCacheFT : expectedRewardsCacheFF); | ||
| Rewards<Value> cached = (Rewards<Value>) cache.get(rewards); | ||
| if (cached != null) { | ||
| return cached; | ||
| } | ||
| Rewards<Value> result = checkRewardObject(rewards, model, eval, expectedRewards, allowNegative); | ||
| cache.put(rewards, result); | ||
| return result; |
Comment on lines
+972
to
+975
| } else if (rsi instanceof Expression) { | ||
| int i = ((Expression) rsi).evaluateInt(constantValues); | ||
| rewards = model.getRewardsByPosition(i - 1); | ||
| } else { |
Comment on lines
+378
to
+380
| if (nameMatch != -1 && positionMatch != -1 && nameMatch != positionMatch) { | ||
| throw new RuntimeException("Reward structure name \"" + name + "\" and position " + position + " refer to different existing reward structures"); | ||
| } |
Comment on lines
42
to
44
| import common.Interval; | ||
| import explicit.rewards.MDPRewards; | ||
| import parser.State; |
The expected-rewards conversion cache in ConstructRewards was keyed only on the identity of the Rewards object, but the (Markov chain) transition-to-expected-state-reward conversion also depends on the model's transition structure. Model views (e.g. DTMCAlteredDistributions) delegate getRewards*() to an underlying model while presenting different transitions, so the same Rewards object can legitimately be paired with different models, and the old cache could return a conversion computed for the wrong one. Key the cache on both rewards and model identity. Flagged by Copilot review on PR prismmodelchecker#291.
When a user specifies a numeric reward-structure index, getRewardsByPosition(i-1) returns null if the model's attached rewards lack positional metadata, even though the model does have attached rewards. This fell through to the reward generator path and produced an unrelated error. Fall back to the i-th attached reward (list order) in this case, mirroring the existing fallback already used for the implicit position-0 case. Flagged by Copilot review on PR prismmodelchecker#291.
Throwing a raw RuntimeException from addRewards()/findRewardsIndex() made this new public API harder for callers to handle and was inconsistent with other argument-validation errors elsewhere. Use IllegalArgumentException instead. Flagged by Copilot review on PR prismmodelchecker#291.
Flagged by Copilot review on PR prismmodelchecker#291.
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.
Allows attaching, managing, and copying reward structures in explicit-state models. The changes unify the handling of rewards across the model hierarchy, provide new APIs for accessing rewards by name or position, and ensure that reward structures are consistently copied and exported. Additionally, model checking now resolves reward structures directly from models when possible, improving flexibility and reusability. Also updates similar existing functionality for labels.