sp
11 months ago
2 changed files with 158 additions and 0 deletions
@ -0,0 +1,40 @@ |
|||
mdp |
|||
|
|||
const int lanes = 5; // Counting the sidewalks as lanes |
|||
const int streetLength = 20; |
|||
|
|||
const int maxVelocity = 3; |
|||
const int minVelocity = 1; |
|||
|
|||
const int pedMove = 0; |
|||
const int car1Move = 1; |
|||
const int car1LaneInit = 2; |
|||
const double probCrossStreet = 0.2; |
|||
|
|||
global move : [0..1] init 0; |
|||
|
|||
formula ped_at_edge = ped_street_pos = 1 | ped_street_pos = streetLength; |
|||
|
|||
formula car_at_end = car_street_pos = streetLength; |
|||
|
|||
formula crash = (car_street_pos =ped_street_pos&car_lane_pos =ped_lane_pos); |
|||
label "crashed" = crash; |
|||
label "maxedOut" = velocity=maxVelocity; |
|||
|
|||
module car |
|||
|
|||
car_street_pos : [0..streetLength]; |
|||
car_lane_pos : [2..lanes-1] init car1LaneInit; |
|||
velocity : [minVelocity..maxVelocity]; |
|||
|
|||
|
|||
endmodule |
|||
|
|||
|
|||
module pedestrian |
|||
|
|||
ped_street_pos : [0..streetLength] init floor(streetLength/2); |
|||
ped_lane_pos : [1..lanes] init 1; |
|||
|
|||
|
|||
endmodule |
@ -0,0 +1,118 @@ |
|||
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 |
Write
Preview
Loading…
Cancel
Save
Reference in new issue