New versions of optional libraries

.github/workflows/make-tests.yml

@@ -26,6 +26,7 @@ jobs:
       run: |
         make
         make unittests
+        make test testz3 testyices
         make tests
 
   build-win:
@@ -54,12 +55,19 @@ jobs:
           wget,
           unzip,
           python
-    - name: make tests
+    - name: make
       shell: bash
       env:
         CYGWIN: winsymlinks:native
       working-directory: ./prism
       run: >-
         make &&
         make unittests &&
+        make test testz3 testyices testppl
+    - name: make tests
+      shell: bash
+      env:
+        CYGWIN: winsymlinks:native
+      working-directory: ./prism
+      run: >-
         make tests

CHANGELOG.txt

@@ -71,6 +71,16 @@ Version 1.0 (first released 18/10/2012)
 
 Below are the details of the changes in each new version of PRISM.
 
+-----------------------------------------------------------------------------
+Changes since last release (up to a6d86d21)
+-----------------------------------------------------------------------------
+
+* Updates/fixes in install/launch/testing scripts and build process
+* New -javaversion switch to show Java version used
+* New tests in etc/tests available for easier build tests
+* Transition reward export (MDP-like models) for explicit engine
+* Various bugfixes
+
 -----------------------------------------------------------------------------
 Version 4.8 (first released 5/7/2023)
 -----------------------------------------------------------------------------

prism/Makefile

