//
// Open/closed queue for bluemoon Prism package
// Budde 2015
//
//{-
// Concept of the mixed open/closed queueing network:
//    l       oq   Server1       |
// ----->[···###]-->(m11)---->   |    Open System
//                  ( | )        | 
//            cq    ( | )        |===================
//    +--->[···#]-->(m12)--->+   |
//    |                      |   |   Closed System
//    |  Server2    cqq      |   |
//    +<---(m2)<--[###·]<----+   |
//
// Open queue 'oq' has capacity b.
// Closed queues 'cq' and 'cqq' have capacity N2, where cq+cqq=N2.
// Packages arrive at oq with rate 'l'.
// Server1 attends packages from oq with rate 'm11' iff cq is empty.
// Server1 attends packages from cq with rate 'm12'.
// Server2 attends packages from cqq with rate 'm2'.
// 
// Initial state: oq is empty and cq has N2 packages.
// Stopping event: oq becoming empty after the first arrival into oq.
// Rare event: oq reaching its maximum capacity b.
//-}

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

const int b;     // -- Open queue (oq) capacity
const int N2=1;  // -- Closed system (cq+cqq) fixed size
const double l=1;    // -- oq arrival rate
const double m11=4;  // -- oq Server1 rate
const double m12=2;  // -- cq Server1 rate
const double m2;     // -- cq Server2 rate

// -- System queues
global oq: [0..b]  init 0;  // -- Open   queue
global cq: [0..N2] init 0;  // -- Closed queue


module Arrival
	lost: bool init false;
	[] oq<b-1 -> l: (oq'=oq+1);
	[] oq=b-1 -> l: (lost'=true);
endmodule

module Server1
	reset: bool init false;
	[] oq>1 & cq=0 -> m11: (oq'=oq-1);
	[] oq=1 & cq=0 -> m11: (reset'=true);
	[] cq>1        -> m12: (cq'=cq-1);
	[] cq=1 & oq>0 -> m12: (cq'=cq-1);
	[] cq=1 & oq=0 -> m12: (reset'=true);
endmodule

module Server2
	[] cq<N2 -> m2: (cq'=cq+1);
endmodule


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