Exact solutions for both MDPs and DTMCs using linear programming.

External GLPK library added for solving lp problems. The library GMP is used for providing arbitrary precision arithmetic.

prism/.classpath

@@ -12,5 +12,6 @@
 	<classpathentry kind="lib" path="lib/jas.jar"/>
 	<classpathentry kind="lib" path="lib/log4j.jar"/>
 	<classpathentry kind="lib" path="lib/nailgun-server.jar"/>
+	<classpathentry kind="lib" path="lib/glpk-java.jar"/>
 	<classpathentry kind="output" path="classes"/>
 </classpath>

prism/Makefile

@@ -298,11 +298,46 @@ MAKE_DIRS = dd jdd odd dv prism mtbdd sparse hybrid parser settings userinterfac
 
 EXT_PACKAGES = lpsolve55 lp_solve_5.5_java
 
+EXACT_LP_PACKAGES = glpk glpk_java
+
+EXACT_LP_REQUIREMENTS_INSTALLED = 1
+
+# Find glpk_java requirements
+DETECT_SWIG = $(shell which swig 2> /dev/null)
+DETECT_MVN = $(shell which mvn 2> /dev/null)
+DETECT_LIBTOOL = $(shell which libtool 2> /dev/null)
+DETECT_ACLOCAL = $(shell which aclocal 2> /dev/null)
+
+ifeq ($(DETECT_SWIG),)
+	EXACT_LP_REQUIREMENTS_INSTALLED = 0
+endif
+ifeq ($(DETECT_MVN),)
+	EXACT_LP_REQUIREMENTS_INSTALLED = 0
+endif
+ifeq ($(DETECT_LIBTOOL),)
+	EXACT_LP_REQUIREMENTS_INSTALLED = 0
+endif
+ifeq ($(DETECT_ACLOCAL),)
+	EXACT_LP_REQUIREMENTS_INSTALLED = 0
+endif
+
 .PHONY: clean javadoc tests
 
 default: all
 
-all: cuddpackage extpackages prism
+all: cuddpackage extpackages exact_lp_requirements exact_lp prism
+
+exact_lp_requirements: checks
+	cp ext/glpk_java/jar/glpk-java.jar lib
+	@if [ "$(DETECT_SWIG)" != "" ]; then echo "Found SWIG in $(DETECT_SWIG)"; \
+	else echo "Warning: SWIG not found. Required for GLPK java bindings."; fi
+	@if [ "$(DETECT_MVN)" != "" ]; then echo "Found MAVEN in $(DETECT_MVN)"; \
+	else echo "Warning: MAVEN not found. Required for GLPK java bindings."; fi
+	@if [ "$(DETECT_LIBTOOL)" != "" ]; then echo "Found LIBTOOL in $(DETECT_LIBTOOL)"; \
+	else echo "Warning: LIBTOOL not found. Required for GLPK java bindings."; fi
+	@if [ "$(DETECT_ACLOCAL)" != "" ]; then echo "Found ACLOCAL in $(DETECT_ACLOCAL)"; \
+	else echo "Warning: ACLOCAL not found. Required for both GLPK and GLPK java bindings."; fi
+	@sed -i '/EXACT_LP_REQUIREMENTS_INSTALLED/c\	public final int EXACT_LP_REQUIREMENTS_INSTALLED = $(EXACT_LP_REQUIREMENTS_INSTALLED);' src/prism/PrismSettings.java;
 
 cuddpackage: checks
 	@if [ "$(CUDD_DIR)" = "" ]; then echo "Error: Cannot find CUDD"; exit 1; fi
@@ -360,6 +395,25 @@ extpackages: checks
 	  ) || exit 1; \
 	done
 
