Spot issueshttps://gitlab.lre.epita.fr/spot/spot/-/issues2024-03-14T12:20:21+01:00https://gitlab.lre.epita.fr/spot/spot/-/issues/564improving inclusion checks2024-03-14T12:20:21+01:00Alexandre Duret-Lutzimproving inclusion checksI'm creating this issue to keep track of ideas that we could use to improve `contains()` as I risk to forget about this otherwise.
@pierreganty sent the following example where `contains_forq()` is much more efficient than the default c...I'm creating this issue to keep track of ideas that we could use to improve `contains()` as I risk to forget about this otherwise.
@pierreganty sent the following example where `contains_forq()` is much more efficient than the default complementation-based implementation of the inclusion check.
[incl.zip](/uploads/c655d09641b398ba54c076135765ada0/incl.zip)
The tests to run on the above example are:
- (A⊆B def.) ```SPOT_CONTAINMENT_CHECK=default autfilt planning_robotic_robustness_3600_A.bs.baccmin --included-in=planning_robotic_robustness_3600_B.bs -c```
- (A⊆B forq) ```SPOT_CONTAINMENT_CHECK=forq autfilt planning_robotic_robustness_3600_A.bs.baccmin --included-in=planning_robotic_robustness_3600_B.bs -c```
In the following, we refer to the two automata as A and B.
Times measured by Pierre & myself using the development version of Spot on our computers are given below for reference
| operation | Pierre | Alexandre |
| --------- | ------ | ------------------ |
| A⊆B def. | 3530 s | Out-of-mem (>17GB) |
| A⊆B forq | 62 s | 25 s |
Those automata are quire large, so not easy to inspect. However one can notice they use 5 atomic propositions, but they don't use all possible valuations of those. In particular A uses only 8 disjoint labels:
```sh
% sed -n 's/^\[\(.*\)\].*/\1/p' \
planning_robotic_robustness_3600_A.bs.baccmin | sort -u
!0&!1&!2&!3&4
!0&!1&!2&3&!4
!0&!1&2&!3&!4
!0&1&!2&!3&!4
0&!1&!2&!3&4
0&!1&!2&3&!4
0&!1&2&!3&!4
0&1&!2&!3&!4
% sed -n 's/^\[\(.*\)\].*/\1/p' \
planning_robotic_robustness_3600_B.bs| sort -u
!0
!0&!1 | !0&2 | !0&3 | !0&4
!0&1 | !0&!2 | !0&3 | !0&4
!0&1 | !0&2 | !0&!3 | !0&4
!0&1 | !0&2 | !0&3 | !0&!4
!0&!1&!2&!3&4
!0&!1&!2&3&!4
!0&!1&2&!3&!4
!0&1&!2&!3&!4
0&!1&!2&!3&4
0&!1&!2&3&!4
0&!1&2&!3&!4
0&1&!2&!3&!4
!1&!2&!3&4
!1&!2&3&!4
!1&2&!3&!4
1&!2&!3&!4
```
So one idea would be to relabel these two automata with only 3 atomic propositions (enough to represent the 2^3=8 labels of A, and restricting the labels of B to only those compatible with that) before checking the inclusion.
Another thing we can notice is that in A, atomic propositions {1,2,3,4} are mutually exclusive. So in this case we can restirct B to only
use labels where those propositions are mutually exclusive as follows. Let's call the new automaton C.
```sh
% autfilt --exclusive-ap=l1,l2,l3,l4 \
planning_robotic_robustness_3600_B.bs > \
planning_robotic_robustness_3600_C.bs
% sed -n 's/^\[\(.*\)\].*/\1/p' \
planning_robotic_robustness_3600_C.bs | sort -u
!0&!1&!2&!3 | !0&!1&!2&!4 | !0&!1&!3&!4
!0&!1&!2&!3 | !0&!1&!2&!4 | !0&!1&!3&!4 | !0&!2&!3&!4
!0&!1&!2&!3 | !0&!1&!2&!4 | !0&!2&!3&!4
!0&!1&!2&!3 | !0&!1&!3&!4 | !0&!2&!3&!4
!0&!1&!2&!3&4
!0&!1&!2&3&!4
!0&!1&2&!3&!4
!0&1&!2&!3&!4
0&!1&!2&!3&4
0&!1&!2&3&!4
0&!1&2&!3&!4
0&1&!2&!3&!4
!0&!1&!2&!4 | !0&!1&!3&!4 | !0&!2&!3&!4
!1&!2&!3&4
!1&!2&3&!4
!1&2&!3&!4
1&!2&!3&!4
```
Or we can also try to simplify those labels based on the fact that we know that the proposition are mutually exclusive in A. Let D be that new automaton:
```
% autfilt --exclusive-ap=l1,l2,l3,l4 \
--simplify-exclusive-ap \
planning_robotic_robustness_3600_B.bs > \
planning_robotic_robustness_3600_D.bs
% sed -n 's/^\[\(.*\)\].*/\1/p' \
planning_robotic_robustness_3600_D.bs | sort -u
!0
!0&!1
!0&1
0&1
!0&!2
!0&2
0&2
!0&!3
!0&3
0&3
!0&!4
!0&4
0&4
1
2
3
4
```
Here are some measurements with the new automata
| command | Alexandre |
| -------- | ---------- |
| A⊆C def. | 509 s |
| A⊆C forq | 30 s |
| A⊆D def. | Out-of-mem |
| A⊆D forq | 30 s |
So restricting the labels of B (as in C) does improve the default approach. It worsens the forq approach, and I'm not sure why. Another remark is that in the case of `A⊆C`, where the labels used in both automata are all minterms, `contains_forq()` does not need to use `bdd_implies` to check compatibility of labels, a constant-time equality check would be faster.
Pierre points out that https://github.com/ravenbeutner/automata-benchmarks-from-hyperproperties/tree/main/planning has smaller instances which are supposed to be generated from nusmv models in https://github.com/HyperQB/HyperQB/tree/master/cases_bmc/
tacas_robotic. Compared to the original, the files included in the current issue have just been simplified with `autfilt --small`, and A has been preprocessed to reduce the number of accepting transitions (an important factor in the forq approach). So probably we can learn more by working on smaller instances.https://gitlab.lre.epita.fr/spot/spot/-/issues/529ltlsynt trivial symplifications2023-11-18T22:38:56+01:00Alexandre Duret-Lutzltlsynt trivial symplificationsThere are a few trivial simplification we could do in ltlsynt to reduce the number of atomic propositions it has to deal with. I'm pretty sure I've seen at least the first one in some Strix paper, but I cannot point to the correct paper...There are a few trivial simplification we could do in ltlsynt to reduce the number of atomic propositions it has to deal with. I'm pretty sure I've seen at least the first one in some Strix paper, but I cannot point to the correct paper at the moment.
- If the specification φ contains an output atomic proposition α that always has the same polarity, then we can simply decide that this is the value our controller will always output, and we can simplify φ accordingly.
- If the specification contains a pattern such a G(α ↔ β) where α is an output atomic proposition, and β is another atomic proposition, then we can remove this pattern by replacing α by β, and then create the output signal for α only while encoding the controller.
The later idea can also work with G(α XOR β). I'm thinking that maybe the synthesis_info structure should have an extra field that maps atomic proposition to constants (to implement the first point) or to another literal (second point).https://gitlab.lre.epita.fr/spot/spot/-/issues/527ratexp_trad_visitor handling of one_star2023-02-09T11:28:14+01:00Alexandre Duret-Lutzratexp_trad_visitor handling of one_star`[*]` a.k.a. `one_star()` is the PSL equivalent of Σ*. Maybe `next_to_concat()` could encode this as `bddtrue`? This would allow formula like `(α∧β)∨(¬α∧[*])` to be simplified as `β∨(¬α∧[*])`. I'm just a bit afraid that several place...`[*]` a.k.a. `one_star()` is the PSL equivalent of Σ*. Maybe `next_to_concat()` could encode this as `bddtrue`? This would allow formula like `(α∧β)∨(¬α∧[*])` to be simplified as `β∨(¬α∧[*])`. I'm just a bit afraid that several places that expect a next variable will have to be adjusted to interpret `bddtrue` as `[*]`.https://gitlab.lre.epita.fr/spot/spot/-/issues/503Philipp's idea for improving the speed of Mealy minimization2022-08-07T13:04:04+02:00Alexandre Duret-LutzPhilipp's idea for improving the speed of Mealy minimizationUse the preprocessing of SAT (compute the variation matrix) to detect the potential number of state a reduction might remove, and skip any reduction (BWOA or SAT) in case the number of state to gain is negligible.Use the preprocessing of SAT (compute the variation matrix) to detect the potential number of state a reduction might remove, and skip any reduction (BWOA or SAT) in case the number of state to gain is negligible.https://gitlab.lre.epita.fr/spot/spot/-/issues/494relabel automata to reduce atomic propositions2022-10-11T09:38:51+02:00Alexandre Duret-Lutzrelabel automata to reduce atomic propositionsJérôme Dubois tells me that he is working with a benchmark of automata where the edges have complex Boolean formulas, but the automaton only uses a handful of different formulas. This is causing slowdowns in algorithms like `simulation(...Jérôme Dubois tells me that he is working with a benchmark of automata where the edges have complex Boolean formulas, but the automaton only uses a handful of different formulas. This is causing slowdowns in algorithms like `simulation()` that are sensible to the BDD sizes. In his case it would make sense to first relabel the entire automaton with shorter formulas, apply the simulation, and then relabel the results. It's not clear how to do that in practice, but that would be a useful function, similar to what we do for Boolean subformulas during LTL translation.https://gitlab.lre.epita.fr/spot/spot/-/issues/493use original-classes in simulation2022-01-05T13:54:52+01:00Alexandre Duret-Lutzuse original-classes in simulationNow that `tgba_determinize()` can produce automata with the `original-classes` property (see 20bcc216a09dafddf930e58a0bde385f0625311a), can we use it somehow to speedup `simulation()`?Now that `tgba_determinize()` can produce automata with the `original-classes` property (see 20bcc216a09dafddf930e58a0bde385f0625311a), can we use it somehow to speedup `simulation()`?https://gitlab.lre.epita.fr/spot/spot/-/issues/408partial (co-)Büchi realizability2020-05-07T00:14:56+02:00Alexandre Duret-Lutzpartial (co-)Büchi realizabilityTaking the same automaton as in #407, let's assume that the condition is not α="(Fin(0)|Fin(1)|Fin(2)) | Inf(3)" but some more complex formula that has α as a subformula. You may also imagine more colors used in the automaton and in the...Taking the same automaton as in #407, let's assume that the condition is not α="(Fin(0)|Fin(1)|Fin(2)) | Inf(3)" but some more complex formula that has α as a subformula. You may also imagine more colors used in the automaton and in the rest of the conditions.
We can still discover that α is Büchi-realizable and replace it with `Inf(x)`. That would work like partial-degeneralization, but for (co-)Büchi-realizability.https://gitlab.lre.epita.fr/spot/spot/-/issues/389LTL->UVW2019-06-06T11:34:05+02:00Alexandre Duret-LutzLTL->UVWThe fragment is defined in http://motesy.cs.uni-bremen.de/pdfs/atva2018.pdf
Is our translation able to produce UVW? (via dualization probably).
Should we add the fragment and the translation?The fragment is defined in http://motesy.cs.uni-bremen.de/pdfs/atva2018.pdf
Is our translation able to produce UVW? (via dualization probably).
Should we add the fragment and the translation?https://gitlab.lre.epita.fr/spot/spot/-/issues/350improve product() when one argument is a weak automaton2018-05-24T07:12:36+02:00Alexandre Duret-Lutzimprove product() when one argument is a weak automatonWhen one argument of `product()` is weak, we can teach `product()` to produce a simpler acceptance condition than what it is doing now.
- `product(non-weak, non-weak)`: standard product
- `product(weak, non-weak)` or `product(non-weak, ...When one argument of `product()` is weak, we can teach `product()` to produce a simpler acceptance condition than what it is doing now.
- `product(non-weak, non-weak)`: standard product
- `product(weak, non-weak)` or `product(non-weak, non-weak)`: use the non-weak acceptance for the output
- `product(weak, weak)`: use a weak acceptance for the outputhttps://gitlab.lre.epita.fr/spot/spot/-/issues/347improve wdba minimization2018-06-05T21:18:28+02:00Alexandre Duret-Lutzimprove wdba minimizationCurrently we do the construction as explained in the Dax et al. paper:
1. from the input A, we build a powerset P.
2. for each SCC C of P we compute a word that we replay on A, and use that to decide if C should be accepting or rejec...Currently we do the construction as explained in the Dax et al. paper:
1. from the input A, we build a powerset P.
2. for each SCC C of P we compute a word that we replay on A, and use that to decide if C should be accepting or rejecting
With this, we get a new P' with SCC tagged as accepting or rejecting. It may accept more words if we flagged a whole SCC as accepting when it was only partially accepting in A. It may reject additional words if we flagged a whole SCC as rejecting when it is partially accepting in A. So we need this double inclusion check to be sure that P' is equivalent to A.
We could probably improve this by building the product P*A and surveying the SCCs of that product. For each accepting SCC of P*A, we declare that the projection on P is accepting. This way, P' necessarily recognizes a superset of the language of A, and only one inclusion check is needed.https://gitlab.lre.epita.fr/spot/spot/-/issues/342$rose & $fell2022-06-16T11:18:37+02:00Alexandre Duret-Lutz$rose & $fellIn SVA we can write:
- `$rose(a)` to mean "`a` is now `1`, but it was `0` in the previous step (if that step exists)".
- `$fell(a)` to mean "`a` is now `0`, but it was `1` in the previous step (if that step exists)".
- `$stable(a)` to me...In SVA we can write:
- `$rose(a)` to mean "`a` is now `1`, but it was `0` in the previous step (if that step exists)".
- `$fell(a)` to mean "`a` is now `0`, but it was `1` in the previous step (if that step exists)".
- `$stable(a)` to mean "`a` has the same value in the previous step if that step exists"
If we had past operators, we would be able to write the first one `a & (Y(!a) | !Y(1))` and the other two similarly. But even without past operators, these seem to be something we could translate quite easily because they are only looking one step back.
For instance if during a translation one state is labeled by `$rose(a)` we know that all outgoing transitions match `a`, and all incoming transitions match `!a`.
Note: SVA can also combine these notations with clocks, and in this case looking one step back is not enough.https://gitlab.lre.epita.fr/spot/spot/-/issues/291generalize the BA-typeness check2021-01-08T14:18:39+01:00Alexandre Duret-Lutzgeneralize the BA-typeness checkThe `is_scc_tba_type()` internal function used by `tra_to_tba()` is currently specialized to Rabin acceptance.
However, the original paper [Krishnan et al., ISAAC'94] presents the check in a way that works regardless of the acceptance c...The `is_scc_tba_type()` internal function used by `tra_to_tba()` is currently specialized to Rabin acceptance.
However, the original paper [Krishnan et al., ISAAC'94] presents the check in a way that works regardless of the acceptance condition. Take an automaton A with arbitrary acceptance condition:
1. find the set of "final transitions" F, i.e., transitions that cannot be part of a rejecting cycle
2. check if A is still accepting after you have removed all final transitions F.
If A - F is not accepting anymore, then the input automaton is equivalent to a Büchi automaton with the same transition structure as A, but acceptance Inf(F).
The difficult point is the first one. Finding a rejecting cycle can be done by complementing the acceptance condition and looking for an accepting cycle, however we do not yet have that for arbitrary acceptance. (At the time of writing, the generic emptiness checks on the `adl/generic-ec` branch only return `true/false` answers, but it feels like it would not be too difficult to teach them to return an accepting cycle.)
The paper then goes on and points that a DRA is DBA-realizable iff it is DBA-type, and this does not hold for all acceptance conditions. However we still have that a BA-type automaton is clearly BA-realizable, so it still makes sense to try this algorithm before attempting some other conversion that add states. For instance the Streett-to-TGBA could be simplified on SCCs that are BA-type, and so would the default strategy of `remove_fin()`. Also the recurrence check based on `LTL->TGBA->DPA->DRA->is_DBA_type?` could skip the `DPA->DRA` step.
In the long run, we should probably aim to refine `remove_fin()` so that the different strategies can be applied at the SCC level instead of the entire automaton.Florian RenkinFlorian Renkinhttps://gitlab.lre.epita.fr/spot/spot/-/issues/277possible translation improvement2017-09-02T15:35:28+02:00Alexandre Duret-Lutzpossible translation improvementCurrently `a U b` is translated as `b ∨ (a ∧ X[a U b] ∧ P(b))`.
@max's idea: if `a` is purely universal, we can translate `a U b` as `b ∨ (a ∧ X[F(b)] ∧ P(b))`.
Of course there is a dual rule for `R` and pure eventuality.
Can this imp...Currently `a U b` is translated as `b ∨ (a ∧ X[a U b] ∧ P(b))`.
@max's idea: if `a` is purely universal, we can translate `a U b` as `b ∨ (a ∧ X[F(b)] ∧ P(b))`.
Of course there is a dual rule for `R` and pure eventuality.
Can this improve the translation?https://gitlab.lre.epita.fr/spot/spot/-/issues/257degen could use some common_in trick2017-09-02T16:07:41+02:00Alexandre Duret-Lutzdegen could use some common_in trick`sbacc()` computes acceptance marks common to input and output edges of each states, but for some (probably historical) reason `degeneralize()` only use common output. I think it would improve things to use information about common inpu...`sbacc()` computes acceptance marks common to input and output edges of each states, but for some (probably historical) reason `degeneralize()` only use common output. I think it would improve things to use information about common input as well.https://gitlab.lre.epita.fr/spot/spot/-/issues/252autcross2017-07-28T11:14:17+02:00Alexandre Duret-LutzautcrossWe need a new tool called `autcross`, and working similarly to `ltlcross` except that the input would be automata, and the tools tested are expected to transform those automata.We need a new tool called `autcross`, and working similarly to `ltlcross` except that the input would be automata, and the tools tested are expected to transform those automata.https://gitlab.lre.epita.fr/spot/spot/-/issues/229improve performance of language_map()2017-09-06T11:39:31+02:00Alexandre Duret-Lutzimprove performance of language_map()instead of making all possible equivalence checks, use the construct from the proof of Lemma 4.1 in [Minimisation of Deterministic Parity and Büchi Automata and Relative Minimisation of Deterministic Finite Automata](https://arxiv.org/pd...instead of making all possible equivalence checks, use the construct from the proof of Lemma 4.1 in [Minimisation of Deterministic Parity and Büchi Automata and Relative Minimisation of Deterministic Finite Automata](https://arxiv.org/pdf/1007.1333.pdf).https://gitlab.lre.epita.fr/spot/spot/-/issues/206ltldo --smallest / ltldo --largest2017-11-15T14:34:32+01:00Alexandre Duret-Lutzltldo --smallest / ltldo --largestI would like to have a new option for `ltldo` to use it as a portfolio.
For instance:
```
ltldo --smallest ltl3ba ltl2ba 'ltl2tgba -B' -f formula
```
would translate the formula using the three tools, and return only the smallest automa...I would like to have a new option for `ltldo` to use it as a portfolio.
For instance:
```
ltldo --smallest ltl3ba ltl2ba 'ltl2tgba -B' -f formula
```
would translate the formula using the three tools, and return only the smallest automaton.
Ideally, `--smallest` would take an optional parameter to specify what we want to minimize. Maybe we could say `--smallest=%s,%e` and then use `strverscmp()` on the strings to compare them. This would allow customizing the order easily.
Then it also make sense to implement `--greatest` and complain of more that one of these option is used.
Finally, this should also combine with `--stats`. So adding `--stats=%T` to the above command should give be the name of the translator whose output was selected.Spot 2.3.1Alexandre Duret-LutzAlexandre Duret-Lutzhttps://gitlab.lre.epita.fr/spot/spot/-/issues/197Change emptiness_check interface2017-11-15T14:34:25+01:00Maximilien ColangeChange emptiness_check interfaceThe class should provide two methods is_empty() and accepting_run(), to be consistent with the method offered by twa.
This allows to optimize the algorithms when there is no need to compute an accepting run (e.g. couvreur on terminal ...The class should provide two methods is_empty() and accepting_run(), to be consistent with the method offered by twa.
This allows to optimize the algorithms when there is no need to compute an accepting run (e.g. couvreur on terminal automata).Spot 3https://gitlab.lre.epita.fr/spot/spot/-/issues/196improve macro `down_cast`2017-11-15T14:34:33+01:00Alexandre Duret-Lutzimprove macro `down_cast`If this macro were an inline function, it could contain the `assert()` (or rather `SPOT_ASSERT`) when compiling in debug mode. That would remove a lot of assertion from the code base.
It would also be easy to specialize `down_cast` fo...If this macro were an inline function, it could contain the `assert()` (or rather `SPOT_ASSERT`) when compiling in debug mode. That would remove a lot of assertion from the code base.
It would also be easy to specialize `down_cast` for shared pointer.Spot 2.3.1Maximilien ColangeMaximilien Colangehttps://gitlab.lre.epita.fr/spot/spot/-/issues/187implement reduction from LTLf to LTL2017-11-15T14:34:33+01:00Alexandre Duret-Lutzimplement reduction from LTLf to LTLSee the function called t in https://www.cs.rice.edu/~vardi/papers/ijcai13.pdf, also used in http://www.cs.rice.edu/~vardi/papers/memocode14a.pdf
That's probably a new feature for `ltlfilt`.See the function called t in https://www.cs.rice.edu/~vardi/papers/ijcai13.pdf, also used in http://www.cs.rice.edu/~vardi/papers/memocode14a.pdf
That's probably a new feature for `ltlfilt`.