Plug-in mechanism + Gurobi + explicit engine MDP LP solution#288
Open
davexparker wants to merge 3 commits into
Open
Plug-in mechanism + Gurobi + explicit engine MDP LP solution#288davexparker wants to merge 3 commits into
davexparker wants to merge 3 commits into
Conversation
…t engine. Uses the built-in lpsolve library. Not particularly efficient, but a useful reference.
Introduces a solver.LPSolver interface so the MDP constraint-building logic (reachability probs and rewards) is written once and is independent of the underlying LP backend. One implementation for now: LpSolveSolver, using the built-in lpsolve library.
Contributor
There was a problem hiding this comment.
Pull request overview
Adds a pluggable LP-solver backend mechanism (Java SPI) and wires the explicit engine’s MDP LP-based reachability/reward solving to use selectable backends (built-in lpsolve, optional Gurobi plugin), along with build-system support and regression tests.
Changes:
- Introduce
solver.LPSolver/solver.LPSolverFactoryplussolver.LPSolverRegistryfor SPI-based backend discovery. - Implement built-in
lpsolvebackend and optionalgurobiplugin backend; add-lpsolver <id>setting/CLI. - Add explicit-engine LP solvers for MDP reachability probabilities and expected reachability rewards, and extend tests to cover
-lp.
Reviewed changes
Copilot reviewed 25 out of 25 changed files in this pull request and generated 4 comments.
Show a summary per file
| File | Description |
|---|---|
| prism/src/solver/LpSolveSolverFactory.java | Registers built-in lpsolve backend via factory. |
| prism/src/solver/LpSolveSolver.java | Implements LPSolver using lpsolve JNI. |
| prism/src/solver/LPSolverRegistry.java | SPI-based registry for discovering/creating LP solver backends. |
| prism/src/solver/LPSolverFactory.java | Defines SPI factory interface for LP solver backends. |
| prism/src/solver/LPSolver.java | Defines common LP solver API used by explicit engine. |
| prism/src/prism/PrismSettings.java | Adds prism.lpSolver setting and -lpsolver CLI switch/help. |
| prism/src/META-INF/services/solver.LPSolverFactory | Registers built-in solver.LpSolveSolverFactory for SPI discovery. |
| prism/src/explicit/StateModelChecker.java | Plumbs LP solver selection into explicit engine base class. |
| prism/src/explicit/MDPModelChecker.java | Adds LP-based solvers for reachability probs/rewards and method gating. |
| prism/plugins/gurobi/src/solver/GurobiSolverFactory.java | Factory for optional Gurobi backend. |
| prism/plugins/gurobi/src/solver/GurobiSolver.java | Implements LPSolver using Gurobi Java API. |
| prism/plugins/gurobi/src/META-INF/services/solver.LPSolverFactory | Registers Gurobi factory via SPI in plugin jar. |
| prism/plugins/gurobi/README.md | Documents building/using the Gurobi plugin. |
| prism/Makefile | Adds optional plugin compilation to prism_java; copies META-INF; cleans plugin jars. |
| prism-tests/pmc/lec13and14mdp.nm.props.args | Adds -lp explicit-engine test invocation. |
| prism-tests/pmc/lec13and14mdp.nm.props | Adds reward properties to exercise LP reward solving. |
| prism-tests/pmc/lec13and14mdp.nm | Adds rewards section for the above test model. |
| prism-tests/functionality/verify/mdps/rewards/rewpoliter.nm.props.args | Adds -lp run for existing rewards tests. |
| prism-tests/functionality/verify/mdps/rewards/mdp_rmin_lp_inf.nm.props.args | Adds LP run to cover infinite-reward edge case. |
| prism-tests/functionality/verify/mdps/rewards/mdp_rmin_lp_inf.nm.props | Adds expected results for LP reward solving (incl. Infinity). |
| prism-tests/functionality/verify/mdps/rewards/mdp_rmin_lp_inf.nm | New model to validate toInf guard in LP rewards. |
| prism-tests/functionality/verify/mdps/reach/mdp_simple.nm.props.args | Adds -lp run for reachability regression coverage. |
| prism-tests/functionality/verify/mdps/reach/mdp_lp_precomp.nm.props.args | Adds LP run to ensure precomp-only early-exit path is exercised. |
| prism-tests/functionality/verify/mdps/reach/mdp_lp_precomp.nm.props | Expected results for precomp-resolved LP run. |
| prism-tests/functionality/verify/mdps/reach/mdp_lp_precomp.nm | New model where prob0/prob1 precomputation resolves all states. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+42
to
+49
| try { | ||
| return new GurobiSolver(numVars); | ||
| } catch (NoClassDefFoundError e) { | ||
| // If we reach this point, the plugin has been built/registered | ||
| // but the Gurobi jar is not on the classpath. | ||
| throw new PrismException("Gurobi LP solver not available:" | ||
| + " place gurobi.jar and native libraries in lib/."); | ||
| } |
Comment on lines
+449
to
+453
| else \ | ||
| echo "Skipping plugin '$$plugin': compilation failed (optional dependencies may be missing from lib/)"; \ | ||
| fi; \ | ||
| rm -rf $(PLUGIN_TMP); \ | ||
| done |
Comment on lines
+9
to
+11
| 2. Copy `gurobi.jar` and the native librares (e.g., `libgurobi130.dylib` | ||
| and `libGurobiJni130.dylib` (macOS) or `libgurobi130.so` and | ||
| `libGurobiJni130.so` (Linux) in to main PRISM the `lib/` directory. |
davexparker
force-pushed
the
lp+gurobi+plugins
branch
from
June 25, 2026 21:07
bdc26a7 to
833f619
Compare
Folders in plugins/xxx containing Java code in the src subfolder are compiled into lib/prism-xxx.jar. If any dependencies (jars not in lib/) cause this to fail, compilation fails gracefully. A "gurobi" plugin, containing a wrapper around Gurobi for LP solving is now provided. Copy the Gurobi jar and native libraries into the lib folder to enable compilation, e.g.: cp /Library/gurobi1201/macos_universal2/lib/gurobi.jar lib cp /Library/gurobi1201/macos_universal2/lib/*lib lib A new LPSolverFactory interface supplies LPSolver instances, with implementations provided for the lpsolve and Gurobi LPSolvers. A registry LPSolverRegistry allows runtime discovery of solvers by id at runtime, via Java SPI. Solvers self-register via classes listed in META-INF/services entries, either in the main set of classes or any plugin jar file. explicit.StateModelChecker provides createLPSolver() which creates a new LPSolver based on an `lpsolve` id (e.g. "lpsolve", "gurobi". The LP solver to use can be configured via CLI switch -lpsolver <id> or the "LP solver" option in the GUI. To test Gurobi-based LP solving of MDPs: prism ../prism-tests/functionality/verify/mdps/reach/mdp_simple.nm ../prism-tests/functionality/verify/mdps/reach/mdp_simple.nm.props -ex -lp -lpsolver gurobi
davexparker
force-pushed
the
lp+gurobi+plugins
branch
from
June 25, 2026 21:10
833f619 to
cf4f17f
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.
No description provided.