MDP solution via linear programming for explicit engine.#149
MDP solution via linear programming for explicit engine.#149davexparker wants to merge 1 commit intoprismmodelchecker:masterfrom
Conversation
davexparker
force-pushed
the
master
branch
2 times, most recently
from
ca12ca0 to
6bf73df
Compare
davexparker
force-pushed
the
lp
branch
3 times, most recently
from
3c6eb7d to
b3944be
Compare
…t engine. Uses the built-in lpsolve library. Not particularly efficient, but a useful reference.
There was a problem hiding this comment.
Pull request overview
Adds explicit-engine support for solving MDP reachability probabilities and expected reachability rewards via linear programming (lp_solve), wiring it into the existing MDPSolnMethod.LINEAR_PROGRAMMING selection and extending tests to exercise -lp.
Changes:
- Implement LP-based solvers for reachability probabilities and reachability rewards in
explicit.MDPModelChecker. - Allow
MDPSolnMethod.LINEAR_PROGRAMMINGin the explicit engine for reachability rewards (previously switched away). - Extend existing test matrices/fixtures to run explicit MDP checks with
-lp, and add reward queries to a lecture example.
Reviewed changes
Copilot reviewed 5 out of 5 changed files in this pull request and generated 3 comments.
Show a summary per file
| File | Description |
|---|---|
| prism/src/explicit/MDPModelChecker.java | Implements LP formulations for Pmin/Pmax and Rmin/Rmax (with some restrictions) and plugs them into the numeric solve dispatch. |
| prism-tests/pmc/lec13and14mdp.nm.props | Adds reachability reward queries with expected results for the lecture MDP. |
| prism-tests/pmc/lec13and14mdp.nm | Adds a rewards structure to support the new reward queries. |
| prism-tests/functionality/verify/mdps/rewards/rewpoliter.nm.props.args | Adds an invocation that runs the rewards suite with -lp. |
| prism-tests/functionality/verify/mdps/reach/mdp_simple.nm.props.args | Adds an invocation that runs the reachability suite with explicit engine + -lp. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| } | ||
| res = computeReachProbsModPolIter(mdp, no, yes, min, strat); | ||
| break; | ||
| case LINEAR_PROGRAMMING: |
There was a problem hiding this comment.
The linear-programming branch ignores the init/known parameters passed into computeReachProbsNumeric(). If callers provide known exact values for some states, they are currently silently not enforced/used when method==LINEAR_PROGRAMMING. Consider either (a) adding equality constraints for known states (and seeding from init if useful), or (b) rejecting init/known for LP with a clear PrismNotSupportedException to avoid surprising behavior.
| case LINEAR_PROGRAMMING: | |
| case LINEAR_PROGRAMMING: | |
| if (init != null || known != null) { | |
| throw new PrismNotSupportedException("Linear programming does not currently support init/known parameters for reachability probability computation"); | |
| } |
| } | ||
| res = computeReachRewardsPolIter(mdp, mdpRewards, target, inf, min, strat); | ||
| break; | ||
| case LINEAR_PROGRAMMING: |
There was a problem hiding this comment.
The linear-programming branch ignores the init/known parameters passed into computeReachRewardsNumeric(). If callers provide known exact values for some states, they are currently silently not enforced/used when method==LINEAR_PROGRAMMING. Consider either (a) adding equality constraints for known states (and seeding from init if useful), or (b) rejecting init/known for LP with a clear PrismNotSupportedException to avoid surprising behavior.
| case LINEAR_PROGRAMMING: | |
| case LINEAR_PROGRAMMING: | |
| if (init != null || (known != null && !known.isEmpty())) { | |
| throw new PrismNotSupportedException("Linear programming does not support init/known parameters for reachability rewards"); | |
| } |
| } | ||
| toInf = toInf || inf.get(t); | ||
| } | ||
| // We ignore choices that may lead to an inf states |
There was a problem hiding this comment.
Grammar: “may lead to an inf states” should be singular (“an inf state”).
| // We ignore choices that may lead to an inf states | |
| // We ignore choices that may lead to an inf state |
No description provided.