Apply TLA+ to real-world problems and gain the building blocks to get started with your own specifications. This book is a practical, comprehensive resource on TLA+ programming with rich, complex examples that show you how to use TLA+ to specify a complex system and test the design itself for bugs.