```// MODEL OF REAL TIME DYNAMIC VOLTAGE SCALING SYSTEM
// static edf scheduler (chooses job with the most immediate deadline)
// gxn/dxp 11/11/03

// non-deterministic (may have cases when two or more jobs have the same deadline)
mdp

//-------------------------------------------------------------------------------------------------
// FREQUENCIES (assume Vi greater than Vj if i<j)
const double V1 = 1;   // corresponding voltage is 5
const double V2 = 3/4; // corresponding voltage is 4
const double V3 = 1/2; // corresponding voltage is 3

//-------------------------------------------------------------------------------------------------
// DISCRETISE TIME
// choose a division of one time unit (one time step) such that to finish on WCET
// is an integer when the task is run on any of the frequencies
// (e.g. WCET at frequency 3/4 is now WCET*4/3 time steps)
const int N=3;
// rescale units of work such that in one step an integer amount of work is done
// since depending on the frequency the work in one time unit is 1, 3/4 or 1/2
// we scale by 4 to get integer values
const int K=4;
// for frequencies V1, V2 and V3 in one time unit we now do 4,3 or 2 units of work respectively

//-------------------------------------------------------------------------------------------------
// CONSTANTS OF THE SYSTEM (assume task deadline equals the period)
// scaled by the chosen discrete time step
const int P1=8*N; // period of the first task
const int C1=3*N; // worst case execution time of the first task
const int T1=3*(K*N); // worst case execution time of the first task (scaled by units of work)

const int P2=10*N; // period of the second task
const int C2=3*N;  // worst case execution time of the second task
const int T2=3*(K*N); // worst case execution time of the second task (scaled by units of work)

const int P3=14*N; // period of the third task
const int C3=1*N;  // worst case execution time of the third task
const int T3=1*(K*N); // worst case execution time of the third task (scaled by units of work)

//-------------------------------------------------------------------------------------------------
// WHEN TO CHOOSE WHAT FREQUENCY
// fi=0 means that process i has not finished in its current period
formula frequency1 = !frequency2 & !frequency3 & ((C1/P1 + C2/P2 + C3/P3) <= V1); // frequency V1
formula frequency2 = !frequency3 & ((C1/P1 + C2/P2 + C3/P3) <= V2); // frequency V2
formula frequency3 = ((C1/P1 + C2/P2 + C3/P3) <= V3); // frequency V3

// WHO TO SCHEDULE
// task with nearest deadline (fi=0 if task i has not finished)
// (only consider task1 get remaining formulae through renaming)
formula schedule   = f1=0 & (!f2=0 | (d1<=d2)) & (!f3=0 | (d1<=d3)); // schedule task1
formula noschedule = f1=1 & f2=1 & f3=1; // schedule nothing

// probabilities of finishing in one time step (uniformly distributed)
// only consider task1 get remaining probabilities through renaming
formula finish1  = min(V1*K/(T1-t1),1); // running at frequency 1 (do 4 units of work)
formula finish2  = min(V2*K/(T1-t1),1); // running at frequency 2 (do 3 units of work)
formula finish3  = min(V3*K/(T1-t1),1); // running at frequency 3 (do 2 units of work)

//-------------------------------------------------------------------------------------------------
// MODULE FOR FIRST TASK

d1 : [1..P1] init P1; // time until next period
t1 : [0..T1] init 0; // work done (time spent running scaled by the frequency)
f1 : [0..2]  init 0; // state of task in current period
// 0 - not finished
// 1 - finished
// 2 - error: not finished and period over

// TASK BEING PERFORMED (cost is the voltage squared)
// task is being performed at frequency 1
[step1] schedule & frequency1 & d1>1 ->
(1-finish1) : (d1'=d1-1) & (t1'=t1+4) // not finished
+ finish1 : (d1'=d1-1) & (f1'=1) & (t1'=0); // finished
[step1] schedule & frequency1 & d1=1 ->
(1-finish1) : (f1'=2)  // not finished (and error)
+ finish1 : (d1'=P1) & (f1'=0) & (t1'=0); // finished
// task is being performed at frequency 0.75
[step1] schedule & frequency2 & d1>1 ->
(1-finish2) : (d1'=d1-1) & (t1'=t1+3) // not finished
+ finish2 : (d1'=d1-1) & (f1'=1) & (t1'=0); // finished
[step1] schedule & frequency2 & d1=1 ->
(1-finish2) : (f1'=2)  // not finished (and error)
+ finish2 : (d1'=P1) & (f1'=0) & (t1'=0); // finished
// task is being performed at frequency 0.5
[step1] schedule & frequency3 & d1>1 ->
(1-finish3) : (d1'=d1-1) & (t1'=t1+2) // not finished
+ finish3 : (d1'=d1-1) & (f1'=1) & (t1'=0); // finished
[step1] schedule & frequency3 & d1=1 ->
(1-finish3) : (f1'=2)  // not finished (and error)
+ finish3 : (d1'=P1) & (f1'=0) & (t1'=0); // finished

// TASK NOT BEING PERFORMED (DEADLINE STILL CHANGES) - task 2 is running
// deadline goes down
[step2] d1>1 -> (d1'=d1-1);
// end of period and finished task - move to next period
[step2] d1=1 & f1=1 -> (d1'=P1) & (f1'=0);
// end of period and not finished - error
[step2] d1=1 & f1=0 -> (f1'=2);
// TASK NOT BEING PERFORMED (DEADLINE STILL CHANGES) - task 3 is running
// deadline goes down
[step3] d1>1 -> (d1'=d1-1);
// end of period and finished task - move to next period
[step3] d1=1 & f1=1 -> (d1'=P1) & (f1'=0);
// end of period and not finished - error
[step3] d1=1 & f1=0 -> (f1'=2);
// TASK NOT BEING PERFORMED (DEADLINE STILL CHANGES) - no task is running
// deadline goes down
[step] noschedule & d1>1 -> (d1'=d1-1);
// end of period and finished task - move to next period
[step] noschedule & d1=1 -> (d1'=P1) & (f1'=0);

endmodule

//-------------------------------------------------------------------------------------------------
// CONSTRUCT OTHER TASKS THROUGH RENAMING

d1=d2, d2=d3, d3=d1,
t1=t2,
f1=f2, f2=f3, f3=f1,
P1=P2, P2=P3, P3=P1,
T1=T2,
step1=step2, step2=step3, step3=step1 ]

endmodule

d1=d3, d2=d1, d3=d2,
t1=t3,
f1=f3, f2=f1, f3=f2,
P1=P3, P2=P1, P3=P2,
T1=T3,
step1=step3, step2=step1, step3=step2 ]

endmodule

//-------------------------------------------------------------------------------------------------
// REWARDS - related to power consumption (equals square of current voltage)

rewards "power"

// task performed at frequency 1 (voltage is 5)
[step1] frequency1 & !noschedule : 25;
[step2] frequency1 & !noschedule : 25;
[step3] frequency1 & !noschedule : 25;
// task performed at frequency 3 (voltage is 4)
[step1] frequency2 & !noschedule : 16;
[step2] frequency2 & !noschedule : 16;
[step3] frequency2 & !noschedule : 16;
// task performed at frequency 3 (voltage is 3)
[step1] frequency3 & !noschedule : 9;
[step2] frequency3 & !noschedule : 9;
[step3] frequency3 & !noschedule : 9;

endrewards
```