cookbook:transporters

In this section various transporters and carrousels are presented. Starting with a simple transporter, more complex transporters are presented. Finally a carrousel is shown. In a transporter we assume that items enter on a first come first basis. We also assume that the entrance time of the items is not equidistant. We distinguish blocking and non-blocking transporters. In a carrousel we assume that all items are transported over a small (and the same) distance inside the machine. If the last item in the carrousel can not be transported to the next process we assume that the whole machine is blocked.

Transporters are generally used to convey a certain transport distance. Carrousels are used as a machine with different process steps as found in the chemical and pharmaceutical industry.

A transporter can be specified by a process whereby the received and sent items
are stored in a list. The processing time of the transporter equals `t`

time units.
We assume that the transporter has an infinite capacity,
so the list in the transporter, denoted by `ys`

has no upper bound.
Items are received via channel `a`

and sent via channel `b`

.
After receiving an item, the item is stored in the list.
The item is stored in a tuple. The first element of the tuple is the item itself,
the second element is the time the item has to leave the transporter.
The item is defined by:

type item = ...

The code of the transporter `T`

is given by:

proc T(chan a?,b!: item, val t: real) = |[ var ys: [(item,real)] = [], x: item :: *( a?x; ys:= ys ++ [ (x,time + t) ] ; len(ys) > 0 *> ( a?x; ys:= ys ++ [ (x,time + t) ] | delay hd(ys).1 - time; b!hd(ys).0; ys:= tl(ys) ) ) ]|

After entrance of the item we add the exit time (`time + t`

) to the item. This time stamp can be considered as
a yellow sticker we put on the item. The yellow sticker is removed before the item is sent to the next process.
In this manner we isolate the item type required outside this process from the item type inside this process.

A transporter, whereby the maximum number of items on the transporter is given by `N`

,
is specified by:

proc T(chan a?,b!: item, val N: nat, t: real) = |[ var ys: [(item,real)] = [], x: item :: *( a?x; ys:= ys ++ [ (x,time + t) ] ; len(ys) > 0 *> ( len(ys) < N -> a?x; ys:= ys ++ [ (x,time + t) ] | delay hd(ys).1 - time; b!hd(ys).0; ys:= tl(ys) ) ) ]|

This transporter functions correctly if sending an item is not blocked.We give two different solutions to resolve this problem.

In this section we present two non-blocking solutions for a transporter.

One solution is to split the transporter in two transporter processes. One part takes care of incoming items, The other part takes care of sending items. If this latter part becomes blocked the first part can carry on. A solution is:

proc T(chan a?,b!: item, val N: nat, t: real) = |[ var ys: [(item,real)] = [], x: item :: *( len(ys) < N -> a?x; ys:= ys ++ [ (x,time + t) ] ) || *( len(ys) > 0 -> skip ; delay hd(ys).1 - time ; b!hd(ys).0; ys:= tl(ys) ) ]|

The blocking behavior can also be avoided by introducing another list `zs`

.
In this list the items are stored that can leave the transporter.
A solution is:

proc T(chan a?,b!: item, val N: nat, t: real) = |[ var ys: [(item,real)] = [], x: item, zs: [item] = [] :: *( ( a?x; ys:= ys ++ [ (x,time + t) ] | len(zs) > 0 -> b!hs(zs); zs:= tl(zs) ) ; len(ys) > 0 *> ( len(ys) < N -> a?x; ys:= ys ++ [ (x,time + t) ] | delay hd(ys).1 - time; zs:= zs ++ [hd(ys).0]; ys:= tl(ys) | len(zs) > 0 -> b!hs(zs); zs:= tl(zs) ) ) ]|

Transporters store their items in a list. This way of modeling is very flexible: we do not know the maximum number of items in the transporter. In some cases we know the maximum number of items. Also we know that the distance between the items is equal. Especially in the field of mechanization we find these type of machines. By rotating some wheel or carrousel we perform the subsequent processing steps. We assume a carrousel with 25 positions. Every position can contain an item. Every position is modeled by an element of a vector.

The items are stored in vector `xv`

. This vector has 25 positions.

type item = ... , vect = 25 * [item]

In the beginning the carrousel is empty.

Initialization of the positions of the carrousel is performed by
function `initV`

:

func initV() -> vect = |[ var j: nat = 0, xt: vect :: j < 25 *> ( xt.j:= []; j:= j + 1 ); ret xt ]|

Carrousel `C`

is specified by the following, whereby
`a`

and `b`

denote the channels, and `pt`

the processing time
for one step:

proc C(chan a?,b!: item, pt: real) = |[ var xt: vect = initV(), x: item, i: nat = 0 :: *( a?x; xt.((i + 24) mod 25):= [x] ; delay pt ; ( xt.i = [] -> skip | xt.i /= [] -> b!hd(xt.i); xt.k:= [] ) ; i:= (i + 1) mod m ) ]|

By incrementing (`i:= (i + 1) mod m`

) we rotate the carrousel. In this process all items are stored at a distance of `pt`

time units. Note: in the beginning the first item is stored in position 24 of `xt`

, while the carrousel tries to send an item (if any) in postion 0 of `xt`

. The next cycle the filling position will be 0, and the unloading position will be 1!

With this specification of the carrousel it is also possible to connect this process to more than one other processes. As an example we can have a machine which perfroms some processes, follwoed by a testprocess. If the item is within its specification, it can go the next step in the carrousel; if the item is outside the specification it can be sent to another process. As an example we have the following process:

proc C(chan a?,b!,c!: item, pt: real) = |[ var xt: vect = initV(), x: item, i: nat = 0, k: nat = 10 :: *( a?x; xt.((i + 24) mod 25):= [x] ; delay pt ; k:= (i + 10) mod 25 ; ( xt.k = [] -> skip | xt.k /= [] -> inSpec:= test(hd(xt.k)) ; ( inSpec -> skip | not inSpec -> c!hd(xt.k); xt.k:= [] ) ) ; ( xt.i = [] -> skip | xt.i /= [] -> b!hd(xt.i); xt.k:= [] ) ; i:= (i + 1) mod m ) ]|

in this process the function `inSpec`

tests if the item is within its specifications.
We assume that testing takes place at a distance of `k`

from the entance of the items.
In this case we have a machine with `k = 10`

.

cookbook/transporters.txt · Last modified: Thursday, 12 February 2009 : 09:49:12 by hvrooy

Except where otherwise noted, content on this wiki is licensed under the following license: CC Attribution-Noncommercial-Share Alike 4.0 International