Skip to content

Commit db2555e

Browse files
committed
Plug-in mechanism + Gurobi wrapper + configurable LP solvers.
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 no 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
1 parent b69c9aa commit db2555e

14 files changed

Lines changed: 476 additions & 11 deletions

prism/Makefile

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -371,6 +371,10 @@ JFLAGS += --release 11 # Enforce Java language level
371371

372372
export CFLAGS CXXFLAGS LDFLAGS JFLAGS LIBPREFIX LIBSUFFIX
373373

374+
# Variables for optional plugin compilation (targets defined later, after default goal)
375+
PLUGIN_TMP := .plugin_build_tmp
376+
PLUGIN_SRC_DIRS := $(wildcard plugins/*/src)
377+
374378
##########################################
375379
# Main part of Makefile: Compiling PRISM #
376380
##########################################
@@ -419,11 +423,41 @@ prism: checks prism_java prism_lib prism_ng bin_scripts
419423
# Compile all Java code, build JNI headers
420424
prism_java: $(JAVA_COMPILED_STAMP)
421425

426+
# Optional plugins: any plugins/xxx/ with Java source in src/ is compiled into
427+
# lib/prism-xxx.jar. If optional SDK jars are absent, compilation is skipped
428+
# with a warning rather than failing the build.
429+
ifneq ($(PLUGIN_SRC_DIRS),)
430+
prism_java: compile-plugins
431+
endif
432+
433+
.PHONY: compile-plugins
434+
compile-plugins: $(JAVA_COMPILED_STAMP)
435+
@for src_dir in $(PLUGIN_SRC_DIRS); do \
436+
plugin=$$(basename $$(dirname $$src_dir)); \
437+
jar_out=$(PRISM_LIB_DIR)/prism-$$plugin.jar; \
438+
java_files=$$(find $$src_dir -name "*.java" 2>/dev/null | tr '\n' ' '); \
439+
[ -z "$$java_files" ] && continue; \
440+
echo "Compiling plugin: $$plugin"; \
441+
rm -rf $(PLUGIN_TMP) && mkdir -p $(PLUGIN_TMP); \
442+
if javac_out=$$($(JAVAC) $(JFLAGS) \
443+
-classpath "$(PRISM_LIB_DIR)/*:$(JAVA_CLASSES_DIR)" \
444+
-d $(PLUGIN_TMP) $$java_files 2>&1); then \
445+
[ -n "$$javac_out" ] && echo "$$javac_out"; \
446+
[ -d $$src_dir/META-INF ] && cp -r $$src_dir/META-INF $(PLUGIN_TMP)/; \
447+
jar cf $$jar_out -C $(PLUGIN_TMP) .; \
448+
echo " -> $$jar_out"; \
449+
else \
450+
echo "Skipping plugin '$$plugin': compilation failed (optional dependencies may be missing from lib/)"; \
451+
fi; \
452+
rm -rf $(PLUGIN_TMP); \
453+
done
454+
422455
$(JAVA_COMPILED_STAMP): $(JAVA_SRC_FILES)
423456
@mkdir -p $(JAVA_CLASSES_DIR) $(PRISM_INCLUDE_DIR)/jni
424457
@find $(JAVA_SRC_DIR) -name "*.java" > $(JAVA_SRC_FILES_LIST)
425458
@echo "Compiling Java files..."
426459
$(JAVAC) $(JFLAGS) -classpath "$(PRISM_LIB_DIR)/*" -d $(JAVA_CLASSES_DIR) -h $(PRISM_INCLUDE_DIR)/jni @$(JAVA_SRC_FILES_LIST)
460+
@if [ -d $(JAVA_SRC_DIR)/META-INF ]; then cp -r $(JAVA_SRC_DIR)/META-INF $(JAVA_CLASSES_DIR)/; fi
427461
@touch $@
428462

429463
# Rebuild PRISM (JavaCC) compiler if needed
@@ -732,6 +766,12 @@ clean: checks
732766
rm -f $(JAVA_SRC_FILES_LIST) $(JAVA_COMPILED_STAMP)
733767
rm -f $(JAVA_TESTS_SRC_FILES_LIST) $(JAVA_TESTS_COMPILED_STAMP)
734768
rm -rf $(PRISM_OBJ_DIR)
769+
@for src_dir in $(PLUGIN_SRC_DIRS); do \
770+
plugin=$$(basename $$(dirname $$src_dir)); \
771+
rm -f $(PRISM_LIB_DIR)/prism-$$plugin.jar; \
772+
done
773+
rm -f $(PRISM_LIB_DIR)/gurobi-plugin.jar
774+
rm -rf $(PLUGIN_TMP)
735775
rm -f $(PRISM_LIB_DIR)/$(LIBPREFIX)prism$(LIBSUFFIX)
736776
rm -f $(OLD_SHARED_LIB_FILES)
737777
rm -f $(PRISM_INCLUDE_DIR)/jni/*.h

prism/plugins/gurobi/README.md

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
# Gurobi LP Solver Plugin
2+
3+
This plugin provides a Gurobi backend for PRISM's LP-based solutions.
4+
It is compiled conditionally — only when `lib/gurobi.jar` is present.
5+
6+
## Installation
7+
8+
1. Obtain a Gurobi licence and download the Gurobi software package.
9+
2. Copy `gurobi.jar` and the native librares (e.g., `libgurobi130.dylib`
10+
and `libGurobiJni130.dylib` (macOS) or `libgurobi130.so` and
11+
`libGurobiJni130.so` (Linux) in to main PRISM the `lib/` directory.
12+
3. Run `make` from the `prism/` directory.
13+
This produces `lib/prism-gurobi.jar` automatically.
14+
15+
The plugin is then active at runtime. To select it, use e.g.:
16+
17+
```
18+
prism model.prism reach.probs -ex -lp -lpsolver gurobi
19+
```
20+
21+
## Pre-built artifact
22+
23+
If you have a pre-built `prism-gurobi.jar`, drop it into `lib/`.
24+
No `make` invocation needed — `lib/*` is on the runtime classpath.
25+
26+
## Removing the plugin
27+
28+
Delete `lib/prism-gurobi.jar`.
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
solver.GurobiSolverFactory
Lines changed: 132 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,132 @@
1+
// ==============================================================================
2+
//
3+
// Copyright (c) 2026-
4+
// Authors:
5+
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
6+
//
7+
// ------------------------------------------------------------------------------
8+
//
9+
// This file is part of PRISM.
10+
//
11+
// PRISM is free software; you can redistribute it and/or modify
12+
// it under the terms of the GNU General Public License as published by
13+
// the Free Software Foundation; either version 2 of the License, or
14+
// (at your option) any later version.
15+
//
16+
// PRISM is distributed in the hope that it will be useful,
17+
// but WITHOUT ANY WARRANTY; without even the implied warranty of
18+
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
19+
// GNU General Public License for more details.
20+
//
21+
// You should have received a copy of the GNU General Public License
22+
// along with PRISM; if not, write to the Free Software Foundation,
23+
// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
24+
//
25+
// ==============================================================================
26+
27+
package solver;
28+
29+
import com.gurobi.gurobi.GRB;
30+
import com.gurobi.gurobi.GRBEnv;
31+
import com.gurobi.gurobi.GRBException;
32+
import com.gurobi.gurobi.GRBLinExpr;
33+
import com.gurobi.gurobi.GRBModel;
34+
import com.gurobi.gurobi.GRBVar;
35+
import prism.PrismException;
36+
37+
/**
38+
* LP solver backend backed by Gurobi.
39+
*/
40+
public class GurobiSolver implements LPSolver
41+
{
42+
private final GRBEnv env;
43+
private final GRBModel model;
44+
private final GRBVar[] xVars;
45+
public static final String ID = "gurobi";
46+
public static final String DISPLAY_NAME = "Gurobi";
47+
48+
@Override public String getId() { return ID; }
49+
@Override public String getDisplayName() { return DISPLAY_NAME; }
50+
51+
private int varCount = 0;
52+
53+
public GurobiSolver(int numVars) throws PrismException
54+
{
55+
xVars = new GRBVar[numVars];
56+
try {
57+
// Empty env suppresses console and file logging
58+
env = new GRBEnv(true);
59+
env.set(GRB.IntParam.OutputFlag, 0);
60+
env.start();
61+
model = new GRBModel(env);
62+
} catch (GRBException e) {
63+
throw new PrismException("Error initialising Gurobi: " + e.getMessage());
64+
}
65+
}
66+
67+
@Override
68+
public void addVar(double lb, double ub, double objCoeff) throws PrismException
69+
{
70+
try {
71+
double gurobiUb = Double.isInfinite(ub) ? GRB.INFINITY : ub;
72+
xVars[varCount] = model.addVar(lb, gurobiUb, objCoeff, GRB.CONTINUOUS, null);
73+
} catch (GRBException e) {
74+
throw new PrismException("Error adding Gurobi variable: " + e.getMessage());
75+
}
76+
varCount++;
77+
}
78+
79+
@Override
80+
public void addConstraint(int count, double[] coeffs, int[] vars, char sense, double rhs) throws PrismException
81+
{
82+
char grbiSense;
83+
switch (sense) {
84+
case '=': grbiSense = GRB.EQUAL; break;
85+
case '<': grbiSense = GRB.LESS_EQUAL; break;
86+
case '>': grbiSense = GRB.GREATER_EQUAL; break;
87+
default: throw new PrismException("Unknown LP constraint sense: " + sense);
88+
}
89+
try {
90+
GRBLinExpr expr = new GRBLinExpr();
91+
for (int j = 0; j < count; j++) {
92+
expr.addTerm(coeffs[j], xVars[vars[j]]);
93+
}
94+
model.addConstr(expr, grbiSense, rhs, null);
95+
} catch (GRBException e) {
96+
throw new PrismException("Error adding Gurobi constraint: " + e.getMessage());
97+
}
98+
}
99+
100+
@Override
101+
public double[] solve(boolean maximize) throws PrismException
102+
{
103+
try {
104+
model.set(GRB.IntAttr.ModelSense, maximize ? GRB.MAXIMIZE : GRB.MINIMIZE);
105+
model.optimize();
106+
int status = model.get(GRB.IntAttr.Status);
107+
if (status == GRB.Status.OPTIMAL) {
108+
double[] soln = new double[varCount];
109+
for (int s = 0; s < varCount; s++) {
110+
soln[s] = xVars[s].get(GRB.DoubleAttr.X);
111+
}
112+
return soln;
113+
} else {
114+
String detail = status == GRB.Status.INFEASIBLE ? " (infeasible)" : status == GRB.Status.UNBOUNDED ? " (unbounded)" : "";
115+
throw new PrismException("Error solving LP" + detail);
116+
}
117+
} catch (GRBException e) {
118+
throw new PrismException("Error solving LP: " + e.getMessage());
119+
}
120+
}
121+
122+
@Override
123+
public void dispose()
124+
{
125+
try {
126+
model.dispose();
127+
env.dispose();
128+
} catch (GRBException e) {
129+
// Suppress — nothing useful can be done during cleanup
130+
}
131+
}
132+
}
Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
// ==============================================================================
2+
//
3+
// Copyright (c) 2026-
4+
// Authors:
5+
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
6+
//
7+
// ------------------------------------------------------------------------------
8+
//
9+
// This file is part of PRISM.
10+
//
11+
// PRISM is free software; you can redistribute it and/or modify
12+
// it under the terms of the GNU General Public License as published by
13+
// the Free Software Foundation; either version 2 of the License, or
14+
// (at your option) any later version.
15+
//
16+
// PRISM is distributed in the hope that it will be useful,
17+
// but WITHOUT ANY WARRANTY; without even the implied warranty of
18+
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
19+
// GNU General Public License for more details.
20+
//
21+
// You should have received a copy of the GNU General Public License
22+
// along with PRISM; if not, write to the Free Software Foundation,
23+
// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
24+
//
25+
// ==============================================================================
26+
27+
package solver;
28+
29+
import prism.PrismException;
30+
31+
/**
32+
* LP solver factory for the Gurobi backend.
33+
*/
34+
public class GurobiSolverFactory implements LPSolverFactory
35+
{
36+
@Override public String getId() { return GurobiSolver.ID; }
37+
@Override public String getDisplayName() { return GurobiSolver.DISPLAY_NAME; }
38+
39+
@Override
40+
public LPSolver create(int numVars) throws PrismException
41+
{
42+
try {
43+
return new GurobiSolver(numVars);
44+
} catch (NoClassDefFoundError e) {
45+
// If we reach this point, the plugin has been built/registered
46+
// but the Gurobi jar is not on the classpath.
47+
throw new PrismException("Gurobi LP solver not available:"
48+
+ " place gurobi.jar and native libraries in lib/.");
49+
}
50+
}
51+
}
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
solver.LpSolveSolverFactory

prism/src/explicit/MDPModelChecker.java

Lines changed: 10 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,6 @@
5151
import io.ModelExportFormat;
5252
import parser.ast.Expression;
5353
import solver.LPSolver;
54-
import solver.LpSolveSolver;
5554
import parser.type.TypeDouble;
5655
import prism.Accuracy;
5756
import prism.Accuracy.AccuracyLevel;
@@ -1211,20 +1210,20 @@ protected ModelCheckerResult computeReachProbsLP(MDP<Double> mdp, BitSet no, Bit
12111210
double[] soln = null;
12121211
long timer;
12131212

1214-
// Start solution
1215-
timer = System.currentTimeMillis();
1216-
mainLog.println("Starting linear programming (" + (min ? "min" : "max") + ")...");
1217-
12181213
// Store num states
12191214
int n = mdp.getNumStates();
12201215

1216+
// Start solution
1217+
timer = System.currentTimeMillis();
1218+
LPSolver lp = createLPSolver(n);
1219+
mainLog.println("Starting linear programming (" + (min ? "min" : "max") + ", " + lp.getDisplayName() + ")...");
1220+
12211221
// Determine set of states actually need to perform computation for
12221222
BitSet unknown = new BitSet();
12231223
unknown.set(0, n);
12241224
unknown.andNot(yes);
12251225
unknown.andNot(no);
12261226

1227-
LPSolver lp = new LpSolveSolver(n);
12281227
double[] coeffs = new double[n + 1];
12291228
int[] vars = new int[n + 1];
12301229
try {
@@ -2758,20 +2757,20 @@ protected ModelCheckerResult computeReachRewardsLP(MDP<Double> mdp, MDPRewards<D
27582757
double[] soln = null;
27592758
long timer;
27602759

2761-
// Start solution
2762-
timer = System.currentTimeMillis();
2763-
mainLog.println("Starting linear programming (" + (min ? "min" : "max") + ")...");
2764-
27652760
// Store num states
27662761
int n = mdp.getNumStates();
27672762

2763+
// Start solution
2764+
timer = System.currentTimeMillis();
2765+
LPSolver lp = createLPSolver(n);
2766+
mainLog.println("Starting linear programming (" + (min ? "min" : "max") + ", " + lp.getDisplayName() + ")...");
2767+
27682768
// Determine set of states actually need to perform computation for
27692769
BitSet unknown = new BitSet();
27702770
unknown.set(0, n);
27712771
unknown.andNot(target);
27722772
unknown.andNot(inf);
27732773

2774-
LPSolver lp = new LpSolveSolver(n);
27752774
double[] coeffs = new double[n + 1];
27762775
int[] vars = new int[n + 1];
27772776
try {

0 commit comments

Comments
 (0)