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

// non-deterministic since may be 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

//-------------------------------------------------------------------------------------------------
// 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 & ((u1/P1 + u2/P2 + u3/P3) <= V1);// frequency V1
formula frequency2 = !frequency3 & ((u1/P1 + u2/P2 + u3/P3) <= V2); // frequency V2
formula frequency3 = ((u1/P1 + u2/P2 + u3/P3) <= V3); // frequency V3

// WHO TO SCHEDULE
// 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(4/(T1-w1),1); // running at frequency 1 (4 units of work)
formula finish2  = min(3/(T1-w1),1); // running at frequency 2 (3 units of work)
formula finish3  = min(2/(T1-w1),1); // running at frequency 3 (2 units of work)

//-------------------------------------------------------------------------------------------------

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

// task is being performed at frequency 1
[step1] schedule & frequency1 & d1>1 ->
(1-finish1) : (d1'=d1-1) & (w1'=w1+4) & (t1'=min(t1+1,C1)) // not finished
+ finish1 : (d1'=d1-1) & (t1'=0) & (f1'=1) & (w1'=0) & (u1'=min(t1+1,C1)); // finished
[step1] schedule & frequency1 & d1=1 ->
(1-finish1) : (f1'=2)  // not finished (and error)
+ finish1 : (d1'=P1) & (t1'=0) & (f1'=0) & (w1'=0) & (u1'=C1); // finished
// task is being performed at frequency 0.75
[step1] schedule & frequency2 & d1>1 ->
(1-finish2) : (d1'=d1-1) & (w1'=w1+3) & (t1'=min(t1+1,C1)) // not finished
+ finish2 : (d1'=d1-1) & (t1'=0) & (f1'=1) & (w1'=0) & (u1'=min(t1+1,C1)); // finished
[step1] schedule & frequency2 & d1=1 ->
(1-finish2) : (f1'=2)  // not finished (and error)
+ finish2 : (d1'=P1) & (t1'=0) & (f1'=0) & (w1'=0) & (u1'=C1); // finished
// task is being performed at frequency 0.5
[step1] schedule & frequency3 & d1>1 ->
(1-finish3) : (d1'=d1-1) & (w1'=w1+2) & (t1'=min(t1+1,C1)) // not finished
+ finish3 : (d1'=d1-1) & (t1'=0) & (f1'=1) & (w1'=0) & (u1'=min(t1+1,C1)); // finished
[step1] schedule & frequency3 & d1=1 ->
(1-finish3) : (f1'=2)  // not finished (and error)
+ finish3 : (d1'=P1) & (t1'=0) & (f1'=0) & (w1'=0) & (u1'=C1); // finished
[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) & (u1'=C1);
// end of period and not finished - error
[step2] d1=1 & f1=0 -> (f1'=2);
[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) & (u1'=C1);
// end of period and not finished - error
[step3] d1=1 & f1=0 -> (f1'=2);
[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) & (u1'=C1);

endmodule

//-------------------------------------------------------------------------------------------------
// CONSTRUCT OTHER TASKS THROUGH RENAMING
d1=d2, d2=d3, d3=d1,
u1=u2, u2=u3, u3=u1,
t1=t2,
w1=w2,
f1=f2, f2=f3, f3=f1,
P1=P2, P2=P3, P3=P1,
C1=C2, C2=C3, C3=C1,
T1=T2,
step1=step2, step2=step3, step3=step1 ]

endmodule
d1=d3, d2=d1, d3=d2,
u1=u3, u2=u1, u3=u2,
t1=t3,
w1=w3,
f1=f3, f2=f1, f3=f2,
P1=P3, P2=P1, P3=P2,
C1=C3, C2=C1, C3=C2,
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
```