Umaudemc

* Recursive algorithms have been transformed to iterative ones due to the limited Python recursion.
* Spot has been added as a new model-checking backend for LTL properties.
* Initial support for checking LTL properties under the semantics of the strategy language whose iteration coincides with the Kleene star. It uses Streett automata from the Spot library.
* Improvements in the test and benchmarking subcommand with support for nested problem specifications, parameters, multiple executions, etc.
* The API is extended with a function to print graphs.
* Bug fixes and code cleanup.

* Other programs can use the model checkers and other auxiliary functions through an API.
* Model-checking jobs can be safely cancelled in the graphical interfaces.
* Alternative graphical interface based on Gtk.
* All the backends calculate and show the number of rewrites executed for their model-checking jobs, and the number of states of the Büchi automaton is shown when using Maude (in addition to LTSmin).
* Other bug fixes.
</details>