From 1571b3a8b85f3a86d5ff891d52e48141472b16ab Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Thu, 8 Mar 2018 13:48:10 +0100
Subject: [PATCH] Tests for various DTMC engine / solver combinations

Exercise the various engine / solver combinations for a simple DTMC,
to guard against changes leading to fundamental breakage.
---
 .../verify/dtmcs/dtmc_pctl.pm.props.args      | 49 +++++++++++++++++++
 1 file changed, 49 insertions(+)
 create mode 100644 prism-tests/functionality/verify/dtmcs/dtmc_pctl.pm.props.args

diff --git a/prism-tests/functionality/verify/dtmcs/dtmc_pctl.pm.props.args b/prism-tests/functionality/verify/dtmcs/dtmc_pctl.pm.props.args
new file mode 100644
index 00000000..74caf841
--- /dev/null
+++ b/prism-tests/functionality/verify/dtmcs/dtmc_pctl.pm.props.args
@@ -0,0 +1,49 @@
+# different engines and iteration methods:
+
+-ex -power
+-ex -jacobi
+-ex -gs
+-ex -bgs
+
+-s -power
+-s -jacobi
+-s -gs
+-s -bgs
+
+-h -power
+-h -jacobi
+-h -pgs
+
+-m -power
+-m -jacobi
+
+# and using interval iteration:
+
+-ii -ex -power
+-ii -ex -jacobi
+-ii -ex -gs
+-ii -ex -bgs
+
+-ii -s -power
+-ii -s -jacobi
+-ii -s -gs
+-ii -s -bgs
+
+-ii -h -power
+-ii -h -jacobi
+-ii -h -pgs
+
+-ii -m -power
+-ii -m -jacobi
+
+# and using -topological
+
+-ex -power -topological
+-ex -jacobi -topological
+-ex -gs -topological
+-ex -bgs -topological
+
+-ii -ex -power -topological
+-ii -ex -jacobi -topological
+-ii -ex -gs -topological
+-ii -ex -bgs -topological