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

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