fixing the closure operator to better match the PSL standard
As noted in tl.pdf, the definition of {r}
we currently use in Spot comes from the cl(r)
operator of Dax et al. (ATVA'09).
The definition of {r}!
corresponds to the PSL for r!
. We should change {r}
to match the definition of r
in PSL, so that {r}!
and {r}
would form a strong/weak pair as in PSL. I would use cl{r}
do denote the old semantics of {r}
, i.e., the one from Dax et al. (I'm favoring cl{r}
over cl(r)
so that SERE always appear between braces in formulas.)
With these changes we would have:
-
{r}
accepts words such that all prefixes can be extended to matchr
(in other words, this works like a monitor) -
{r}!
is (already) sugar for{r}<>->1
and accepts all words that have at least one prefix matchingr
-
cl{r}
is sugar for{r}|{r}!
: it accepts words that have one prefix matchingr
or such that all prefixes can be extended to matchr
I suggest that without changing {r}
, we already include cl{r}
in