tir_arc.prism

dtmc
const int k;

module Dmitry
	scoreD: [0..3];
	pretD : bool;
	nbTirsD : [0..100] init 0;
	[initD] pretD=false & nbTirsD < 100 -> (pretD'=true);
	[tirD] pretD=true & nbTirsD < 100 -> 1/10 : (scoreD'=3) & (pretD'=false) & (nbTirsD'=nbTirsD+1) + 
				1/6 : (scoreD'=2) & (pretD'=false) & (nbTirsD'=nbTirsD+1) + 
				1/4 : (scoreD'=1) & (pretD'=false) & (nbTirsD'=nbTirsD+1) + 
				(1-(1/10+1/6+1/4)) : (scoreD'=0) & (pretD'=false) & (nbTirsD'=nbTirsD+1) ;
endmodule

rewards
	[initD] true : scoreD;
	[initH] true : scoreH;
endrewards