> And it's very easy to make specs that will take forever to validate - and often tough to tell what change made it so. For example, if you simulate four indepe

> And it's very easy to make specs that will take forever to validate - and often tough to tell what change made it so. For example, if you simulate four independent processes that count to three, it'll evaluate all the ways those processes could be interleaved in a fraction of a second. But if you increase that three to ten? The model checker will run and run and run. Do you need to leave it to run over night? Wait the age of the universe? As far as I can tell, the only way to know is to wait, and the only way to figure out the cause of the slowness is to undo the changes to your file until it starts checking in a reasonable time. Given N deterministic sequential processes with M steps each, the total number of possible behaviors is `(NxM)!/M!^N`. So for 4 processes that count to 10 each, that's `40!/10!^4`, or 4.7 * 10^21 behaviors. If they count to 3 each, that's just 370,000 behaviors.