Hello, 

I am a student in Computer Science at the Technical University of Denmark (DTU), currently working on my master's thesis and I am using the random generator for LTL formulas of Spot. 

Upon exploring the GitHub repository of the project, 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?

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?

Arianna