diff --git a/examples/pdtmc/tiny/tiny.pm b/examples/pdtmc/tiny/tiny.pm new file mode 100644 index 000000000..fca4f4de3 --- /dev/null +++ b/examples/pdtmc/tiny/tiny.pm @@ -0,0 +1,11 @@ +dtmc + +module tiny + s : [0 .. 2] init 0; + + [] s = 0 -> 1/2 : (s'=1) + 1/2 : (s'=2); + [] s = 1 -> 1 : (s'=2); + [] s = 2 -> 1/2 : (s'=2) + 1/2 : (s'=1); + +endmodule +