// 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; 

module SP
	
	// Power state of SP: 0=sleep, 1=idle, 2=busy
	sp : [0..2] init 1;
	
	// 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

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

// Reward structures

rewards "queue_size"
	true : q;
endrewards