  We report on COOL-MC, a model checking tool for fixpoint logics that is
parametric in the branching type of models (nondeterministic, game-based,
probabilistic etc.) and in the next-step modalities used in formulae. The tool
implements generic model checking algorithms developed in coalgebraic logic
that are easily adapted to concrete instance logics. Apart from the standard
modal $\mu$-calculus, COOL-MC currently supports alternating-time, graded,
probabilistic and monotone variants of the $\mu$-calculus, but is also
effortlessly extensible with new instance logics. The model checking process is
realized by polynomial reductions to parity game solving, or, alternatively, by
a local model checking algorithm that directly computes the extensions of
formulae in a lazy fashion, thereby potentially avoiding the construction of
the full parity game. We evaluate COOL-MC on informative benchmark sets.
