// SERVICE PROVIDER
// assume SP automatically
// moves from idle to busy when ever a request arrives
// moves from busy to idle when ever a request is served

// rates of local state changes
const double sleep2idle=10/16;
const double idle2sleep=100/67;
// rate of service
const double service=1000/8; 

module SP

	sp : [0..2]; // 0 - sleep, 1 - idle,  2 - busy
	
	// SLEEP TO IDLE
	// when there is nothing in the queue go to idle
	[sleep2idle] sp=0 & q=0 -> sleep2idle : (sp'=1);
	// when there is something in the queue so start serving immediately
	[sleep2idle] sp=0 & q>0 -> sleep2idle : (sp'=2);

	// IDLE TO SLEEP
	[idle2sleep] sp=1 & q=0 -> idle2sleep : (sp'=0);

	// IDLE TO BUSY (when a request arrives)
	[request] sp=1  -> (sp'=2);
	[request] !sp=1 -> true; // need to add loop for other states
	
	// SERVE REQUESTS
	[serve] sp=2 & q>1 -> service : (sp'=2); 
	[serve] sp=2 & q=1 -> service : (sp'=1); 

endmodule