I have generated a few machines for performance testing of ProB (see how it scales with increasing number of variables, constants, operations, ...).
This can be used to maybe help detect some supoptimal parts of probcli and ProB2UI.
When moving from Generated1000.mch to Generated2000.mch the time to execute an operation (or move back in the animator) increases from 5 seconds to 30-40 seconds. This is an indication of some quadratic (or worse) behaviour.
(For a quadratic algorithm doubling the input size quadruples the runtime).