Spot issueshttps://gitlab.lre.epita.fr/spot/spot/-/issues2017-04-28T11:40:55+02:00https://gitlab.lre.epita.fr/spot/spot/-/issues/243syntactic characterization of PSL subclasses2017-04-28T11:40:55+02:00Alexandre Duret-Lutzsyntactic characterization of PSL subclassesI think `{r_F}` and `!{r_F}` both belong to the `φ_F` fragment. I'd also add `{r_F}[]->φ_F` and `{r_F}<>->φ_F`.I think `{r_F}` and `!{r_F}` both belong to the `φ_F` fragment. I'd also add `{r_F}[]->φ_F` and `{r_F}<>->φ_F`.spot 2.3.2Alexandre Duret-LutzAlexandre Duret-Lutzhttps://gitlab.lre.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 cha...As 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.lre.epita.fr/spot/spot/-/issues/178out-of-date example on satmin.html2017-11-15T14:34:29+01:00Alexandre Duret-Lutzout-of-date example on satmin.htmlOn https://spot.lrde.epita.fr/satmin.html#sec-2 there the following example:
> There are cases where ltl2tgba's tba-det algorithm fails to produce a deterministic automaton. In that case, SAT-based minimization is simply skipped. For...On https://spot.lrde.epita.fr/satmin.html#sec-2 there the following example:
> There are cases where ltl2tgba's tba-det algorithm fails to produce a deterministic automaton. In that case, SAT-based minimization is simply skipped. For instance:
>
> ltl2tgba -D -x sat-minimize "Ga R (F!b & (c U b))" --stats='states=%s, det=%d'
> states=5, det=1
outputting a **determinitic** automaton contradicts the text.
This is a case where tba-det works. I'm not sure what changed and when it started to work, but we need to find another example of syntactic-recurrence that tba-det cannot determinize.
PS: while we are at it, we should try to favor single-quotes over double-quotes in examples so that users do not get any surprise with interactive shells interpreting `!`.https://gitlab.lre.epita.fr/spot/spot/-/issues/445show C++/Python example of game-based simulation checks for documenting2021-11-13T11:51:21+01:00Alexandre Duret-Lutzshow C++/Python example of game-based simulation checks for documenting@jdubois wrote a game-based simulation check at the beginning of his internship (see e43c2aaae27001c04b46601e2bed51b887ad7b5b). But in the end, he found a much faster way to do it and we are not going to keep this implementation in the ...@jdubois wrote a game-based simulation check at the beginning of his internship (see e43c2aaae27001c04b46601e2bed51b887ad7b5b). But in the end, he found a much faster way to do it and we are not going to keep this implementation in the C++ library. This algorithm would however make a nice tutorial for the documentation, showing how games can be built and solved.https://gitlab.lre.epita.fr/spot/spot/-/issues/371Bad links in LTSmin documentation2019-06-27T15:03:27+02:00Clément GillardBad links in LTSmin documentationNone of the URLs in `tests/ltsmin/README` point to resources that are actually there. The links are all either dead or redirected.None of the URLs in `tests/ltsmin/README` point to resources that are actually there. The links are all either dead or redirected.https://gitlab.lre.epita.fr/spot/spot/-/issues/239improve documentation of `spot::translator` and `spot::postprocessor`2017-11-15T14:34:31+01:00Alexandre Duret-Lutzimprove documentation of `spot::translator` and `spot::postprocessor`Without going too much into details need the point to the main algorithms that are used, with references when appropriate.
This is related to the following discussion on the Spot mailing list.
On Fri, Mar 3, 2017 at 5:08 AM, Marvin Ste...Without going too much into details need the point to the main algorithms that are used, with references when appropriate.
This is related to the following discussion on the Spot mailing list.
On Fri, Mar 3, 2017 at 5:08 AM, Marvin Stenger wrote:
> Hello dear spot devs,
>
> I need to know which construction is used when I'm translating an LTL
> formula into a monitor automaton. By that I mean:
>
> ```c++
> spot::formula some_ltl;
> spot::translator trans;
> trans.set_type(spot::postprocessor::Monitor)
> spot::const_twa_graph_ptr aut = trans.run(some_ltl)
> ```
> I couldn't find documentation about this, besides some rather informal
> description.
> It would be great if you could point me to some more useful documentation
> about the algorithm or even better a paper on it.
>
> Best,
> Marvin Stenger
On Fri, Mar 3, 2017 at 10:33 AM, Alexandre Duret-Lutz wrote:
> Hi Marvin,
>
> To build deterministic monitors we use the construction from Marcelo
> d’Amorim and Grigoire Roşu: Efficient monitoring of ω-languages
> (CAV’05, LNCS 3576) as it was described by Deian Tabakov and Moshe Y.
> Vardi: Optimized Temporal Monitors for SystemC. (RV’10, LNCS 6418).
> Note that (1) the latter paper uses Spot, but when it was written,
> Spot could not produce monitors, and (2) these papers describe a
> construction that starts from a Büchi automaton, but we start from a
> TGBA instead as that is faster. So basically: translate to TGBA,
> remove useless SCCs, strip acceptance condition, determinize,
> minimize.
>
> To build non-deterministic monitors (that's what your code is asking
> for) we do the same, except that "determinize, minimize" is replaced
> by a pass of forward&backward simulation-based reductions. (These
> simulation-based reductions are presented in a Büchi context in
> Section 4.2 of https://www.lrde.epita.fr/~adl/dl/adl/babiak.13.spin.pdf
> ) and by default we compare the size non-deterministic and the
> deterministic monitors and output the smallest of the two.
>
> I checked and currently the only places where we give these references
> are in the man page of ltl2tgba
> https://spot.lrde.epita.fr/man/ltl2tgba.1.html#NOTE%20ON%20GENERATING%20MONITORS
> as well as in the documentation of the minimize_monitor() function,
> which is called indirectly by spot::translator. But I could not find
> a description of the non-deterministic case.
>
> I will make a note to improve the documentation of
> spot::translator/spot::postprocessor with more clues about what is
> going on.
>
> --
> Alexandre Duret-Lutzspot 2.3.2https://gitlab.lre.epita.fr/spot/spot/-/issues/230README updates for Mac2017-11-15T14:34:31+01:00Alexandre Duret-LutzREADME updates for MacJust as a reminder. You said you wanted to update some text files before the next release.Just as a reminder. You said you wanted to update some text files before the next release.Spot 2.3.1Etienne RenaultEtienne Renaulthttps://gitlab.lre.epita.fr/spot/spot/-/issues/176SEO2017-11-15T14:34:33+01:00Alexandre Duret-LutzSEO- The index page should have a more descriptive title, like "Spot: LTL and omega-automata manipulation library"
- The index page should have a `<meta>` tags for [`description`](https://www.w3.org/TR/html5/document-metadata.html#meta-des...- The index page should have a more descriptive title, like "Spot: LTL and omega-automata manipulation library"
- The index page should have a `<meta>` tags for [`description`](https://www.w3.org/TR/html5/document-metadata.html#meta-description) and [`keywords`](https://www.w3.org/TR/html5/document-metadata.html#meta-keywords).
- The on-line translator should use a `<h1>` tag for the the box "*LTL (or PSL) Formula to translate*"https://gitlab.lre.epita.fr/spot/spot/-/issues/171man 7 spot2017-11-15T14:34:34+01:00Alexandre Duret-Lutzman 7 spotAkim suggested we add a man-page for Spot, that would point to all the command-line installed.
I guess it has to go in section 7.Akim suggested we add a man-page for Spot, that would point to all the command-line installed.
I guess it has to go in section 7.https://gitlab.lre.epita.fr/spot/spot/-/issues/161document emptiness_check::parse_options()2017-11-15T14:34:34+01:00Alexandre Duret-Lutzdocument emptiness_check::parse_options()Requested by Yann.
The different options that can be passed are not specified.
The only doc is currently on the old site at http://spot.lip6.fr/wiki/EmptinessCheckOptionsRequested by Yann.
The different options that can be passed are not specified.
The only doc is currently on the old site at http://spot.lip6.fr/wiki/EmptinessCheckOptionsAlexandre Duret-LutzAlexandre Duret-Lutzhttps://gitlab.lre.epita.fr/spot/spot/-/issues/157document all automata properties in concept.org2017-11-15T14:34:34+01:00Alexandre Duret-Lutzdocument all automata properties in concept.orghttps://gitlab.lre.epita.fr/spot/spot/-/issues/145the list of features on the main page should mention determinization2017-11-15T14:34:34+01:00Alexandre Duret-Lutzthe list of features on the main page should mention determinizationSpot 2.0https://gitlab.lre.epita.fr/spot/spot/-/issues/137table of acceptance condition examples is missing from concepts.html2017-11-15T14:34:34+01:00Alexandre Duret-Lutztable of acceptance condition examples is missing from concepts.htmlFor some reason the list of examples of acceptance conditions is generated in `concepts.org`, but not in `concepts.html`.For some reason the list of examples of acceptance conditions is generated in `concepts.org`, but not in `concepts.html`.Spot 2.0https://gitlab.lre.epita.fr/spot/spot/-/issues/136documentation: twa prop_set2017-11-15T14:34:34+01:00Laurent Xudocumentation: twa prop_setIn twa/twa.hh, it is not clear whether {true, true, .., true} means that the properties can be modified or the properties must be preserved.In twa/twa.hh, it is not clear whether {true, true, .., true} means that the properties can be modified or the properties must be preserved.Spot 2.0