MC-ProbMC-PrismFiles/task_scheduling.prism

mdp

const int MULT_DUR_1 = 8;
const int ADD_DUR_1  = 4;
const double P1_SUCCESS = 1.0;
const int MULT_DUR_2 = 3;
const int ADD_DUR_2  = 3;
const double P2_SUCCESS = 0.8;

// target state (all tasks complete)
label "tasks_complete" = (task6=3);
label "no_P1_mult" =  (mult_tick_1=0);
label "no_P2_mult" =  (mult_tick_2=0);

// reward structure: elapsed time
rewards "time"
  task6!=3 : 1;
endrewards

// reward structures: energy consumption
rewards "energy"
  p1=0 : 10/1000;  // processor 1 idle
  p1>0 : 100/1000;  // processor 1 working
  p2=0 : 10/1000;  // processor 2 idle
  p2>0 : 100/1000;  // processor 2 working
endrewards

module scheduler

//┌t1─┐   ┌t3─────┐   ┌t5───────┐
//│A+B│-->│Cx(A+B)│-->│DxCx(A+B)│--.     ┌t6─────────────────────┐
//└───┘\  └───────┘   └─────────┘   \___\│DxCx(A+B)+((A+B)+(CxD))│
//┌t2─┐ \ ┌t4─────────┐             /   /└───────────────────────┘
//│CxD│-->│(A+B)+(CxD)│------------°
//└───┘   └───────────┘

task1 : [0..3]; // A+B, add
task2 : [0..3]; // CxD, mult
task3 : [0..3]; // Cx(A+B), mult
task4 : [0..3]; // (A+B)+(CxD), add
task5 : [0..3]; // DxCx(A+B), mult
task6 : [0..3]; // (DxCx(A+B)) + ((A+B)+(CxD)), add

p1_idle : bool init true;
p2_idle : bool init true;

// task status:
// 0 - not started
// 1 - running on processor 1
// 2 - running on processor 2
// 3 - task complete

// start task 1
[t1p1] task1=0 & p1_idle-> (task1'=1) & (p1_idle'=false);
[t1p2] task1=0 & p2_idle-> (task1'=2) & (p2_idle'=false);

// start task 2
[t2p1] task2=0 & p1_idle-> (task2'=1) & (p1_idle'=false);
[t2p2] task2=0 & p2_idle-> (task2'=2) & (p2_idle'=false);

// start task 3 (must wait for task 1 to complete)
[t3p1] task3=0 & task1=3 & p1_idle-> (task3'=1) & (p1_idle'=false);
[t3p2] task3=0 & task1=3 & p2_idle-> (task3'=2) & (p2_idle'=false);

// start task 4 (must wait for tasks 1 and 2 to complete)
[t4p1] task4=0 & task1=3 & task2=3 & p1_idle-> (task4'=1) & (p1_idle'=false);
[t4p2] task4=0 & task1=3 & task2=3 & p2_idle-> (task4'=2) & (p2_idle'=false);

// start task 5 (must wait for task 3 to complete)
[t5p1] task5=0 & task3=3 & p1_idle-> (task5'=1) & (p1_idle'=false);
[t5p2] task5=0 & task3=3 & p2_idle-> (task5'=2) & (p2_idle'=false);

// start task 6 (must wait for tasks 4 and 5 to complete)
[t6p1] task6=0 & task4=3 & task5=3 & p1_idle -> (task6'=1) & (p1_idle'=false);
[t6p2] task6=0 & task4=3 & task5=3 & p2_idle -> (task6'=2) & (p2_idle'=false);

// a task finishes on processor 1
[p1_done] task1=1 & p1=3 -> (task1'=3) & (p1_idle'=true);
[p1_done] task2=1 & p1=3 -> (task2'=3) & (p1_idle'=true);
[p1_done] task3=1 & p1=3 -> (task3'=3) & (p1_idle'=true);
[p1_done] task4=1 & p1=3 -> (task4'=3) & (p1_idle'=true);
[p1_done] task5=1 & p1=3 -> (task5'=3) & (p1_idle'=true);
[p1_done] task6=1 & p1=3 -> (task6'=3) & (p1_idle'=true);

// a task finishes on processor 2
[p2_done] task1=2 & p2=3 -> (task1'=3) & (p2_idle'=true);
[p2_done] task2=2 & p2=3 -> (task2'=3) & (p2_idle'=true);
[p2_done] task3=2 & p2=3 -> (task3'=3) & (p2_idle'=true);
[p2_done] task4=2 & p2=3 -> (task4'=3) & (p2_idle'=true);
[p2_done] task5=2 & p2=3 -> (task5'=3) & (p2_idle'=true);
[p2_done] task6=2 & p2=3 -> (task6'=3) & (p2_idle'=true);

[] task6=3 -> 1 : true;
[] task6=3 -> 1 : true;

endmodule

// processor 1
module P1
  p1 : [0..3]; // 0 inactive, 1 - adding, 2 - multiplying, 3 - done
  mult_tick_1 : ;
  add_tick_1  : ;

  [p1_done] p1=3 -> 1: (p1'=0) & (mult_tick_1'=0) & (add_tick_1'=0);  // finished task

endmodule

// processor 2
// Note: You may also use module renaming to define processor 2
module P2
	p2 : [0..3]; // 0 inactive, 1 - adding, 2 - multiplying, 3 - done
  mult_tick_2 : ;
  add_tick_2  : ;


	[p2_done] p2=3 -> 1: (p2'=0) & (mult_tick_2'=0) & (add_tick_2'=0);  // finished task

endmodule