| |
| |
| List of Figures and Tables | |
| |
| |
| Acknowledgments | |
| |
| |
| Introduction | |
| |
| |
| |
| Getting Started | |
| |
| |
| |
| A Little Simple Math | |
| |
| |
| |
| Propositional Logic | |
| |
| |
| |
| Sets | |
| |
| |
| |
| Predicate Logic | |
| |
| |
| |
| Formulas and Language | |
| |
| |
| |
| Specifying a Simple Clock | |
| |
| |
| |
| Behaviors | |
| |
| |
| |
| An Hour Clock | |
| |
| |
| |
| A Closer Look at the Specification | |
| |
| |
| |
| The Specification in TLA+ | |
| |
| |
| |
| An Alternative Specification | |
| |
| |
| |
| An Asynchronous Interface | |
| |
| |
| |
| The First Specification | |
| |
| |
| |
| Another Specification | |
| |
| |
| |
| Types: A Reminder | |
| |
| |
| |
| Definitions | |
| |
| |
| |
| Comments | |
| |
| |
| |
| A Fifo | |
| |
| |
| |
| The Inner Specification | |
| |
| |
| |
| Instantiation Examined | |
| |
| |
| |
| Instantiation Is Substitution | |
| |
| |
| |
| Parametrized Instantiation | |
| |
| |
| |
| Implicit Substitutions | |
| |
| |
| |
| Instantiation Without Renaming | |
| |
| |
| |
| Hiding the Queue | |
| |
| |
| |
| A Bounded FIFO | |
| |
| |
| |
| What We're Specifying | |
| |
| |
| |
| A Caching Memory | |
| |
| |
| |
| The Memory Interface | |
| |
| |
| |
| Functions | |
| |
| |
| |
| A Linearizable Memory | |
| |
| |
| |
| Tuples as Functions | |
| |
| |
| |
| Recursive Function Definitions | |
| |
| |
| |
| A Write-Through Cache | |
| |
| |
| |
| Invariance | |
| |
| |
| |
| Proving Implementation | |
| |
| |
| |
| Some More Math | |
| |
| |
| |
| Sets | |
| |
| |
| |
| Silly Expressions | |
| |
| |
| |
| Recursion Revisited | |
| |
| |
| |
| Functions versus Operators | |
| |
| |
| |
| Using Functions | |
| |
| |
| |
| Choose | |
| |
| |
| |
| Writing a Specification: Some Advice | |
| |
| |
| |
| Why Specify | |
| |
| |
| |
| What to Specify | |
| |
| |
| |
| The Grain of Atomicity | |
| |
| |
| |
| The Data Structures | |
| |
| |
| |
| Writing the Specification | |
| |
| |
| |
| Some Further Hints | |
| |
| |
| |
| When and How to Specify | |
| |
| |
| |
| More Advanced Topics | |
| |
| |
| |
| Liveness and Fairness | |
| |
| |
| |
| Temporal Formulas | |
| |
| |
| |
| Temporal Tautologies | |
| |
| |
| |
| Temporal Proof Rules | |
| |
| |
| |
| Weak Fairness | |
| |
| |
| |
| The Memory Specification | |
| |
| |
| |
| The Liveness Requirement | |
| |
| |
| |
| Another Way to Write It | |
| |
| |
| |
| A Generalization | |
| |
| |
| |
| Strong Fairness | |
| |
| |
| |
| The Write-Through Cache | |
| |
| |
| |
| Quantification | |
| |
| |
| |
| Temporal Logic Examined | |
| |
| |
| |
| A Review | |
| |
| |
| |
| Machine Closure | |
| |
| |
| |
| Machine Closure and Possibility | |
| |
| |
| |
| Refinement Mappings and Fairness | |
| |
| |
| |
| The Unimportance of Liveness | |
| |
| |
| |
| Temporal Logic Considered Confusing | |
| |
| |
| |
| Real Time | |
| |
| |
| |
| The Hour Clock Revisited | |
| |
| |
| |
| Real-Time Specifications in General | |
| |
| |
| |
| A Real-Time Caching Memory | |
| |
| |
| |
| Zeno Specifications | |
| |
| |
| |
| Hybrid System Specifications | |
| |
| |
| |
| Remarks on Real Time | |
| |
| |
| |
| Composing Specifications | |
| |
| |
| |
| Composing Two Specifications | |
| |
| |
| |
| Composing Many Specifications | |
| |
| |
| |
| The FIFO | |
| |
| |
| |
| Composition with Shared State | |
| |
| |
| |
| Explicit State Changes | |
| |
| |
| |
| Composition with Joint Actions | |
| |
| |
| |
| A Brief Review | |
| |
| |
| |
| A Taxonomy of Composition | |
| |
| |
| |
| Interleaving Reconsidered | |
| |
| |
| |
| Joint Actions Reconsidered | |
| |
| |
| |
| Liveness and Hiding | |
| |
| |
| |
| Liveness and Machine Closure | |
| |
| |
| |
| Hiding | |
| |
| |
| |
| Open-System Specifications | |
| |
| |
| |
| Interface Refinement | |
| |
| |
| |
| A Binary Hour Clock | |
| |
| |
| |
| Refining a Channel | |
| |
| |
| |
| Interface Refinement in General | |
| |
| |
| |
| Open-System Specifications | |
| |
| |
| |
| Should You Compose? | |
| |
| |
| |
| Advanced Examples | |
| |
| |
| |
| Specifying Data Structures | |
| |
| |
| |
| Local Definitions | |
| |
| |
| |
| Graphs | |
| |
| |
| |
| Solving Differential Equations | |
| |
| |
| |
| BNF Grammars | |
| |
| |
| |
| Other Memory Specifications | |
| |
| |
| |
| The Interface | |
| |
| |
| |
| The Correctness Condition | |
| |
| |
| |
| A Serial Memory | |
| |
| |
| |
| A Sequentially Consistent Memory | |
| |
| |
| |
| The Memory Specifications Considered | |
| |
| |
| |
| The Tools | |
| |
| |
| |
| The Syntactic Analyzer | |
| |
| |
| |
| The TLATEX Typesetter | |
| |
| |
| |
| Introduction | |
| |
| |
| |
| Comment Shading | |
| |
| |
| |
| How It Typesets the Specification | |
| |
| |
| |
| How It Typesets Comments | |
| |
| |
| |
| Adjusting the Output Format | |
| |
| |
| |
| Output Files | |
| |
| |
| |
| Trouble-Shooting | |
| |
| |
| |
| Using LATEX Commands | |
| |
| |
| |
| The TLC Model Checker | |
| |
| |
| |
| Introduction to TLC | |
| |
| |
| |
| What TLC Can Cope With | |
| |
| |
| |
| TLC Values | |
| |
| |
| |
| How TLC Evaluates Expressions | |
| |
| |
| |
| Assignment and Replacement | |
| |
| |
| |
| Evaluating Temporal Formulas | |
| |
| |
| |
| Overriding Modules | |
| |
| |
| |
| How TLC Computes States | |
| |
| |
| |
| How TLC Checks Properties | |
| |
| |
| |
| Model-Checking Mode | |
| |
| |
| |
| Simulation Mode | |
| |
| |
| |
| Views and Fingerprints | |
| |
| |
| |
| Taking Advantage of Symmetry | |
| |
| |
| |
| Limitations of Liveness Checking | |
| |
| |
| |
| The TLC Module | |
| |
| |
| |
| How to Use TLC | |
| |
| |
| |
| Running TLC | |
| |
| |
| |
| Debugging a Specification | |
| |
| |
| |
| Hints on Using TLC Effectively | |
| |
| |
| |
| What TLC Doesn't Do | |
| |
| |
| |
| The Fine Print | |
| |
| |
| |
| The Grammar of the Configuration File | |
| |
| |
| |
| Comparable TLC Values | |
| |
| |
| |
| The TLA[superscript +] Language | |
| |
| |
| Mini-Manual | |
| |
| |
| |
| The Syntax of TLA[superscript +] | |
| |
| |
| |
| The Simple Grammar | |
| |
| |
| |
| The Complete Grammar | |
| |
| |
| |
| Precedence and Associativity | |
| |
| |
| |
| Alignment | |
| |
| |
| |
| Comments | |
| |
| |
| |
| Temporal Formulas | |
| |
| |
| |
| Two Anomalies | |
| |
| |
| |
| The Lexemes of TLA[superscript +] | |
| |
| |
| |
| The Operators of TLA[superscript +] | |
| |
| |
| |
| Constant Operators | |
| |
| |
| |
| Boolean Operators | |
| |
| |
| |
| The Choose Operator | |
| |
| |
| |
| Interpretations of Boolean Operators | |
| |
| |
| |
| Conditional Constructs | |
| |
| |
| |
| The Let/In Construct | |
| |
| |
| |
| The Operators of Set Theory | |
| |
| |
| |
| Functions | |
| |
| |
| |
| Records | |
| |
| |
| |
| Tuples | |
| |
| |
| |
| Strings | |
| |
| |
| |
| Numbers | |
| |
| |
| |
| Nonconstant Operators | |
| |
| |
| |
| Basic Constant Expressions | |
| |
| |
| |
| The Meaning of a State Function | |
| |
| |
| |
| Action Operators | |
| |
| |
| |
| Temporal Operators | |
| |
| |
| |
| The Meaning of a Module | |
| |
| |
| |
| Operators and Expressions | |
| |
| |
| |
| The Arity and Order of an Operator | |
| |
| |
| |
| [lambda] Expressions | |
| |
| |
| |
| Simplifying Operator Application | |
| |
| |
| |
| Expressions | |
| |
| |
| |
| Levels | |
| |
| |
| |
| Contexts | |
| |
| |
| |
| The Meaning of a [lambda] Expression | |
| |
| |
| |
| The Meaning of a Module | |
| |
| |
| |
| Extends | |
| |
| |
| |
| Declarations | |
| |
| |
| |
| Operator Definitions | |
| |
| |
| |
| Function Definitions | |
| |
| |
| |
| Instantiation | |
| |
| |
| |
| Theorems and Assumptions | |
| |
| |
| |
| Submodules | |
| |
| |
| |
| Correctness of a Module | |
| |
| |
| |
| Finding Modules | |
| |
| |
| |
| The Semanties of Instantiation | |
| |
| |
| |
| The Standard Modules | |
| |
| |
| |
| Module Sequences | |
| |
| |
| |
| Module FiniteSets | |
| |
| |
| |
| Module Bags | |
| |
| |
| |
| The Numbers Modules | |