diff --git a/resources/examples/testfiles/pdtmc/simple4.pm b/resources/examples/testfiles/pdtmc/simple4.pm new file mode 100644 index 000000000..1bdc3e004 --- /dev/null +++ b/resources/examples/testfiles/pdtmc/simple4.pm @@ -0,0 +1,17 @@ +dtmc + +const double p; + +module test + + // local state + s : [0..4] init 0; + + [] s=0 -> p*(1-p) : (s'=1) + (1-p*(1-p)) : (s'=2); + [] s=1 -> p : (s'=3) + (1-p) : (s'=4); + [] s=2 -> (1-p) : (s'=3) + (p) : (s'=4); + [] s=3 -> 1 : (s'=3); + [] s=4 -> 1 : (s'=4); + +endmodule +