Re: [abc] On the need for "skip" in tracematches

Result of the IRC discussion:

Consider events A(x), B(y), C(y), the pattern A B C and the trace A(1),
C(2), B(2), C(2). A tracematch should not trigger advice, while it seems
that J-LO deliberately picks out events 1, 3, 4 and matches them. In
J-LO, if you want to achieve the effect of the pattern ABC with
tracematches, you have to encode it explicitly (something like "A and
not C until B and not (A or B) until C").

It seems both designs are better suited for what they are meant for --
J-LO for verification, tracematches (and skip transitions, and negative
bindings) for triggering advice after certain trace patterns.

- P

Eric Bodden wrote:

>Hi all.
>
>I have been discussing on IRC with some of you lately about why you use
>"skip" for tracematches - because interestingly in J-LO we don't, despite
>the fact that we have quite similar semantics.
>
>I still don't really see the use for "skip". Maybe you can help me,
>though...
>
>The guys gave me basically the following:
>
>- Two symbols foo(x) and bar(y) binding x/y.
>- The tracematch foo bar bar =: f(x) b(y) b(y).
>- The trace f(1) b(1) b(2) b(2).
>
>I was told that in your semantics, the TM matches the trace with x/1, y/2.
>
>Converting to LTL, the regex means "at some time f(x) and later at some time
>b(y) and later at some time b(y)", which is:
>
>F( f(x) /\ XF( b(y) /\ XF( b(y) ) ) )
>
>where "F" means "Finally" with semantics delta(F \phi,\pi[i]) =
>delta(\phi,\pi[i]) \/ X delta(\phi,\pi[i]) and "X" means "neXt" with
>semantics delta(X \phi,\pi[i]) = delta(\phi,\pi[i+1]).
>
>In J-LO we do the following, *without* any equivalent to "skip":
>
>We start with the original formula:
>F( f(x) /\ XF( b(y) /\ XF( b(y) ) ) )
>Here x and y are free!
>
>Reading f(1), we apply the semantics, which yields the original formula
>(this is the part quarded by the "X" in the semantics above) and an
>instantiated(!) version of the subformula:
>
>F( f(x) /\ XF( b(y) /\ XF( b(y) ) ) ) --f(1)-->
>F( f(x) /\ XF( b(y) /\ XF( b(y) ) ) ) \/ F( b(y) /\ XF( b(y) ) )
>"instantiated" here means that if the subformula contained an x, this would
>have been bound.
>
>This becomes clear when reading the b(1):
>We apply the semantics to the current formula:
>F( f(x) /\ XF( b(y) /\ XF( b(y) ) ) ) \/ F( b(y) /\ XF( b(y) ) ) --b(1)-->
>F( f(x) /\ XF( b(y) /\ XF( b(y) ) ) ) \/ F( b(y) /\ XF( b(y) ) ) \/ F(
>b(1) )
>Note that in the last subformula, y has been bound to 1 because, at the
>current state, y was 1.
>
>When now reading the first b(2), the following happens:
>F( f(x) /\ XF( b(y) /\ XF( b(y) ) ) ) \/ F( b(y) /\ XF( b(y) ) ) \/ F(
>b(1) ) --b(2)-->
>F( f(x) /\ XF( b(y) /\ XF( b(y) ) ) ) \/ F( b(y) /\ XF( b(y) ) ) \/ F(
>b(1) ) \/ F( b(2) )
>... because the first of the three parts of the three disjuncts does not
>"match", the second does match and produces F( b(2) ) and the third one F(
>b(1) ) does *not* match.
>
>When reading the last b(2) this yields:
>F( f(x) /\ XF( b(y) /\ XF( b(y) ) ) ) \/ F( b(y) /\ XF( b(y) ) ) \/ F(
>b(1) ) \/ F( b(2) ) --b(2)-->
>F( f(x) /\ XF( b(y) /\ XF( b(y) ) ) ) \/ F( b(y) /\ XF( b(y) ) ) \/ F(
>b(1) ) \/ F( b(2) ) \/ <true>
>= <true>
>... because the last disjunct F( b(2) ) goes to delta( b(2), b(2) ) \/
>F(b(2)) and delta(b(2),b(2)) is <true>.
>
>
>So the recipe speking in automata and states is:
>Whenever we leave a state, bind all variables in the regex/formula
>representing this state when moving to this next state, also you remain *as
>well* in the current state with an unbound instance (this is because you
>want to match *all* occurences).
>Whenever taking a loop to / remaining in the same state, leave all variables
>unbound.
>
>
>In tracematches that means:
>You start with in the initial state:
>{f(x) b(y) b(y)}
>
>reading f(1) you get:
>{f(x) b(y) b(y), b(y) b(y)}
>
>reading b(1) you get:
>{f(x) b(y) b(y), b(y) b(y), b(1)}
>
>reading b(2) you get:
>{f(x) b(y) b(y), b(y) b(y), b(2), b(1)}
>
>reading b(2) you get:
>{f(x) b(y) b(y), b(y) b(y), <true>, b(1)}
>= {f(x) b(y) b(y), b(y) b(y), b(1)}
>
>So whenever seeing the state <true> you hit the light and execute the
>tracematch.
>The sets above at any time reflect the set of still not fully matched
>matches.
>
>So what's wrong with this?
>Where did I miss the "skip"?
>
>
>Thanks,
>Eric
>
>--
>Eric Bodden
>Chair I2 for Programming Languages and Program Analysis
>RWTH Aachen University
>
>
>
>
>
>
>
Received on Thu Aug 25 17:09:50 2005