+exact_lp: checks
+	@(if [ "$(EXACT_LP_REQUIREMENTS_INSTALLED)" = 1 ]; then \
+	  for ext in $(EXACT_LP_PACKAGES); do \
+           echo Making $$ext; \
+           (cd ext/$$ext && \
+           $(MAKE) \
+           OSTYPE="$(OSTYPE)" \
+           ARCH="$(ARCH)" \
+           LIBPREFIX="$(LIBPREFIX)" \
+           LIBSUFFIX="$(LIBSUFFIX)" \
+           LIBMATH="$(LIBMATH)" \
+           BINDISTSUFFIX="$(BINDISTSUFFIX)" \
+           JAVA_DIR="$(JAVA_DIR)" \
+           JAVA_JNI_H_DIR="$(JAVA_JNI_H_DIR)" \
+           JAVA_JNI_MD_H_DIR="$(JAVA_JNI_MD_H_DIR)" \
+           ) || exit 1; \
+	  done \
+	fi)
+
 prism: checks make_dirs bin_scripts
 
 make_dirs:
@@ -543,7 +597,7 @@ clean_cudd:
 	@(cd $(CUDD_DIR) && $(MAKE) distclean)
 
 clean_ext:
-	@(for ext in $(EXT_PACKAGES); do \
+	@(for ext in $(EXT_PACKAGES) $(EXACT_LP_PACKAGES); do \
 	  echo Cleaning $$ext ...; \
 	  (cd ext/$$ext && \
 	  $(MAKE) -s LIBPREFIX="$(LIBPREFIX)" LIBSUFFIX="$(LIBSUFFIX)" clean) \

prism/ext/glpk/Makefile

@@ -0,0 +1,57 @@
+################################################
+#  NB: This Makefile is designed to be called  #
+#      from the main PRISM Makefile. It won't  #
+#      work on its own because it needs        #
+#      various options to be passed in         #
+################################################
+
+default: all
+
+all: checks ../../lib/glpk
+
+glpkvers = "4.60"
+
+IS_SRC_CREATED = $(shell find . -name "src" 2> /dev/null)
+ALREADY_DOWNLOADED = $(shell ls src | grep glpk-$(glpkvers).tar.gz 2> /dev/null)
+ALREADY_INSTALLED_LIB = $(shell find src/glpk/src/.libs -name $(LIBPREFIX)glpk$(LIBSUFFIX).40 2> /dev/null)
+ALREADY_INSTALLED = 1
+
+ifeq ($(ALREADY_INSTALLED_LIB),)
+	ALREADY_INSTALLED = 0
+endif
+
+# Try and prevent accidental makes (i.e. called manually, not from top-level Makefile)
+checks:
+	@if [ "$(LIBSUFFIX)" = "" ]; then \
+	  (echo "Error: This Makefile is designed to be called from the main PRISM Makefile"; exit 1) \
+	fi; 
+
+../../lib/glpk:
+	@(if [ "$(OSTYPE)" != "cygwin" ]; then \
+	  (if [ "$(IS_SRC_CREATED)" = "" ]; then \
+	   mkdir src; fi) && \
+	   (cd src/ && \
+	   (if [ "$(ALREADY_DOWNLOADED)" = "" ]; then \
+	    wget http://ftp.gnu.org/gnu/glpk/glpk-$(glpkvers).tar.gz && \
+	    tar -xzf glpk-$(glpkvers).tar.gz && \
+	    mv glpk-$(glpkvers) glpk; \
+	   fi) && \
+	   cd glpk/ && \
+	   (if [ $(ALREADY_INSTALLED) = 0 ]; then \
+	    patch -p1 < ../../glpk_exact_solutions.patch && \
+	    ./autogen.sh > /dev/null && \
+            ./configure --with-gmp > /dev/null && \
+	    echo Building GLPK. This may take several minutes... && \
+            make > /dev/null; \
+	   fi) \
+	  ) && cp --remove-destination src/glpk/src/.libs/$(LIBPREFIX)glpk$(LIBSUFFIX).40 ../../lib/; \
+	fi)
+
+clean: checks
+	rm -f ../../lib/$(LIBPREFIX)glpk$(LIBSUFFIX)
+	rm -f ../../lib/$(LIBPREFIX)glpk$(LIBSUFFIX).40
+	rm -rf src/*
+
+celan:	clean
+
+#################################################