HELP (Write description for Queueing Network)

[Momtez Benmbarek]

hello could you please write the description of  Tandem Queueing Network for every statement thank you,  is wrote in the site PRISME

http://www.prismmodelchecker.org/casestudies/tandem.php

im not really understand some lines .

// tandem queueing network [HKMKS99]
// gxn/dxp 25/01/00

ctmc

const int c; // queue capacity

const double lambda = 4*c;
const double mu1a = 0.1*2;
const double mu1b = 0.9*2;
const double mu2 = 2;
const double kappa = 4;

module serverC
	
	sc : [0..c];
	ph : [1..2];
	
	[] (sc<c) -> lambda: (sc'=sc+1); 
	[route] (sc>0) & (ph=1) -> mu1b: (sc'=sc-1);
	[] (sc>0) & (ph=1) -> mu1a: (ph'=2); 
	[route] (sc>0) & (ph=2) -> mu2: (ph'=1) & (sc'=sc-1);
	
endmodule  

module serverM
	
	sm : [0..c];
	
	[route]	(sm<c) -> 1: (sm'=sm+1);
	[] (sm>0) -> kappa: (sm'=sm-1);
	
endmodule

// reward - number of customers in network
rewards "customers"
	true : sc + sm;
endrewards

[Momtez Benmbarek]

who can explain this code pls?

[Gethin Norman]

I have added some comments to the code below to help with understanding

thanks

Gethin

// tandem queueing network [HKMKS99]
// gxn/dxp 25/01/00

ctmc

const int c; // queue capacity

// M/C(2)/1 queue

const double lambda = 4*c; // arrival rate

// Coxian (order 2) server
// rate of first phase is 2
const double mu1a = 0.1*2; // rate move to second phase
const double mu1b = 0.9*2; // rate service ends after first phase
const double mu2 = 2; // rate of second phase is 2

module serverC

sc : [0..c]; // size of queue
ph : [1..2]; // current phase of service

[] (sc<c) -> lambda: (sc'=sc+1); // customer arrives
[route] (sc>0) & (ph=1) -> mu1b: (sc'=sc-1); // end of first phase (and complete)
[] (sc>0) & (ph=1) -> mu1a: (ph'=2); // end of first phase (and move to second)
[route] (sc>0) & (ph=2) -> mu2: (ph'=1) & (sc'=sc-1); // second phase ends (service complete)

endmodule

// Markovian server
const double kappa = 4; // rate of service
module serverM

sm : [0..c]; // size of queue

[route] (sm<c) -> 1: (sm'=sm+1); // customer arrives (from first server)
[] (sm>0) -> kappa: (sm'=sm-1); // complete service

endmodule

// reward - number of customers in network
rewards "customers"
true : sc + sm;
endrewards

> On 23 Oct 2016, at 19:46, Momtez Benmbarek <momtez.b...@gmail.com> wrote:
>
> who can explain this code pls?
>

> --
> You received this message because you are subscribed to the Google Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to prismmodelchec...@googlegroups.com.
> To post to this group, send email to prismmod...@googlegroups.com.
> Visit this group at https://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.