PEPA — Performance Evaluation Process Algebra

PC-LAN4.pepa

PC10 = (arrive,lambda).PC11 + (walkon2,infty).PC10;
PC11 = (serve1,infty).PC10;


PC20 = (arrive,lambda).PC21 + (walkon3,infty).PC20;
PC21 = (serve2,infty).PC20;


PC30 = (arrive,lambda).PC31 + (walkon4,infty).PC30;
PC31 = (serve3,infty).PC30;


PC40 = (arrive,lambda).PC41 + (walkon1,infty).PC40;
PC41 = (serve4,infty).PC40;


S1 = (walkon2,omega).S2 + (serve1,mu).(walk2,omega).S2;
S2 = (walkon3,omega).S3 + (serve2,mu).(walk3,omega).S3;
S3 = (walkon4,omega).S4 + (serve3,mu).(walk4,omega).S4;
S4 = (walkon1,omega).S1 + (serve4,mu).(walk1,omega).S1;


(PC10 <> PC20 <> PC30 <> PC40)
     <walkon1,walkon2,walkon3,walkon4,
     serve1,serve2,serve3,serve4> S1