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

@@ -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

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