From e2ac8ee84e4bd8b1810e8b67c311eef8f72ed7c8 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Wed, 3 Mar 2021 22:56:10 +0000
Subject: [PATCH] More POMDP tests.

---
 .../verify/pomdps/guess-multi.prism           | 29 +++++++++++++++++++
 .../verify/pomdps/guess-multi.prism.props     |  5 ++++
 .../pomdps/guess-multi.prism.props.args       |  4 +++
 .../functionality/verify/pomdps/guess.prism   | 28 ++++++++++++++++++
 .../verify/pomdps/guess.prism.props           |  2 ++
 5 files changed, 68 insertions(+)
 create mode 100644 prism-tests/functionality/verify/pomdps/guess-multi.prism
 create mode 100644 prism-tests/functionality/verify/pomdps/guess-multi.prism.props
 create mode 100644 prism-tests/functionality/verify/pomdps/guess-multi.prism.props.args
 create mode 100644 prism-tests/functionality/verify/pomdps/guess.prism
 create mode 100644 prism-tests/functionality/verify/pomdps/guess.prism.props

diff --git a/prism-tests/functionality/verify/pomdps/guess-multi.prism b/prism-tests/functionality/verify/pomdps/guess-multi.prism
new file mode 100644
index 00000000..d3a2306d
--- /dev/null
+++ b/prism-tests/functionality/verify/pomdps/guess-multi.prism
@@ -0,0 +1,29 @@
+pomdp
+
+const int N;
+
+module M
+
+	s : [0..2]; // state
+	h : [0..3]; // hidden var
+	g : [0..N] init N; // num guesses left
+
+	[toss] s=0 -> 0.1:(s'=1)&(h'=1) + 0.3:(s'=1)&(h'=2) + 0.6:(s'=1)&(h'=3);
+	[guess1] s=1&g>0 -> (s'=(h=1)?2:s) & (g'=g-1);
+	[guess2] s=1&g>0 -> (s'=(h=2)?2:s) & (g'=g-1);
+	[guess3] s=1&g>0 -> (s'=(h=3)?2:s) & (g'=g-1);
+	[timeup] s=1&g=0 -> (s'=3);
+	[loop] s=2 -> true;
+
+endmodule
+
+observables s, g endobservables
+
+label "correct" = s=2;
+
+rewards "guesses"
+	[guess1] true : 1;
+	[guess2] true : 1;
+	[guess3] true : 1;
+endrewards
+
diff --git a/prism-tests/functionality/verify/pomdps/guess-multi.prism.props b/prism-tests/functionality/verify/pomdps/guess-multi.prism.props
new file mode 100644
index 00000000..c17a6dcb
--- /dev/null
+++ b/prism-tests/functionality/verify/pomdps/guess-multi.prism.props
@@ -0,0 +1,5 @@
+// RESULT (N=1): 0.6
+// RESULT (N=2): 0.9
+// RESULT (N=3): 1.0
+// RESULT (N=4): 1.0
+Pmax=? [ F "correct" ];
diff --git a/prism-tests/functionality/verify/pomdps/guess-multi.prism.props.args b/prism-tests/functionality/verify/pomdps/guess-multi.prism.props.args
new file mode 100644
index 00000000..6cd9032a
--- /dev/null
+++ b/prism-tests/functionality/verify/pomdps/guess-multi.prism.props.args
@@ -0,0 +1,4 @@
+-const N=1
+-const N=2
+-const N=3
+-const N=4
diff --git a/prism-tests/functionality/verify/pomdps/guess.prism b/prism-tests/functionality/verify/pomdps/guess.prism
new file mode 100644
index 00000000..d41bed39
--- /dev/null
+++ b/prism-tests/functionality/verify/pomdps/guess.prism
@@ -0,0 +1,28 @@
+pomdp
+
+const double p = 0.2;
+
+module M
+
+	s : [0..2]; // state
+	h : [0..3]; // hidden var
+
+	[toss] s=0 -> 0.1:(s'=1)&(h'=1) + 0.3:(s'=1)&(h'=2) + 0.6:(s'=1)&(h'=3);
+	//[loop] s=0 -> true; // uncommenting this gives bad bounds
+	[guess1] s=1 -> (s'=(h=1)?2:3);
+	[guess2] s=1 -> (s'=(h=2)?2:3);
+	[guess3] s=1 -> (s'=(h=3)?2:3);
+	[loop] s=2 -> true;
+
+endmodule
+
+observables s endobservables
+
+label "correct" = s=2;
+
+rewards "guesses"
+	[guess1] true : 1;
+	[guess2] true : 1;
+	[guess3] true : 1;
+endrewards
+
diff --git a/prism-tests/functionality/verify/pomdps/guess.prism.props b/prism-tests/functionality/verify/pomdps/guess.prism.props
new file mode 100644
index 00000000..3f8640c7
--- /dev/null
+++ b/prism-tests/functionality/verify/pomdps/guess.prism.props
@@ -0,0 +1,2 @@
+// RESULT: 0.6
+Pmax=? [ F "correct" ];