Add missing reward computation functionality, including discounts by davexparker · Pull Request #295 · prismmodelchecker/prism

davexparker · 2026-08-14T07:59:20Z

New: discounted rewards

New property syntax {discount=...}, attachable to the C and F operators of an R
operator (e.g. R=?[C{discount=0.9}], R=?[F{discount=0.9} "target"]); parser, AST,
semantic and type checks included.
Explicit engine: discounted total (C), cumulative (C<=k) and reachability (F)
rewards for DTMCs and MDPs; discounted total reward also for IDTMCs/IMDPs.
Symbolic engines (MTBDD, sparse, hybrid): discounted C, C<=k and F for DTMCs and
MDPs, implemented by scaling the transition matrix, so the native solvers are unchanged.
Discounting makes every value finite, so the Prob0/Prob1 and end-component precomputation is
skipped on these paths — it reasons about the undiscounted structure and would wrongly
report states as infinite.

New: minimum total reward `Rmin=?[C]`

Supported on MDPs in both the explicit and symbolic engines (previously rejected as
unsupported), by reduction to Rmin=?[F Z] where Z is the union of zero-reward end
components.
Total reward R[C], with and without discount, added for IDTMCs and IMDPs.

Fixes

Rmin=?[F target] gave wrong (too low) answers in the symbolic engines when a zero-reward
end component lay on the path to the target. Now collapsed via a quotient model — the
symbolic analogue of the explicit engine's ZeroRewardECQuotient. This replaces the old
"PRISM hasn't checked for zero-reward loops. Your minimum rewards may be too low..."
warning with an actual computation.
Negative rewards are now permitted for instantaneous-reward (I=k) properties, where a
single state's reward is read rather than cumulated. They remain rejected for cumulative
properties.

Engine coverage

MTBDD: MDP R[C<=k].
Hybrid: MDP reachability/total reward, R[C<=k] and R[I=k] — these previously fell
back to sparse or errored out.

Removed

The -zerorewardcheck switch and Prism.setCheckZeroLoops() / getCheckZeroLoops(), now
that the zero-reward-EC handling above is unconditional.
Note for reviewers: this drops a public API method.

Known limitations

Rmin=?[C] leaves the strategy undefined in Z — the states where the minimiser must
commit to staying put. Values are correct; only an exported strategy is incomplete.
Discounting is rejected (not silently ignored) for co-safe LTL reward properties and for
model types where it isn't implemented.

Instantaneous-reward properties (R=?[I=k], Rmin/Rmax=?[I=k]) report a single state's reward rather than a cumulated sum, so unlike C<=k etc. negative rewards are not an issue there and should not be rejected. Restores this for the explicit engine and extends it to the symbolic engines (mtbdd/sparse/hybrid). Doing so exposed a latent bug in the native MTBDD nondeterministic instantaneous-reward routine (PM_NondetInstReward.cc): its min-reduction used an APPLY_MAX(tmp, new_mask) trick to push non-existent choices to +infinity, relying on real values always being non-negative (max(x, 0) == x). With negative rewards this silently clipped Rmin results to 0 instead of computing the correct value. Replaced with a direct ITE substitution that works for any sign. Adds regression tests covering both DTMC and MDP models across all four engines (-ex -m -s -h).

… and MDPs Adds a {discount=...} option on the C and (bare, reachability) F temporal operators inside an R operator, e.g. R{"r1"}=?[C{discount=0.5}<=100] or Rmin=?[F{discount=0.9} target], and applies it to Rmax/Rmin=?[C], Rmax/Rmin=?[C<=k], and Rmax/Rmin=?[F target] on the explicit DTMC and MDP engines, with value iteration, Gauss-Seidel and backwards Gauss-Seidel variants all wired to the existing -gs/-bgs switches. In each case, discounting guarantees finite values regardless of reachability/end-component structure, so the usual precomputation (BSCC/positive-EC detection for total reward, Prob1/zero-reward-EC handling for reachability reward) is skipped entirely when enabled, going straight to a small dedicated discounted value-iteration/Gauss-Seidel loop instead. Support for (discounted-only) Rmin=?[C] is also added.

