// pta model of robot moving through terrain that is divided up into a 3×2 grid
pta

module robot

	l : [0..5];
	x : clock;
	y : clock;

	invariant
	    (l=0 => x<=4)
	  & (l=1 => x<=4)
	  & (l=2 => true)
	  & (l=3 => true)
	  & (l=4 => x<=4)
	  & (l=5 => x<=4)
	endinvariant

	[east] l=0 & x>=2 -> 0.6 : (l'=1) & (x'=0) + 0.4 : (l'=0) & (x'=0);
	[south] l=0 & x>=2 & y<=8 -> 0.8 : (l'=3) & (x'=0) + 0.1 : (l'=1) & (x'=0) + 0.1 : (l'=4) & (x'=0);
	[east] l=1 & x>=2 -> 1 : (l'=2) & (x'=0);
	[south] l=1 & x>=2 & y<=8 -> 0.5 : (l'=4) & (x'=0) + 0.5 : (l'=2) & (x'=0);
	[stuck] l=2 & x>=1 -> 1 : (l'=2) & (x'=0);
	[stuck] l=3 & x>=1 -> 1 : (l'=3) & (x'=0);
	[east] l=4 & x>=2 -> 1 : (l'=5) & (x'=0);
	[west] l=4 & x>=2 -> 0.6 : (l'=3) & (x'=0) + 0.4 : (l'=4) & (x'=0);
	[north] l=5 & x>=2 & y<=8 -> 0.9 : (l'=2) & (x'=0) + 0.1 : (l'=5) & (x'=0);
	[west] l=5 & x>=2 -> 1 : (l'=4) & (x'=0);

endmodule

// atomic propositions labelling states
label "hazard" = l=1;
label "goal1" = l=5;
label "goal2" = l=2|l=3;

// reward structure
rewards "time" 
	true : 1;
endrewards