@@ -163,32 +163,6 @@ JAVA_JNI_H_DIR = $(shell \
 JAVA_JNI_MD_H_DIR = $(shell (ls "$(JAVA_JNI_H_DIR)"/jni_md.h "$(JAVA_JNI_H_DIR)"/*/jni_md.h | head -n 1 | sed 's/\/jni_md.h//') 2>/dev/null)
 JAVA_INCLUDES = -I $(JAVA_JNI_H_DIR) -I $(JAVA_JNI_MD_H_DIR)
 
-########
-# PPL  #
-########
-
-# PPL_DIR needs to be set to the location of the Parma Polyhedra Library installation.
-# (More precisely PPL_DIR should contain a directory 'ppl' containing libppl_java.* and ppl_java.jar)
-# This makefile will try to detect this automatically based on the information provided by the ppl-config command.
-# If this detection does not work, or you wish to override it,
-# either set the variable yourself by uncommenting and/or modifying one of the lines below
-# or pass a value to make directly, e.g.: make PPL_DIR=/usr/local/ppl/lib
-
-# Find PPL
-PPL_DIR = $(shell src/scripts/findppl.sh)
-
-#PPL_DIR = 		/usr/local/ppl/lib
-#PPL_DIR = 		/usr/local/lib
-
-# Expected names of (some) PPL files
-ifeq ($(OSTYPE),linux)
-	PPL_JAVA_LIB = libppl_java.so
-endif
-ifeq ($(OSTYPE),darwin)
-	PPL_JAVA_LIB = libppl_java.jnilib
-endif
-PPL_JAVA_JAR = ppl_java.jar
-
 ##################
 # Compilers etc. #
 ##################
@@ -368,7 +342,7 @@ export CFLAGS CXXFLAGS LDFLAGS JFLAGS LIBPREFIX LIBSUFFIX
 
 MAKE_DIRS = dd jdd odd dv prism mtbdd sparse hybrid parser settings userinterface pepa/compiler simulator jltl2ba jltl2dstar explicit pta param strat automata common cex
 
-EXT_PACKAGES = lpsolve55 lp_solve_5.5_java z3 yices
+EXT_PACKAGES = lpsolve55 lp_solve_5.5_java z3 yices ppl
 
 .PHONY: clean javadoc tests release
 
@@ -377,42 +351,14 @@ EXT_PACKAGES = lpsolve55 lp_solve_5.5_java z3 yices
 
 default: all
 
-all: cuddpackage ppl extpackages prism
+all: cuddpackage extpackages prism
 
 # Build our customised version of CUDD
 cuddpackage: checks
 	@echo Making cudd ...; \
 	cd $(CUDD_DIR) && \
 	$(MAKE) ICFLAGS="$(DEBUG) $(OPTIMISE) $(WARNINGS)" XCFLAGS="$(filter-out $(DEBUG) $(OPTIMISE) $(WARNINGS),$(CFLAGS))"
 
-# Copy PPL libraries to lib dir
-# (only if not already there, to avoid repeated copying).
-# We check for PPL_JAVA_LIB, which is consistently named
-# and whose presence likely indicates that the files have already been copied.
-# If not found, we use a local copy of the JAR (in ext/ppl_java) since this is needed for compilation.
-ppl: checks
-	@echo Copying PPL files ...; \
-	if [ "$(PPL_DIR)" = "" ]; then \
-		echo "PPL_DIR not specified/detected: cannot copy files"; \
-	else \
-		if [ -f "$(PRISM_LIB_DIR)"/"$(PPL_JAVA_LIB)" ]; then \
-			echo "PPL Java library $(PRISM_LIB_DIR)/$(PPL_JAVA_LIB) detected: nothing to do"; \
-		else \
-			(cp "$(PPL_DIR)"/ppl/"$(PPL_JAVA_LIB)" "$(PRISM_LIB_DIR)" || echo Failed to copy PPL Java library); \
-			(cp "$(PPL_DIR)"/ppl/"$(PPL_JAVA_JAR)" "$(PRISM_LIB_DIR)" || echo Failed to copy PPL Java JAR); \
-			if [ "$(OSTYPE)" = "linux" ]; then \
-				(cp "$(PPL_DIR)"/libppl.so.[0-9][0-9] "$(PRISM_LIB_DIR)" || echo Failed to copy PPL library); \
-			fi; \
-			if [ "$(OSTYPE)" = "darwin" ]; then \
-				(cp "$(PPL_DIR)"/libppl.[0-9][0-9].*lib "$(PRISM_LIB_DIR)" || echo Failed to copy PPL library); \
-			fi; \
-		fi; \
-	fi ; \
-	if [ ! -f "$(PRISM_LIB_DIR)"/"$(PPL_JAVA_JAR)" ]; then \
-		echo "PPL library files not copied; using local copy of JAR"; \
-		cp ext/ppl_java/"$(PPL_JAVA_JAR)" "$(PRISM_LIB_DIR)"; \
-	fi
-
 # Use this to force a rebuild (with javacc) of the main parser
 parser:
 	@echo Making parser ...; \
@@ -525,20 +471,6 @@ checks:
 	  echo "\033[0m"; \
 	  exit 1; \
 	fi; \
-	if [ "$(PPL_DIR)" = "" ]; then \
-	  echo "\033[33mPRISM was unable to find the directory which contains"; \
-	  echo "the Parma Polyhedra Library (PPL). Please specify this "; \
-	  echo "manually to make, as in this example:"; \
-	  echo; \
-	  echo "  make PPL_DIR=/usr/local/ppl/lib"; \
-	  echo; \
-	  echo "See the PRISM manual for further information."; \
-	  echo; \
-	  echo "Alternatively, if you wish, you can set the environment"; \
-	  echo "variable yourself (using setenv or export) or you"; \
-	  echo "can edit the value of PPL_DIR directly in the Makefile."; \
-	  echo "\033[0m"; \
-	fi; \
 	if [ ! -d "$(JAVA_DIR)" ]; then \
 	  echo "\033[33mJava directory \"$(JAVA_DIR)\" does not exist."; \
 	  echo "\033[0m"; \
@@ -562,7 +494,6 @@ checks:
 	echo "JAVA_DIR_BACKUP: $(JAVA_DIR_BACKUP)"; \
 	echo "JAVAC (which): "`which $(JAVAC)`; \
 	echo "JAVAC (version): "$(shell $(JAVAC) -version) \
-	echo "PPL_DIR: $(PPL_DIR)" \
 	)
 
 # Misc: count the number of lines of code
@@ -602,21 +533,21 @@ testyices:
 # Optionally, extra arguments for prism-auto are picked up via variable TESTS_ARGS
 tests: testslocal
 	@if [ -d ../prism-tests ]; then \
-	  etc/scripts/prism-auto -t -m ../prism-tests -p bin/prism --nailgun --ngprism bin/ngprism $(TESTS_ARGS); \
+	  etc/scripts/prism-auto -t -m ../prism-tests -p bin/prism --print-failures --nailgun --ngprism bin/ngprism $(TESTS_ARGS); \
 	else \
 	  echo "Skipping tests"; \
 	fi
 
 # Just display the command to run the test suite on this version of PRISM
 # Optionally, extra arguments for prism-auto are picked up via variable TESTS_ARGS
 testsecho:
-	@echo etc/scripts/prism-auto -t -m ../prism-tests -p bin/prism --nailgun --ngprism bin/ngprism $(TESTS_ARGS)
+	@echo etc/scripts/prism-auto -t -m ../prism-tests -p bin/prism --print-failures --nailgun --ngprism bin/ngprism $(TESTS_ARGS)
 
 # Run local tests (in ./tests)
 # Optionally, extra arguments for prism-auto are picked up via variable TESTS_ARGS
 testslocal:
 	@if [ -d tests ]; then \
-	  etc/scripts/prism-auto -t -m tests -p bin/prism --nailgun --ngprism bin/ngprism $(TESTS_ARGS); \
+	  etc/scripts/prism-auto -t -m tests -p bin/prism --print-failures --nailgun --ngprism bin/ngprism $(TESTS_ARGS); \
 	else \
 	  echo "Skipping local tests"; \
 	fi
@@ -629,7 +560,7 @@ testslocal:
 testsfull:
 	etc/scripts/prism-auto -t -m ../prism-tests \
 	--skip-export-runs --skip-duplicate-runs --test-all -a ../prism-tests/all-engines.args --timeout 1m \
-	-p bin/prism --nailgun $(TESTS_ARGS);
+	-p bin/prism --print-failures --nailgun $(TESTS_ARGS);
 
 ##########################
 # Building distributions #
@@ -735,20 +666,16 @@ clean: checks
 celan: clean
 
 # Clean PRISM + CUDD and external libs
-clean_all: checks clean_cudd clean_ppl clean_ext clean clean_tests
+clean_all: checks clean_cudd clean_ext clean clean_tests
 
 clean_cudd:
 	@(cd $(CUDD_DIR) && $(MAKE) distclean)
 
-# Remove PPL libraries copied to lib
-clean_ppl:
-	@rm -f $(PRISM_LIB_DIR)/libppl* $(PRISM_LIB_DIR)/"$(PPL_JAVA_JAR)"
-
 clean_ext:
 	@(for ext in $(EXT_PACKAGES); do \
 	  echo Cleaning $$ext ...; \
 	  (cd ext/$$ext && \
-	  $(MAKE) -s clean) \
+	  $(MAKE) -s OSTYPE="$(OSTYPE)" ARCH="$(ARCH)" clean) \
 	  || exit 1; \
 	done )
 

prism/etc/scripts/prism-auto

@@ -679,8 +679,13 @@ def runPrism(args, bmArgs, dir=""):
             for line in open(logFile, 'r').readlines():
                 if re.match('Error:', line):
                     printTestResult(line)
-            print("To see log file, run:")
-            print("edit " + logFile)
+            if (options.printFailures):
+                print("Failing test log file:")
+                for line in open(logFile, 'r').readlines():
+                    print(line, end="")
+            else:
+                print("To see log file, run:")
+                print("edit " + logFile)
             prismArgsPrint = list(prismArgs)
             prismArgsPrint[0] = options.prismExec
             print("To re-run failing test:")
@@ -1162,6 +1167,7 @@ parser.add_option("--skip-duplicate-runs", action="store_true", dest="skipDuplic
 parser.add_option("--timeout", dest="timeout", metavar="N", default=None, help='Timeout for each PRISM run (examples values for N: 5 / 5s for seconds, 5m / 5h for minutes / hours)')
 parser.add_option("--dd-warnings", action="store_true", dest="ddWarnings", default=False, help="Print the DD reference count warnings")
 parser.add_option("--colour", dest="colourEnabled", metavar="X", type="choice", choices=["yes","no","auto"], default="auto", help="Whether to colour test results: yes, no, auto (yes iff in terminal mode) [default=auto]")
+parser.add_option("--print-failures", action="store_true", dest="printFailures", default=False, help="Display logs for failing tests")
 (options, args) = parser.parse_args()
 if len(args) < 1:
     parser.print_help()

prism/etc/scripts/prism-install-cygwin

@@ -12,5 +12,5 @@ git clone https://github.com/prismmodelchecker/prism-games.git
 # Compile PRISM-games and run a few tests (unless --nobuild passed)
 # (should ultimately display: "Testing result: PASS")
 if [ "$*" = "${*/--nobuild}" ]; then
-  (cd prism-games/prism && make && make test testz3)
+  (cd prism-games/prism && make && make test testyices testz3 testppl)
 fi

prism/etc/scripts/prism-install-fedora

@@ -19,5 +19,5 @@ git clone https://github.com/prismmodelchecker/prism-games.git
 # Compile PRISM-games and run a few tests (unless --nobuild passed)
 # (should ultimately display: "Testing result: PASS")
 if [ "$*" = "${*/--nobuild}" ]; then
-  (cd prism-games/prism && make && make test testppl testyices testz3)
+  (cd prism-games/prism && make && make test testyices testz3 testppl)
 fi

prism/etc/scripts/prism-install-ubuntu

@@ -20,55 +20,8 @@ sudo apt -y install python3
 # Download the latest development version from GitHub
 git clone https://github.com/prismmodelchecker/prism-games.git
 
-# Find the Java directory
-export JAVA_HOME=`prism-games/prism/src/scripts/findjavac.sh | sed 's/\/bin\/javac//'`
-
-# Download/build PPL + dependencies (needs Java 8 it seems)
-# Comment out the section below if multi-obj support not needed
-sudo apt -y install openjdk-8-jdk libgmp-dev m4
-export JAVA8_HOME=`find /usr/lib/jvm -name 'java-8*'`
-wget http://www.bugseng.com/products/ppl/download/ftp/releases/1.2/ppl-1.2.tar.gz
-tar xfz ppl-1.2.tar.gz
-cd ppl-1.2
-./configure --enable-interfaces=java --with-java=$JAVA8_HOME
-make
-sudo make install
-cd ..
-
-# Download and build Yices 2.6.2 + Java wrapper
-# Commented out for now since yices binaries are included
-# sudo apt -y install gperf libgmp-dev
-# wget https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-src.tar.gz
-# tar xvfz yices-2.6.2-src.tar.gz
-# cd yices-2.6.2
-# ./configure
-# make
-# sudo make install
-# cp /usr/local/lib/libyices.so.2.6 ../prism-games/prism/ext/yices
-# cd ..
-# git clone https://github.com/SRI-CSL/yices2_java_bindings
-# cd yices2_java_bindings
-# ./ant.sh
-# jar cvfm dist/lib/yices.jar MANIFEST.txt -C build/classes .
-# cp dist/lib/libyices2java.so ../prism-games/prism/ext/yices
-# cp dist/lib/yices.jar ../prism-games/prism/ext/yices
-# cd ..
-
-# Download and build Z3 4.8.7
-# Commented out for now since z3 binaries are included
-# sudo apt -y install python
-# wget https://github.com/Z3Prover/z3/archive/z3-4.8.7.tar.gz
-# tar xvfz z3-4.8.7.tar.gz
-# cd z3-z3-4.8.7
-# python scripts/mk_make.py --java
-# cd build
-# make
-# sudo make install
-# cp /usr/lib/libz3.so ../prism-games/prism/lib
-# cd ..
-
 # Compile PRISM-games and run a few tests (unless --nobuild passed)
 # (should ultimately display: "Testing result: PASS")
 if [ "$*" = "${*/--nobuild}" ]; then
-  (cd prism-games/prism && make && make test testppl testyices testz3)
+  (cd prism-games/prism && make && make test testyices testz3 testppl)
 fi

prism/etc/scripts/prism-install-windows.bat

@@ -17,3 +17,6 @@ setx PATH "%ProgramFiles(x86)%\NSIS;%PATH%"
 @REM Get and install Cygwin, with core packages needed for PRISM install
 "%SystemRoot%\System32\WindowsPowerShell\v1.0\powershell.exe" -Command "wget -Uri  http://cygwin.com/setup-x86_64.exe -Outfile setup-x86_64.exe
 .\setup-x86_64.exe -P make -P mingw64-x86_64-gcc-g++ -P binutils -P dos2unix -P git -P wget -P unzip -P python -P nano -q -s http://ftp.inf.tu-dresden.de/software/windows/cygwin/
+
+@REM Launch a Cygwin terminal
+"%HOMEDRIVE%\cygwin64\bin\mintty.exe" -

prism/ext/README.md

@@ -4,6 +4,12 @@ To simplify maintenance of scripts and config files, we mostly omit version numb
 
 * lpsolve (and its Java wrapper) - modification of version 5.5.2.0 (and version 5.5.0.14)
 
+* Z3 (and its Java interface) - version 4.12.4
+
+* Yices 2 (and its Java interface) - version 2.6.4 (and version 1.0.1 ish)
+
+* PPL (and its Java interface) - modification of version 1.2
+
 See here for more details and links:
 
 http://www.prismmodelchecker.org/other-downloads.php

prism/ext/ppl/Makefile

@@ -0,0 +1,62 @@
+################################################
+#  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 libfiles
+
+# Files to copy
+NATIVE_LIBS =
+ifdef OSTYPE
+	NATIVE_LIBS = $(wildcard $(OSTYPE)/$(ARCH)/*)
+endif
+NATIVE_LIBS_COPY = $(NATIVE_LIBS:$(OSTYPE)/$(ARCH)/%=../../$(PRISM_LIB_DIR)/%)
+COMMON_LIBS = $(wildcard common/*)
+COMMON_LIBS_COPY = $(COMMON_LIBS:common/%=../../$(PRISM_LIB_DIR)/%)
+
+# 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; 
+
+# Copy files/links if they exist and are newer
+# If a file is in both an OS-specific directory and common, the former takes precedence
+
+libfiles: $(NATIVE_LIBS_COPY) $(COMMON_LIBS_COPY)
+	@if [ "$(NATIVE_LIBS_COPY)" = "" ]; then \
+	  echo "Missing pre-built native libraries for $(OSTYPE) $(ARCH)"; \
+	fi
+
+../../$(PRISM_LIB_DIR)/%: $(OSTYPE)/$(ARCH)/%
+	@if [ -f "$<" ]; then \
+	  echo cp -R $< $@; \
+	  cp -R $< $@; \
+	fi
+
+../../$(PRISM_LIB_DIR)/%: common/%
+	@if [ -f "$<" ]; then \
+	  echo cp -R $< $@; \
+	  cp -R $< $@; \
+	fi
+
+clean: checks
+	# Remove installed files if present
+	@if [ "$(COMMON_LIBS_COPY)" != "" ]; then \
+	  echo Removing "$(COMMON_LIBS_COPY)" && rm -f "$(COMMON_LIBS_COPY)"; \
+	fi
+	@if [ "$(NATIVE_LIBS_COPY)" != "" ]; then \
+	  echo Removing "$(NATIVE_LIBS_COPY)" && rm -f "$(NATIVE_LIBS_COPY)"; \
+	fi
+	# Overapproximate and remove all native libraries files for any OS
+	rm -f ../../$(PRISM_LIB_DIR)/*lib*ppl*
+	rm -f ../../$(PRISM_LIB_DIR)/*ppl*dll*
+
+celan:	clean
+
+
+#################################################