Yes, thank you, that was very interesting and insightful -- I've read it before, in fact it sparked my initial interest in TLA+. Unfortunately this is not necessarily applicable for a "working programmer" aka "poor man without huge resources at his disposal". Maybe I should work on the latter problem and then start to apply TLA+. Or maybe it should be the other way 'round. :)