www.prismmodelchecker.org

Flexible Manufacturing System

(Ciardo & Trivedi)

Contents

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
View: printable version          Download: fms.sm

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,52651,385
7 1,639,440 13,552,968 120,83471 2,360165,227
8 4,459,455 38,533,968 215,25084 4,204468,989
9 11,058,19099,075,405 309,0671086,0321,204,235
1025,397,658234,523,289406,0181267,9302,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.1739
2 0.44917
3 0.82925
4 2.62 33
5 5.25 41
6 14.2 49
7 35.8 57
8 44.2 65
9 61.0 73
1093.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 ]
View: printable version          Download: fms.csl

All experiments were carried out on a 2.80GHz PC with 1 Gb memory running Linux and in all iterative methods we stop iterating when the relative error between subsequent iteration vectors is less than 1e-6, that is:

relative error equation

The table below gives the times taken to compute the steady state probabilities using both the Jacobi and (backwards) Gauss Seidel methods. The number of iterations required and the time taken using the MTBDD, sparse and hybrid engines is as follows.

N:   Jacobi:   Gauss Seidel:
Iterations: Time per iteration: (s) Iterations: Time per iteration: (s)
MTBDD Sparse Hybrid Sparse Hybrid
1 434 0.004788< 0.000010.00000575 < 0.00001< 0.00001
2 378 0.1546110.000032 0.00004092 0.000043 0.000087
3 554 1.6263470.000343 0.0003881060.000557 0.000943
4 729 - 0.001771 0.0036601180.002610 0.005992
5 905 - 0.008700 0.0232811270.011992 0.027898
6 1,080- 0.033600 0.0844651360.044419 0.104735
7 1,258- 0.109400 0.2600221440.143736 0.331993
8 1,438- 0.325950 0.8874261510.420152 0.949457
9 1,619- 0.865450 3.7129321591.077013 2.335075
101,804- - 10.00491166- 5.505777

The graphs below present the results obtained for the different CSL properties.

  • The expected throughput of each machine:

    plots throughput of each machine
  • The expected productivity of the system:

    plots productivity

Case Studies