Spot issueshttps://gitlab.lrde.epita.fr/spot/spot/-/issues2020-07-22T21:33:58+02:00https://gitlab.lrde.epita.fr/spot/spot/-/issues/385ltl2tgba -G cases that can be improved2020-07-22T21:33:58+02:00Alexandre Duret-Lutzltl2tgba -G cases that can be improvedOn Sun, Apr 21, 2019 at 9:46 PM Juraj Major <major@fi.muni.cz> wrote:
>
> Hi Alexandre,
>
> Jan asked me to send you some formulae from LTL(F,G,X) where Delag
> produces smaller automata than ltl2tgba. I use Spot 2.7.3 and call
> `ltl2tgba -G 'formula'`.
[...]
> GFX((e & XXXa) -> (e & X!d)) (ltl2tgba 2 states vs. Delag 1 state)<br/>
> G(Gc | Fa | F!G(c | Ge)) (6 vs. 3)
These looks like cases where Spot is simply not applying rewritings
like GF(a | b) = GF(a)|GF(b). Those rules would make sense for -G,
but they usually don't make sense when building other types of
automata, so I haven't worked on those yet. It's unfortunate that the
rewriting rules in Spot is not very modular.
> Ge | XGF(Ge & X(c & Fd)) (5 vs. 2) <br/>
> G!GXXe -> GF(b & c & Gc) - this one is interesting, because ltl2tgba
> -DG produces smaller automaton (2 states) then ltl2tgba -G (3 states).
> However, Delag still wins with 1 state
These are cases where Spot is missing the rule GF(a & Gb) = GFa & FGb
Because GF(b & c & Gc) is not a GF(guarantee), it's determinized via
Safra if -D is given, and this is not tried without -D. The
non-deterministic automaton output by -G for GF(b & c & Gc) is a
2-state incomplete automaton and deterministic automaton from -G -D is
a 2-state complete automaton, so the incompleteness is what makes the
difference during the product, as you need complete automata to make a
disjunction.
> G!(Gd & (c | Fb)) (4 vs. 2)
Running delag with "-f ltl2tgba" will output the same automaton as
ltl2tgba, so this is a case where the fallback translator used by
delag (I'm not sure what that is) does a better job. In their paper,
they used Spot as fallback I think, but it seems they are now using
something else.
The tool ltl2da, distributed with Owl, also produces a 2-state (but
nicer IMHO) TELA for this.
> XF(F(Gc & Xb) -> a) (6 vs. 3)
Again we are missing whatever rule needed to reduce this to:
GF(!c) | FG(!b) | XF(a)
(in which case its 3 states if deterministic or 2 if non-deterministic)
> From the genltl's patterns, there's a --sejk-f pattern where Delag
> performs better than Spot but those are not LTL(F,G,X) formulae.
I'm not sure how that one works. Look like some kind of suspension
would be useful.
So it seems a large part of these issues would be solved by LTL rewritings.On Sun, Apr 21, 2019 at 9:46 PM Juraj Major <major@fi.muni.cz> wrote:
>
> Hi Alexandre,
>
> Jan asked me to send you some formulae from LTL(F,G,X) where Delag
> produces smaller automata than ltl2tgba. I use Spot 2.7.3 and call
> `ltl2tgba -G 'formula'`.
[...]
> GFX((e & XXXa) -> (e & X!d)) (ltl2tgba 2 states vs. Delag 1 state)<br/>
> G(Gc | Fa | F!G(c | Ge)) (6 vs. 3)
These looks like cases where Spot is simply not applying rewritings
like GF(a | b) = GF(a)|GF(b). Those rules would make sense for -G,
but they usually don't make sense when building other types of
automata, so I haven't worked on those yet. It's unfortunate that the
rewriting rules in Spot is not very modular.
> Ge | XGF(Ge & X(c & Fd)) (5 vs. 2) <br/>
> G!GXXe -> GF(b & c & Gc) - this one is interesting, because ltl2tgba
> -DG produces smaller automaton (2 states) then ltl2tgba -G (3 states).
> However, Delag still wins with 1 state
These are cases where Spot is missing the rule GF(a & Gb) = GFa & FGb
Because GF(b & c & Gc) is not a GF(guarantee), it's determinized via
Safra if -D is given, and this is not tried without -D. The
non-deterministic automaton output by -G for GF(b & c & Gc) is a
2-state incomplete automaton and deterministic automaton from -G -D is
a 2-state complete automaton, so the incompleteness is what makes the
difference during the product, as you need complete automata to make a
disjunction.
> G!(Gd & (c | Fb)) (4 vs. 2)
Running delag with "-f ltl2tgba" will output the same automaton as
ltl2tgba, so this is a case where the fallback translator used by
delag (I'm not sure what that is) does a better job. In their paper,
they used Spot as fallback I think, but it seems they are now using
something else.
The tool ltl2da, distributed with Owl, also produces a 2-state (but
nicer IMHO) TELA for this.
> XF(F(Gc & Xb) -> a) (6 vs. 3)
Again we are missing whatever rule needed to reduce this to:
GF(!c) | FG(!b) | XF(a)
(in which case its 3 states if deterministic or 2 if non-deterministic)
> From the genltl's patterns, there's a --sejk-f pattern where Delag
> performs better than Spot but those are not LTL(F,G,X) formulae.
I'm not sure how that one works. Look like some kind of suspension
would be useful.
So it seems a large part of these issues would be solved by LTL rewritings.https://gitlab.lrde.epita.fr/spot/spot/-/issues/354new LTL simplification rules2018-06-05T10:11:37+02:00Alexandre Duret-Lutznew LTL simplification rulesthe following two rules generalize the two rules in the rightmost column of section 5.4.2
```
f M u = Ff & u
f W e = Gf | e
```
the following two rules are new
```
q R Xf = X(q R f)
q U Xf = X(q U f)
```the following two rules generalize the two rules in the rightmost column of section 5.4.2
```
f M u = Ff & u
f W e = Gf | e
```
the following two rules are new
```
q R Xf = X(q R f)
q U Xf = X(q U f)
```https://gitlab.lrde.epita.fr/spot/spot/-/issues/242fixing the closure operator to better match the PSL standard2017-04-28T11:40:55+02:00Alexandre Duret-Lutzfixing the closure operator to better match the PSL standardAs noted in [tl.pdf](http://spot.lrde.epita.fr/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 match `r` (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 matching `r`
- `cl{r}` is sugar for `{r}|{r}!`: it accepts words that have one prefix matching `r` or such that all prefixes can be extended to match `r`
I suggest that without changing `{r}`, we already include `cl{r}` inAs noted in [tl.pdf](http://spot.lrde.epita.fr/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 match `r` (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 matching `r`
- `cl{r}` is sugar for `{r}|{r}!`: it accepts words that have one prefix matching `r` or such that all prefixes can be extended to match `r`
I suggest that without changing `{r}`, we already include `cl{r}` inspot 2.3.2Alexandre Duret-LutzAlexandre Duret-Lutzhttps://gitlab.lrde.epita.fr/spot/spot/-/issues/185missing LTL simplification2017-11-15T14:34:33+01:00Alexandre Duret-Lutzmissing LTL simplification`ltl2tgba 'GF(a && GF(b))'` has two states, while the equivalent `ltl2tgba 'G(Fa && Fb)'` has only one.`ltl2tgba 'GF(a && GF(b))'` has two states, while the equivalent `ltl2tgba 'G(Fa && Fb)'` has only one.https://gitlab.lrde.epita.fr/spot/spot/-/issues/12even more LTL simplification for GF formulas2017-11-15T14:34:27+01:00Alexandre Duret-Lutzeven more LTL simplification for GF formulaswe could implement those rules:
```
GF(a & Fb) = G(Fa & Fb)
GF(a & XXXXXFb) = G(Fa & Fb)
GF(a & eventual) = G(Fa & eventual)
```we could implement those rules:
```
GF(a & Fb) = G(Fa & Fb)
GF(a & XXXXXFb) = G(Fa & Fb)
GF(a & eventual) = G(Fa & eventual)
```https://gitlab.lrde.epita.fr/spot/spot/-/issues/11more LTL simplifications for GF formulas2017-11-15T14:34:27+01:00Alexandre Duret-Lutzmore LTL simplifications for GF formulas`(GF(a)&GF(b)) | (GF(c)&GF(d))` is equivalent to `(GF(a|c) & GF(a|d) & GF(b|c) & GF (b|d))`.
It's a bigger formula, but it can be translated into a one-state automaton.
> Jan Strejcek:
>> ADL:
>> we like to simplify `GFa | GFb` as
>> `GF(a|b)` because `GF(a|b)` is easily translated as a deterministic
>> automaton. In the same way, `(GFa & GFb) | (GFc & GFd)`, which is
>> currently translated as a non-deterministic automaton, could be
>> rewritten as `GF(a|c) & GF(a|d) & GF(b|c) & GF(b|d)` which will be
>> translated as a deterministic automaton. Can this kind of rewriting
>> be generalized?
>
> I think I can provide a (partial) answer. The only
> non-obvious rule we have to add is the following:
>
> for pure eventually formulae m1,m2 (roughly speaking, the formulae starting
> with F), the following
> equivalence holds: G m1 | G m2 <=> G (m1|m2)
>
> With this rule and the standard rules
>
> G f1 & G f2 <=> G (f1&f2)
> distributivity: (A&B) | (C&D) <=> (A|C) & (A|D) & (B|C) & (B|D)
> or simply A | (C&D) <=> (A|C) & (A|D) applied twice
> F f1 | F f2 <=> F (f1|f2)
>
> one can transform `(GFa & GFb) | (GFc & GFd)` into `G( F(a|c) & F(a|d) & F(b|c) & F(b|d))`,
> which is enough to get determinstic automaton. A more interesting
> question may be "How to detect the situation when such rules should be
> applied". This especially applies to the distributivity as all other rules
> simply replace two modalities with one, which has usually positive effect on
> the translation and therefore the rules should be applied by default. I can
> imagine that distributivity will be applied only with `--deter` option and
> only to propagate disjunction downwards the syntactic tree (as disjunction
> is often a source of nondeterminism).
> Jan:
>> ADL:
>> It isn't as straightforward as it seems. For instance
>> adding only the `G(e1)|G(e2) = G(e1|e2)` without distribution
>> can be a serious regression:
>>
>> `G(Fa & Fb) | G(Fc & Fd)`: 3 states
>> `G((Fa & Fb) | (Fc & Fd))`: 15 states
>> `G(F(a | c) & F(a | d) & F(b | c) & F(b | d))`: 1 state
>>
>> I think for this to work we have to guarantee that all pure
>> eventualities will be rewritten as F(something).
>
> I guess that you want to say that each pure eventuality formula can be
> rewritten into a conjunction of F(something) formulae. I'm afraid this
> doesn't hold. For example, `GFa R Fb` is a pure eventuality formula
> equivalent to `GFa | GFb`... Hmm, but there is no problem in this
> particular case. I have to think about it with a fresh mind.
`(GF(a)&GF(b)) | (GF(c)&GF(d))` is equivalent to `(GF(a|c) & GF(a|d) & GF(b|c) & GF (b|d))`.
It's a bigger formula, but it can be translated into a one-state automaton.
> Jan Strejcek:
>> ADL:
>> we like to simplify `GFa | GFb` as
>> `GF(a|b)` because `GF(a|b)` is easily translated as a deterministic
>> automaton. In the same way, `(GFa & GFb) | (GFc & GFd)`, which is
>> currently translated as a non-deterministic automaton, could be
>> rewritten as `GF(a|c) & GF(a|d) & GF(b|c) & GF(b|d)` which will be
>> translated as a deterministic automaton. Can this kind of rewriting
>> be generalized?
>
> I think I can provide a (partial) answer. The only
> non-obvious rule we have to add is the following:
>
> for pure eventually formulae m1,m2 (roughly speaking, the formulae starting
> with F), the following
> equivalence holds: G m1 | G m2 <=> G (m1|m2)
>
> With this rule and the standard rules
>
> G f1 & G f2 <=> G (f1&f2)
> distributivity: (A&B) | (C&D) <=> (A|C) & (A|D) & (B|C) & (B|D)
> or simply A | (C&D) <=> (A|C) & (A|D) applied twice
> F f1 | F f2 <=> F (f1|f2)
>
> one can transform `(GFa & GFb) | (GFc & GFd)` into `G( F(a|c) & F(a|d) & F(b|c) & F(b|d))`,
> which is enough to get determinstic automaton. A more interesting
> question may be "How to detect the situation when such rules should be
> applied". This especially applies to the distributivity as all other rules
> simply replace two modalities with one, which has usually positive effect on
> the translation and therefore the rules should be applied by default. I can
> imagine that distributivity will be applied only with `--deter` option and
> only to propagate disjunction downwards the syntactic tree (as disjunction
> is often a source of nondeterminism).
> Jan:
>> ADL:
>> It isn't as straightforward as it seems. For instance
>> adding only the `G(e1)|G(e2) = G(e1|e2)` without distribution
>> can be a serious regression:
>>
>> `G(Fa & Fb) | G(Fc & Fd)`: 3 states
>> `G((Fa & Fb) | (Fc & Fd))`: 15 states
>> `G(F(a | c) & F(a | d) & F(b | c) & F(b | d))`: 1 state
>>
>> I think for this to work we have to guarantee that all pure
>> eventualities will be rewritten as F(something).
>
> I guess that you want to say that each pure eventuality formula can be
> rewritten into a conjunction of F(something) formulae. I'm afraid this
> doesn't hold. For example, `GFa R Fb` is a pure eventuality formula
> equivalent to `GFa | GFb`... Hmm, but there is no problem in this
> particular case. I have to think about it with a fresh mind.
https://gitlab.lrde.epita.fr/spot/spot/-/issues/3simplify {r;1} as {r}2018-05-07T17:30:13+02:00Alexandre Duret-Lutzsimplify {r;1} as {r}Apparently we do not have the following simplification rules for SERE
{r;1} = {r}
!{r;1} = !{r} Apparently we do not have the following simplification rules for SERE
{r;1} = {r}
!{r;1} = !{r} https://gitlab.lrde.epita.fr/spot/spot/-/issues/2find a way to reduce {b*;r} = (b W r) when r is satisfiable2017-11-15T14:34:27+01:00Alexandre Duret-Lutzfind a way to reduce {b*;r} = (b W r) when r is satisfiableCommit 11568666 removed the following rules
{b*;r} = b W r
!{b*;r} = !b M !{r}
because it is only true when `r` is satisifiable, but the code did not check that.
Currently the only way we have to ensure that `r` is satisifiable is to translate it into an automaton. Doing so seems unlikely to be efficient.
But there are many formulas that we can tell as satisfiable without even translation: for instance any SERE that do not involve `&`, `&&`, and `false` is satisfiable. So maybe each formula could have a Boolean property that tells when it is trivially satisfiable.Commit 11568666 removed the following rules
{b*;r} = b W r
!{b*;r} = !b M !{r}
because it is only true when `r` is satisifiable, but the code did not check that.
Currently the only way we have to ensure that `r` is satisifiable is to translate it into an automaton. Doing so seems unlikely to be efficient.
But there are many formulas that we can tell as satisfiable without even translation: for instance any SERE that do not involve `&`, `&&`, and `false` is satisfiable. So maybe each formula could have a Boolean property that tells when it is trivially satisfiable.