popta
observables
task1, task2, task3, task4, task5, task6, p1, p2, x1, x2, c1, c2
endobservables
const double sleep;
module scheduler
task1 : [0..3];
task2 : [0..3];
task3 : [0..3];
task4 : [0..3];
task5 : [0..3];
task6 : [0..3];
[p1_add1] task1=0 -> (task1'=1);
[p2_add1] task1=0 -> (task1'=2);
[p1_mult2] task2=0 -> (task2'=1);
[p2_mult2] task2=0 -> (task2'=2);
[p1_mult3] task3=0 & task1=3 -> (task3'=1);
[p2_mult3] task3=0 & task1=3 -> (task3'=2);
[p1_add4] task4=0 & task1=3 & task2=3 -> (task4'=1);
[p2_add4] task4=0 & task1=3 & task2=3 -> (task4'=2);
[p1_mult5] task5=0 & task3=3 -> (task5'=1);
[p2_mult5] task5=0 & task3=3 -> (task5'=2);
[p1_add6] task6=0 & task4=3 & task5=3 -> (task6'=1);
[p2_add6] task6=0 & task4=3 & task5=3 -> (task6'=2);
[p1_done] task1=1 -> (task1'=3);
[p1_done] task2=1 -> (task2'=3);
[p1_done] task3=1 -> (task3'=3);
[p1_done] task4=1 -> (task4'=3);
[p1_done] task5=1 -> (task5'=3);
[p1_done] task6=1 -> (task6'=3);
[p2_done] task1=2 -> (task1'=3);
[p2_done] task2=2 -> (task2'=3);
[p2_done] task3=2 -> (task3'=3);
[p2_done] task4=2 -> (task4'=3);
[p2_done] task5=2 -> (task5'=3);
[p2_done] task6=2 -> (task6'=3);
endmodule
module P1
p1 : [0..6];
c1 : [0..2];
sleep1 : [0..1];
x1 : clock;
invariant
(p1=0 => x1<=0) &
(p1=1 => true) &
(p1=2 => x1<=4) &
(p1=3 => x1<=4) &
(p1=4 => x1<=1) &
((p1=5 & c1=0) => x1<=2) &
((p1=5 & c1>0) => x1<=1) &
(p1=6 => x1<=0)
endinvariant
[start] p1=0 -> 0.5 : (p1'=1) & (sleep1'=0) + 0.5 : (p1'=1) & (sleep1'=1);
[p1_add1] p1=1 & sleep1=1 -> (p1'=2) & (x1'=0) & (sleep1'=0);
[p1_add4] p1=1 & sleep1=1 -> (p1'=2) & (x1'=0) & (sleep1'=0);
[p1_add6] p1=1 & sleep1=1 -> (p1'=2) & (x1'=0) & (sleep1'=0);
[p1_mult2] p1=1 & sleep1=1 -> (p1'=3) & (x1'=0) & (sleep1'=0);
[p1_mult3] p1=1 & sleep1=1 -> (p1'=3) & (x1'=0) & (sleep1'=0);
[p1_mult5] p1=1 & sleep1=1 -> (p1'=3) & (x1'=0) & (sleep1'=0);
[p1_add1] p1=1 & sleep1=0 -> (p1'=4) & (x1'=0);
[p1_add4] p1=1 & sleep1=0 -> (p1'=4) & (x1'=0);
[p1_add6] p1=1 & sleep1=0 -> (p1'=4) & (x1'=0);
[p1_mult2] p1=1 & sleep1=0 -> (p1'=5) & (x1'=0);
[p1_mult3] p1=1 & sleep1=0 -> (p1'=5) & (x1'=0);
[p1_mult5] p1=1 & sleep1=0 -> (p1'=5) & (x1'=0);
[p1] p1=2 & x1=4 -> (p1'=4) & (x1'=0);
[p1] p1=3 & x1=4 -> (p1'=5) & (x1'=0);
[p1] p1=4 & x1=1 & c1=0 -> 1/3 : (p1'=6) & (x1'=0) & (c1'=0)
+ 2/3 : (c1'=1) & (x1'=0);
[p1] p1=4 & x1=1 & c1=1 -> 1/2 : (p1'=6) & (x1'=0) & (c1'=0)
+ 1/2 : (c1'=2) & (x1'=0);
[p1] p1=4 & x1=1 & c1=2 -> (p1'=6) & (x1'=0) & (c1'=0);
[p1] p1=5 & x1=2 & c1=0 -> 1/3 : (p1'=6) & (x1'=0) & (c1'=0)
+ 2/3 : (c1'=1) & (x1'=0);
[p1] p1=5 & x1=1 & c1=1 -> 1/2 : (p1'=6) & (x1'=0) & (c1'=0)
+ 1/2 : (c1'=2) & (x1'=0);
[p1] p1=5 & x1=1 & c1=2 -> (p1'=6) & (x1'=0) & (c1'=0);
[p1_done] p1=6 -> (1-sleep) : (p1'=1) + sleep : (p1'=1) & (sleep1'=1);
endmodule
module P2
p2 : [0..3];
c2 : [0..2];
x2 : clock;
invariant
(p1=1 => true) &
((p2=1 & c2=0) => x2<=4) &
((p2=1 & c2>0)=> x2<=1) &
((p2=2 & c2=0) => x2<=6) &
((p2=2 & c2>0) => x2<=1) &
(p2=3 => x2<=0)
endinvariant
[p2_add1] (p2=0) -> (p2'=1) & (x2'=0);
[p2_add4] (p2=0) -> (p2'=1) & (x2'=0);
[p2_add6] (p2=0) -> (p2'=1) & (x2'=0);
[p2] (p2=1) & (x2=4) & (c2=0) -> 1/3 : (p2'=3) & (x2'=0) & (c2'=0) + 2/3 : (c2'=1) & (x2'=0);
[p2] (p2=1) & (x2=1) & (c2=1) -> 1/2 : (p2'=3) & (x2'=0) & (c2'=0) + 1/2 : (c2'=2) & (x2'=0);
[p2_done] (p2=1) & (x2=1) & (c2=2) -> (p2'=0) & (x2'=0) & (c2'=0);
[p2_mult2] (p2=0) -> (p2'=2) & (x2'=0);
[p2_mult3] (p2=0) -> (p2'=2) & (x2'=0);
[p2_mult5] (p2=0) -> (p2'=2) & (x2'=0);
[p2] (p2=2) & (x2=6) & (c2=0) -> 1/3 : (p2'=3) & (x2'=0) & (c2'=0) + 2/3 : (c2'=1) & (x2'=0);
[p2] (p2=2) & (x2=1) & (c2=1) -> 1/2 : (p2'=3) & (x2'=0) & (c2'=0) + 1/2 : (c2'=2) & (x2'=0);
[p2_done] (p2=2) & (x2=1) & (c2=2) -> (p2'=0) & (x2'=0) & (c2'=0);
[p2_done] (p2=3) -> (p2'=0);
endmodule
rewards "time"
true : 1;
endrewards
rewards "energy"
p1=0 & sleep1=1 : 1/1000;
p1=0 & sleep1=0 : 10/1000;
p1>0 : 90/1000;
p2=0 : 20/1000;
p2>0 : 30/1000;
endrewards
label "tasks_complete" = (task6=3);