# Flexible Manufacturing System

(Ciardo & Trivedi)

### Introduction:

This case study is based on the flexible manufacturing system of [CT93]. The model is represented as a CTMC. We use N to denote the number of tokens in the system. The PRISM source code for this case study given below.

```// flexible manufacturing system [CT93]
// gxn/dxp 11/06/01

ctmc

const int n; // number of tokens

// rates from Pi equal #(Pi) * min(1, np/r)
// where np = (3n)/2 and r = P1+P2+P3+P12
const int np=floor((3*n)/2);
formula r = P1+P2+P3+P12;

module machine1

P1 : [0..n] init n;
P1wM1 : [0..n];
P1M1 : [0..3];
P1d : [0..n];
P1s : [0..n];
P1wP2 : [0..n];
M1 : [0..3] init 3;

[t1] (P1>0) & (M1>0) & (P1M1<3)  -> P1*min(1,np/r) : (P1'=P1-1) & (P1M1'=P1M1+1) & (M1'=M1-1);
[t1] (P1>0) & (M1=0) & (P1wM1<n) -> P1*min(1,np/r) : (P1'=P1-1) & (P1wM1'=P1wM1+1);

[] (P1M1>0) & (P1wM1=0) & (M1<3) & (P1s<n) -> 0.2*P1M1 : (P1M1'=P1M1-1) & (M1'=M1+1) & (P1s'=P1s+1);
[] (P1M1>0) & (P1wM1>0) & (P1s<n) -> 0.2*P1M1 : (P1wM1'=P1wM1-1) & (P1s'=P1s+1);

[] (P1M1>0) & (P2wP1=0) & (P1wM1=0) & (M1<3) & (P1wP2<n) -> 0.05*P1M1 : (P1M1'=P1M1-1) & (M1'=M1+1) & (P1wP2'=P1wP2+1);
[] (P1M1>0) & (P2wP1=0) & (P1wM1>0) & (P1wP2<n) -> 0.05*P1M1 : (P1wM1'=P1wM1-1) & (P1wP2'=P1wP2+1);

[p1p2] (P1M1>0) & (P2wP1>0) & (P1wM1=0) & (M1<3) -> 0.05*P1M1 : (P1M1'=P1M1-1) & (M1'=M1+1);
[p1p2] (P1M1>0) & (P2wP1>0) & (P1wM1>0) -> 0.05*P1M1 : (P1wM1'=P1wM1-1);

[p1p2] (P1wP2>0)  -> 1: (P1wP2'=P1wP2-1);
[]     (P1s>0) & (P1+P1s<=n) -> 1/60 : (P1s'=0) & (P1'=P1+P1s);
[fp12] (P1+P12s<=n) -> 1: (P1'=P1+P12s);

endmodule

module machine2

P2 : [0..n] init n;
P2wM2 : [0..n];
P2M2 : [0..1];
P2s : [0..n];
P2wP1 : [0..n];
M2 : [0..1] init 1;

[t2] (P2>0) & (M2>0) & (P2M2<1)  -> P2*min(1,np/r) : (P2'=P2-1) & (P2M2'=P2M2+1) & (M2'=M2-1);
[t2] (P2>0) & (M2=0) & (P2wM2<n) -> P2*min(1,np/r) : (P2'=P2-1) & (P2wM2'=P2wM2+1);

[] (P2M2>0) & (P2wM2=0) & (M2<1) & (P2s<n) -> 0.1 : (P2M2'=P2M2-1) & (M2'=M2+1) & (P2s'=P2s+1);
[] (P2M2>0) & (P2wM2>0) & (P2s<n) -> 0.1 : (P2wM2'=P2wM2-1) & (P2s'=P2s+1);

[] (P2M2>0) & (P1wP2=0) & (P2wM2=0) & (M2<1) & (P2wP1<n) -> 1/15: (P2M2'=P2M2-1) & (M2'=M2+1) & (P2wP1'=P2wP1+1);
[] (P2M2>0) & (P1wP2=0) & (P2wM2>0) & (P2wP1<n) -> 1/15: (P2wM2'=P2wM2-1) & (P2wP1'=P2wP1+1);

[p1p2] (P2M2>0) & (P1wP2>0) & (P2wM2=0) & (M2<1) -> 1/15: (P2M2'=P2M2-1) & (M2'=M2+1);
[p1p2] (P2M2>0) & (P1wP2>0) & (P2wM2>0) -> 1/15: (P2wM2'=P2wM2-1);

[p1p2] (P2wP1>0) -> 1 : (P2wP1'=P2wP1-1);
[]     (P2s>0) & (P2+P2s<=n) -> 1/60 : (P2s'=0) & (P2'=P2+P2s);
[fp12] (P2+P12s<=n) -> 1 : (P2'=P2+P12s);
[p2p3] (M2>0) -> 1 : (M2'=M2);

endmodule

module machine3

P3 : [0..n] init n;
P3M2 : [0..n];
P3s : [0..n];

[t3] (P3>0) & (P3M2<n) -> P3*min(1,np/r) : (P3'=P3-1) & (P3M2'=P3M2+1);

[p2p3] (P3M2>0) & (P3s<n) -> 1/2 : (P3M2'=P3M2-1) & (P3s'=P3s+1);
[]     (P3s>0) & (P3+P3s<=n) -> 1/60 : (P3s'=0) & (P3'=P3+P3s);

endmodule

module machine12

P12 : [0..n];
P12wM3 : [0..n];
P12M3 : [0..2];
P12s : [0..n];
M3 : [0..2] init 2;

[p1p2] (P12<n) -> 1: (P12'=P12+1);

[t12] (P12>0) & (M3>0) & (P12M3<2) -> P12*min(1,np/r) : (P12'=P12-1) & (P12M3'=P12M3+1) & (M3'=M3-1);
[t12] (P12>0) & (M3=0) & (P12wM3<n) -> P12*min(1,np/r) : (P12'=P12-1) & (P12wM3'=P12wM3+1);

[] (P12M3>0) & (P12wM3=0) & (P12s<n) & (M3<2) -> P12M3 : (P12M3'=P12M3-1) & (P12s'=P12s+1) & (M3'=M3+1);
[] (P12M3>0) & (P12wM3>0) & (P12s<n) -> P12M3 : (P12wM3'=P12wM3-1) & (P12s'=P12s+1);

[fp12] (P12s>0) -> 1/60 : (P12s'=0);

endmodule

// reward structures

// throughput of machine1
rewards "throughput_m1"
[t1]  true : 1;
endrewards
// throughput of machine2
rewards "throughput_m2"
[t2]  true : 1;
endrewards
// throughput of machine3
rewards "throughput_m3"
[t3]  true : 1;
endrewards
// throughput of machine12
rewards "throughput_m12"
[t12]  true : 1;
endrewards
// productivity of the system
rewards "productivity"
[t1]  true : 400;
[t2]  true : 600;
[t3]  true : 100;
[t12] true : 1100;
endrewards
```

