I wonder how Alloy compares to Spin/Promela. Alloy sounds like a different way to do precisely the same things. Has it made any progress in reducing the resource requirements via improved algorithms/data structures? That would enable it to model/check larger systems. Or is it just a better language/UI wrapping the same methods?