1. I can't help you on that.
2. The diameter isn't a particular important measure. What you want
to do is limit the size of the state space. To learn the mechanisms
for doing that, see the Model Checking section of the Help. Of
special interest is the State Constraint section of Creating a Model >
Advanced Option Page. The mistake beginners usually make is not to
start by checking very small models (ones with few enough states to
terminate quickly).
The most effective way to limit the number of states is to write a
better spec. The art of specification is to find the simplest, most
abstract spec that captures the essence of your algorithm. For an
example, you might want to look at my specification of Paxos that I
believe is in the examples on git.
When you've got the simplest abstraction that accurately describes the
algorithm, model checking reasonable sized models may still take a lot
of time. One thing you can then do is to check a simpler, less
accurate model whose executions take fewer steps--that is, a spec with
larger atomic actions that describe multiple separate actions of the
original spec. Any error in the simple spec reveals an error in the
original spec. When you're convinced that the system with large steps
is correct, you can then start looking for errors in the more accurate
spec.