SAT Checking for the full guarded fragment of the coalgebraic mu-calculus, using Compact Safra Trees

This merge request introduces a SAT decision procedure for the entire guarded fragment of the coalgebraic mu calculus, by extending the existing Tableau- and OneStep-function-based reasoners with a parity game construction using Compact Safra Trees as states. This implements the procedure described in https://doi.org/10.1007/978-3-030-17127-8_16.

Primary Contribution: SafraTreeTracking.ml(i) provides CstTracker as a new implementation of FocusTracking.FocusTracker, which uses compact safra trees as described by Piterman (https://arxiv.org/pdf/0705.2205.pdf).

Secondary Changes:

• The cool-coalg executable is updated; its --fragment parameter is now respected by selecting the reasoner implementation at runtime.
• The fragSpec argument to CoAlgReasoner.isSat and CoAlgReasoner.initReasoner is removed. Instead, all FocusTracker implementations are annotated with a fragment, against which compatibility of formulas is checked in initReasoner. This ensures that the fragment used in the reasoner is always compatible with the selected focus tracking, and the formulas actually lie in that fragment.
• Series.ml and cool-gen_exec are extended with new, non-aconjunctive formula series describing Streett games.