Skip to content

MDP solution via linear programming for explicit engine.#149

Open
davexparker wants to merge 11 commits intoprismmodelchecker:masterfrom
davexparker:lp
Open

MDP solution via linear programming for explicit engine.#149
davexparker wants to merge 11 commits intoprismmodelchecker:masterfrom
davexparker:lp

Conversation

@davexparker
Copy link
Member

No description provided.

…t engine.

Uses the built-in lpsolve library.

Not particularly efficient, but a useful reference.
… engine.

Gurobi is made the default (over lpsolve) for now.

Test e.g. with:

prism ../prism-tests/functionality/verify/mdps/reach/mdp_simple.nm ../prism-tests/functionality/verify/mdps/reach/mdp_simple.nm.props -ex -lp -test

This requires the Gurobi libraries to be copied into lib, e.g.:

cp /Library/gurobi1201/macos_universal2/lib/gurobi.jar lib
cp /Library/gurobi1201/macos_universal2/lib/*lib lib
@davexparker davexparker force-pushed the lp branch 2 times, most recently from 3982b8a to 3c6eb7d Compare May 6, 2025 16:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants

Comments