mdp

const double lambda1 = 0.25;
const double lambda2 = 0.33;
const double lambda3 = 1.25;
const double lambda4 = 1.50;

formula todo = (job1<2?1:0) + (job2<2?1:0) + (job3<2?1:0) + (job4<2?1:0);

module jsp

	job1 : [0..2] init 1;
	job2 : [0..2] init 0;
	job3 : [0..2] init 1;
	job4 : [0..2] init 0;
	
	// 1&3 initially scheduled
	// a_ij_kl: when i (k) finishes, schedule j (l)
	[a_12_32] todo=4 & job1=1 & job3=1 -> lambda1 : (job1'=2)&(job2'=1) + lambda3 : (job3'=2)&(job2'=1);
	[a_12_34] todo=4 & job1=1 & job3=1 -> lambda1 : (job1'=2)&(job2'=1) + lambda3 : (job3'=2)&(job4'=1);
	[a_14_32] todo=4 & job1=1 & job3=1 -> lambda1 : (job1'=2)&(job4'=1) + lambda3 : (job3'=2)&(job2'=1);
	[a_14_34] todo=4 & job1=1 & job3=1 -> lambda1 : (job1'=2)&(job4'=1) + lambda3 : (job3'=2)&(job4'=1);
	
	// 1&2 scheduled (3 done, 4 next)
	[step2] todo=3 & job1=1 & job2=1 -> lambda1 : (job1'=2)&(job4'=1) + lambda2 : (job2'=2)&(job4'=1);
	// 1&4 scheduled (3 done, 2 next)
	[step2] todo=3 & job1=1 & job4=1 -> lambda1 : (job1'=2)&(job2'=1) + lambda4 : (job4'=2)&(job2'=1);
	// 3&2 scheduled (1 done, 4 next)
	[step2] todo=3 & job3=1 & job2=1 -> lambda3 : (job3'=2)&(job4'=1) + lambda2 : (job2'=2)&(job4'=1);
	// 3&4 scheduled (1 done, 2 next)
	[step2] todo=3 & job3=1 & job4=1 -> lambda3 : (job3'=2)&(job2'=1) + lambda4 : (job4'=2)&(job2'=1);

	// two scheduled
	[step3] todo=2 & job1=1 & job2=1 -> lambda1 : (job1'=2) + lambda2 : (job2'=2);
	[step3] todo=2 & job1=1 & job3=1 -> lambda1 : (job1'=2) + lambda3 : (job3'=2);
	[step3] todo=2 & job1=1 & job4=1 -> lambda1 : (job1'=2) + lambda4 : (job4'=2);
	[step3] todo=2 & job2=1 & job1=1 -> lambda2 : (job2'=2) + lambda1 : (job1'=2);
	[step3] todo=2 & job2=1 & job3=1 -> lambda2 : (job2'=2) + lambda3 : (job3'=2);
	[step3] todo=2 & job2=1 & job4=1 -> lambda2 : (job2'=2) + lambda4 : (job4'=2);
	[step3] todo=2 & job3=1 & job1=1 -> lambda3 : (job3'=2) + lambda1 : (job1'=2);
	[step3] todo=2 & job3=1 & job2=1 -> lambda3 : (job3'=2) + lambda2 : (job2'=2);
	[step3] todo=2 & job3=1 & job4=1 -> lambda3 : (job3'=2) + lambda4 : (job4'=2);
	[step3] todo=2 & job4=1 & job1=1 -> lambda4 : (job4'=2) + lambda1 : (job1'=2);
	[step3] todo=2 & job4=1 & job2=1 -> lambda4 : (job4'=2) + lambda2 : (job2'=2);
	[step3] todo=2 & job4=1 & job3=1 -> lambda4 : (job4'=2) + lambda3 : (job3'=2);

	// one scheduled
	[step4] todo=1 & job1=1 -> lambda1 : (job1'=2);
	[step4] todo=1 & job2=1 -> lambda1 : (job2'=2);
	[step4] todo=1 & job3=1 -> lambda1 : (job3'=2);
	[step4] todo=1 & job4=1 -> lambda1 : (job4'=2);
	
	// done
	[done] todo=0 -> true;
	
endmodule

label "done" = todo=0;