// SERVICE PROVIDER

module SP 

	sp : [0..10] init 9;
	// 0 active
	// 1 idle
	// 2 active_idlelp
	// 3 idlelp
	// 4 idlelp_active
	// 5 active_stby
	// 6 stby
	// 7 stby_active
	// 8 active_sleep
	// 9 sleep
	// 10 sleep_active
	
	// states where PM has no control (transient states)
	[tick2] sp=2  -> 0.75   : (sp'=2) + 0.25   : (sp'=3);  // active_idlelp
	[tick2] sp=4  -> 0.25   : (sp'=0) + 0.75   : (sp'=4);  // idlelp_active
	[tick2] sp=5  -> 0.995  : (sp'=5) + 0.005  : (sp'=6);  // active_stby
	[tick2] sp=7  -> 0.005  : (sp'=0) + 0.995  : (sp'=7);  // stby_active
	[tick2] sp=8  -> 0.9983 : (sp'=8) + 0.0017 : (sp'=9);  // active_sleep
	[tick2] sp=10 -> 0.0017 : (sp'=0) + 0.9983 : (sp'=10); // sleep_active

	// states where PM has control
	// goto_active
	[tick2] sp=0 & pm=0 -> sp'=0; // active
	[tick2] sp=1 & pm=0 -> sp'=0; // idle
	[tick2] sp=3 & pm=0 -> sp'=4; // idlelp
	[tick2] sp=6 & pm=0 -> sp'=7; // stby
	[tick2] sp=9 & pm=0 -> sp'=10; // sleep
	// goto_idle
	[tick2] sp=0 & pm=1 -> sp'=1; // active
	[tick2] sp=1 & pm=1 -> sp'=1; // idle
	[tick2] sp=3 & pm=1 -> sp'=3; // idlelp
	[tick2] sp=6 & pm=1 -> sp'=6; // stby
	[tick2] sp=9 & pm=1 -> sp'=9; // sleep
	// goto_idlelp
	[tick2] sp=0 & pm=2 -> sp'=2; // active
	[tick2] sp=1 & pm=2 -> sp'=2; // idle
	[tick2] sp=3 & pm=2 -> sp'=3; // idlelp
	[tick2] sp=6 & pm=2 -> sp'=6; // stby
	[tick2] sp=9 & pm=2 -> sp'=9; // sleep
	// goto_stby
	[tick2] sp=0 & pm=3 -> sp'=5; // active
	[tick2] sp=1 & pm=3 -> sp'=5; // idle
	[tick2] sp=3 & pm=3 -> sp'=5; // idlelp
	[tick2] sp=6 & pm=3 -> sp'=6; // stby
	[tick2] sp=9 & pm=3 -> sp'=9; // sleep
	// goto_sleep
	[tick2] sp=0 & pm=4 -> sp'=8; // active
	[tick2] sp=1 & pm=4 -> sp'=8; // idle
	[tick2] sp=3 & pm=4 -> sp'=8; // idlelp
	[tick2] sp=6 & pm=4 -> sp'=8; // stby
	[tick2] sp=9 & pm=4 -> sp'=9; // sleep
	  
endmodule