From 6b15078f4a4fa1c19a02c612fae720f71985922b Mon Sep 17 00:00:00 2001
From: Mateusz Ujma <mateusz.ujma@cs.ox.ac.uk>
Date: Fri, 19 Jul 2013 15:57:40 +0000
Subject: [PATCH] Added counterexamples for explicit engine MEC decomposition

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7092 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism-examples/mec-tests/5.pm | 13 +++++++++++++
 prism-examples/mec-tests/6.pm | 13 +++++++++++++
 2 files changed, 26 insertions(+)
 create mode 100644 prism-examples/mec-tests/5.pm
 create mode 100644 prism-examples/mec-tests/6.pm

diff --git a/prism-examples/mec-tests/5.pm b/prism-examples/mec-tests/5.pm
new file mode 100644
index 00000000..851a1801
--- /dev/null
+++ b/prism-examples/mec-tests/5.pm
@@ -0,0 +1,13 @@
+mdp
+
+module mec_tests
+
+	s : [0..3] init 0;
+	
+	[] s=0 -> 1.0 : (s'=1);
+	[] s=1 -> 1.0 : (s'=0);
+	[] s=0 -> 1.0 : (s'=2);
+	[] s=2 -> 1.0 : (s'=3);
+	[] s=3 -> 1.0 : (s'=2);
+	
+endmodule
diff --git a/prism-examples/mec-tests/6.pm b/prism-examples/mec-tests/6.pm
new file mode 100644
index 00000000..c3dd9537
--- /dev/null
+++ b/prism-examples/mec-tests/6.pm
@@ -0,0 +1,13 @@
+mdp
+
+module mec_tests
+
+	s : [0..3] init 0;
+	
+	[] s=0 -> 1.0 : (s'=1);
+	[] s=1 -> 1.0 : (s'=0);
+	[] s=1 -> 1.0 : (s'=2);
+	[] s=2 -> 0.5 : (s'=3) + 0.5 : (s'=0);
+	[] s=3 -> 1.0 : (s'=3);
+	
+endmodule