### Model Statistics

The table below shows statistics for each model we have built. The first section gives information about the CTMC representing the model: the number of states and the number of non zeros (transitions). The second part refers to the MTBDD which represents this CTMC: the total number of nodes, the number of leaves (terminal nodes), and the amount of memory needed to store it. The last column gives the amount of memory a sparse matrix would need to represent the same CTMC.

 N: Model: MTBDD: Sparse: States: NNZ: Nodes: Leaves: Kb: Kb: 1 54 155 783 9 15.3 2.03 2 810 3,699 4,371 14 85.4 46.5 3 6,520 37,394 10,896 22 212 463 4 35,910 237,120 28,470 30 556 2,919 5 152,712 1,111,482 50,877 43 992 13,621 6 537,768 4,205,670 78,125 53 1,526 51,385 7 1,639,440 13,552,968 120,834 71 2,360 165,227 8 4,459,455 38,533,968 215,250 84 4,204 468,989 9 11,058,190 99,075,405 309,067 108 6,032 1,204,235 10 25,397,658 234,523,289 406,018 126 7,930 2,847,529

### Model Construction Times

The table below gives the times taken to construct the models. This process involves first building a CTMC (represented as an MTBDD) from the system description (in our module based language), and then computing the reachable states using a BDD based fixpoint algorithm. The total time required and the number of fixpoint iterations are given below.

 N: Construction: Time (s): Iter.s: 1 0.173 9 2 0.449 17 3 0.829 25 4 2.62 33 5 5.25 41 6 14.2 49 7 35.8 57 8 44.2 65 9 61.0 73 10 93.7 81

### Model Checking

We now report on the model checking results obtained using PRISM when verifying the following CSL properties.

```// expected throughput of each machine
R{"throughput_m1"}=?  [ S ]
R{"throughput_m2"}=?  [ S ]
R{"throughput_m3"}=?  [ S ]
R{"throughput_m12"}=? [ S ]

// expected productivity of the system
R{"productivity"}=? [ S ]
```