NB: the LTL mode only prints the formula to be checked for satisfiability, which can then be analysed with a tool such as https://spot.lrde.epita.fr/
NB: the LTL mode only prints the formula to be checked for satisfiability, which can then be analysed with a tool such as https://spot.lrde.epita.fr/