We present some PEPA and DNAmaca examples that have been through ipc:
The active badge model represents a person in a corridor of 3 rooms ('P14', 'P15' and 'P16'), each fitted with active badge sensors. The sensors are linked to a tracking database which registers which sensor was activated last.
% 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. # P14 = (reg14, r).P14 + (move15, m).P15; % This little component went to market # 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; # Sys = P14 < reg14,reg15,reg16 > (S14 <> S15 <> S16) < rep14, rep15, rep16 > DB14; Sys
The active badge model was simply extended to have an arbitrary number of rooms and people moving through them. In these instances the database still only tracks the last sensor activation. A possible extension of this would be to design the database to keep track of all the individual movements.