Practical TLA+: Planning Driven Development

© Hillel Wayne 2018

Hillel WaynePractical TLA+https://doi.org/10.1007/978-1-4842-3829-5_6

6. Temporal Logic

Hillel Wayne¹ 

(1)

Chicago, Illinois, USA

 

So far everything we’ve done has been testing invariants: statements that must be true for all states in a behavior. In this chapter, we introduce temporal properties: statements about the behavior itself. Temporal properties considerably expand the kinds of things we can check, providing a range of techniques that few other tools can match. Some examples of temporal properties:

• Does the algorithm always terminate?

• Will all messages in the queue get processed?

• If disrupted, will the system return to a stable state over time?

• Is the database eventually consistent?

Temporal properties are very powerful but ...