cookbook:buffers

# Differences

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

 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 Thursday, 12 February 2009 : 09:48:54 hvrooy Thursday, 30 November 2006 : 16:48:02 external edit Thursday, 12 February 2009 : 09:48:54 hvrooy Thursday, 30 November 2006 : 16:48:02 external edit 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''​. + + 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) + ) + ]| +  ​ + A finite buffer, whereby the buffer size is denoted by ''​N'', ​ can be specified by: + + 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) + ) + ]| +  ​ + + ===== 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''​. + + 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) + ) + ]| +  ​ + Another solution is to assume that the items to be received are lists. + We have the following specification. + + 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) + ) + ]| +  ​ + + + + ===== 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: + + type item  = (nat,real) + , batch = [item] + ​ + 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: + + 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 ) + ]| + ​ + The generator sends with an exponential interarrival time an item encapsulated in a list in the system. + + Batch buffer ''​B''​ is: + + 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) + ) + ]| + ​ + The buffer is self explanory. + + Machine ''​M''​ is: + + proc M(chan a?,b!: batch, val t0: real) = + |[ xs: batch + :: *( a?xs; delay t0; b!xs) + ]| + ​ + 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: + + 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"​ + ) + ) + ]| + ​ + + + {{ :​cookbook:​manufacturingline2.png |The buffered manufacturing line}} + + Model ''​L''​ is: + + 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) + ]| +
cookbook/buffers.txt · Last modified: Thursday, 12 February 2009 : 09:48:54 by hvrooy