// polling example [IT90]
// gxn/dxp 26/01/00

ctmc

const int N=5;

const double mu= 1;
const double gamma= 200;
const double lambda= mu/N;

module server

	s : [1..5]; // station
	a : [0..1]; // action: 0=polling, 1=serving
	
	[loop1a] (s=1)&(a=0) -> gamma	: (s'=s+1);
	[loop1b] (s=1)&(a=0) -> gamma	: (a'=1);
	[serve1] (s=1)&(a=1) -> mu	: (s'=s+1)&(a'=0);
	
	[loop2a] (s=2)&(a=0) -> gamma	: (s'=s+1);
	[loop2b] (s=2)&(a=0) -> gamma	: (a'=1);
	[serve2] (s=2)&(a=1) -> mu	: (s'=s+1)&(a'=0);
	
	[loop3a] (s=3)&(a=0) -> gamma	: (s'=s+1);
	[loop3b] (s=3)&(a=0) -> gamma	: (a'=1);
	[serve3] (s=3)&(a=1) -> mu	: (s'=s+1)&(a'=0);
	
	[loop4a] (s=4)&(a=0) -> gamma	: (s'=s+1);
	[loop4b] (s=4)&(a=0) -> gamma	: (a'=1);
	[serve4] (s=4)&(a=1) -> mu	: (s'=s+1)&(a'=0);
	
	[loop5a] (s=5)&(a=0) -> gamma	: (s'=1);
	[loop5b] (s=5)&(a=0) -> gamma	: (a'=1);
	[serve5] (s=5)&(a=1) -> mu	: (s'=1)&(a'=0);
	
endmodule

module station1

	s1 : [0..1];
	
	[loop1a] (s1=0) -> 1 : (s1'=0);
	[]       (s1=0) -> lambda : (s1'=1);
	[loop1b] (s1=1) -> 1 : (s1'=1);
	[serve1] (s1=1) -> 1 : (s1'=0);
	
endmodule

// construct further stations through renaming
module station2 = station1 [s1=s2, loop1a=loop2a, loop1b=loop2b, serve1=serve2] endmodule
module station3 = station1 [s1=s3, loop1a=loop3a, loop1b=loop3b, serve1=serve3] endmodule
module station4 = station1 [s1=s4, loop1a=loop4a, loop1b=loop4b, serve1=serve4] endmodule
module station5 = station1 [s1=s5, loop1a=loop5a, loop1b=loop5b, serve1=serve5] endmodule

// cumulative rewards

rewards "waiting" // expected time the station 1 is waiting to be served
	s1=1 & !(s=1 & a=1) : 1;
endrewards

rewards "served" // expected number of times station1 is served
	[serve1] true : 1;
endrewards