next up previous
Next: Fusion of Trace Properties Up: Formal Model of Traces, Previous: Meta-properties

Tagged Events

When we reason about a combination of protocols, we associate a label with each protocol and tag the events handled by each protocol with that protocol's label. To model these tagged events, we make a subtype of the type EventStruct by replacing the final component Top with E Label Top to get the subtype
\begin{program*} \> \\ \> TaggedEventStruct ==\\ \> E:\mBbbU{}\\ \> \mtimes{}... ...bB{}\\ \> \mtimes{} E {}\mrightarrow{} Label\\ \> \mtimes{} Top \end{program*}
If E is a tagged event structure, then it is also an event structure, but it has an additional component, a function tag $_{\mbox{\small {E}}}$ of type |E| Label. A trace tr over E is still a trace as defined previously, but every event tr[i] has a tag tag $_{\mbox{\small {E}}}$ tr[i]. The sublist of tr consisting of all events in tr with a given tag tg is defined by
\begin{program*} \> \\ \> tr$\mid$\ ==\\ \> <e\mmember{}tr \vert tag$_{\mbox{\small {E}}}$\ \\ \> e =\msubone{} tg> \end{program*}

We will need the following property of tagged traces. It holds of traces in which events with the same message have the same tag.
\begin{program*} \> \\ \> Tag-by-msg$_{\mbox{\small {E}}}$\ tr ==\\ \> \mforal... ...E}}}$\ tr[i])\\ \> = (tag$_{\mbox{\small {E}}}$\ \\ \> tr[j]))) \end{program*}

Richard Eaton 2002-02-20