Practical TLA+ pp 137-148 | Cite as

State Machines

  • Hillel Wayne


Specifications are more expressive than code. This comes at a cost: it’s not always clear how to go from a specification to reality. A technique for handling this is to write a very abstract spec and expand it into a more detailed, lower-level “implementation” that is closer to the program you’ll be writing. One very common pattern for doing this is to use a state machine. In this chapter, we will learn how to represent them and use them in writing our specifications.

Copyright information

© Hillel Wayne 2018

Authors and Affiliations

  • Hillel Wayne
    • 1
  1. 1.ChicagoUSA

Personalised recommendations