CIF to mCRL2 should linearize the input specification

Currently, the CIF to mCRL2 transformation supports multiple CIF automata, that are all translated to mCRL2 separately.

There are some issues with this:

• The implementation is quite complex. This relates mostly to the complexities of the instance tree, and its relation to the use of events and variables in various CIF automata.
• I looked into adding tau event support (#226 (closed)), but found that rather complex to add, as the whole instance tree and event usage needs to be adapted as well.
• Michel Reniers mentioned to me that "[...] after years of use in education I've found that linearization in mCRL2 of a composition of CIF automata is practically infeasible. Sometimes students have to wait for more than a day on linearization, while in CIF it is finished in seconds." He thus recommends students to first linearize the CIF specification, and then transform it to mCRL2.

I therefore propose to first linearize the CIF specification, and then transform it to mCRL2. The CIF to mCRL2 transformed could do the linearization internally, like we do with most transformations. This has several benefits:

• Simpler code, and less code.
• Easier to extend and maintain the transformation.
• Better performance for using the resulting mCRL2 specifications.

I can't really think of any reasons not to do this. We would lose the structure of the CIF specification in the mCRL2 specification. But as long as the names of objects closely relate to the original names in the CIF specification, and can thus be used in mCRL2 property specifications, I don't see this as a problem.