Introduction to TLA+ Model Checking in the Command LineI started playing around with TLA+ and its more programmer friendly variant PlusCal about a year ago. At that time the amount of documentation that was understandable to people like me who do not enjoy reading white papers full of mathematical notation was slim to none. (Today you can buy Hillel Wayne’s excellent book Practical TLA+) So I started reading other people’s code (errr…specs) and began
