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