//
// Tandem queue for bluemoon Prism package
// Budde 2014
//
// {-
// Stochastic discrete-time tandem queue concept:
//                       q1                     q2
// >-----(o)------> [..@@@@] >----(o)----> [....@@] >----(o)---->
// Arrival (lambda)          Server1 (mu1)          Server2 (mu2)
//
// Reference events: packages entering (or bouncing on) Queue1
// Rare events: packages bouncing on Queue2
//
//
// Compositional overview of the model:
//
// Arrival:
// 	[tick] q1=c -> lambda: {bounce} + (1-lambda): {};
// 	[tick] q1<c -> lambda: {q1++}   + (1-lambda): {};
// Server1:
// 	[tick] q1=0 -> {};
// 	[tick] q1>0 & q2<c -> mu1: {q1--,q2++}   + (1-mu1): {};
// 	[tick] q1>0 & q2=c -> mu1: {q1--,bounce} + (1-mu1): {};
// Server2:
// 	[tick] q2=0 -> {};
// 	[tick] q2>0 -> mu2: {q2-- } + (1-mu2): {};
//
//
// Pseudo-PRISM version of the compositional overview:
//
// dtmc
// global q1 [0..c] init 0;
// global q2 [0..c] init 0;
// module Arrival
//  lost1 [0..1] init 0;
// 	[tick] q1=c -> lambda: lost1'=1              + (1-lambda): lost1'=0;
// 	[tick] q1<c -> lambda: (q1'=q1+1)&(lost1'=0) + (1-lambda): lost1'=0;
// endmodule
// module Server1
//  lost2 [0..1] init 0;
// 	[tick] q1=0 -> lost2'=0;
// 	[tick] q1>0 & q2<c ->   (mu1): (q1'=q1-1) & (q2'=q2+1) & (lost2'=0)
//                      + (1-mu1): lost2'=0;
// 	[tick] q1>0 & q2=c ->   (mu1): (q1'=q1-1) & (lost2'=1)
//                      + (1-mu1): lost2'=0;
// endmodule
// module Server2
// 	[tick] q2=0 -> true;
// 	[tick] q2>0 -> mu2: (q2'=q2-1) + (1-mu2): true;
// endmodule
// -}


dtmc

const int c;                //{-  Queues capacity          -}
const double lambda = 0.1;  //{-  Prob(--> q1           )  -}
const double mu1 = 0.14;    //{-  Prob(    q1 --> q2    )  -}
const double mu2 = 0.19;    //{-  Prob(           q2 -->)  -}
const bool _TIME_ = true;

