Hi Arianna,
Arianna Bianchi s222890@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.