// optimal program for the sum of two dice

dtmc

module sum_of_two_dice
	
	// local state
	s : [0..34] init 0;
	// total of two dice
	d : [0..12] 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'=7  + 0.5 : s'=34 & d'=6;
	[] s=4  -> 0.5 : s'=8  + 0.5 : s'=34 & d'=7;
	[] s=5  -> 0.5 : s'=9  + 0.5 : s'=34 & d'=8;
	[] s=6  -> 0.5 : s'=10 + 0.5 : s'=11;
	[] s=7  -> 0.5 : s'=12 + 0.5 : s'=34 & d'=4;
	[] s=8  -> 0.5 : s'=13 + 0.5 : s'=34 & d'=5;
	[] s=9  -> 0.5 : s'=14 + 0.5 : s'=34 & d'=9;
	[] s=10 -> 0.5 : s'=15 + 0.5 : s'=34 & d'=10;
	[] s=11 -> 0.5 : s'=16 + 0.5 : s'=17;
	[] s=12 -> 0.5 : s'=18 + 0.5 : s'=34 & d'=3;
	[] s=13 -> 0.5 : s'=19 + 0.5 : s'=34 & d'=5;
	[] s=14 -> 0.5 : s'=20 + 0.5 : s'=34 & d'=7;
	[] s=15 -> 0.5 : s'=21 + 0.5 : s'=34 & d'=9;
	[] s=16 -> 0.5 : s'=22 + 0.5 : s'=34 & d'=11;
	[] s=17 -> 0.5 : s'=23 + 0.5 : s'=24;
	[] s=18 -> 0.5 : s'=25 + 0.5 : s'=34 & d'=2;
	[] s=19 -> 0.5 : s'=26 + 0.5 : s'=34 & d'=3;
	[] s=20 -> 0.5 : s'=27 + 0.5 : s'=34 & d'=4;
	[] s=21 -> 0.5 : s'=34 & d'=5 + 0.5 : s'=34 & d'=9;
	[] s=22 -> 0.5 : s'=28 + 0.5 : s'=34 & d'=10;
	[] s=23 -> 0.5 : s'=29 + 0.5 : s'=34 & d'=11;
	[] s=24 -> 0.5 : s'=30 + 0.5 : s'=34 & d'=12;
	[] s=25 -> 0.5 : s'=1  + 0.5 : s'=34 & d'=2;
	[] s=26 -> 0.5 : s'=31 + 0.5 : s'=34 & d'=3;
	[] s=27 -> 0.5 : s'=32 + 0.5 : s'=34 & d'=6;
	[] s=28 -> 0.5 : s'=34 & d'=7 + 0.5 : s'=34 & d'=8;
	[] s=29 -> 0.5 : s'=33 + 0.5 : s'=34 & d'=11;
	[] s=30 -> 0.5 : s'=2  + 0.5 : s'=34 & d'=12;
	[] s=31 -> 0.5 : s'=34 & d'=2 + 0.5 : s'=34 & d'=4;
	[] s=32 -> 0.5 : s'=34 & d'=6 + 0.5 : s'=34 & d'=8;
	[] s=33 -> 0.5 : s'=34 & d'=10 + 0.5 : s'=34 & d'=12;
	[] s=34 -> s'=34;

	
endmodule

rewards "coin flips"
        [] s<34 : 1;
endrewards