Reduces the (undiscounted) case to an expected reachability reward computation with target Z, the union of "zero-reward" maximal end components (states from which a strategy exists to remain forever without accumulating any further reward). A minimising strategy always prefers entering such an MEC over continuing to pay reward, so Rmin[C] = Rmin[F Z]. Adds regression tests for trap-avoidance (minimiser prefers a costlier guaranteed-safe action over a cheaper one that risks an inescapable positive-reward loop) and for a state where every action unavoidably leads to positive reward, so Rmin=?[C] is Infinity there too.

Copilot

Pull request overview

Adds discounted reward computations and minimum total rewards across explicit and symbolic engines, while fixing zero-reward end components and negative instantaneous rewards.

Changes:

Adds {discount=...} parsing, validation, AST support, and reward algorithms.
Adds Rmin=?[C], uncertain-model total rewards, and broader native-engine coverage.
Replaces zero-reward warnings with quotient computation and removes the obsolete switch/API.

Reviewed changes

Copilot reviewed 68 out of 68 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
`prism/src/symbolic/model/MDPQuotient.java`	Exposes reward transformations.
`prism/src/symbolic/comp/StochModelChecker.java`	Updates cumulative-reward signature.
`prism/src/symbolic/comp/StateModelChecker.java`	Adds symbolic discount helpers.
`prism/src/symbolic/comp/ProbModelChecker.java`	Implements symbolic discounted rewards.
`prism/src/symbolic/comp/NondetModelChecker.java`	Adds MDP reward algorithms and quotienting.
`prism/src/prism/PrismSettings.java`	Removes zero-reward switch.
`prism/src/prism/PrismCL.java`	Updates switch registration.
`prism/src/prism/Prism.java`	Removes obsolete public API.
`prism/src/parser/visitor/TypeCheck.java`	Type-checks discount factors.
`prism/src/parser/visitor/PropertiesSemanticCheck.java`	Validates discount placement.
`prism/src/parser/visitor/ASTTraverseModify.java`	Traverses mutable discount expressions.
`prism/src/parser/visitor/ASTTraverse.java`	Traverses discount expressions.
`prism/src/parser/PrismParser.jj`	Parses discount options.
`prism/src/parser/ast/ExpressionTemporal.java`	Stores and renders discounts.
`prism/src/mtbdd/PrismMTBDD.java`	Exposes cumulative-reward JNI.
`prism/src/mtbdd/PM_NondetInstReward.cc`	Corrects negative-reward masking.
`prism/src/mtbdd/PM_NondetCumulReward.cc`	Implements MTBDD cumulative rewards.
`prism/src/hybrid/PrismHybrid.java`	Exposes new hybrid routines.
`prism/src/hybrid/PH_NondetReachReward.cc`	Handles infinite reward states.
`prism/src/hybrid/PH_NondetInstReward.cc`	Implements hybrid instantaneous rewards.
`prism/src/hybrid/PH_NondetCumulReward.cc`	Implements hybrid cumulative rewards.
`prism/src/explicit/UMDPModelChecker.java`	Adds uncertain-MDP total rewards.
`prism/src/explicit/UDTMCModelChecker.java`	Adds uncertain-DTMC total rewards.
`prism/src/explicit/ProbModelChecker.java`	Dispatches discounted explicit rewards.
`prism/src/explicit/MDPModelChecker.java`	Adds discounted and minimum rewards.
`prism/src/explicit/MDP.java`	Adds discounted MDP primitives.
`prism/src/explicit/DTMCModelChecker.java`	Adds discounted DTMC algorithms.
`prism/src/explicit/DTMC.java`	Adds discounted DTMC primitives.
`prism/include/jni/mtbdd_PrismMTBDD.h`	Declares cumulative-reward JNI.
`prism/include/jni/hybrid_PrismHybrid.h`	Declares hybrid reward JNI.
`prism/etc/scripts/bash_prism_completion.sh`	Removes obsolete completion option.
`prism-tests/functionality/verify/mdps/rewards/zero-reward-ec-rmin.prism.props.args`	Configures zero-EC regression engines.
`prism-tests/functionality/verify/mdps/rewards/zero-reward-ec-rmin.prism.props`	Defines zero-EC expectations.
`prism-tests/functionality/verify/mdps/rewards/zero-reward-ec-rmin.prism`	Models zero-reward EC scenarios.
`prism-tests/functionality/verify/mdps/rewards/total-reward-min.prism.props.args`	Configures minimum-total tests.
`prism-tests/functionality/verify/mdps/rewards/total-reward-min.prism.props`	Defines minimum-total expectations.
`prism-tests/functionality/verify/mdps/rewards/total-reward-min.prism.discount.props.args`	Configures discounted tests.
`prism-tests/functionality/verify/mdps/rewards/total-reward-min.prism.discount.props`	Tests discounted total rewards.
`prism-tests/functionality/verify/mdps/rewards/total-reward-min.prism`	Models minimum-total scenarios.
`prism-tests/functionality/verify/mdps/rewards/reach-reward-discount.prism.props.args`	Configures reach-reward tests.
`prism-tests/functionality/verify/mdps/rewards/reach-reward-discount.prism.props`	Tests discounted reach rewards.
`prism-tests/functionality/verify/mdps/rewards/reach-reward-discount.prism`	Models discounted reachability.
`prism-tests/functionality/verify/mdps/rewards/mdp_rewards.nm.props.args`	Expands reward engine coverage.
`prism-tests/functionality/verify/mdps/rewards/discount-symbolic.prism.props.args`	Configures cross-engine discount tests.
`prism-tests/functionality/verify/mdps/rewards/discount-symbolic.prism.props`	Defines cross-engine expectations.
`prism-tests/functionality/verify/mdps/rewards/discount-symbolic.prism`	Models symbolic discount cases.
`prism-tests/functionality/verify/imdps/imdp_total_reward.prism.props`	Tests IMDP total rewards.
`prism-tests/functionality/verify/imdps/imdp_total_reward.prism`	Models IMDP reward scenarios.
`prism-tests/functionality/verify/idtmcs/idtmc_total_reward.prism.props`	Tests infinite IDTMC rewards.
`prism-tests/functionality/verify/idtmcs/idtmc_total_reward.prism`	Models infinite IDTMC rewards.
`prism-tests/functionality/verify/idtmcs/idtmc_total_reward_finite.prism.props`	Tests finite IDTMC rewards.
`prism-tests/functionality/verify/idtmcs/idtmc_total_reward_finite.prism`	Models finite IDTMC rewards.
`prism-tests/functionality/verify/dtmcs/dtmc_total_reward.prism.props.args`	Configures DTMC solver coverage.
`prism-tests/functionality/verify/dtmcs/dtmc_total_reward.prism.props`	Tests DTMC total rewards.
`prism-tests/functionality/verify/dtmcs/dtmc_total_reward.prism`	Models DTMC total rewards.
`prism-tests/functionality/verify/dtmcs/dtmc_reach_reward_discount.prism.props.args`	Configures discounted DTMC reach tests.
`prism-tests/functionality/verify/dtmcs/dtmc_reach_reward_discount.prism.props`	Tests discounted DTMC reach rewards.
`prism-tests/functionality/verify/dtmcs/dtmc_reach_reward_discount.prism`	Models DTMC discounted reachability.
`prism-tests/bugfixes/neg-reward-instantaneous-mdp.prism.props.args`	Configures negative MDP tests.
`prism-tests/bugfixes/neg-reward-instantaneous-mdp.prism.props`	Tests mixed-sign instantaneous rewards.
`prism-tests/bugfixes/neg-reward-instantaneous-mdp.prism`	Models mixed-sign MDP rewards.
`prism-tests/bugfixes/neg-reward-instantaneous-mdp-all-neg.prism.props.args`	Configures all-negative MDP tests.
`prism-tests/bugfixes/neg-reward-instantaneous-mdp-all-neg.prism.props`	Tests all-negative optimization.
`prism-tests/bugfixes/neg-reward-instantaneous-mdp-all-neg.prism`	Models all-negative MDP rewards.
`prism-tests/bugfixes/neg-reward-instantaneous-dtmc.prism.props.args`	Configures negative DTMC tests.
`prism-tests/bugfixes/neg-reward-instantaneous-dtmc.prism.props`	Tests negative DTMC rewards.
`prism-tests/bugfixes/neg-reward-instantaneous-dtmc.prism`	Models negative DTMC rewards.

