From cb3c8abe348b43ffe938982e5ee25154bea45811 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 16 Oct 2014 11:51:27 +0200 Subject: [PATCH] Introduced parameter (for coin flip probability) in die example and added it to the list of parametric examples. Former-commit-id: a59c4ebd525ecca33564ae003b3366d8d3abecea --- examples/pdtmc/die/die.pm | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 examples/pdtmc/die/die.pm diff --git a/examples/pdtmc/die/die.pm b/examples/pdtmc/die/die.pm new file mode 100644 index 000000000..84e466a18 --- /dev/null +++ b/examples/pdtmc/die/die.pm @@ -0,0 +1,33 @@ +// Knuth's model of a fair die using only fair coins +dtmc + +const double coinProb; + +module die + + // local state + s : [0..7] init 0; + // value of the dice + d : [0..6] init 0; + + [] s=0 -> coinProb : (s'=1) + (1-coinProb) : (s'=2); + [] s=1 -> coinProb : (s'=3) + (1-coinProb) : (s'=4); + [] s=2 -> coinProb : (s'=5) + (1-coinProb) : (s'=6); + [] s=3 -> coinProb : (s'=1) + (1-coinProb) : (s'=7) & (d'=1); + [] s=4 -> coinProb : (s'=7) & (d'=2) + (1-coinProb) : (s'=7) & (d'=3); + [] s=5 -> coinProb : (s'=7) & (d'=4) + (1-coinProb) : (s'=7) & (d'=5); + [] s=6 -> coinProb : (s'=2) + (1-coinProb) : (s'=7) & (d'=6); + [] s=7 -> 1: (s'=7); + +endmodule + +rewards "coin_flips" + [] s<7 : 1; +endrewards + +label "one" = s=7&d=1; +//label "two" = s=7&d=2; +//label "three" = s=7&d=3; +//label "four" = s=7&d=4; +//label "five" = s=7&d=5; +//label "six" = s=7&d=6;