activebadge.pepa

PEPA模型性能分析工具

// A small model (72 states) of a location tracking system based on 
// active badges made by Stephen Gilmore, Jane Hillston and  
// Graham Clark.  The paper ``Specifying performance measures for
// PEPA'' appeared in the proceedings of Fifth International AMAST 
// Workshop on Real-Time and Probabilistic Systems, Bamberg 1999.
// The proceedings were published as Springer-Verlag LNCS 1601.

// an example file for use with the Java Edition of the PEPA Workbench 0.9 and beyond

r = 1.0;
m=1.0;
s=1.0;

P14 = (reg14, r).P14 + (move15, m).P15;
P15 = (reg15, r).P15 + (move14, m).P14 + (move16, m).P16;
P16 = (reg16, r).P16 + (move15, m).P15;

S14 = (reg14, infty).(rep14, s).S14;
S15 = (reg15, infty).(rep15, s).S15;
S16 = (reg16, infty).(rep16, s).S16;

DB14 = (rep14,infty).DB14 + (rep15,infty).DB15 + (rep16,infty).DB16;
DB15 = (rep14,infty).DB14 + (rep15,infty).DB15 + (rep16,infty).DB16;
DB16 = (rep14,infty).DB14 + (rep15,infty).DB15 + (rep16,infty).DB16;

P14 <reg14,reg15,reg16>(S14 <> S15 <> S16) <rep14, rep15, rep16> DB14