You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
58 lines
2.6 KiB
58 lines
2.6 KiB
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;
|