//
// Fluid Queues with breakdowns for bluemoon Prism package
// Budde & D'Argenio, 2015
//
//{-
// Concept of the queue with breakdowns:
//                        
// (Source1: on/off) --->||
//                       ||
// (Source2: on/off) --->||
//         .             ||        Buffer
//         .             ||---> [·····###]--(Server: on/off)---->
//         .             ||
// (SourceN: on/off) --->||
//                        
// Buffer has maximum capacity K.
// The single Server: processes     with rate c,
//                    fails         with rate gamma,
//                    gets repaired with rate delta.
// Sources can be of Type 1 or 2.
// Sources of Type i: produce       with rate lambdai,
//                    fail          with rate betai,
//                    get repaired  with rate alphai.
//
// Initial state: the buffer has a single customer, the server is down,
//                and all sources are also down except one of Type 2.
// Stopping event: empty buffer.
// Rare event: buffer reaching full capacity K.
//-}

ctmc

// -- The following values were extracted from Kroese & Nicola,
// -- "Efficient estimation of overflow probabilities in queues
// -- with breakdowns", Performance Evaluation, 36-37, 1999, pp. 471-484.
// -- This model corresponds to the system described in the section 4.4
// -- (p. 481) of said article.

// -- Buffer capacity
const int K;

// -- Server
const double c = 100;
const double gamma = 3;
const double delta = 4;

// -- Sources of Type 1
const int NSrc1 = 5;
const double lambda1 = 3;
const double alpha1  = 3;
const double beta1   = 2;

// -- Sources of Type 2
const int NSrc2 = 5;
const double lambda2 = 6;
const double alpha2  = 1;
const double beta2   = 4;


module QueueWithBreakdowns

	// -- Initializations
	lost:  bool init false;
	reset: bool init false;
	buf: [0..K-1] init 1;     // -- Buffer, initially with one customer
	server: bool init false;  // -- Server, initially down
	src1: [0..NSrc1] init 0;  // -- Sources of Type 1, initially none active
	src2: [0..NSrc2] init 1;  // -- Sources of Type 2, initially  one active

	// -- Sources failure and recovery
	[] src1>0     -> (src1 * beta1)          : (src1'=src1-1);
	[] src1<NSrc1 -> ((NSrc1-src1) * alpha1) : (src1'=src1+1);
	[] src2>0     -> (src2 * beta2)          : (src2'=src2-1);
	[] src2<NSrc2 -> ((NSrc2-src2) * alpha2) : (src2'=src2+1);

	// -- Server failure and recovery
	[]  server -> gamma: (server'=false);
	[] !server -> delta: (server'=true);

	// -- Buffer in
	[] src1>0 & buf<K-1 -> (src1 * lambda1) : (buf'=buf+1);
	[] src1>0 & buf=K-1 -> (src1 * lambda1) : (lost'=true);
	[] src2>0 & buf<K-1 -> (src2 * lambda2) : (buf'=buf+1);
	[] src2>0 & buf=K-1 -> (src2 * lambda2) : (lost'=true);

	// -- Buffer out
	[] server & buf>1 -> c : (buf'=buf-1);
	[] server & buf=1 -> c : (reset'=true);
endmodule


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