User Tools

Site Tools


cookbook:ept:mmmodel

— Model of multimachine workstation with downs during process —

Here, a model is given of a workstation with two parallel machines. The machines go down every mtf seconds and are in repair for mtr seconds then. Downs only occur during processing lots. Arrivals and departures of lots are printed in process M. It is used in the python script that can be found in ept.

from standardlib import *
 
type lot   = (nat,real)   // (lotnumber,generation time)
   , event = (real,string,nat)
 
proc G(chan a!: lot, val mta: real) =
|[ var dta :-> real = exponential(mta) , ta: real, i: nat = 1
:: *( a!(i,time); ta:= sample dta; delay ta; i:= i + 1 )
]|
 
proc B(chan a?: lot, b!: 2 # lot) =
|[ var xs: [lot] = [], x: lot
:: *( a?x; xs:= xs ++ [ x ]
    | ( |, j <- 0..1, len(xs) > 0 -> b.j!hd(xs); xs:= tl(xs) )
    )
]|
 
proc M(chan a?,b!:lot, val m: nat, mt0,c0,mtf,mtr: real) =
|[ var x: lot
 , dt0 :-> real = gamma(1/c0^2,c0^2*mt0)
 , dtf :-> real = exponential(mtf)
 , dtr :-> real = exponential(mtr)
 , t0,t0rem,tf,tr,rtot: real, d: bool
:: tf:= sample dtf
 ; *( a?x; !!x.1,"\t\"A\"\t",m, "\n"   
      ; t0:= sample dt0; d:= true; rtot:= 0.0; t0rem:= t0
      ; d *> 
          ( tf >= t0rem -> tf:= tf - t0rem; d:= false
          | tf <  t0rem -> t0rem:= t0rem - tf; tr:= sample(dtr)
            ; rtot:= rtot + tr; tf:= sample dtf
          ) 
 
       ; delay t0 + rtot; b!x 
       ; !!time,"\t\"D\"\t",m, "\n"    
    )
]|
 
proc E(chan a?: lot, val nlots,nr_idd: nat) =
|[ var i: nat = 0, x: lot, quit: real
:: i < nlots *> ( a?x; i:= i + 1 )
 ; quit:= -1.0; delay quit
]|

The line quit:= -1.0; delay quit causes blocking of process E in the form of a deadlock.

Finally the model becomes:

model S(val nlots,nr_idd: nat, ta,t0,c0,mttf,mttr: real) =
|[ chan gb,me: lot, bm: 2 # lot
:: G(gb,ta)
|| B(gb,bm)
|| M(bm.0,me,0,t0,c0,mttf,mttr) || M(bm.1,me,1,t0,c0,mttf,mttr)
|| E(me,nlots,nr_idd)
]|
cookbook/ept/mmmodel.txt · Last modified: Friday, 01 December 2006 : 16:03:34 (external edit)