```// turn based probabilistic timed game model of the task graph 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

tptg

// scheduler
player sched
endplayer

// environment
player env
P1, P2, [p1_done], [p2_done]
endplayer

module scheduler

turn : [0..1]; 	// use to classify player 1 and player 2 states

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

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

y : clock; // local clock

invariant
// cannot let time pass if a task is scheduled
// as must pass over control to the environment
((turn=0 & ((p1>1 | p2>1)|(task6!=3))) => y<=0)
endinvariant

// finished scheduling and hand control over to the environment
[] turn=0 -> (turn'=1);

// 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
// and the scheduler takes over control

// a task finishes on processor 2
// and the scheduler takes over control

endmodule

// processor 1
module P1

p1 : [0..2];
// 0 - idle
// 2 - multiply

x1 : clock; // local clock

invariant
(p1=1 => x1<=2) &
(p1=2 => x1<=3)
endinvariant

[p1_add] p1=0 -> (p1'=1) & (x1'=0); // start
[p1_done] turn=1 & p1=1 & x1<=2 -> (p1'=0) & (x1'=0); // finish

// multiplication
[p1_mult] p1=0 -> (p1'=2) & (x1'=0); // start
[p1_done] turn=1 & p1=2 & x1<=3 -> (p1'=0) & (x1'=0);  // finish

endmodule

// processor 2
module P2

p2 : [0..2];
// 0 - idle
// 2 - multiply

x2 : clock; // local clock

invariant
(p2=1 => x2<=5) &
(p2=2 => x2<=7)
endinvariant

[p2_add] p2=0 -> (p2'=1) & (x2'=0); // start
[p2_done] turn=1 & p2=1 & x2<=5 -> (p2'=0) & (x2'=0); // finish

// multiplication
[p2_mult] p2=0 -> (p2'=2) & (x2'=0); // start
[p2_done] turn=1 & p2=2 & x2<=7 -> (p2'=0) & (x2'=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)