smg

player p1 
	[lane], [honk], [brake] 
endplayer
player p2 
	[jam], [ped] 
endplayer
player p3
	[pr]
endplayer

module M
	s : [0..13] init 0;

	[pr] s=0 -> 0.2 : (s'=1) + 0.3 : (s'=2) + 0.3 : (s'=3) + 0.2 : (s'=10);

	[jam] s=1 -> (s'=2);
	[ped] s=1 -> (s'=3);

	[lane] s=2 -> (s'=4);
	[honk] s=2 -> (s'=5);
	[brake] s=2 -> (s'=6);

	[pr] s=4 -> 0.8 : (s'=0) + 0.2 : (s'=12);
	[pr] s=5 -> 0.95 : (s'=0) + 0.05 : (s'=11);
	[pr] s=6 -> 0.98 : (s'=0) + 0.02 : (s'=11);

	[lane] s=3 -> (s'=7);
	[honk] s=3 -> (s'=8);
	[brake] s=3 -> (s'=9);

	[pr] s=7 -> 0.93 : (s'=0) + 0.07 : (s'=11);
	[pr] s=8 -> 0.95 : (s'=0) + 0.05 : (s'=11);
	[pr] s=9 -> 0.8 : (s'=0) + 0.16 : (s'=3) + 0.04 : (s'=11);

        [pr] s=10 -> (s'=13);  
	[pr] s=11 -> (s'=13); 
	[pr] s=12 -> (s'=12);
	[pr] s=13 -> (s'=13);

endmodule

label "succ" = s=10; 
label "coll" = s=11; 
label "viol" = s=12; 

rewards "energy"

	[lane] s=2 : 3 ;
	[honk] s=2 : 1;
	[brake] s=2 : 2;

        [lane] s=3 : 3;
        [honk] s=3 : 1;
	[brake] s=3 : 2;

endrewards

rewards "time"

	[lane] s=2 : 1;
	[honk] s=2 : 2;
	[brake] s=2 : 1;

        [lane] s=3 : 1;
        [honk] s=3 : 1;
	[brake] s=3 : 3;

endrewards

rewards "success"

	[pr] s=10 : 1;

endrewards

rewards "collision"

	[pr] s=11 : 1;

endrewards