Suppressed comments (2)

prism/src/hybrid/PH_NondetCumulReward.cc:160

mtbdd_to_double_vector returns an array (and this pointer is released with delete[] on the non-compact cleanup path), so scalar delete here is undefined behavior whenever compact reward storage is selected.
prism/src/symbolic/comp/NondetModelChecker.java:2767
Filtering trr == 0 at edge level can remove a positive-reward exit while retaining a zero-reward internal edge of the same choice. EC analysis then sees a closed zero-reward choice that does not exist in the original MDP, so the quotient can still return an artificially low minimum reachability reward. Compute zero reward at (state, choice) level by excluding every choice with any positive-reward enabled successor.

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

+					+ " reward operator for " + model.getModelType() + "s");
+		}
+		double disc = expr.getDiscount().evaluateDouble(constantValues);
+		if (disc < 0.0 || disc > 1.0) {


+			throw new PrismNotSupportedException("Discounting is not currently supported for " + modelType + "s");
+		}
+		double disc = discExpr.evaluateDouble(constantValues);
+		if (disc < 0.0 || disc > 1.0) {


+		// (state,choice) pairs with zero transition reward
+		JDD.Ref(trr);
+		JDDNode zeroTrr = JDD.Apply(JDD.EQUALS, trr, JDD.Constant(0));
+		// Restrict the transition relation (and its probabilities) to those zero-reward choices
+		JDD.Ref(tr);


Mirrors the just added explicit-engine approach, which reduces the computation to expected reachability reward of zero-reward MECs. Extends the existing Rmin=?[C] trap-avoidance/infinity regression tests (total-reward-min.prism.props) to also run under -m and -s.

…s and IMDPs. - Discounted: values are finite everywhere regardless of end-component structure, so a small custom value-iteration loop suffices. It reuses the existing (undiscounted) per-row primitives mvMultRewUncSingle by passing a temporary copy of the solution vector pre-scaled by the discount factor - valid because the interval-constrained min/max optimization at each state is linear in the successor values, so scaling commutes with it. - Undiscounted max: since interval lower bounds are required to be positive, the transition graph is fixed regardless of how uncertainty is resolved, so end components (IMDP, via the existing ECComputer) / bottom SCCs (IDTMC, via SCCComputer) - and which of them contain a positive reward - can be identified exactly as for (non-uncertain) MDPs/DTMCs. - Undiscounted min: reduced to an expected reachability reward computation with target Z, the maximal set of states from which the minimiser can guarantee remaining forever without seeing another reward. This reuses the existing UDTMC/UMDP computeReachRewards, including its Prob1-based infinite-state precomputation. Discounting is only added here for total reward, so getRewardDiscount takes the set of model types the calling reward operator actually implements it for, rather than checking against one branch-wide set. Widening a single shared set would let R=?[F{discount=...}] through on an uncertain model, where checkRewardReach does not pass the discount factor on to UDTMCModelChecker/UMDPModelChecker - silently answering the undiscounted query instead of reporting that the combination is unsupported. Covered by new properties on the IDTMC/IMDP fixtures. Note these register as UNSUPPORTED rather than PASS, since ResultTesting rethrows a PrismNotSupportedException before it gets to matching "RESULT: Error:..."; they still have teeth, because a silently-dropped discount returns a number and is then reported as "FAIL: Was expecting an error" (verified by reintroducing the fault).

…ngines. Naive value iteration for minimum reachability reward can converge to a spurious "stuck at zero reward forever" fixed point whenever a zero-reward end component sits on the path to the target: looping forever trivially satisfies the Bellman equation V = min(V, escape_cost) at V=0, even though looping never actually reaches the target and should not be counted. The explicit engine has always avoided this by collapsing each zero-reward EC into a single representative state before solving (ZeroRewardECQuotient); the symbolic engines (MTBDD, sparse) previously only detected and *warned* about this condition ("your minimum rewards may be too low..."), without fixing the underlying computation - silently returning 0 instead of the true escape cost. Fixes this by building the same kind of quotient symbolically: restricted to the "maybe" region, find maximal end components of the (state,choice) pairs with zero reward, then collapse each into a single representative state using the existing (previously underused) MDPQuotient machinery - originally built for min/max probability MEC-quotienting - extended here with two small passthroughs for transformed state/transition rewards. Solve on the quotient, then project results back to the original model. This replaces the old warning-only detection entirely. Hybrid continues to fall back to sparse, as before, so it inherits the fix automatically. Also fix two DD reference leaks.

Prism.checkZeroLoops, and the -zerorewardcheck switch that set it, only ever gated the symbolic engine's opt-in handling of zero-reward end components for Rmin=?[F target]: it computed the offending states purely to print a "your minimum rewards may be too low" warning, leaving the answer itself wrong. The preceding commit replaces that with unconditional, correct handling, so the field now has no readers. Removes the field, its setter and getter, and the switch. Also drops the Prism parameter of PrismSettings.registerSwitchHandlers, which the switch was the only user of (its sole caller, in PrismCL, is updated), and the stale -zerorewardcheck entry in the bash completion switch list.

The sparse engine already implemented PS_NondetCumulReward; MTBDD had none, so computeCumulRewards() threw PrismNotSupportedException for -m. Add PM_NondetCumulReward.cc, combining the accumulate-then-iterate pattern from PM_ProbCumulReward.cc (DTMC) with the min/max masking from PM_NondetInstReward.cc, and wire it into the MTBDD case.

PH_NondetReachReward.cc has existed since ~2006 but was never wired in - NondetModelChecker.computeReachRewards hard-threw for the hybrid engine, with the actual call left commented out. Wire it up (mirroring the zero-reward-EC-quotient dispatch already used for MTBDD/sparse), and do the same for computeTotalRewardsMax, which shares the same native entry point via an empty goal set. The dormant code itself had a real, never-triggered bug: it accepted an 'inf' (infinite-value) state set parameter but never used it, so 'inf' state rows - filtered out of the iteration matrix - fell through to a stale "unvisited row" default of 0 instead of being pinned to +infinity. This silently produced too-low results (e.g. exact-tie Rmin[C] over a target with a zero-reward MEC and an escape to a positive-reward trap) whenever the "maybe" region could reach an inf state, which is exactly why the call was presumably left disabled. Fixed by building an inf-state indicator vector and re-pinning those rows to +infinity after every iteration, matching the pattern already used by PS_NondetReachReward.cc (sparse) and PM_NondetReachReward.cc (MTBDD). C<=k and I=k still fall back to sparse for hybrid (no native code exists at all); this is unaffected.

No PH_NondetCumulReward.cc/PH_NondetInstReward.cc ever existed, so computeCumulRewards/computeInstRewards silently redirected the hybrid engine to sparse. Add both, adapted from the (now fixed) reachability reward file's HDD-traversal/matrix-per-choice architecture: - PH_NondetCumulReward.cc: same accumulate-then-iterate structure as PH_NondetReachReward.cc, minus the goal/inf/maybe boundary handling (cumulative reward has no target, just a fixed number of steps). - PH_NondetInstReward.cc: simpler still - no transition rewards, just a plain probability matrix multiply against a vector seeded with the state rewards, one iteration per time step, mirroring the sparse and MTBDD implementations.

… hybrid). Brings {discount=...} on the C and (bare) F operators to -m/-s/-h, which until now parsed it and then refused it, leaving discounting explicit-only. Covers Rmax/Rmin=?[C], Rmax/Rmin=?[C<=k] and Rmax/Rmin=?[F target] for DTMCs and MDPs, matching what the explicit engine supports; CTMCs and everything else are still rejected, now by getRewardDiscount in symbolic.comp. StateModelChecker rather than a blanket engine-level throw. No new native code is needed. Every native solution routine computes a step of the form V'(s) = rew(s) + sum_j P(s,j)*V(j), so multiplying the matrix through by the discount factor first turns that into the discounted step V'(s) = rew(s) + disc * sum_j P(s,j)*V(j). The result is sub-stochastic, which those routines handle fine - it is exactly the textbook reduction that sends the missing 1-disc of each row to an absorbing zero-reward sink. Transition rewards need care: the natives read them by multiplying against that same (now scaled) matrix, i.e. as sum_j rew(s,j)*P(s,j), so they are pre-divided by disc to leave the immediate reward undiscounted. Only future value should be discounted. This is why discountTrans and discountTransRewards come as a pair. The precomputation has to be skipped under discounting: Prob0/Prob1 (and, for Rmin, the zero-reward end component quotient) reason about the *undiscounted* reachability structure, via the unscaled tr01 that matrix scaling never touches. Left in place they report states as having infinite value even though discounting bounds every value by r_max/(1-disc). Discounted runs therefore take inf = {} and maybe = reach \ target, and total reward becomes an ordinary reachability reward computation with an empty target set rather than going through the BSCC/end-component analysis. Discount factor 0 is handled separately, since the 1/disc scaling is undefined there: no future value contributes at all, so the answer is just the immediate expected reward, computed as a single step of cumulative reward on the undiscounted model (with target rewards zeroed out for the reachability case).

