User Tools

Site Tools


cookbook:buffers

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

cookbook:buffers [Thursday, 30 November 2006 : 16:48:02]
127.0.0.1 external edit
cookbook:buffers [Thursday, 12 February 2009 : 09:48:54] (current)
hvrooy
Line 1: Line 1:
 +====== Buffers ======
  
 +In this section various buffers are presented. Starting with a simple buffer, more complex bufers are presented.
 +
 +
 +
 +===== Simple buffers =====
 +An infinite buffer can be specified by a process whereby the received and sent items are stored in a list.
 +Items are received via channel ''​a''​ and sent via channel ''​b''​. The list is denoted by ''​xs''​.
 +<code chi>
 +proc B(chan a?,b!: item) =
 +|[ var xs: [item] = [], x: item
 +:: *( a?x; xs:= xs ++ [x]
 +    | len(xs) > 0 -> b!hd(xs); xs:= tl(xs)
 +    )
 +]|
 +</​code> ​
 +A finite buffer, whereby the buffer size is denoted by ''​N'', ​ can be specified by:
 +<code chi>
 +proc B(chan a?,b!: item, val N: nat) =
 +|[ var xs: [item] = [], x: item
 +:: *( len(xs) < N -> a?x; xs:= xs ++ [x]
 +    | len(xs) > 0 -> b!hd(xs); xs:= tl(xs)
 +    )
 +]|
 +</​code> ​
 +
 +===== Batch buffers =====
 +
 +A machine in a manufacturing system can require more then one item or product before processing can start. Well-known examples of such machines are furnaces in the semiconductor industry. In that case a total of 6 items is required before processing can begin. In front of these type of machines you find batch buffers. In a batch buffer items are collected. If the number of items in the buffer is equal or more then a given batchsize ''​k''​ this batch can be sent to a process via channel ''​b''​.
 +
 +In this specification use has been made of the functions ''​take''​ and ''​drop''​. ''​take(xs,​k)''​ takes the first ''​k''​ or less items from list ''​xs''​. ''​drop(xs,​k)''​ removes the first ''​k''​ or less items from list ''​xs''​. Note: ''​take([1,​2,​3],​1) = [1]'';​ ''​hd([1,​2,​3]) = 1''​.
 +<code chi>
 +proc B(chan a?: item, b!: [item], val k: nat) =
 +|[ var xs: [item] = [], x: item
 +:: *( a?x; xs:= xs ++ [x]
 +    | len(xs) > 0 -> b!take(xs,​k);​ xs:= drop(xs,k)
 +    )
 +]|
 +</​code> ​
 +Another solution is to assume that the items to be received are lists.
 +We have the following specification.
 +<code chi>
 +proc B(chan a?, b!: [item], val k: nat) =
 +|[ var xs: [item] = [], ys: [item]
 +:: *( a?ys; xs:= xs ++ ys
 +    | len(xs) > 0 -> b!take(xs,​k);​ xs:= drop(xs,k)
 +    )
 +]|
 +</​code> ​
 +
 +
 +
 +===== A buffered manufacturing line =====
 +
 +As an example of a small line in the semiconductor industry, we present a buffered line with 2 etching machines processing lots in batches of 2, and 3 furnaces processing lots in batches of 6.
 +
 +The objects, the items, are denoted by:
 +<code chi>
 +type item  = (nat,real)
 +   , batch = [item]
 +</​code>​
 +An item consists of an identifier, a natural number and the entry time, a real number. We also introduce type ''​batch''​. A batch is a list of items. ​
 +
 +Generator ''​G''​ sends items to batching buffer ''​B''​. From the buffer the items are sent to two etch processes ''​M''​. From the etch processes the items are sent to another batch buffer and to three furnaces ''​M''​. Finally the items are sent to exit process ''​E''​. The exit process does some bookkeeping.
 +
 +Generator ''​G''​ is:
 +<code chi>
 +proc G(chan a!: batch, val ta: real) =
 +|[ id: nat = 1, u: -> real = expontential(ta),​ t: real
 +:: *( a![(id,​time)];​ t:= sample u; delay t; id:= id + 1 )
 +]|
 +</​code>​
 +The generator sends with an exponential interarrival time an item encapsulated in a list in the system.
 +
 +Batch buffer ''​B''​ is:
 +<code chi>
 +proc B(chan a?, b!: batch, val k: nat) =
 +|[ var xs: batch = [], ys: batch
 +:: *( a?ys; xs:= xs ++ ys
 +    | len(xs) > 0 -> b!take(xs,​k);​ xs:= drop(xs,k)
 +    )
 +]|
 +</​code>​
 +The buffer is self explanory.
 +
 +Machine ''​M''​ is:
 +<code chi>
 +proc M(chan a?,b!: batch, val t0: real) =
 +|[ xs: batch
 +:: *( a?xs; delay t0; b!xs)
 +]|
 +</​code>​
 +A machine has a processing time ''​t0''​. The batch size in the machine is determined by the buffer in fornt of the machine.
 +
 +Exit process ''​E''​ is:
 +<code chi>
 +proc E(chan a?: batch) =
 +|[ i: nat = 0, mp: real = 0.0, phi: real
 + , xs: batch, x: item
 +:: *( a?xs
 +      ; len(xs) > 0
 +        *> ( x:= hd(xs); xs:= tl(xs); i:= i + 1
 +             ; phi:= time - x.1
 +             ; mp:= (i - 1) / i * mp + phi / i
 +             ; !! time, "​\tE\tflow time=",​ phi
 +                , "​\tmean flow time=",​ mp
 +                , "​\tthroughput=",​ i / time, "​\n"​
 +           )
 +    )
 +]|
 +</​code>​
 +
 +
 +{{ :​cookbook:​manufacturingline2.png |The buffered manufacturing line}}
 +
 +Model ''​L''​ is:
 +<code chi>
 +model L(var ta: real) =
 +|[ chan a,b,c,d,e: batch
 +:: G(a,ta)
 +|| B(a,​b,​2) ​
 +|| M(b,c, 4.0) || M(b,c,4.0)
 +|| B(c,​d,​6) ​
 +|| M(d,e,12.0) || M(d,e,12.0) || M(d,e,12.0)
 +|| E(e)
 +]|
 +</​code>​
cookbook/buffers.txt · Last modified: Thursday, 12 February 2009 : 09:48:54 by hvrooy