//
// Tandem queue for bluemoon Prism package
// Budde 2014
//
//{-
// Stochastic continuous-time tandem queue concept:
//                       q1                     q2
// >-----(o)------> [..@@@@] >----(o)----> [....@@] >----(o)---->
// Arrival (lambda)          Server1 (mu1)          Server2 (mu2)
//
// Reference events: packages entering (or bouncing on) Queue1
// Stopping events: Queue2 becoming empty
// Rare events: packages bouncing on Queue2
//-}

ctmc

// -- Values taken from Marnix Garvels' PhD Thesis:
// -- "The splitting method in rare event simulation", p. 85.

const int c;                // Queues capacity
const double lambda = 3;	// rate(--> q1           )
const double    mu1 = 2;	// rate(    q1 --> q2    )
const double    mu2 = 6;	// rate(           q2 -->)

// -- The following values are in p. 61 of the same work:
// -- const double lambda = 1;
// -- const double    mu1 = 4;
// -- const double    mu2 = 2;

const bool _TIME_ = true;

module ContinuousTandemQueue

	q1: [0..c-1] init 0;
	q2: [0..c-1] init 1;
	arr:  [0..2] init 0;  // Arrival: (0:none) (1:lost) (2:successfull)
	lost: [0..1] init 0;  // Package loss in q2: (0:none) (1:lost)

	// {- Package arrival at first queue -}
	[] q1<c-1 -> lambda: (arr'=2) & (lost'=0) & (q1'=q1+1);
	[] q1=c-1 -> lambda: (arr'=1) & (lost'=0);
	
	// {- Passing from first to second queue -}
	[] q1>0 & q2<c-1 -> mu1: (arr'=0) & (lost'=0) & (q1'=q1-1) & (q2'=q2+1);
	[] q1>0 & q2=c-1 -> mu1: (arr'=0) & (lost'=1) & (q1'=q1-1);

	// {- Package departure from second queue -}
	[] q2>0 -> mu2: (arr'=0) & (lost'=0) & (q2'=q2-1);

endmodule


label "goal" = lost=1;
label "stop" = q2=0;
label "running" = q2!=0;
label "reference" = _TIME_;  //arr!=0;

//{-
// formula importance = q2;

// const double confidence = 0.90;
// const double precision  = 5.0E-7;
//-}