```// Simple dynamic power management (DPM) model
// Based on:
// Qinru Qiu, Qing Wu and Massoud Pedram
// Stochastic modeling of a power-managed system: Construction and optimization
// Proc. International Symposium on Low Power Electronics and Design, pages 194--199, ACM Press, 1999

ctmc

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

// Service Queue (SQ)
// Stores requests which arrive into the system to be processed.

// Maximum queue size
const int q_max = 20;

// Request arrival rate
const double rate_arrive = 1/0.72; // (mean inter-arrival time is 0.72 seconds)

module SQ

// q = number of requests currently in queue
q : [0..q_max] init 0;

// A request arrives
[request] true -> rate_arrive : (q'=min(q+1,q_max));
// A request is served
[serve] q>1 -> (q'=q-1);
// Last request is served
[serve_last] q=1 -> (q'=q-1);

endmodule

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

// Service Provider (SP)
// Processes requests from service queue.
// The SP has 3 power states: sleep, idle and busy

// Rate of service (average service time = 0.008s)
const double rate_serve = 1/0.008;
// Rate of switching from sleep to idle (average transition time = 1.6s)
const double rate_s2i = 1/1.6;
// Rate of switching from idle to sleep (average transition time = 0.67s)
const double rate_i2s = 1/0.67;

module SP

// Power state of SP: 0=sleep, 1=idle, 2=busy
sp : [0..2] init 0;

// Respond to controls from power manager (PM):

// Switch from sleep state to idle state
// (in fact, if the queue is non-empty, go straight to "busy" , rather than "idle")
[sleep2idle] sp=0 & q=0 -> rate_s2i : (sp'=1);
[sleep2idle] sp=0 & q>0 -> rate_s2i : (sp'=2);
// Switch from idle state to sleep state
[idle2sleep] sp=1 -> rate_i2s : (sp'=0);

// Synchronise with service queue (SQ):

// If in the idle state, switch to busy when a request arrives in the queue
[request] sp=1  -> (sp'=2);
// If in other power states when a request arrives, do nothing
// (need to add this explicitly because otherwise SP blocks SQ from moving)
[request] sp!=1 -> (sp'=sp);

// Serve a request from the queue
[serve]      sp=2 -> rate_serve : (sp'=2);
[serve_last] sp=2 -> rate_serve : (sp'=1);

endmodule

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

// Power Manager (PM)
// Controls power state of service provider
// (this is done via synchronisation on idle2sleep/sleep2idle actions)

// Bound on queue size, above which sleep2idle command is sent
const int q_trigger;

module PM

// Send sleep2idle command to SP (when queue is of size q_trigger or greater)
[sleep2idle] q>=q_trigger -> true;

// Send idle2sleep command to SP (when queue is empty)
[idle2sleep] q=0 -> true;

endmodule

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

// Reward structures

rewards "queue_size"
true : q;
endrewards

```