Re: [abc-users] Tracematch and "if(thisJoinPoint.getThis() != aParticularObject)"

From: Pavel Avgustinov <pavel.avgustinov_at_magd.ox.ac.uk>
Date: Wed, 23 Apr 2008 22:26:49 +0100

Hi Paul,

> /** Writers entered concurrently but between them can exit zero or more
> objects except w1 and w2 **/
> enterWrite1 exitWriteAnother* enterWrite2
>
I'm slightly confused about your choice of pattern. Why do you have the
fragment "exitWriteAnother*"? Since that symbol binds none of the
tracematch variables, and you intend it to match exit events that bind
something other than w1 and w2, I believe the correct way of achieving
this is simply having the pattern "enterWrite1 enterWrite2", which will
allow zero or more objects distinct from w1 and w2 to exit in between
the two events...

> My finally intention is to avoid that w1.exitWrite(); matches with
> exitWriteAnother because I want to express that "exitWriteAnother" is
> any object other except w1 and w2. The object bounded in
> exitWriteAnother symbol is not important because this symbol can
> happened several times(zero or more) and I do not want to bind these
> variables.
>
> To differentiate between the "exitWrite" and "exitWriteAnother" symbols,
> I tried modifying the "exitWriteAnother" symbol this way:
>
> sym exitWriteAnother after:
> call (* Database.exitWrite()) &&
> if(thisJoinPoint.getThis() != w1) &&
> if(thisJoinPoint.getThis() != w2);
>
> But when I compile this tracematch, I get the following errors:
> Local w1 is not bound by this symbol so it cannot be used within.
> Local w2 is not bound by this symbol so it cannot be used within.
>
Yes... unfortunately you cannot refer to arbitrary tracematch formals
that aren't bound by the current symbols. This is a known limitation
caused by complications such a feature would entail: The semantics of
matching a pattern become ill-defined.

Currently there is no way of expressing the above; however we have
noticed that it is often desirable to be able to do something like this,
particular in the context of concurrency patterns. I plan to introduce a
new feature (tentatively named "distinctness annotations") that would
allow you to do something very similar. My idea is to allow statements
like this in a tracematch body:

    distinct w1, w2, w3;

Given such a statement, the matching machinery would guarantee that
these formal parameters always bind to distinct objects. Unfortunately
things are rather hectic at the moment so I don't know when I'll be able
to complete the implementation of this feature, but it looks like you
don't need it for this particular pattern (see my comment above).

> In other low level, I need an automaton state without free variables
> than accesses previously bounded variables. Thus, I can add the
> constraint "X != v", where v is a free variable previously bounded.
>
> Can you help me?
>
As I mentioned, this is unsupported due to the formal semantics of
matching [all but the most trivial examples result in undefined matching
behaviour]. What exactly are you trying to do? Maybe we can help in some
other way...

> Now, if I can have an automaton state without free variables than
> accesses previously bounded variables. What's happened with the
> following sequence of events?
>
> w1.exitWrite();
> w2.exitWrite();
> w3.exitWrite();
>
> In this sequence, which are symbols matched with w1.exitWrite(); event?
>
> 1) exitWrite1
> 2) exitWriteAnother
>
> Possible answers:
> 1) yes.
> 2) I do not know because it depends on:
> 2.1) if the exitWrite1 symbol is matched before exitWriteAnother.
> 2.2) if the exitWriteAnother symbol is matched before exitWrite1.
>
This is precisely the kind of issue that crops up if you allow
references to arbitrary tracematch variables from symbols that don't
bind them... we have no good answer to these questions, which is why we
do not allow such references.

Cheers,
- Pavel
Received on Wed Apr 23 2008 - 22:29:44 BST

This archive was generated by hypermail 2.2.0 : Wed Apr 23 2008 - 23:00:11 BST