Performance of distributed TLC

[Ilya Shchepetkov]

Hello everybody,

Recently I've tried to run TLC in distributed mode (ad hoc), but was a bit disappointed with its performance. If I run server and worker on the same computer, then the performance (number of explored states per minute) is roughly twice as bad as when running TLC in its usual mode. When I add another worker, on a separate computer, the performance barely improves, if at all.

Is it an expected behavior? How many computers are typically required to see the benefits of distributed mode?

~ ilya shchepetkov