From 316371cc1b3615dbc2aa47855f392aef9597fca7 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 16 Aug 2019 08:36:26 +0100
Subject: [PATCH] Simple sanity check regression test for simulator.

---
 .../functionality/verify/sim/chain.prism        | 17 +++++++++++++++++
 .../functionality/verify/sim/chain.prism.props  | 15 +++++++++++++++
 .../verify/sim/chain.prism.props.args           |  2 ++
 3 files changed, 34 insertions(+)
 create mode 100644 prism-tests/functionality/verify/sim/chain.prism
 create mode 100644 prism-tests/functionality/verify/sim/chain.prism.props
 create mode 100644 prism-tests/functionality/verify/sim/chain.prism.props.args

diff --git a/prism-tests/functionality/verify/sim/chain.prism b/prism-tests/functionality/verify/sim/chain.prism
new file mode 100644
index 00000000..c7f3c5f0
--- /dev/null
+++ b/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;
diff --git a/prism-tests/functionality/verify/sim/chain.prism.props b/prism-tests/functionality/verify/sim/chain.prism.props
new file mode 100644
index 00000000..0daa4b22
--- /dev/null
+++ b/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" ]
diff --git a/prism-tests/functionality/verify/sim/chain.prism.props.args b/prism-tests/functionality/verify/sim/chain.prism.props.args
new file mode 100644
index 00000000..43f3d9e3
--- /dev/null
+++ b/prism-tests/functionality/verify/sim/chain.prism.props.args
@@ -0,0 +1,2 @@
+-sim
+-ex