From 764b6c9a3b6fdebf0c2ee33806ee1291faf0cb1b Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 4 Jun 2020 13:57:06 +0200
Subject: [PATCH] Added small pomdp example.

---
 resources/examples/testfiles/pomdp/simple.prism | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 resources/examples/testfiles/pomdp/simple.prism

diff --git a/resources/examples/testfiles/pomdp/simple.prism b/resources/examples/testfiles/pomdp/simple.prism
new file mode 100644
index 000000000..5076de9fb
--- /dev/null
+++ b/resources/examples/testfiles/pomdp/simple.prism
@@ -0,0 +1,17 @@
+pomdp
+
+observable "start" = s<3;
+observable "end" = s>4;
+
+const double slippery;
+
+module main
+    s : [0..6] init 0;
+    [alpha] s=0 -> (1-slippery) * 0.7: (s'=1) + (1-slippery) * 0.3: (s'=2) + slippery: true;
+    [alpha] s>0 & s<5 -> (1-slippery): (s'=s+2) + slippery: true;
+    [beta]  s=3 -> (1-slippery): (s'=6)   + slippery: true;
+    [beta]  s=4 -> (1-slippery): (s'=5) + slippery: true;
+endmodule
+
+
+label "goal" = s=5;