mdp

module M

	// t=0,1,2 for t_0,t_1,t_2
	// t=3 for s_{1} and t=4 for s_{2}
	t : [0..4];

	[b2] t=0 -> 0.5:(t'=0) + 0.5:(t'=2);
	[b1] t=0 -> (t'=1);
	[b1] t=1 -> (t'=1);
	[b2] t=2 -> (t'=0);
	
	[a2] t=0 -> (t'=4);
	[a1] t=1 -> (t'=3);
	[a2] t=0 -> (t'=4);

endmodule

label "T1" = t=3;
label "T2" = t=4;