```// 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

task6 : [0..3]; // (DxCx(A+B)) + ((A+B)+(CxD))

// 0 - not started
// 1 - running on processor 1
// 2 - running on processor 2

// start task 4 (must wait for tasks 1 and 2 to complete)

// start task 6 (must wait for tasks 4 and 5 to complete)

// a task finishes on processor 1

// a task finishes on processor 2

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

[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

[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)