4 Apr
2024
4 Apr
'24
9:58 a.m.
Hi Arianna,
Arianna Bianchi <s222890(a)student.dtu.dk> writes:
Upon exploring the GitHub repository of the project,
Spot's repository is at https://gitlab.lre.epita.fr/spot/spot/
not on GitHub, so I'm not sure what you are looking at.
I noticed the presence of simplification functions for
generating the
random LTL formulas. For instance, with these functions, equivalences
are simplified and non-reducible formulas are generated. Could you
provide insight into how this simplification functionality operates?
And which specific function is responsible for this process?
All LTL simplifications implemented are documented in
https://spot.lre.epita.fr/tl.pdf
some "trivial" simplification are always performed during the
construction of an LTL formula, so those cannot be disabled.
The rest of the simplification is performed by the tl_simplifier
class. You can try those online on the "rewrite" tab of
https://spot.lre.epita.fr/app/
Or you can use the --simplify option of command-line tool ltlfilt for
this. https://spot.lre.epita.fr/ltlfilt.html
Furthermore, I noticed that the files responsible for
generating the
formulas are located in "spot/gen/formulas.cc" and "spot/gen/
formulas.hh". How can I execute the formulas.cc file using a terminal
(command line) to generate the random LTL formulas?
Those generating function are available through the genltl command-line
utility.
https://spot.lre.epita.fr/genltl.html