added a smg example for checking test-modelchecker-rpatl-smg

resources/examples/testfiles/smg/walker.nm

@@ -0,0 +1,29 @@
+smg
+
+player walker
+  [a0], [a00], [a1], [a2], [a3]
+endplayer
+
+player blocker
+  [a40], [a41]
+endplayer
+
+label "s0" = c=0 & b=0 & a=0;
+label "s1" = c=0 & b=0 & a=1;
+label "s2" = c=0 & b=1 & a=0;
+label "s3" = c=0 & b=1 & a=1;
+label "s4" = c=1 & b=0 & a=0;
+
+module transitions
+   a : [0..1] init 0;
+   b : [0..1] init 0;
+   c : [0..1] init 0;
+
+  [a0] a=0 & b=0 & c=0 -> 4/10 : (a'=1) + 6/10 : (b'=1);
+  [a00] a=0 & b=0 & c=0 -> true;
+  [a1] a=1 & b=0 & c=0 -> 3/10 : (a'=0) + 3/10 : (a'=0) & (b'=1) + 4/10 : (b'=1);
+  [a2] a=0 & b=1 & c=0 -> 2/10 : (a'=1) + 8/10 : (b'=0) & (c'=1);
+  [a3] a=1 & b=1 & c=0 -> true;
+  [a40] a=0 & b=0 & c=1 -> 3/10 : (c'=0) + 7/10 : (a'=1) & (b'=1) & (c'=0);
+  [a41] a=0 & b=0 & c=1 -> true;
+endmodule