Specifying Concurrent Systems with TLA
Leslie Lamport · 1999
Contents 1 Introduction 1 2 A Little Simple Math 2 2.1 Propositional Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2.2 Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.3 Predicate Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 3 Specifying a Simple Clock 6 3.1 Behaviors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.2 An Hour Clock . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.3 A Closer Look at the Hour-Clock Specification . . . . . . . . . . . . . . . . . . 8 3.4 The Hour-Clock Specification in TLA + . . . . . . . . . . . . . . . . . . . . . . . 8 3.5 Another Way to Specify the Hour Clock . . . . . . . . . . . . . . . . . . . . . . 10 4 An Asynchronous Interface 11 4.1 The First Specification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .