From 670ab6e241c2a035c2dce6c49331ab1971a249d1 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@rwth-aachen.de>
Date: Mon, 23 May 2016 16:00:54 +0200
Subject: [PATCH] added a simple example

Former-commit-id: 1af510712a473f94610401a5fc0a0050573565dd
---
 examples/multi-objective/mdp/simple/simple.nm | 26 +++++++++++++++++++
 .../multi-objective/mdp/simple/simple.pctl    |  3 +++
 2 files changed, 29 insertions(+)
 create mode 100644 examples/multi-objective/mdp/simple/simple.nm
 create mode 100644 examples/multi-objective/mdp/simple/simple.pctl

diff --git a/examples/multi-objective/mdp/simple/simple.nm b/examples/multi-objective/mdp/simple/simple.nm
new file mode 100644
index 000000000..50c4fe344
--- /dev/null
+++ b/examples/multi-objective/mdp/simple/simple.nm
@@ -0,0 +1,26 @@
+// sum of two dice as the asynchronous parallel composition of
+// two copies of Knuth's model of a fair die using only fair coins
+
+mdp
+
+module simple
+
+	// local state
+	s : [0..2] init 0;
+
+	[A] s=0 -> 0.2 : (s'=1) + 0.8 : (s'=0);
+	[B] s=0 -> 1 : (s'=2);
+	[]  s>0 -> 1 : (s'=s);
+endmodule
+
+rewards "actA"
+	[A] true : 1;
+endrewards
+
+rewards "actB"
+	[B] true : 2;
+endrewards
+
+
+label "a" = s=1;
+label "b" = s=2;
\ No newline at end of file
diff --git a/examples/multi-objective/mdp/simple/simple.pctl b/examples/multi-objective/mdp/simple/simple.pctl
new file mode 100644
index 000000000..1300542f9
--- /dev/null
+++ b/examples/multi-objective/mdp/simple/simple.pctl
@@ -0,0 +1,3 @@
+Pmax=? [ F "a" ] ;
+Pmax=? [ F "b" ] ;
+multi(P>0.4 [ F "a"], P>0.3 [ F "b"] )
\ No newline at end of file