Detect non-confluent rewrite rules

[tneele]

The data specification of an mCRL2 model is, in general, not assumed to be confluent. However, non-confluent rewrite systems typically lead to unexpected and undesired behaviour. For example: tools yield different results on consecutive runs, the behaviour of jitty and jittyc is different (see issue #1557) etc.

Since a small mistake in a data specification can have such nasty effects, it would be nice if the toolset can detect non-confluence. Of course, this is a very hard problem, but a safe under-approximation may already be able to catch most of the common mistakes. This can for example be built into the lineariser.

[tneele]

Next to confluence detection, we can also consider to add termination detection. This prevents unexpected stack overflows in the rewriter.