Simple test cases/sanity checks for DTMC steady-state computation

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

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 ];

prism-tests/functionality/verify/dtmcs/dtmc_steady_1.pm.props.args

@@ -0,0 +1,5 @@
+-explicit
+-hybrid
+-sparse
+-mtbdd
+-exact

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

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 ];
+

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