Spinroot

[quote=spinroot]there is a way to compile the model checker so that it can take advantage of a network of machines, but splitting memory across those machine in an exhaustive search would add significant overhead. so this currently is not attractive, or even practical.
[/quote]
Thank you for your clarification.

I'm a Spin novice, and my main trouble is estimating the complexity/scalability of the problem I've coded.
Your book explains in detail a number of approaches in order to reduce complexity, and I tried to consider such approaches. However, it is difficult for me to estimate the approximate number of reachable states when I try to scale my problem.

Without (for now) entering the boring details of my specific problem, I'm wondering if it is possible to outline a strategy to estimate the number of reachable states of a Promela program, in order to understand the amount of work required to make the problem tractable. In other words, it is difficult to me to understand if I'm covering 50% or 0.000001% of the reachable states... Knowing such an estimate would be a great help to define a verification strategy, also taking advantage of the swarm tool.