From f5f04a1c055a64dbf9a28008095d78ad05874e7f Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 16 Jan 2013 22:28:14 +0100 Subject: [PATCH] Added dummy test to check for valid push to new repo. --- anothertest.input | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 anothertest.input diff --git a/anothertest.input b/anothertest.input new file mode 100644 index 000000000..700951a05 --- /dev/null +++ b/anothertest.input @@ -0,0 +1,24 @@ +// Knuth's model of a fair die using only fair coins +dtmc + +module die + + // local state + s : [0..7] init 0; + // value of the dice + d : [0..6] init 0; + + [] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); + [] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4); + [] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6); + [] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1); + [] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3); + [] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5); + [] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6); + [] s=7 -> 1: (s'=7); + +endmodule + +rewards "coin_flips" + [] s<7 : 1; +endrewards