Spot issueshttps://gitlab.lre.epita.fr/spot/spot/-/issues2017-06-09T16:53:18+02:00https://gitlab.lre.epita.fr/spot/spot/-/issues/265more families of LTL formulas for genltl2017-06-09T16:53:18+02:00Alexandre Duret-Lutzmore families of LTL formulas for genltlThe page http://www.schuppan.de/viktor/atva11/ has a link to a tarball with 3723 formulas (each of them is expressed in various syntax and also in negated form, so the total appears to be much larger). All these formulas comes with refe...The page http://www.schuppan.de/viktor/atva11/ has a link to a tarball with 3723 formulas (each of them is expressed in various syntax and also in negated form, so the total appears to be much larger). All these formulas comes with references to their sources, and many of them are actually scalable patterns (manually?) instantiated for multiple values. I suspect that many of those scalable patterns would fit well in `genltl`; and it might make sense to also consider some of the non-scalable satisfiability formulas even if these are not model-checking properties.