Hi Alexandre,
Currently r[*i:j] is SSI iff j=inf and i<=1 (used
to be i==1 before your mail).
I'm not sure if this is correct, as it implies that r* is ssi if r is ssi, even if r
is not a Boolean, but Dax at al. mentioned that the use of * has to be restricted (but
without giving an example of ssi violation). So it's your word against theirs :-) Do
you have a proof? (I played with Spot a couple of minutes and could not quickly find a
violation, so you may well be right.)
[=i:j] and [->i:j] are sugar on top of ; and
[*i:j], so it follows from those
definitions.
(Spot's AST has no representation of those operators, they only exist in the
parser and printer.)
The situation with [=i:j] and [->i:j] is less boring than that! E.g. b[->1:$] would
be translated to something like (!b[*];b)[+], which is si but not ssi. I've worked out
the cases for these operators as follows (the proofs rely on the magic regex equivalence
(a[*];b)[+];a[*] = (a|b)[*];b[+] which can be checked e.g. here:
https://regex-equality.herokuapp.com/):
Lemma: b[->i:j] is si iff j=0 or (j=$ and i<=1)
j=0: then i=0 and so b[->i..j] = (!b[*];b)[*0] = [*0], so si
j!=0 and j!=$: then b[->i..j] accepts b[*j] but not b[*j+1], so not si
j=$ and i>1: then b[->i..j] accepts b[*i] but not b[*i-1], so not si
j=$ and i=1: then b[->i..j]=(!b[*];b)[+]=[by regex magic]=(!b|b)[*];b[+]=[*];b[+], so
si
j=$ and i=0: then b[->i..j]=(!b[*];b)[*]=[*0]|above line, so si
Lemma: b[=i:j] is si iff j=0 or (j=$ and i<=1)
j=0: then i=0 and so b[=i..j] = (!b[*];b)[*0];!b[*] = !b[*], so si
j!=0 and j!=$: then b[=i..j] accepts b[*j] but not b[*j+1], so not si
j=$ and i>1: then b[=i..j] accepts b[*i] but not b[*i-1], so not si
j=$ and i=1: then b[=i..j] = (!b[*];b)[+];!b[*] = [by regex magic] = (!b|b)[*];b[+];!b[*]
= [*];b[+];!b[*], so si
j=$ and i=0: then b[=i..j] = (!b[*];b)[*]];!b[*] = (e|(!b[*];b)[+]);!b[*] = !b[*] |
(!b[*];b)[+];!b[*] = [due to previous case] = !b[*] | [*];b[+];!b[*] = [*] so si
cl(r) in Dax et al. is the same as {r} in Spot.
But you are not the only one having trouble with closure :-) See
https://gitlab.lrde.epita.fr/spot/spot/issues/242
So, just to confirm, Dax et al.'s cl(), PSL's {}, and Spot's {} are all the
same, aren't they?
I would suggest that at the SERE level the rule for
the n-ary concatenation
r1;r2;r3;...;rn
could be extended so that the entire concatenation is SSI iff each ri is SSI and
at most one of them rejects the empty word.
Wow, that is a nice generalisation! Do you have a proof? I think it will be nicer and
easier to state for the binary ";", and then the n-ary case immediately
follows.
Transposed to {s}|=>t, that rule would state that
{s}|=>t is SSI iff
- s and t are both SSI, and
- s recognizes the empty word
I did some experiments with the online tool, and what you say seems correct, but I
don't understand why there is asymmetry w.r.t. s (but not t) recognising the empty
word - the intuition of s;t seems symmetric?
If we had complementation of SERE, would
first_match(r) be implementable
as r && ((!r);1[+]) ?
I think you meant r && !(r;[+]), which is a nice idea, but Spot won't accept
it (I guess), and generally it seems computationally expensive. I think at the level of
automata one can simply get an NFA for r, and then delete all arcs from accepting
states?
The other things you mentioned, like $rose etc. seem to need past modalities? Or you can
mix state-based and action-based logics?
Generally, "throughout" and "within" are just syntactic sugar, so
should be easy to add. The ?: can be added as syntax sugar, but hopefully one can do
better than that and avoid the exponential blow-up due to repeating A in A&B|!A&C
- this is in fact just a theoretical blow-up, unlikely to happen in practice. The
first_match requires some work with automata, but seems possible. I'd say Spot is just
a few steps away from full alignment with SVA and PSL.
Regards,
Victor.