// task graph model with random execution times // extends the task graph problem from // Bouyer, Fahrenberg, Larsen and Markey // Quantitative analysis of real-time systems using priced timed automata // Communications of the ACM, 54(9):78–87, 2011 pta // model is a PTA module scheduler task1 : [0..3]; // A+B task2 : [0..3]; // CxD task3 : [0..3]; // Cx(A+B) task4 : [0..3]; // (A+B)+(CxD) task5 : [0..3]; // DxCx(A+B) task6 : [0..3]; // (DxCx(A+B)) + ((A+B)+(CxD)) // task status: // 0 - not started // 1 - running on processor 1 // 2 - running on processor 2 // 3 - task complete // start task 1 [p1_add] task1=0 -> (task1'=1); [p2_add] task1=0 -> (task1'=2); // start task 2 [p1_mult] task2=0 -> (task2'=1); [p2_mult] task2=0 -> (task2'=2); // start task 3 (must wait for task 1 to complete) [p1_mult] task3=0 & task1=3 -> (task3'=1); [p2_mult] task3=0 & task1=3 -> (task3'=2); // start task 4 (must wait for tasks 1 and 2 to complete) [p1_add] task4=0 & task1=3 & task2=3 -> (task4'=1); [p2_add] task4=0 & task1=3 & task2=3 -> (task4'=2); // start task 5 (must wait for task 3 to complete) [p1_mult] task5=0 & task3=3 -> (task5'=1); [p2_mult] task5=0 & task3=3 -> (task5'=2); // start task 6 (must wait for tasks 4 and 5 to complete) [p1_add] task6=0 & task4=3 & task5=3 -> (task6'=1); [p2_add] task6=0 & task4=3 & task5=3 -> (task6'=2); // a task finishes on processor 1 [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); // a task finishes on processor 2 [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 // processor 1 module P1 p1 : [0..3]; // 0 inactive, 1 - adding, 2 - multiplying, 3 - done c1 : [0..2]; // used for the uniform probabilistic choice of execution time x1 : clock; // local clock invariant (p1=1 => x1<=1) & ((p1=2 & c1=0) => x1<=2) & ((p1=2 & c1>0)=> x1<=1) & (p1=3 => x1<=0) endinvariant // addition [p1_add] p1=0 -> (p1'=1) & (x1'=0); // start [] p1=1 & x1=1 & c1=0 -> 1/3 : (p1'=3) & (x1'=0) & (c1'=0) + 2/3 : (c1'=1) & (x1'=0); // k-1 [] p1=1 & x1=1 & c1=1 -> 1/2 : (p1'=3) & (x1'=0) & (c1'=0) + 1/2 : (c1'=2) & (x1'=0); // k [p1_done] p1=1 & x1=1 & c1=2 -> (p1'=0) & (x1'=0) & (c1'=0); // k+1 // multiplication [p1_mult] p1=0 -> (p1'=2) & (x1'=0); // start [] p1=2 & x1=2 & c1=0 -> 1/3 : (p1'=3) & (x1'=0) & (c1'=0) + 2/3 : (c1'=1) & (x1'=0); // k-1 [] p1=2 & x1=1 & c1=1 -> 1/2 : (p1'=3) & (x1'=0) & (c1'=0) + 1/2 : (c1'=2) & (x1'=0); // k [p1_done] p1=2 & x1=1 & c1=2 -> (p1'=0) & (x1'=0) & (c1'=0); // k+1 [p1_done] p1=3 -> (p1'=0); // finish endmodule // processor 2 module P2 p2 : [0..3]; // 0 inactive, 1 - adding, 2 - multiplying, 3 - done c2 : [0..2]; // used for the uniform probabilistic choice of execution time x2 : clock; // local clock invariant ((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 // addition [p2_add] p2=0 -> (p2'=1) & (x2'=0); // start [] p2=1 & x2=4 & c2=0 -> 1/3 : (p2'=3) & (x2'=0) & (c2'=0) + 2/3 : (c2'=1) & (x2'=0); // k-1 [] p2=1 & x2=1 & c2=1 -> 1/2 : (p2'=3) & (x2'=0) & (c2'=0) + 1/2 : (c2'=2) & (x2'=0); // k [p2_done] p2=1 & x2=1 & c2=2 -> (p2'=0) & (x2'=0) & (c2'=0); // k+1 // multiplication [p2_mult] p2=0 -> (p2'=2) & (x2'=0); // start [] p2=2 & x2=6 & c2=0 -> 1/3 : (p2'=3) & (x2'=0) & (c2'=0) + 2/3 : (c2'=1) & (x2'=0); // k-1 [] p2=2 & x2=1 & c2=1 -> 1/2 : (p2'=3) & (x2'=0) & (c2'=0) + 1/2 : (c2'=2) & (x2'=0); // k [p2_done] p2=2 & x2=1 & c2=2 -> (p2'=0) & (x2'=0) & (c2'=0); // k+1 [p2_done] p2=3 -> (p2'=0); // finish endmodule // reward structure: elapsed time rewards "time" true : 1; endrewards // reward structures: energy consumption rewards "energy" p1=0 : 10/1000; p1>0 : 90/1000; p2=0 : 20/1000; p2>0 : 30/1000; endrewards // target state (all tasks complete) label "tasks_complete" = (task6=3);