Spot issueshttps://gitlab.lre.epita.fr/spot/spot/-/issues2017-09-06T11:39:30+02:00https://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/567swig 4 has doxygen support2024-03-21T23:58:26+01:00Alexandre Duret-Lutzswig 4 has doxygen supportSwig 4.0 introduced a [`-doxygen` flag](https://www.swig.org/Doc4.2/SWIGDocumentation.html#Doxygen) that allows converting doxygen comments into pydoc for automatic attachement to the bindings. It would be great to enable this. It will...Swig 4.0 introduced a [`-doxygen` flag](https://www.swig.org/Doc4.2/SWIGDocumentation.html#Doxygen) that allows converting doxygen comments into pydoc for automatic attachement to the bindings. It would be great to enable this. It will require some important reviewing work, because several of the comments are C++ specific.https://gitlab.lre.epita.fr/spot/spot/-/issues/542alternative techniques for when autcross fails to complement an automaton2023-08-30T17:25:57+02:00Alexandre Duret-Lutzalternative techniques for when autcross fails to complement an automatonCurrently `autcross` needs to complement automata in order to test equivalence. If the complementation is not possible (for instance maybe the automaton is too big for determinization to be reasonable, see #541) it would be nice to have...Currently `autcross` needs to complement automata in order to test equivalence. If the complementation is not possible (for instance maybe the automaton is too big for determinization to be reasonable, see #541) it would be nice to have alternate techniques we could use to test equivalence or even just approximate it.
For instance if I compute A*B and find that there is an accepting SCC of A that is never synchronized with any accepting SCC of B, than I can exhibit a word of A rejected by B, and I have a proved that A isn't included in B. This is only an implication, but surely this is better than nothing.https://gitlab.lre.epita.fr/spot/spot/-/issues/506reducing the number of gates by using don't care in the aiger encoding of states2022-08-07T13:03:38+02:00Alexandre Duret-Lutzreducing the number of gates by using don't care in the aiger encoding of statesCurrently if the winning strategy has n states, we use ⌈log n⌉ latches to binary encode the current state. However if n is not a power of two, some of the states could be encoded with fewer bits, leaving the rest of the bits as "don't c...Currently if the winning strategy has n states, we use ⌈log n⌉ latches to binary encode the current state. However if n is not a power of two, some of the states could be encoded with fewer bits, leaving the rest of the bits as "don't care". That's fewer latches to read to decide when we are in those states, and that's more flexibility to decide how to update those latches.
In fact any binary tree with n leaves can be used to encode n states using a number of latches equal to the depth of the tree, so we could also decide to use more latches in order to make certain states very easy to encode.https://gitlab.lre.epita.fr/spot/spot/-/issues/484rank-based complementation and elevator automata2021-11-02T09:58:23+01:00Alexandre Duret-Lutzrank-based complementation and elevator automataThis could be the subject of an internship.
[This paper](https://arxiv.org/abs/2110.10187) defines a class of "elevator" automata (transition-based NBA where SCC are either deterministic or inherently weak) for which the rank-based conm...This could be the subject of an internship.
[This paper](https://arxiv.org/abs/2110.10187) defines a class of "elevator" automata (transition-based NBA where SCC are either deterministic or inherently weak) for which the rank-based conmplementation can be simplified. I'd like to have an implementation of that, as well as an implementation of Schewe's rank-based complementation (for the non-elevator case).https://gitlab.lre.epita.fr/spot/spot/-/issues/483better AIGER format support for model checking2021-11-02T09:50:07+01:00Alexandre Duret-Lutzbetter AIGER format support for model checkingThis could be the subject of an internship.
We should improve our support of the [AIGER format](http://fmv.jku.at/aiger/FORMAT.aiger) by:
- supporting the binary version of the format for input or output
- either making class `aig` a su...This could be the subject of an internship.
We should improve our support of the [AIGER format](http://fmv.jku.at/aiger/FORMAT.aiger) by:
- supporting the binary version of the format for input or output
- either making class `aig` a subclass of `twa` with support for on-the-fly iteration, or providing a `as_otf_automaton()` method. (Currently `as_automaton()` builds an explicit automaton, but that might be very large.)
This way we can use large aig instances as models for model checking benchmars.https://gitlab.lre.epita.fr/spot/spot/-/issues/475find a way to add a timeout to dot, or kill it when the current process is ki...2021-09-09T12:22:19+02:00Alexandre Duret-Lutzfind a way to add a timeout to dot, or kill it when the current process is killedWhen we try to render a very large automaton with dot, it sometimes takes years. If we are in a jupyter notebook, killing the python kernel do not seem to kill the `dot` process. That is an issue on our `spot-sandbox` VM.
Can we arran...When we try to render a very large automaton with dot, it sometimes takes years. If we are in a jupyter notebook, killing the python kernel do not seem to kill the `dot` process. That is an issue on our `spot-sandbox` VM.
Can we arrange things so that dot is automatically killed when the parent Python process is killed? Or should we run it with a timeout? (I'm a bit afraid that forcing timeout my create some spurious failure in the test suite on overloaded hosts.)https://gitlab.lre.epita.fr/spot/spot/-/issues/466we need an "autdo" command2021-09-10T10:16:21+02:00Alexandre Duret-Lutzwe need an "autdo" commandWe need an `autdo` command, that works like [`ltldo`](https://spot.lrde.epita.fr/ltldo.html), but for wrapping tools that take automata as input and that (possibly) produce automata.
The input option of `autdo` should be the same as tho...We need an `autdo` command, that works like [`ltldo`](https://spot.lrde.epita.fr/ltldo.html), but for wrapping tools that take automata as input and that (possibly) produce automata.
The input option of `autdo` should be the same as those of [`autcross`](https://spot.lrde.epita.fr/autcross.html) (which also call tools that read automata), but the rest of the feature and options should be similar to what [`ltldo`](https://spot.lrde.epita.fr/ltldo.html) provides (e.g., ability to output the smallest or largest output from multiple tools, changing the output format, killing the called tools on timeout...)https://gitlab.lre.epita.fr/spot/spot/-/issues/454case where ltl-split is harmful2021-05-03T11:08:32+02:00Alexandre Duret-Lutzcase where ltl-split is harmful```sh
ltl2tgba -x ltl-split=1 -G -D 'GF(a&Xa) & FG(!a <-> XXX!a)'
```
![with-split](/uploads/b306dec6a6efee0706b83d8b76203e39/with-split.png)
```sh
ltl2tgba -x ltl-split=0 -G -D 'GF(a&Xa) & FG(!a <-> XXX!a)'
```
![without-split](/upload...```sh
ltl2tgba -x ltl-split=1 -G -D 'GF(a&Xa) & FG(!a <-> XXX!a)'
```
![with-split](/uploads/b306dec6a6efee0706b83d8b76203e39/with-split.png)
```sh
ltl2tgba -x ltl-split=0 -G -D 'GF(a&Xa) & FG(!a <-> XXX!a)'
```
![without-split](/uploads/a6ad5af9767b966649c4fb8aa5cbbcd6/without-split.png)https://gitlab.lre.epita.fr/spot/spot/-/issues/451do_simul on automata with non-separated Fin/Inf2021-02-17T10:45:22+01:00Alexandre Duret-Lutzdo_simul on automata with non-separated Fin/InfThere is a discrepency in `postproc.cc` where `do_simul()` does not call the simulation if the automaton has overlapping Fin/Inf sets (there is a FIXME about this), but `do_sba_simul()` does it.
I suspect it may also be possible that `w...There is a discrepency in `postproc.cc` where `do_simul()` does not call the simulation if the automaton has overlapping Fin/Inf sets (there is a FIXME about this), but `do_sba_simul()` does it.
I suspect it may also be possible that `wrap_simul()` call of `separate_sets_here()` raises an exception because it attempt to use too many colors. That probably should not be a reason to abort the translation.https://gitlab.lre.epita.fr/spot/spot/-/issues/450generalize defrag_state()2021-01-20T10:02:47+01:00Alexandre Duret-Lutzgeneralize defrag_state()Currently defrag_state() has the undocumented requirement that the new number should be smaller than the old one.
To allow users to renumber states arbitrarily we could detect cases where that's not true, and use a slightly slower imple...Currently defrag_state() has the undocumented requirement that the new number should be smaller than the old one.
To allow users to renumber states arbitrarily we could detect cases where that's not true, and use a slightly slower implementation.https://gitlab.lre.epita.fr/spot/spot/-/issues/444improve determinisation of automata matching string-like patterns2022-08-07T20:37:42+02:00Alexandre Duret-Lutzimprove determinisation of automata matching string-like patternsThe following NBA for formula `(!(G({(a)} |=> {(b)[*10]})))` is derived from #443.
![nba](/uploads/84f009e5d0bca9e1072129f567ba546f/nba.png)
It can be represented by a DBA with as many states, where the states essentially keep track of...The following NBA for formula `(!(G({(a)} |=> {(b)[*10]})))` is derived from #443.
![nba](/uploads/84f009e5d0bca9e1072129f567ba546f/nba.png)
It can be represented by a DBA with as many states, where the states essentially keep track of the number of `!a & b` seen since the last `a`.
![dba](/uploads/d3508ab2c8242272a744abef017ce983/dba.png)
However the WDBA-minimization code used to obtain the above is suboptimal. Currently it:
1. calls the powerset construction to build a 2048-state automaton without looking at the acceptance condition,
2. fixes the accepting states of the DBA by comparing it with the NBA (using a product to locate the accepting SCCs),
3. minimize it to get the above 12 states.
Changing the formula from `*10` to something larger will led to very large intermediate automata. (The original formula used in #443 was with `*32`...)
However in this case most of these steps seem overkill.
- [X] The powerset construction could be taught about the notion of "accepting sink": if a powerstate contains an accepting sink, it can be reduced to this sink. Doing so (I have a patch already) reduces the intermediate automaton to 1025 states.
- [X] Since we have a terminal NBA as input, the output should be terminal as well, and we could avoid running the product in step 2.
- [ ] Finally, I suspect there should be a way to build this DBA from the input NBA right away, but it not yet very clear how.https://gitlab.lre.epita.fr/spot/spot/-/issues/440iterate over bit sets in bitvect or bitset2021-10-01T09:52:50+02:00Alexandre Duret-Lutziterate over bit sets in bitvect or bitsetIt would be nice to be able to iterate efficiently on the bits that are sets in a `bitset` or `bitvect`. For the `bitset` case, which is used to implement `mark_t`, we already have such an implementation in `mark_container`, but this fe...It would be nice to be able to iterate efficiently on the bits that are sets in a `bitset` or `bitvect`. For the `bitset` case, which is used to implement `mark_t`, we already have such an implementation in `mark_container`, but this feature could better be implemented in `bitset`.https://gitlab.lre.epita.fr/spot/spot/-/issues/438support for exclusive APs in ltl2tgba2020-11-12T19:10:27+01:00Alexandre Duret-Lutzsupport for exclusive APs in ltl2tgbaIt would be nice to have an option to support exclusive APs in `ltl2tgba`. Currently it requires chaining three commands as in
http://lists.lrde.epita.fr/pipermail/spot/2020q3/000293.htmlIt would be nice to have an option to support exclusive APs in `ltl2tgba`. Currently it requires chaining three commands as in
http://lists.lrde.epita.fr/pipermail/spot/2020q3/000293.htmlhttps://gitlab.lre.epita.fr/spot/spot/-/issues/423for ltlsynt parity game solving could stop once the winner of initial state i...2023-03-29T13:47:16+02:00Alexandre Duret-Lutzfor ltlsynt parity game solving could stop once the winner of initial state is known`ltlsynt` only needs to know if the initial state is winning for player 0 or 1, so Zielonka can possibly be aborted erlier, as soon as the initial state is know to be winning for either player.`ltlsynt` only needs to know if the initial state is winning for player 0 or 1, so Zielonka can possibly be aborted erlier, as soon as the initial state is know to be winning for either player.https://gitlab.lre.epita.fr/spot/spot/-/issues/415handling unconstrained I/O in ltlsynt2023-03-29T13:51:15+02:00Alexandre Duret-Lutzhandling unconstrained I/O in ltlsyntIt's possible to call `ltlsynt` with `--ins` and `--outs` options that refers to AP that are not in the formula, or that disappear from the formula after simplification. Currently those AP are added to the automaton after translation, b...It's possible to call `ltlsynt` with `--ins` and `--outs` options that refers to AP that are not in the formula, or that disappear from the formula after simplification. Currently those AP are added to the automaton after translation, but it's probably more efficient to just add them to the output once the game has been solved.https://gitlab.lre.epita.fr/spot/spot/-/issues/400random conjunctions of patterns2020-03-12T10:56:36+01:00Alexandre Duret-Lutzrandom conjunctions of patternshttps://www.cs.rice.edu/~vardi/papers/time13.pdf suggests building random LTL formulas from conjunctions of known patterns. They use the DAC patterns. We could offer such a service and even generalize it to all the patterns that `genlt...https://www.cs.rice.edu/~vardi/papers/time13.pdf suggests building random LTL formulas from conjunctions of known patterns. They use the DAC patterns. We could offer such a service and even generalize it to all the patterns that `genltl` supports.
I'm not sure what the ideal interface would be. Maybe some `ltlcombine` tool that takes a list of formulas as input, some yet-to-be-specified parameters, and outputs combinations of the input formulas.https://gitlab.lre.epita.fr/spot/spot/-/issues/397a case when -G -D produce a parity automaton more than twice smaller than -P -D2020-01-16T12:21:35+01:00Alexandre Duret-Lutza case when -G -D produce a parity automaton more than twice smaller than -P -DThe following formula comes from https://www.ruediger-ehlers.de/blog/deterministicparity.html
```sh
% f='!g & (GFr -> GFg) & FGinit & G(XXg -> (init & Xinit & XXinit)) & !Xg & G(!g | X!g) & G((init & !Xinit) -> (!r & !Xr))'
```
With Sp...The following formula comes from https://www.ruediger-ehlers.de/blog/deterministicparity.html
```sh
% f='!g & (GFr -> GFg) & FGinit & G(XXg -> (init & Xinit & XXinit)) & !Xg & G(!g | X!g) & G((init & !Xinit) -> (!r & !Xr))'
```
With Spot 2.8.5.dev
```sh
% ltl2tgba -G -D -f "$f" --stats="%s states, %[o]g"
5 states, parity min odd 3
% ltl2tgba -P -D -f "$f" --stats="%s states, %[o]g"
11 states, parity min odd 3
```
It's related to LTL-splitting:
```sh
% ltl2tgba -G -D -x ltl-split=0 -f "$f" --stats="%s states, %[o]g"
11 states, parity min odd 3
```
Once we remove the obligation terms of the formula, we can reduce the case to this:
```sh
% ltl2tgba -P -D "(GFr -> GFg) & FGinit" --stats=%s
4
% ltl2tgba -G -D "(GFr -> GFg) & FGinit" --stats=%s
1
% ltl2tgba -G -D -x ltl-split=0 "(GFr -> GFg) & FGinit" --stats=%s
4
```
It's seem it's just "luck" that the construction of the formula follows a "parity pattern" and leads to a parity acceptance with `-G`. Can we detect those cases?https://gitlab.lre.epita.fr/spot/spot/-/issues/394use graphviz layers for interactive display2019-11-28T11:36:28+01:00Alexandre Duret-Lutzuse graphviz layers for interactive displayUsing [the `layer` and `layerselect` attributes of GraphViz](https://www.graphviz.org/faq/#FaqOverlays) it should be possible to write an interactive widget that has a slider showing the different layers of an automaton. This could be u...Using [the `layer` and `layerselect` attributes of GraphViz](https://www.graphviz.org/faq/#FaqOverlays) it should be possible to write an interactive widget that has a slider showing the different layers of an automaton. This could be used to replay the progression of an algorithm interactively, while preserving the global layout, for instance
I believe this could be implemented by adding some named properties "layer-edges" and "layer-states" which would be vectors of layer numbers, and let `print_dot()` know about it. Then we also need some Python functions to set those layer attributes.https://gitlab.lre.epita.fr/spot/spot/-/issues/386postprocessing twice may improve things2019-07-31T15:41:49+02:00Alexandre Duret-Lutzpostprocessing twice may improve thingsThis example was sent by Fanda.
```sh
% cat p.hoa
HOA: v1 States: 6 Start: 0 AP: 3 "a" "b" "c" acc-name: Buchi
Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc
semi-deterministic --BODY-- State: 0 [t] 0 [!0&1&2] 1...This example was sent by Fanda.
```sh
% cat p.hoa
HOA: v1 States: 6 Start: 0 AP: 3 "a" "b" "c" acc-name: Buchi
Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc
semi-deterministic --BODY-- State: 0 [t] 0 [!0&1&2] 1 [0&2 | !1] 2
[0&!1] 3 State: 1 [!0&1&2] 1 [0&2 | !1] 2 [0&!1] 3 State: 2 [!0&1&2]
1 [0&2 | !1] 2 [0&!1] 3 State: 3 [!1] 3 [!1] 4 State: 4 [0&!1] 4 {0}
[!0&!1] 5 {0} State: 5 [!0&!1] 5 [0&!1] 5 {0} --END--
% autfilt --stats=%s p.hoa
6
% autfilt --small --stats=%s p.hoa
4
% autfilt --small p.hoa | autfilt --small --stats=%s
3
```
Here are the three automata:<br/>
![p](/uploads/96b378748b2648f8fb492dd4caf05007/p.png)![pp](/uploads/63a59faefe4cdab366a76da3e64622d3/pp.png)![ppp](/uploads/d3a7fc0c31a9cb12f4082f9b256a336f/ppp.png)
It would nice if the first postprocessing would give the smallest reasult already.