mdp

// Probability of fast job failing
const double p_fail = 0.1;

// Number of jobs
const int jmax = 2;

// Machine
module M_m

	j : [0..jmax];
	on : bool init true;
	
	[fast] on & j<jmax -> p_fail:(j'=j) + (1-p_fail):(j'=j+1);
	[slow] on & j<jmax -> (j'=j+1);
	[off] on & j<jmax -> (on'=false);
	[on] !on & j<jmax -> (on'=true);
	[done] j=jmax -> true;
	
endmodule

// Automaton for G!off
label "A1_K" = a1=1;
module A1

	a1 : [0..1] init 0;
	
	[off] true -> (a1'=1);

endmodule

// Reward structures

rewards "fast"
	[fast] true : 1;
endrewards

rewards "slow"
	[slow] true : 1;
endrewards

rewards "time"
	[fast] true : 1;
	[slow] true : 3;
endrewards