How to compute the avg resp time of an M/M/c/K queue?

[c.klo...@gmail.com]

Hi, I'm trying to model an M/M/c/K queue in Prism (as a CTMC) and I think I've got it right but cannot figure out how to compute the average response time (ART).

For some other metrics I'm getting the results I expect according to the formulae I've found here: http://profs.degroote.mcmaster.ca/ads/parlar/courses/o711/documents/Formulas-HL-9e-2011-10-31.pdf

The probability that there are n requests waiting in the queue is computed correctly, as is the expected number of requests in the queue, and the dot graph of the system looks like I expected it.

But for the ART I cannot figure out how to express the property that would produce the correct results.
I'm attaching a model of an M/M/c/K queue, where I'm using a varying input rate (range [3,7]), a service rate of 5, the number of servers (c) is 3, and the queue capacity (K) is 10.
According to the formula in the aforementioned PDF, the resuts for ART should be:
lambda ART
3          0.2020546215799792
4          0.2047274706905417
5          0.2090677308502383
6          0.2155562306816493
7          0.2247420207877567

I've tried this (for n in [1,10], i.e., for [1, K]):
 const int n;
 filter(avg, R{"time"}=? [ (F waiting=n-1) ], (waiting=n&n>0))
The results are wrong - interestingly, the results for n in [3,7] are close to what the model should produce for an M/M/1/K queue that has a service rate of 15 (which is 0.08333326506665968).
The average of the results obtained for the different values of N is 0.104583312 - wrong again.

I've also tried counting the requests that had been served by time T and dividing T by them:
R{"requestsServed"}=? [ C<=T ]
Again, not close (results obtained are almost close to 1/lambda).

I've finally tried counting the time spent waiting on some request and dividing that by the number of served requests:
filter(sum, R{"time"}=? [ C<=T ], (waiting>0))
Wrong again... For T=1e9 and lambda=3, I get R{"time"}=1.8999999999999996e10 and R{"requestsServed"}=2.9999992383348365e9, which gives 6.33333494129353 instead of 0.2020546215799792...

Anyone can help out with this/point me towards the right direction?

I'm attaching the Prism model and properties.

Best,
Chris
P.S. It's not my coursework by the way - long passed that point... :-)

[Gethin Norman]

Chris,

for the average waiting time you need to consider the different positions a specific customer arrives into the queue and then how long this customer gets to be served rather than how long it takes for the queue to decrease by 1 (I hope you can see that this is not the waiting time of any customer except in the case when a customer arrives into an empty queue).

To calculate this time, the model would have to be extended so it keeps track of a specific customer as it moves through the queue to when it is served.

You would then need to average these values over all positions the customer can arrive.

thanks

Gethin

> --
> 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.
> <MMcK.prism><properties-MMcK.props>

[Christos Kloukinas]

Thanks Gethin for the response!


Any suggestions on how the model could be extended to keep track of
individual requests as they move through the queue?

Or pointers to some model that does something similar?

I'm having trouble thinking of a way this could be done. :-(


It'd be nice if there were some models of such classic problems in the
manual/tutorial, showing how the different metrics can be calculated
with Prism - they'd be extremely valuable to get people started with
Prism I think (and maybe also serve as test cases, comparing the results
against the analytical solutions).


Best,

Christos

[Gethin Norman]

Christos,

you could add a separate module that has a variable denoting the current position in the queue and the variable gets updated when a customer is removed from the queue (i.e. synchronises with the the serve action). You can then vary its initial value to give the waiting time when it arrives into diffferent positions in the queue.

Also thanks for the idea on have classical problems in the tutorial, we will certainly look into doing this (when we have the time).

Gethin

[Christos Kloukinas]

Hi Gethin,
Thanks for the suggestion.

I'm attaching the model I came up with and the property I came up with.

I've managed to get a result that is correct in the first two decimal
digits. Compare file expected-avg-resp-time.csv (results calculated
analytically) with either MMcK-right-10-3.csv or MMcK-right-20-3.csv (10
or 20 servers, results are the same).

