10 May
2019
10 May
'19
11:32 a.m.
Hi Alexandre,
I've reconsidered first_match, apparently my suggestion to eliminate the exit arcs of
the accepting states in the NFA is wrong, e.g. for (a|a;a) the NFA has two accepting
states with no exit arcs and the transformation does not have any effect, whereas
first_match(a|a;a)=a. I guess the automaton has to be determinised before applying this
transformation (unless you have a better idea).
Regards,
Victor.
-----Original Message-----
From: Alexandre Duret-Lutz <adl(a)lrde.epita.fr>
Sent: Tuesday, May 7, 2019 3:15 PM
To: Victor Khomenko <victor.khomenko(a)newcastle.ac.uk>
Cc: spot <spot(a)lrde.epita.fr>
Subject: Re: [Spot] syntactic stutter-invariance
On Tue, May 7, 2019 at 10:41 AM Victor Khomenko
<victor.khomenko(a)newcastle.ac.uk> wrote:
yet.
That would not work when B=[*0], because A:[*0] = false. However if you
assume that B has at least one letter, I believe that works.
In the case of "a ##[i:j] b" if i>0 Spot actually rewrite this as
"a;[*i-1:j-1];b"
without using ":".
I have machine proofs for most of these,
including the proof that K;L is si
if both K and L are si and either K is prefix-closed or L is suffix-closed.
Interesting.
a ##[i:j]
b = a:([*i:j];b)
Do you know whether A:(B;C)=(A:B);C ? I'd guess yes, but have no proof
I'd add:
first_match(L+)= first_match(L) [* is already handled by your rules]
So the general case is first_match(L[*i:j]) = first_match(L[*i]).
And if L is boolean, this becomes just L[*i].
first_match(K;L)= first_match(K) if the
empty word is in L
first_match(K;L)= K;first_match(L) [correct?? It would then
imply the above rule]
That last rule doesn't look right to me.
first_match(a[*];b[*]) = [*0]
a[*];first_match(b[*]) = a[*]
Maybe that rule works if all words accepted by K have the same length.
(So for an easier rule, if K is Boolean).
So to summarize, assuming b is Boolean, e accepts empty words, and f, and
g are anything else:
first_match(b[*i..j]) = b[*i]
first_match(f[*i..j]) = first_match(f[*i])
first_match(b;f) = b;first_match(f)
first_match(f;g[*i..j]) = first_match(f;g[*i])
first_match(f;e) = first_match(f)
It's not clear that any of those is going to improve the output
--
Alexandre Duret-Lutz