From 1363d2b586409f0016a0a27d4f043f6e70fc83ca Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 1 Jun 2018 11:01:00 +0200
Subject: [PATCH] Simple test cases/sanity checks for DTMC steady-state
 computation

---
 .../verify/dtmcs/dtmc_steady_1.pm             | 16 ++++++++++
 .../verify/dtmcs/dtmc_steady_1.pm.props       | 32 +++++++++++++++++++
 .../verify/dtmcs/dtmc_steady_1.pm.props.args  |  5 +++
 .../verify/dtmcs/dtmc_steady_2.pm             | 10 ++++++
 .../verify/dtmcs/dtmc_steady_2.pm.props       | 12 +++++++
 .../verify/dtmcs/dtmc_steady_2.pm.props.args  |  7 ++++
 6 files changed, 82 insertions(+)
 create mode 100644 prism-tests/functionality/verify/dtmcs/dtmc_steady_1.pm
 create mode 100644 prism-tests/functionality/verify/dtmcs/dtmc_steady_1.pm.props
 create mode 100644 prism-tests/functionality/verify/dtmcs/dtmc_steady_1.pm.props.args
 create mode 100644 prism-tests/functionality/verify/dtmcs/dtmc_steady_2.pm
 create mode 100644 prism-tests/functionality/verify/dtmcs/dtmc_steady_2.pm.props
 create mode 100644 prism-tests/functionality/verify/dtmcs/dtmc_steady_2.pm.props.args

diff --git a/prism-tests/functionality/verify/dtmcs/dtmc_steady_1.pm b/prism-tests/functionality/verify/dtmcs/dtmc_steady_1.pm
new file mode 100644
index 00000000..190a6452
--- /dev/null
+++ b/prism-tests/functionality/verify/dtmcs/dtmc_steady_1.pm
@@ -0,0 +1,16 @@
+// simple sanity test case for DTMC steady state computations (2 BSCCs)
+
+dtmc
+
+module m1
+  s: [0..2] init 0;
+
+  [] s=0 -> 1/4:(s'=0) + 1/2:(s'=1) + 1/4:(s'=2);
+  [] s>0 -> true;
+endmodule
+
+module m2
+  t: [0..2] init 0;
+
+  [] true -> 1/2:(t'=0) + 1/4:(t'=1) + 1/4:(t'=2);
+endmodule
diff --git a/prism-tests/functionality/verify/dtmcs/dtmc_steady_1.pm.props b/prism-tests/functionality/verify/dtmcs/dtmc_steady_1.pm.props
new file mode 100644
index 00000000..01252ac8
--- /dev/null
+++ b/prism-tests/functionality/verify/dtmcs/dtmc_steady_1.pm.props
@@ -0,0 +1,32 @@
+// RESULT: 0
+S=?[ s=0 ];
+
+// RESULT: 0
+S=?[ s=0 & t=0 ];
+
+// RESULT: 1/3
+S=?[ s=1 & t=0 ];
+
+// RESULT: 1/6
+S=?[ s=1 & t=1 ];
+
+// RESULT: 1/6
+S=?[ s=1 & t=2 ];
+
+// RESULT: 1/6
+S=?[ s=2 & t=0 ];
+
+// RESULT: 1/12
+S=?[ s=2 & t=1 ];
+
+// RESULT: 1/12
+S=?[ s=2 & t=2 ];
+
+// RESULT: 1/2
+S=?[ t=0 ];
+
+// RESULT: 1/4
+S=?[ t=1 ];
+
+// RESULT: 1/4
+S=?[ t=1 ];
diff --git a/prism-tests/functionality/verify/dtmcs/dtmc_steady_1.pm.props.args b/prism-tests/functionality/verify/dtmcs/dtmc_steady_1.pm.props.args
new file mode 100644
index 00000000..d21284d2
--- /dev/null
+++ b/prism-tests/functionality/verify/dtmcs/dtmc_steady_1.pm.props.args
@@ -0,0 +1,5 @@
+-explicit
+-hybrid
+-sparse
+-mtbdd
+-exact
diff --git a/prism-tests/functionality/verify/dtmcs/dtmc_steady_2.pm b/prism-tests/functionality/verify/dtmcs/dtmc_steady_2.pm
new file mode 100644
index 00000000..62af59ad
--- /dev/null
+++ b/prism-tests/functionality/verify/dtmcs/dtmc_steady_2.pm
@@ -0,0 +1,10 @@
+// simple test case for DTMC steady state computation (exhibits non-convergence using "naive" iteration)
+
+dtmc
+
+module m
+  s: [0..2] init 0;
+
+  [] s=0 -> 1/2:(s'=1) + 1/2:(s'=2);
+  [] s>0 -> (s'=0);
+endmodule
diff --git a/prism-tests/functionality/verify/dtmcs/dtmc_steady_2.pm.props b/prism-tests/functionality/verify/dtmcs/dtmc_steady_2.pm.props
new file mode 100644
index 00000000..ff54cb7a
--- /dev/null
+++ b/prism-tests/functionality/verify/dtmcs/dtmc_steady_2.pm.props
@@ -0,0 +1,12 @@
+// RESULT: 1
+S=?[ s=0 | s=1 | s=2 ];
+
+// RESULT: 1/2
+S=?[ s=0 ];
+
+// RESULT: 1/4
+S=?[ s=1 ];
+
+// RESULT: 1/4
+S=?[ s=2 ];
+
diff --git a/prism-tests/functionality/verify/dtmcs/dtmc_steady_2.pm.props.args b/prism-tests/functionality/verify/dtmcs/dtmc_steady_2.pm.props.args
new file mode 100644
index 00000000..9a4cebfa
--- /dev/null
+++ b/prism-tests/functionality/verify/dtmcs/dtmc_steady_2.pm.props.args
@@ -0,0 +1,7 @@
+# sanity check for convergence for the different engines
+# mtbdd/sparse/hybrid currently require the switch to the power method for convergence
+-mtbdd -power
+-sparse -power
+-hybrid -power
+-explicit
+-exact