Hi Victor,
On Sun, Apr 28, 2019 at 11:33 PM Victor Khomenko victor.khomenko@newcastle.ac.uk wrote:
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.)
Sorry, The code actually checks that r is Boolean as well, so I really meant to write b[*i:j] is SSI iff ...
However now that you have written this down, I think your interpretation r SSI => r[+] SSI and r[*] SSI is also sound, but I have no proof for this.
[=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
Interesting.
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?
Yes.
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.
No proof.
My intuition is that if all subformulas of a SERE can accept a zero-or-one-letter word, then the SERE should be SI. (This intuition does not really work for the && operator which allow building language that only accept words of length >1, but SI is closed under Boolean operation anyway.)
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?
Because t in "{s}|=>t" recognizes an infinite word, so when interpreted as "s;t", t must be the term that does not accept the empty word.
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,
Yes, I realised that as well yesterday.
but Spot won't accept it (I guess), and generally it seems computationally expensive.
It's not implemented, but it could be.
A sister project of Spot, called Vcsn, actually implements translation of extended-regexs (with complement and another bunch of operators) to DFA. See http://vcsn-sandbox.lrde.epita.fr/notebooks/Doc%20(read%20only)/expression.d...
I think at the level of automata one can simply get an NFA for r, and then delete all arcs from accepting states?
Yes, that would be trivial to implement. I can have a look at this after the ATVA deadline.
The other things you mentioned, like $rose etc. seem to need past modalities? Or you can mix state-based and action-based logics?
I'm not very familiar with those. It seems to me that unless clocks are involved $rose/$fell/$stable only look one step back; so we would only need support for Y(b), and that does not look frightening.
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.