Pt-chain



next up previous
Next: Other Facilities Up: Ariadne: Modeling Language Previous: P-chain

Pt-chain

Pt-chains are patterns over p-chains representing sequences of concurrent events over time. The syntax is much like the regular expression-based syntax of chain definition, but does not include the @, <: or :> symbols. Instead three different angular brackets, - < > to indicate the precedes relationship holds between the enclosed abstract events, |[ ]| to indicate that the enclosed abstract events are pairwise parallel, and { } to indicate that the user does not care about the relationship between the enclosed abstract events - are present. The syntax is:

ptch <ptch-name> = <ptch-expr> [wrt <wrt-list>];

Pattern matching conceptually proceeds in two steps: first the specified events are found in the event trace and then the specified logical relations between those events are asserted. Thus, for example, to describe a pattern in which two p-chains and are logically parallel, we use which is matched as

This means that expressions on this level actually denote two kinds of ``orderings''. The first specifies the search order and the second specifies the required logical ordering relations. The search order is linear and thus can easily be expressed using standard regular expressions. For example, we might have an expression like

which matches as many occurrances of

as it can and then matches a single occurrance of

. The specification of the required logical orderings is ``overlaid'' on these regular expressions.

To express the required logical orderings, we need abstract events which are the collection of things found in a particular match. Our use of regular expression to describe behavior associates a ``search order'' with each set; thus, an abstract event is a list of events in search order; the empty list will be denoted by nil. (This will greatly simplify our expressions and provide for uniform treatment of precedes and parallels.) Does this extraneous ordering cause any problem? No, since abstract events that has the precedes relation holding between them need to be matched in a order anyway, and in case of parallels or interleaving the order should not matter if the match is to be successful.

We use different forms of left and right brackets to specify assertions of logical relations. The set braces used above -

- denote an abstract event without an asserted ordered (note: this does not mean unordered, it means ``don't care''). composite brackets -

- denote parallels and angular brackets -

- denote precedes. Thus

means

where the symbols used in the assert refers to the matched instance of the pt-chain. The expression

indicates that precedes must hold between each pair of ``adjacent'' matched events where adjacent is defined by the search order after supression of nil events as discussed below. Thus using quotes to distinguish instances of matched patterns, a match of three repetitions would result in the assertion of

Further examples include

The expression:

defines an abstract event

composed of abstract events abstract events

,

,

,

,

,

,

,

,

,

, and

, meeting the following requirements:

For more complicated patterns, we have to consider the possibility of nil results. Thus, we can now write patterns like

which should succeed in the event that the

is matched once,

not at all and

once. The

thus ``successfully'' matches the nil abstract event. How should this match be treated during the assertion of precedes? Initially, we decided to extend the definition of precedes so that, for all events

,

This was uniformly denounced as completely unaesthetic. We therefore now assume that there is a function which strips nil matches from the sequence. Thus in the event that

matches 0 times,

initially finds three events but the middle nil event is stripped and thus ignored by the precedes assertion. What if only nil is left? The event is stripped automatically, and the relation holds true trivially.



next up previous
Next: Other Facilities Up: Ariadne: Modeling Language Previous: P-chain



Joydip Kundu