Re: [abc] Tracematch-Question: Symbols both negated and unnegated

Eric Bodden wrote:

>Hmmm, I could really have seen this before :-) Looks like a sufficiently
>equivalent version. Thanks!
>
>Anyway, what is the general behaviour if the a state on the trace is matched
>by "the last symbol on a tracematch" and at the same time a symbol which is
>not contained in the tracematch? On the one hand, this should trigger an
>advice, because the state is matched by the last symbol of the tm, but on
>the other hand the fact that it is also matched by a symbol which is not
>contained should prevent the advice from executing.
>
>
What I think of as "the natural thing" happens. Any outgoing transitions
in the NFA that are marked with one of the two symbols that match the
event are 'triggered'. In the case of the symbol that doesn't occur in
the tracematch, this is 'no transition'. In the case of the symbol that
does occur, there are transitions which happen, depending on whether
there are "source" states of such transitions which are currently not
labelled with a false constraint. Also, all "skips" would match with the
corresponding negative bindings, causing the corresponding transitions
to be triggered.

This, writing 'a' for the symbol that matches the current event and
occurs in the tracematch and 'b' for the symbol that matches and doesn't
occur, after the event happens all possible transitions labelled 'a'
have been taken, and the respective bindings checked/recorded. All skip
transitions have been triggered, with the respective negative bindings
checked/recorded.

The way to think about declaring symbols in the tracematch that aren't
actually used in the pattern is simply that they prevent the respective
events from being filtered out of the trace before matching. Thus, if we
have two identical symbols A and A', one of which occurs in the pattern
and one of which doesn't, there will be no change in behaviour from
omitting the symbol that doesn't occur in the tracematch.

In the case where two symbols A and B (where B doesn't occur) are not
identical but not disjoint, you can think of B having no effect whenever
A also matches, and having the effect of keeping extra events in the
relevant trace when no other declared symbol other than B matches (thus
causing matching failures, if appropriate).

(Sorry if this doesn't make sense, it's early and I would much rather
try to explain this with a whiteboard... Do tell me if I can clarify any
of it further.)

- P
Received on Sun Aug 28 09:24:49 2005