  MCC is a tool designed for a very specific task: to transform the models of
High-Level Petri nets, given in the PNML syntax, into equivalent
Place/Transition nets. The name of the tool derives from the annual
Model-Checking Contest, a competition of model-checking tools that provides a
large and diverse collection of PNML models. This choice in naming serves to
underline the main focus of the tool, which is to provide an open and efficient
solution that lowers the access cost for developers wanting to engage in this
competition. We describe the architecture and functionalities of our tool and
show how it compares with other existing solutions. Despite the fact that the
problem we target is abundantly covered in the literature, we show that it is
still possible to innovate. To substantiate this assertion, we put a particular
emphasis on two distinctive features of MCC that have proved useful when
dealing with some of the most challenging colored models in the contest, namely
the use of a restricted notion of higher-order invariant, and the support of a
Petri net scripting language.

Logic in Computer Science