//
// Queue with On-Off Sources (ATM model)
// D'Argenio & Budde, 2015
//
//{-
// Concept of the queue with breakdowns (Glasserman version):
//                        
// (Source1: on/off) --->||
//                       ||
// (Source2: on/off) --->||
//         .             ||        Buffer
//         .             ||---> [·····###]--(Server)---->
//         .             ||
// (SourceN: on/off) --->||
//                        
// Buffer has maximum capacity 'b'.
// The single Server processes with rate mu,
// Sources : produce       with rate lambda,
//           fail          with rate alpha1,
//           get repaired  with rate alpha0.
//
// Initial state: the buffer is empty, the server is down,
//                and a steady-state average # of sources is on.
// Stopping event: return to the initial state.
// Rare event: buffer reaching maximum capacity.
//-}

ctmc

// -- The following values were extracted from Glasserman, Heidelberger,
// -- Shahabuddin, and Zajic:
// -- "Multilevel Splitting For Estimating Rare Event Probabilities",
// -- Operations Research, Vol. 47, No. 4, July–August 1999, pp. 585–600

// -- Buffer capacity
const int b = 40;       // -- Capacity
const double u = 0.25;  // -- Overall utilization

// -- Server
const double mu = 10;

// -- Sources
const int N = 20;
const double lambda;
// -- Possible values for lambda:  0.5  4.0
const double alpha0 = 1;
const double alpha1 = (alpha0*N*lambda) / (u*mu) - alpha0;
// -- Possible values for alpha1: 3 if lambda=0.5, 31 if lambda=4
const int srcInitOn = floor( N * alpha0 / (alpha0+alpha1) );
// -- Possible values for srcInitOn: 5 if lambda=0.5, 0 if lambda=4 


module ATM

	// -- Initializations
	lost:  bool init false;
	reset: bool init false;
	buf: [0..b] init 0;          // -- Buffer
	src: [0..N] init srcInitOn;  // -- Sources

	// -- Sources failure and recovery
	[] src>0 & ((src!=srcInitOn+1) | (buf!=0)) -> (src * alpha1)     : (src'=src-1);
	[] src>0 &  (src =srcInitOn+1) & (buf =0)  -> (src * alpha1)     : (reset'=true);
	[] src<N & ((src!=srcInitOn-1) | (buf!=0)) -> ((N-src) * alpha0) : (src'=src+1);
	[] src<N &  (src =srcInitOn-1) & (buf =0)  -> ((N-src) * alpha0) : (reset'=true);

	// -- Buffer in
	[] src>0 & buf<b-1 -> (src * lambda) : (buf'=buf+1);
	[] src>0 & buf=b-1 -> (src * lambda) : (lost'=true);

	// -- Buffer out
	[] buf>1                  -> mu : (buf'=buf-1);
	[] buf=1 & src!=srcInitOn -> mu : (buf'=buf-1);
	[] buf=1 & src =srcInitOn -> mu : (reset'=true);

endmodule


label "goal" = lost;
label "stop" = reset;
label "running" = !reset;