Simple sanity check regression test for simulator.

Author: davexparker

prism-tests/functionality/verify/sim/chain.prism

@@ -0,0 +1,17 @@
+// Completely deterministic model
+// used to do some sanity checks on statistical model checking
+
+dtmc
+
+const int N = 10;
+
+module M
+
+	x : [0..N];
+	
+	[] x<N -> (x'=x+1);
+	[] x=N -> true;
+
+endmodule
+
+label "end" = x=N;

prism-tests/functionality/verify/sim/chain.prism.props

@@ -0,0 +1,15 @@
+const int K = 0;
+
+label "not_end" = x<N;
+
+// RESULT: 1.0
+P=? [ F "end" ]
+
+// RESULT: 1.0
+P=? [ F x=(N+K) ]
+
+// RESULT: 0.0
+P=? [ F x=(N+K+1) ]
+
+// RESULT: 1.0
+P=? [ "not_end" U "end" ]

prism-tests/functionality/verify/sim/chain.prism.props.args

@@ -0,0 +1,2 @@
+-sim
+-ex