The zero-reward end component regression covered the MTBDD and sparse engines but not hybrid, even though computeReachRewards has a separate hybrid branch for solving the quotient model, which could therefore regress unnoticed.

DTMCEmbeddedSimple (the CTMC->DTMC embedding used by the explicit engine) overrides mvMultJacSingle/mvMultRewJacSingle with its own rate-based algebra (dividing by E(s)-diag instead of 1-P(s,s)) and never got the 2017 self-loop guard that DTMC.java's mvMultRewJacSingle has (onlySelfLoops, added alongside MDP's total-reward GS support). A CTMC state whose only transition is a self-loop has E(s)-diag == 0 exactly, so any Jacobi/GS sweep through it hit 0.0/0.0 -> NaN. Ported the same guard: the probability-only mvMultJacSingle now skips the division when the denominator is exactly 0 (d is guaranteed to still be 0 there), and mvMultRewJacSingle special-cases states whose entire probability mass is a self-loop, returning 0 or +-Infinity by the sign of the (already reward-scaled) numerator instead of dividing. Currently unreachable since CTMC reward computations that currently support Gauss-Seidel (target-based computeReachRewards) never put a pure self-loop state into Gauss-Seidel's "maybe" set to begin with (states that can't reach a target have probability 0, so they fall out via prob1-based precomputation before Gauss-Seidel runs at all), and computeTotalRewards - whose BSCC-based precomputation can leave a zero-reward self-loop state in "maybe" - is still hard-locked to Power. This fix allows the latter to be extended to GS.

