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/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/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/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/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/175investigate how ra_to_ba can be generalized2017-11-15T14:34:25+01:00Alexandre Duret-Lutzinvestigate how ra_to_ba can be generalizedCan we write `ra_to_ba()` for transition-based generalized Rabin automata? Generalizing the technique of Krishnan et al. (ISAAC'94)?
If that works, we can combine that with #174 and our determinization procedure to obtain a way to deci...Can we write `ra_to_ba()` for transition-based generalized Rabin automata? Generalizing the technique of Krishnan et al. (ISAAC'94)?
If that works, we can combine that with #174 and our determinization procedure to obtain a way to decide whether an automaton represents a recurrence property.https://gitlab.lre.epita.fr/spot/spot/-/issues/167Implement Kurshan's "poorman's inclusion test"2017-11-15T14:34:25+01:00Alexandre Duret-LutzImplement Kurshan's "poorman's inclusion test"Cf. R.P. Kurshan, *Complementing Büchi Automata in Polynomia Time*, J. of Comp. and Sys. Sc.
The complementation of deterministic automata is already implemented: it corresponds to calling remove_fin() after complementing the accepta...Cf. R.P. Kurshan, *Complementing Büchi Automata in Polynomia Time*, J. of Comp. and Sys. Sc.
The complementation of deterministic automata is already implemented: it corresponds to calling remove_fin() after complementing the acceptance condition. The paper discusses doing this for non-deterministic automata in order to test inclusion. This could be useful, especially in non-Büchi cases, where the determinization procedure will require a degeneralization first.https://gitlab.lre.epita.fr/spot/spot/-/issues/110investigate use of SAT-based synthezis of deterministic automata using non-de...2017-11-15T14:34:25+01:00Alexandre Duret-Lutzinvestigate use of SAT-based synthezis of deterministic automata using non-deterministic inputI believe the code should work as-is, provided we should lift the "deterministic input" restriction, and document that the number of states needed to synthesize a deterministic automaton from a nondeterministic maybe need to be greater.
...I believe the code should work as-is, provided we should lift the "deterministic input" restriction, and document that the number of states needed to synthesize a deterministic automaton from a nondeterministic maybe need to be greater.
This came up in an email conversation with Jan Strejček, who assumed the SAT stuff was accepting non-deterministic input.https://gitlab.lre.epita.fr/spot/spot/-/issues/36study effect of degen-lcache on ba-simul2017-11-15T14:34:26+01:00Alexandre Duret-Lutzstudy effect of degen-lcache on ba-simul % ltl2tgba --ba -x degen-lcache=0,degen-reset=1,ba-simul=0 '(GFa -> GFb) & (GFc -> GFd) & GF(Fe & X(f | X!f))' --stats '%s %t %e'
68 4272 511
enabling `lcache` causes some transitions to be merged
% ltl2tgba --ba -x d... % ltl2tgba --ba -x degen-lcache=0,degen-reset=1,ba-simul=0 '(GFa -> GFb) & (GFc -> GFd) & GF(Fe & X(f | X!f))' --stats '%s %t %e'
68 4272 511
enabling `lcache` causes some transitions to be merged
% ltl2tgba --ba -x degen-lcache=1,degen-reset=1,ba-simul=0 '(GFa -> GFb) & (GFc -> GFd) & GF(Fe & X(f | X!f))' --stats '%s %t %e'
68 4272 499
but it hinders the BA simulation-based reductions
% ltl2tgba --ba -x degen-lcache=1,degen-reset=1,ba-simul=1 '(GFa -> GFb) & (GFc -> GFd) & GF(Fe & X(f | X!f))' --stats '%s %t %e'
45 2032 183
% ltl2tgba --ba -x degen-lcache=0,degen-reset=1,ba-simul=1 '(GFa -> GFb) & (GFc -> GFd) & GF(Fe & X(f | X!f))' --stats '%s %t %e'
45 2016 187
This suggest that either we could fine-tune `degen-lcache` to pick a
more suitable level when offered the choice (maybe take the "natural"
level when offered the choice), or we could devise a simulation-based
reduction that is tailored to degeneralized automata (where we know
that cloned states recognized the same languages).
https://gitlab.lre.epita.fr/spot/spot/-/issues/35better translation or simplification of GF(a & Fb)2017-11-15T14:34:26+01:00Alexandre Duret-Lutzbetter translation or simplification of GF(a & Fb)`G(F(a & Fb))` is equivalent to `G(Fa & Fb)`, yet I know of no translator that is able to translate the first as efficiently as the second.
It gets worse with `G(F(a & F(b & Fc)))` etc.
Look at the rewriting rules in the [LIO2ALBA pape...`G(F(a & Fb))` is equivalent to `G(Fa & Fb)`, yet I know of no translator that is able to translate the first as efficiently as the second.
It gets worse with `G(F(a & F(b & Fc)))` etc.
Look at the rewriting rules in the [LIO2ALBA paper](http://arxiv.org/abs/0911.2033).
It has `GF(a & Fb) = GFa & GFb` as well as `GF(a | Gb) = GFa | FGb` (to apply in the other direction).
https://gitlab.lre.epita.fr/spot/spot/-/issues/33add support for EQLTL2017-11-15T14:34:27+01:00Alexandre Duret-Lutzadd support for EQLTLRead [Stutter-Invariant Languages, ω-Automata, and Temporal-Logic](http://homepages.inf.ed.ac.uk/kousha/stut_eqltl_vac.ps).
A basic plan would be:
- [ ] Add an ∃ unary operator
- [ ] modify the LTL parser to accept ∃ only at the t...Read [Stutter-Invariant Languages, ω-Automata, and Temporal-Logic](http://homepages.inf.ed.ac.uk/kousha/stut_eqltl_vac.ps).
A basic plan would be:
- [ ] Add an ∃ unary operator
- [ ] modify the LTL parser to accept ∃ only at the top-level.
- [ ] add a function `label_filter(tgba_digraph_ptr& aut, bdd vars)` that removes all variables in `vars` from the labels of `aut`.
- [ ] Adjust the translations. To translate `∃(a,b) f(a,b,c,d)`, first translate `f(a,b,c,d)`, and then apply `label_filter` to remove `a`, and `b`. (Note in Couvreur/FM, removing `a,b` could be done during the same pass that complements promises.)
- [ ] Implement Etessami's conversion from BA to EQLTL.
- [ ] Implement a conversion from TGBA to EQLTL.
A more general idea would be to allow ∃ at all level in the
formulas, during the translation, we have to apply `bdd_exist` on
the BDD-rewriting of any subformula of a ∃ operator.
Would it be correct to do the same with ∀ and `bdd_forall`? If that is true, that gives us a conceptually simple way to negate an automaton: translate it to EQLTL, negate it (giving an ∀-quantified LTL formula), and translate it back.
https://gitlab.lre.epita.fr/spot/spot/-/issues/31Converting a TGBA into a PSL formula2017-11-15T14:34:27+01:00Alexandre Duret-LutzConverting a TGBA into a PSL formula[The ForSpec Temporal Logic: A New Temporal Property-Specification Language](http://www.cs.rice.edu/~vardi/papers/tacas02.ps.gz) gives a conversion from Büchi automata to PSL.
Here is my reinterpretation of their theorem.
Any omega...[The ForSpec Temporal Logic: A New Temporal Property-Specification Language](http://www.cs.rice.edu/~vardi/papers/tacas02.ps.gz) gives a conversion from Büchi automata to PSL.
Here is my reinterpretation of their theorem.
Any omega regular language can be converted into a finite union of
the form $L_1.L_2$ where $L_1$ is a regular language, and $L_2$ can
be described by a deterministic automaton. An expression `e` for $L_1$ can be computed easily using the classical state-elimination algorithm, so $L_1.L_2$ can be encoded by `{e}!<>->f` where `f` is a formula for $L_2$.
$L_2$ can be represented by disjunctions of the formulae of the form `{e1;e2[*]}! && {e1;e2[*]}[]=> {e2[*]}!` where `e1` is a word going to an accepting state, and `e2[*]` is the loop language of that state (i.e., the language of all words that will come back to this state).
Running this construction on the Büchi automaton we produce for `FGa` will give `{1*;a}<>-> ({a;a*}! & {a;a*}[]=>{a*}!)`. The negation of this formula, on translated to TGBA and reduced by simulation, will give exactly the TGBA we want for `GFa`.
The above algorithm works with Büchi automata as input. The
resulting formula would be translated to a TBA (i.e., a
transition-based non-generalized Büchi automaton) because in the
current PSL translation `<>->` and `{...}!` are all translated with
the same unique acceptance condition (this probably makes
complementation of Büchi automata via PSL uninteresting).
- Can we find a translation from TGBA to PSL that will work with transition-based generalized acceptance?
- Can we find a translation to PSL to relies on the `GF` operators instead pf `[]=>`? The idea is that these would add generalized conditions, so that we obtain a TGBA when translating the formula back automata.
https://gitlab.lre.epita.fr/spot/spot/-/issues/30Build TGTA from the LTL formula2017-11-15T14:34:27+01:00Alexandre Duret-LutzBuild TGTA from the LTL formulaAdjusting Couvreur's translation to produce TGTA directly seems doable.
Can it be done in a way that avoid duplicating the code completely?
Adjusting Couvreur's translation to produce TGTA directly seems doable.
Can it be done in a way that avoid duplicating the code completely?
https://gitlab.lre.epita.fr/spot/spot/-/issues/21TBA→BA2017-11-15T14:34:27+01:00Alexandre Duret-LutzTBA→BAWe have an involved degeneralization procedure that does TGBA→BA. However in practice, many TGBA have a single acceptance set (i.e., they are TBA). I believe we could work on a more efficient procedure for the TBA→BA case, it might eve...We have an involved degeneralization procedure that does TGBA→BA. However in practice, many TGBA have a single acceptance set (i.e., they are TBA). I believe we could work on a more efficient procedure for the TBA→BA case, it might even include some optimisations that are easier to do using a single acceptance set.