But I actually have no idea if it's correct or just happened to get
something that looks almost right... :-(

I've added these modules in the model, per your suggestion (waiting is
the current number of requests in the queue), each one setting a boolean
to true while the n-th request is being processed:
#for i=1:c#
module Timing#i#
  processing#i# : bool init false;
  // Clients drive these actions
  [req1]   (waiting =#i#-1) -> 1 : (processing#i#'=true); // started
processing
  [req1]   (waiting!=#i#-1) -> 1 : true;
  // Service providers drive these actions
#for j=1:c#
  [srv#j#] (waiting =#i#) -> 1 : (processing#i#'=false); // finished
processing
  [srv#j#] (waiting!=#i#) -> 1 : true;
#end#
endmodule
#end#


The property I'm trying to calculate is:
( 0.0 #for i=1:s# + ( (S=? [ (waiting=#i#) ]) * filter(avg, R{"time"}=?
[ S ], (processing#i#)) ) #end# ) / Capacity

So I'm trying to average the time spent while processing request in slot
#i#, multiplied by the probability that there are #i# requests, and
dividing everything with the number of slots in the queue (to get the
two first digits right - clinging from ones' one hair...).


I run prism this way:
Capacity=10
servers=10
srvRate=11
reqRateMin=50
reqRateMax=100
reqRateStp=10
prop=3
prismpp properties.props.pp ${Capacity} > properties.props
prismpp MMcK-right.prism.pp ${servers} > MMcK-right-${servers}.prism
prism \
                -gs \
                -maxiters 1000000 \
                MMcK-right-${servers}.prism \
                properties.props \
                -prop ${prop} \
                -const
srvRate=${srvRate},Capacity=${Capacity},reqRate=${reqRateMin}:${reqRateStp}:${reqRateMax}
\
                -exportresults results.txt \
                > MMcK-right-${servers}-${prop}.log 2>&1
tr '\t' , < results.txt > MMcK-right-${servers}-${prop}.csv

Is this approach correct? Have strong doubts myself...

Best,
Christos

[Christos Kloukinas]

Dear Gethin,
Thank you very much for your response, I really appreciate the time you
took to respond!

You're right, my module was not counting the requests that were before
mine in the queue.

Following your description I came up with this module:

// Request arrives when there are J-1 requests in the queue, so needs
// to wait for J srv_x actions to be served. 0 < J <= Capacity
#for i=1:Cap#
module Processing#i#
  processing#i# : bool init false;
  count_#i# : [0 .. #i#] init #i#;
  //// Clients drive these actions
  /// Other request arrivals - ignore them.

  [req1]   (waiting!=#i#-1) -> 1 : true;

  /// My arrival - start stopwatch.
  [req1]   (waiting =#i#-1) -> 1 : (processing#i#'=true) &
(count_#i#'=#i#);
   //// Service providers drive these actions
#for j=1:s#
  /// There's no processing for me - ignore.
  [srv#j#] !(processing#i#) -> 1 : true;
  /// There are still earlier requests waiting service - waiting.
  [srv#j#] (processing#i#) & (count_#i# != 1) -> 1 :
(count_#i#'=max(0,count_#i#-1));
  /// I am being served now - stop stopwatch.
  [srv#j#] (processing#i#) & (count_#i#  = 1) -> 1 :
(processing#i#'=false) & (count_#i#'=#i#);
#end#
endmodule
#end#

So there are K modules - one for each slot of the waiting queue (getting
the same result if I use just one of them and vary J externally).
When there are J-1 requests in the queue, a request sets signal
processingJ to true and count_J to J.
Then, while processingJ is true, each srv action reduces count_J.
I unset processingJ when count_J is equal to 1, since this is the
service of my request.

The property I'm then calculating is this one:
// Attempt at a generic Avg Resp. Time.
( 0.0 #for i=1:Cap# + ( (S=? [ (waiting=#i#) ]) * filter(avg,

R{"time"}=? [ S ], (processing#i#)) ) #end# )

So I add all the average times the system stays at a state where
processingJ is true, weighted by the probability there are J requests in
the queue.

For the case I'm testing (s=10,Cap=10,srvRate=11), the correct result is
0.090909091 for different values of the input rate (reqRate=50:10:100) -
the results I'm getting are far from that though... :-(
reqRate,Result
50,0.9893081518715127
60,0.9956181135207659
70,0.9981678841506308
80,0.9992120073301123
90,0.9996492594680785
100,0.9998378983125484

I'm at a loss as to where this is going wrong.
I don't understand why the numbers differ when the reqRate changes (they
should be the same), nor why they look like they're about (Cap+1) times
greater than the correct result.

Wonder whether I'm again doing something silly here... :-/

Commands used:
Capacity=10
srvRate=11
reqRateMin=50
reqRateMax=100
reqRateStp=10
servers=10
res=results
test -d ${res} || mkdir ${res}
prismpp ${model}.prism.pp ${servers} ${Capacity} >
${res}/${model}-${servers}.prism
prismpp properties-MMcK.props.pp ${servers} ${Capacity} >
${res}/properties.props
prop=4
prism \
                                -pgs \
                                -maxiters 10000 \
                                ${res}/${model}-${servers}.prism \
                                ${res}/properties.props \
                                -prop ${prop} \
                                -const
srvRate=${srvRate},reqRate=${reqRateMin}:${reqRateStp}:${reqRateMax} \
                                -exportresults ${res}/results.txt \
                                2>&1 \
                                | tee
${res}/${model}-${servers}-${prop}.log \
                                | egrep '(Error|^Model constants:|^Result)'
tr '\t' , < ${res}/results.txt > ${res}/${model}-${servers}-${prop}.csv


Best,
Christos

On 22/11/2017 15:17, Gethin Norman wrote:
> Christos,
>
> I am not sure I have followed what you have done but it does not look like you are tracking a single customer. What I was proposing was to calculate the waiting time for each possible arrival position in the queue through separate models and then average the results (based on the probability that the customer arrives at that position in the queue). I cannot see how it can be combined into a single module.
>
> For example, consider the case where customer arrives into the kth position in the queue. This will be the initial state for the corresponding model, so in the queue module you would need to set “waiting” to take k as its initial value. In addition to keep tack of this customers position add the module to record the time to respond:
>
> module Timing
>
> position : [0..k] init k;
>
> #for j=1:c#
> [srv#j#] (position>0) -> 1 : (position’=position-1);
> [srv#j#] (position=0) -> 1 : true; // just to prevent deadlocks in the model
>
> #end#
>
> endmodule
>
> Essentially, he customer moves up the queue as customers ahead in the queue are served and then when it reaches position 1 it is then served moving to position=0.
>
> The property of interest is (from the initial state) the expected time to reach a state where position=0 (this is the time for the customer to move through the queue and get served, i.e. the waiting and serving time).
>
> You would need to compute this for all possible values of k and then average based on the long run probability of arriving into the kth position into the queue.
>
> Does this make sense?
>
> thanks
>
> Gethin

>> <MMcK-right.prism.pp><properties.props.pp><expected-avg-resp-time.csv><MMcK-right-10-3.csv><MMcK-right-20-3.csv>

[Gethin Norman]

Christos,

this is not a steady state property, but a transient property: after a customer arrives into the queue then the expected time to be served. So you need to calculate R=?[F “served"] where served represents a state where the customer is served (position=0 in the module I gave below) for the initial state.

You need to calculate this expected waiting time for each possible arrival position in the queue, if you have the initial position as a parameter you can just check the same property as this parameter varies of the capacity. Then you need to average the results (based on the probability that the customer arrives at that position in the queue).

thanks

Gethin

> <MMcK-right.prism.pp><properties-MMcK.props.pp>