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

Eric Bodden wrote:
> Pavel Avgustinov wrote:
>> Correct me if I'm wrong, but it seems to me that the regular pattern
>> "a c* b" would be equivalent to the above, provided that b() and c()
>> are disjoint. (If there are events matched by both b() and c(),
>> define symbols b'() := b() && !c() and c'() := c() && !b(), and use
>> the pattern "a c'* b'".)

Hi again. I was wondering, if this is really equivalent, since it does
actually not express that c(y) should *not* hold when b occurs. When
expressing b as b'() := b() && !c(), this would lead to a symbol declaration
with !c(y) binding y under negation, which is not allowed AFAIK...

Eric

-- 
Eric Bodden
Chair I2 for Programming Languages and Program Analysis
RWTH Aachen University