Spot issueshttps://gitlab.lre.epita.fr/spot/spot/-/issues2017-11-15T14:34:25+01:00https://gitlab.lre.epita.fr/spot/spot/-/issues/182implement simulation-based inclusion checks2017-11-15T14:34:25+01:00Alexandre Duret-Lutzimplement simulation-based inclusion checks- compute the signatures and classes of the states of both automata,
- if the initial state of A is a class implied by the class of B, then L(B) is included in L(A).
That only a sufficient condition, but it may help us avoid computin...- compute the signatures and classes of the states of both automata,
- if the initial state of A is a class implied by the class of B, then L(B) is included in L(A).
That only a sufficient condition, but it may help us avoid computing the complement of A to decide B ⊂ Ahttps://gitlab.lre.epita.fr/spot/spot/-/issues/180missed simplification2017-11-15T14:34:25+01:00Alexandre Duret-Lutzmissed simplification```
ltl2tgba 'G(!p0 | ((!p1 | X((!p2 U (p3 & Fp4)) | (p2 R !p3))) W p2))'
```
Gives a 10-state TGBA:
![tgba](/uploads/ea69267bd849dd97fdab8b20e8cd9506/tgba.png)
```
ltl2tgba -B 'G(!p0 | ((!p1 | X((!p2 U (p3 & Fp4)) | (p2 R !p3)))...```
ltl2tgba 'G(!p0 | ((!p1 | X((!p2 U (p3 & Fp4)) | (p2 R !p3))) W p2))'
```
Gives a 10-state TGBA:
![tgba](/uploads/ea69267bd849dd97fdab8b20e8cd9506/tgba.png)
```
ltl2tgba -B 'G(!p0 | ((!p1 | X((!p2 U (p3 & Fp4)) | (p2 R !p3))) W p2))'
```
Gives a 9-state BA:
![ba](/uploads/70f6dd19c1d890b7d2513dba59a1d5fd/ba.png)
Looks like a case where simulation is more efficient on BA that on TGBA.https://gitlab.lre.epita.fr/spot/spot/-/issues/177connect tgba_determinize() and dtwa_sat_minimize() in ltl2tgba2017-11-15T14:34:25+01:00Alexandre Duret-Lutzconnect tgba_determinize() and dtwa_sat_minimize() in ltl2tgbaThe framework illustrated by the figure at https://spot.lrde.epita.fr/satmin.html#sec-4 could be improved since we can now generate deterministic parity automata for any LTL formula.
In short, I'd like
```
ltl2tgba -D -x sat-minim...The framework illustrated by the figure at https://spot.lrde.epita.fr/satmin.html#sec-4 could be improved since we can now generate deterministic parity automata for any LTL formula.
In short, I'd like
```
ltl2tgba -D -x sat-minimize formula
```
to work for any formula for which a deterministic TGBA exists.https://gitlab.lre.epita.fr/spot/spot/-/issues/173missed simplifications2017-09-06T11:39:30+02:00Alexandre Duret-Lutzmissed simplifications```
ltl2tgba -f '(XXG!b M F!b) W (!a | !b)'
```
![output](/uploads/e743ce948b8fb8ee3ec3a18456f1f499/out.png)
```
ltl2tgba -f '(XXG!b M F!b) W (!a | !b)' | autfilt --small
```
![out2](/uploads/9c2c60f66f23205974158fb4df975131/o...```
ltl2tgba -f '(XXG!b M F!b) W (!a | !b)'
```
![output](/uploads/e743ce948b8fb8ee3ec3a18456f1f499/out.png)
```
ltl2tgba -f '(XXG!b M F!b) W (!a | !b)' | autfilt --small
```
![out2](/uploads/9c2c60f66f23205974158fb4df975131/out2.png)
I'm really surprised the first command does not produce exactly the second output.https://gitlab.lre.epita.fr/spot/spot/-/issues/163Rewrite testing automata as Fin( ! 0)2017-11-15T14:34:25+01:00Etienne RenaultRewrite testing automata as Fin( ! 0)Testing automata can be re-write using the acceptance F(!0) for livelock accepting states.
Thus ta will be consistent with the rest of the libraryTesting automata can be re-write using the acceptance F(!0) for livelock accepting states.
Thus ta will be consistent with the rest of the libraryhttps://gitlab.lre.epita.fr/spot/spot/-/issues/151Produce fair Kripke when loading DVE file2017-11-15T14:34:25+01:00Etienne RenaultProduce fair Kripke when loading DVE fileWhen loading a DVE model, we are (sometimes) unable to detect the process that progress. Thus we cannot check fair properties on these models. In the code attached, we cannot express that P or Q progress. We could directly inherit fair k...When loading a DVE model, we are (sometimes) unable to detect the process that progress. Thus we cannot check fair properties on these models. In the code attached, we cannot express that P or Q progress. We could directly inherit fair kripke to annotate transitions.
[file.dve](/uploads/63897a6731830c1aa8640e4bcac92f3e/file.dve)
https://gitlab.lre.epita.fr/spot/spot/-/issues/140case where ltlcross consumes too much memory2017-11-15T14:34:25+01:00Alexandre Duret-Lutzcase where ltlcross consumes too much memoryThis is a very large automaton created by `ltl2dstar`, and `remove_fin` create even larger automata. Maybe there is something to improve.
```
% ltlcross --verbose -f 'F(Ga | Gb | Gc | Gd | Ge)' 'ltl2dstar --union=no --ltl2nba=spin:l...This is a very large automaton created by `ltl2dstar`, and `remove_fin` create even larger automata. Maybe there is something to improve.
```
% ltlcross --verbose -f 'F(Ga | Gb | Gc | Gd | Ge)' 'ltl2dstar --union=no --ltl2nba=spin:ltl2tgba@-Ds --output-format=hoa %L %O'
F | | | | G p0 G p1 G p2 G p3 G p4
Running [P0]: ltl2dstar --union=no --ltl2nba=spin:ltl2tgba@-Ds --output-format=hoa 'lcr-i0-kcDtFC' 'lcr-o0-DaCj7N'
Running [N0]: ltl2dstar --union=no --ltl2nba=spin:ltl2tgba@-Ds --output-format=hoa 'lcr-i0-iJErXM' 'lcr-o0-P5qANL'
Performing sanity checks and gathering statistics...
info: getting rid of any Fin acceptance...
info: P0 (58852 st., 1883264 ed., 18 sets) -> (250133 st., 5917479 ed., 1 sets)
info: Comp(P0) (58852 st., 1883264 ed., 18 sets) -> (3896448 st., 103304326 ed., 18 sets)
info: Comp(N0) (11 st., 352 ed., 1 sets) -> (16 st., 610 ed., 1 sets)
info: check_empty P0*N0
^C
```https://gitlab.lre.epita.fr/spot/spot/-/issues/127add an intersect() method to twa_graph2018-06-28T21:27:12+02:00Alexandre Duret-Lutzadd an intersect() method to twa_graphThe use of
```
bool res = product(l->translation, g->translation)->is_empty();
```
in `language_containment_checker::incompatible_(l,g)` is bad for two reasons:
1. `product()` builds the entire product, even in the cases where t...The use of
```
bool res = product(l->translation, g->translation)->is_empty();
```
in `language_containment_checker::incompatible_(l,g)` is bad for two reasons:
1. `product()` builds the entire product, even in the cases where the product is non-empty and `is_empty()` does not need to explore it fully.
2. `is_empty()` calls an emptiness checks that uses the "on-the-fly" interface, therefore allocating states and iterators all over the place.
The product could be done on-the-fly with `otf_product()`. But `otf_product()` would also use the on-the-fly interface of the two input automata, so allocating memory. In the case where `is_empty()` has to explore the entire product, this would be a net loss.
So the proposal is to implement a function
`bool intersects(const twa_graph_ptr& left, const twa_graph_ptr& right);`
that would do an emptiness check over the product of left and right, computed on-the-fly. Because the two automata are `twa_graph_ptr`, the emptiness check will be easier to implement efficiently, because it can refer to states by their numbers. Then we would also add a method `bool twa_graph::intersect(const twa_graph_ptr& right)`.
This should be useful in other contexts. For instance `ltlcross` and `autfilt --intersect` would benefit from that as well (although in the case of `ltlcross`, a counterexample would be better than `bool`).
For benchmarking, `reduc.test` seems to be a nice candidate. This test currently takes several minutes
and the checks for LTL equivalence spend approx 20% of time building products, and 13% testing those products for emptiness.https://gitlab.lre.epita.fr/spot/spot/-/issues/124Python API documentation2017-11-15T14:34:25+01:00Alexandre Duret-LutzPython API documentationIt would be nice to have a complete documentation of the Python API.It would be nice to have a complete documentation of the Python API.https://gitlab.lre.epita.fr/spot/spot/-/issues/121minimize_wdba() should have improved detection of terminal automata in its ou...2017-11-15T14:34:25+01:00Alexandre Duret-Lutzminimize_wdba() should have improved detection of terminal automata in its outputBut this should not be done at the cost of computing another SCC decomposition. Can it be done inside `minimize_dfa()`?But this should not be done at the cost of computing another SCC decomposition. Can it be done inside `minimize_dfa()`?https://gitlab.lre.epita.fr/spot/spot/-/issues/120minimize_wdba() should be specialized for terminal automata2017-11-15T14:34:25+01:00Alexandre Duret-Lutzminimize_wdba() should be specialized for terminal automatain particular, the call to `wdba_scc_is_accepting()` seems overkillin particular, the call to `wdba_scc_is_accepting()` seems overkillhttps://gitlab.lre.epita.fr/spot/spot/-/issues/111Automatic build for various distributions2017-11-15T14:34:25+01:00Alexandre Duret-LutzAutomatic build for various distributionsRegister on the https://build.opensuse.org/ service, and use it to build Spot for many distributions.Register on the https://build.opensuse.org/ service, and use it to build Spot for many distributions.https://gitlab.lre.epita.fr/spot/spot/-/issues/102named temporal operators2017-11-15T14:34:25+01:00Alexandre Duret-Lutznamed temporal operatorsSpin's LTL syntax allows `always`, `equivalent`, `eventually`, `until`, `next` for the command line (i.e., `spin -f`). The syntax for LTL formula specified inside a promela model additionally accept `stronguntil`, `weakuntil`, `release`...Spin's LTL syntax allows `always`, `equivalent`, `eventually`, `until`, `next` for the command line (i.e., `spin -f`). The syntax for LTL formula specified inside a promela model additionally accept `stronguntil`, `weakuntil`, `release`.
PSL has `always`, `never`, `next!` and `next`, `eventually!`, `until!`, `until`, `until!_`, `until_`, `before!`, `before`, `before!_`, `before_`. Where the `!` denotes the strong variant.
It would be nice to support these operators as well. Unfortunately, there is one semantics incompatibility: `until` means `U` for Spin, and `W` for PSL.
https://gitlab.lre.epita.fr/spot/spot/-/issues/75An example of BA translation that is better than its original TGBA2020-12-14T11:24:53+01:00Alexandre Duret-LutzAn example of BA translation that is better than its original TGBAIn this example a TGBA with 2 acceptance sets is degeneralized into a BA with one transition less (a self loop is removed).
```
% ltl2tgba -H 'GF(!a & X!a & Fa)'
HOA: v1
name: "GF(!a & X!a & Fa)"
States: 3
Start: 0
AP: 1 "a"
a...In this example a TGBA with 2 acceptance sets is degeneralized into a BA with one transition less (a self loop is removed).
```
% ltl2tgba -H 'GF(!a & X!a & Fa)'
HOA: v1
name: "GF(!a & X!a & Fa)"
States: 3
Start: 0
AP: 1 "a"
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[t] 0 {0}
[!0] 1 {1}
State: 1
[!0] 1 {1}
[!0] 2
State: 2
[0] 0 {0}
--END--
```
```
% ltl2tgba -BH 'GF(!a & X!a &Fa)'
HOA: v1
name: "GF(!a & X!a & Fa)"
States: 3
Start: 2
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
[!0] 1
State: 1 {0}
[0] 2
State: 2
[!0] 0
[t] 2
--END--
```
If we disable the simulation on the BA, we get a BA with the same structure as the original TGBA.
```
% ltl2tgba -x ba-simul=0 -BH 'GF(!a & X!a &Fa)'
HOA: v1
name: "GF(!a & X!a & Fa)"
States: 3
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
[t] 0
[!0] 1
State: 1
[!0] 1
[!0] 2
State: 2 {0}
[0] 0
--END--
```
It would be nice to have a similar reduction on the TGBA.https://gitlab.lre.epita.fr/spot/spot/-/issues/74'Step by step' mode for algorithms in python2017-11-15T14:34:25+01:00Etienne Renault'Step by step' mode for algorithms in pythonIf spot has educational objectives it could be interesting to
have a step by step mode in order to run algorithms such as degeneralisation,
emptiness check, ...
How can we do this without modifying C++ interface?If spot has educational objectives it could be interesting to
have a step by step mode in order to run algorithms such as degeneralisation,
emptiness check, ...
How can we do this without modifying C++ interface?https://gitlab.lre.epita.fr/spot/spot/-/issues/58are_isomorphic and canonicalize should also consider reorderings of acceptanc...2017-11-15T14:34:25+01:00Alexandre Duret-Lutzare_isomorphic and canonicalize should also consider reorderings of acceptance setsFor instance
HOA: v1
States: 2
Start: 0
Acceptance: 2 Inf(0)&Inf(1)
--BODY--
State: 0 {0} [t] 1
State: 1 {1} [t] 0
--END--
should be considered as isomorphic to
HOA: v1
States: 2
...For instance
HOA: v1
States: 2
Start: 0
Acceptance: 2 Inf(0)&Inf(1)
--BODY--
State: 0 {0} [t] 1
State: 1 {1} [t] 0
--END--
should be considered as isomorphic to
HOA: v1
States: 2
Start: 0
Acceptance: 2 Inf(0)&Inf(1)
--BODY--
State: 0 {1} [t] 1
State: 1 {0} [t] 0
--END--
since we just flipped the acceptance set numbers.https://gitlab.lre.epita.fr/spot/spot/-/issues/54hoa: use acc-name to validate Acceptance2017-11-15T14:34:25+01:00Alexandre Duret-Lutzhoa: use acc-name to validate AcceptanceWith version 1.1.1, `ltl3ba -H2 -f Fa` outputs
acc-name: generalized-Buchi 1
Acceptance: 1 t
instead of
acc-name: generalized-Buchi 1
Acceptance: 1 Inf(0)
Since tonight our parser ignores useless acceptance ...With version 1.1.1, `ltl3ba -H2 -f Fa` outputs
acc-name: generalized-Buchi 1
Acceptance: 1 t
instead of
acc-name: generalized-Buchi 1
Acceptance: 1 Inf(0)
Since tonight our parser ignores useless acceptance sets (see [this HOA issue](https://github.com/adl/hoaf/issues/36)), so the first example is silently converted to
acc-name: all
Acceptance: 0 t
To catch the error in the first example, we should probably look at `acc-name:` and match the values we recognize against the `Acceptance:` line.https://gitlab.lre.epita.fr/spot/spot/-/issues/51fusion-star support2017-11-15T14:34:25+01:00Alexandre Duret-Lutzfusion-star supportThis keep tracks of the support for the `[:*i..j]` operator. This is currently on branch `adl/si-psl`.
* [x] documentation of semantics, parsing, pretty-printing, trivial simplifications, translation
* [x] update `ltl2tgba.html` to ...This keep tracks of the support for the `[:*i..j]` operator. This is currently on branch `adl/si-psl`.
* [x] documentation of semantics, parsing, pretty-printing, trivial simplifications, translation
* [x] update `ltl2tgba.html` to mention the operator
* [ ] non-trivial simplifications
* [x] `is_syntactic_stutter_invariant()` following Def.2 of [Dax et al. (ATVA'09)][]
* [x] generalize `remove_x()` following function κ and τ in [Dax et al. (ATVA'09)][] (bug this seems bogus, see comment below)
* [ ] investigate why we need a bidirectional check in our implementation of `is_stutter_invariant()` using Etessami's rewriting, why [Dax et al. (ATVA'09)] claim that their τ function (based on the paper of Peled & Wilke) is an overapproximation, and therefore would need only one inclusion check. Is it the case that Etessami's function is also an overapproximation and we are doing to much work or is it the case that Etessami's is not an overapproximation?
* [ ] generalize the syntactic version of `is_stutter_invariant()` to use `stutterize_psl()`
[Dax et al. (ATVA'09)]: http://www.daxc.de/eth/paper/09atva.pdfAlexandre Duret-LutzAlexandre Duret-Lutzhttps://gitlab.lre.epita.fr/spot/spot/-/issues/38improve failure reporting of ltlcross2017-11-15T14:34:25+01:00Alexandre Duret-Lutzimprove failure reporting of ltlcrossImprove failure reporting of `ltlcross`. Currently it only reports
counterexample for errors in cross products. We should improve
diagnostics in the other checks.
Also we could have heuristics to highlight the most pertinent
erro...Improve failure reporting of `ltlcross`. Currently it only reports
counterexample for errors in cross products. We should improve
diagnostics in the other checks.
Also we could have heuristics to highlight the most pertinent
error to look at (e.g., the smallest automaton causing a problem),
and to hint at probable erroneous translators (e.g., if the
$P_i\otimes N_i$ is non-empty, or if $P_i\otimes N_j$ is non-empty
for one $i$ and multiple $j$).
https://gitlab.lre.epita.fr/spot/spot/-/issues/37implement a feed-back arc set heuristic2017-11-15T14:34:26+01:00Alexandre Duret-Lutzimplement a feed-back arc set heuristicThis is needed to improve conversion from DRA to NBA, as well as
complementation of DBA.
Alexandre L has a branch for this, but it is out-of-date w.r.t. to the current code base, and as far as I know the FAS hasn't been integrated in...This is needed to improve conversion from DRA to NBA, as well as
complementation of DBA.
Alexandre L has a branch for this, but it is out-of-date w.r.t. to the current code base, and as far as I know the FAS hasn't been integrated into both algorithms.Alexandre LewkowiczAlexandre Lewkowicz