module DiscreteTandemQueue

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

	[] (q1=0) & (q2=0)
		-> (lambda): (q1'=q1+1) & (arr1'=2) & (lost2'=0)
		 + (1-lambda): (arr1'=0) & (lost2'=0);

	[] (0<q1 & q1<c) & (q2=0)
		-> (lambda*mu1): (q2'=q2+1) & (arr1'=2) & (lost2'=0)
		 + (lambda*(1-mu1)): (q1'=q1+1) & (arr1'=2) & (lost2'=0)
		 + (mu1*(1-lambda)): (q1'=q1-1) & (q2'=q2+1) & (arr1'=0) & (lost2'=0)
		 + ((1-lambda)*(1-mu1)): (arr1'=0) & (lost2'=0);

	[] (q1=c) & (q2=0)
		-> (lambda*mu1): (q2'=q2+1) & (arr1'=2) & (lost2'=0)
		 + (lambda*(1-mu1)): (arr1'=1) & (lost2'=0)
		 + ((1-lambda)*mu1): (q1'=q1-1) & (q2'=q2+1) & (arr1'=0) & (lost2'=0)
		 + ((1-lambda)*(1-mu1)): (arr1'=0) & (lost2'=0);

	[] (q1=0) & (0<q2)
		-> (lambda*mu2): (q1'=q1+1) & (q2'=q2-1) & (arr1'=2) & (lost2'=0)
		 + (lambda*(1-mu2)): (q1'=q1+1) & (arr1'=2) & (lost2'=0)
		 + ((1-lambda)*mu2): (q2'=q2-1) & (arr1'=0) & (lost2'=0)
		 + ((1-lambda)*(1-mu2)): (arr1'=0) & (lost2'=0);
	
	[] (0<q1 & q1<c) & (0<q2 & q2<c)
		-> (lambda*mu1*mu2): (arr1'=2) & (lost2'=0)
		 + (lambda*mu1*(1-mu2)): (q2'=q2+1) & (arr1'=2) & (lost2'=0)
		 + (lambda*(1-mu1)*mu2): (q1'=q1+1) & (q2'=q2-1) & (arr1'=2) & (lost2'=0)
		 + (lambda*(1-mu1)*(1-mu2)): (q1'=q1+1) & (arr1'=2) & (lost2'=0)
		 + ((1-lambda)*mu1*mu2): (q1'=q1-1) & (arr1'=0) & (lost2'=0)
		 + ((1-lambda)*mu1*(1-mu2)): (q1'=q1-1) & (q2'=q2+1) & (arr1'=0) & (lost2'=0)
		 + ((1-lambda)*(1-mu1)*mu2): (q2'=q2-1) & (arr1'=0) & (lost2'=0)
		 + ((1-lambda)*(1-mu1)*(1-mu2)): (arr1'=0) & (lost2'=0);

	[] (q1=c) & (0<q2 & q2<c)
		-> (lambda*mu1*mu2): (arr1'=2) & (lost2'=0)
		 + (lambda*mu1*(1-mu2)): (q2'=q2+1) & (arr1'=2) & (lost2'=0)
		 + (lambda*(1-mu1)*mu2): (q2'=q2-1) & (arr1'=1) & (lost2'=0)
		 + (lambda*(1-mu1)*(1-mu2)): (arr1'=1) & (lost2'=0)
		 + ((1-lambda)*mu1*mu2): (q1'=q1-1) & (arr1'=0) & (lost2'=0)
		 + ((1-lambda)*mu1*(1-mu2)): (q1'=q1-1) & (q2'=q2+1) & (arr1'=0) & (lost2'=0)
		 + ((1-lambda)*(1-mu1)*mu2): (q2'=q2-1) & (arr1'=0) & (lost2'=0)
		 + ((1-lambda)*(1-mu1)*(1-mu2)): (arr1'=0) & (lost2'=0);

	[] (0<q1 & q1<c) & (q2=c)
		-> (lambda*mu1*mu2): (arr1'=2) & (lost2'=0)
		 + (lambda*mu1*(1-mu2)): (arr1'=2) & (lost2'=1)
		 + (lambda*(1-mu1)*mu2): (q1'=q1+1) & (q2'=q2-1) & (arr1'=2) & (lost2'=0)
		 + (lambda*(1-mu1)*(1-mu2)): (q1'=q1+1) & (arr1'=2) & (lost2'=0)
		 + ((1-lambda)*mu1*mu2): (q1'=q1-1) & (arr1'=0) & (lost2'=0)
		 + ((1-lambda)*mu1*(1-mu2)): (q1'=q1-1) & (arr1'=0) & (lost2'=1)
		 + ((1-lambda)*(1-mu1)*mu2): (q2'=q2-1) & (arr1'=0) & (lost2'=0)
		 + ((1-lambda)*(1-mu1)*(1-mu2)): (arr1'=0) & (lost2'=0);

	[] (q1=c) & (q2=c)
		-> (lambda*mu1*mu2): (arr1'=2) & (lost2'=0)
		 + (lambda*mu1*(1-mu2)): (arr1'=2) & (lost2'=1)
		 + (lambda*(1-mu1)*mu2): (q2'=q2-1) & (arr1'=1) & (lost2'=0)
		 + (lambda*(1-mu1)*(1-mu2)): (arr1'=1) & (lost2'=0)
		 + ((1-lambda)*mu1*mu2): (q1'=q1-1) & (arr1'=0) & (lost2'=0)
		 + ((1-lambda)*mu1*(1-mu2)): (q1'=q1-1) & (arr1'=0) & (lost2'=1)
		 + ((1-lambda)*(1-mu1)*mu2): (q2'=q2-1) & (arr1'=0) & (lost2'=0)
		 + ((1-lambda)*(1-mu1)*(1-mu2)): (arr1'=0) & (lost2'=0);
endmodule


label "goal" = lost2=1;
label "reference" = _TIME_;  //arr1!=0;

//{-
//formula importance = q2;

//const double confidence = 0.95;
//const double precision  = 1E-7;
//-}