From 799285f9218630591b171f126469a7de4db4cf7f Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Wed, 25 Jul 2018 21:06:52 +0200
Subject: [PATCH] Makefile: new target 'testsfull'

'testsfull' runs the test cases from prism-tests against all the
different engines (explicit, hybrid, sparse, mtbdd, exact), with and
without interval iteration and topological ordering, where appropriate.
---
 prism-tests/all-engines.args | 10 ++++++++++
 prism/Makefile               | 11 +++++++++++
 2 files changed, 21 insertions(+)
 create mode 100644 prism-tests/all-engines.args

diff --git a/prism-tests/all-engines.args b/prism-tests/all-engines.args
new file mode 100644
index 00000000..59cf572c
--- /dev/null
+++ b/prism-tests/all-engines.args
@@ -0,0 +1,10 @@
+-explicit
+-explicit -ii -maxiters 100000
+-explicit -ii -topological -maxiters 100000
+-mtbdd
+-mtbdd -ii -maxiters 100000 -cuddepsilon 1E-20
+-hybrid
+-hybrid -ii -maxiters 100000
+-sparse
+-sparse -ii -maxiters 100000
+-exact
diff --git a/prism/Makefile b/prism/Makefile
index f57ab7da..0e36fcc8 100644
--- a/prism/Makefile
+++ b/prism/Makefile
@@ -436,6 +436,17 @@ testslocal:
 	  echo "Skipping local tests"; \
 	fi
 
+# Run the tests from ../prism-tests (with different engine settings, picked up from ../prism-tests/all-engines.args)
+# - Export tests are disabled, as there is currently no robust test mechanism for dealing with the
+#   variations in the output of the different engines.
+# - We run with --test-all, as failures for some engines should not abort the tests
+# - We run with a timeout of 1 minute, as some engines take a long time for some properties
+testsfull:
+	cd ../prism-tests && \
+	"$(PWD)"/etc/scripts/prism-auto -t -m . \
+	--skip-export-runs --skip-duplicate-runs --test-all -a all-engines.args --timeout 1m \
+	-p "$(PWD)"/bin/prism --nailgun $(TESTS_ARGS);
+
 bin_scripts:
 	@for target in $(BIN_TARGETS); do \
 	  target_trunc=`echo $$target | sed 's/\.[^.]*$$//'` && \