Use the IterationMethod/GS code already in computeReachRewards. Needs the bug fix in the previous commit to avoid 0/0. Extended deadlock-rewards-issue-29's args to exercise -power/-jacobi/-gs/-bgs for DTMC/CTMC/MDP, locking in both fixes.

mvMultRewGS/mvMultRewGSMinMax/mvMultRewUncGS's relative-error check divided by the newly-computed iterate d, not Math.abs(d). When rewards are negative, this breaks convergence checks. Currently unreachable, but can be triggered in upcoming multi-objective code, where minimisation of rewards is done via negation + maximisation. Other occurrences of the same division pattern are probability-only (d always in [0,1]) and don't need it.

davexparker added 3 commits August 13, 2026 20:33

davexparker requested a balanced review from Copilot August 14, 2026 07:59

Copilot started reviewing on behalf of davexparker August 14, 2026 07:59 View session

Copilot AI reviewed Aug 14, 2026

View reviewed changes

davexparker added 14 commits August 15, 2026 08:30

Reject NaN discount factors in reward properties.

d4e295f

Fix memory accounting in some hybrid MDP reward routines.

9cffaaf

Also test the zero-reward EC quotient on the hybrid engine

62efded

The zero-reward end component regression covered the MTBDD and sparse engines but not hybrid, even though computeReachRewards has a separate hybrid branch for solving the quotient model, which could therefore regress unnoticed.

davexparker force-pushed the rewards branch from d017c7d to 0310226 Compare August 18, 2026 10:03

Navigation Menu

Uh oh!

Add missing reward computation functionality, including discounts - #295

Add missing reward computation functionality, including discounts#295
davexparker wants to merge 17 commits into
prismmodelchecker:masterfrom
davexparker:rewards

davexparker commented Aug 14, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

davexparker commented Aug 14, 2026

New: discounted rewards

New: minimum total reward Rmin=?[C]

Fixes

Engine coverage

Removed

Known limitations

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

New: minimum total reward `Rmin=?[C]`