Abstract
In this chapter, we will introduce TLA+ proper and use it to write more powerful specs with complex invariants. We’ve already been using some TLA+. All of our variables were defined in terms of TLA+ expressions. All of our values, sets, sequences, and structures were TLA+ expressions. All of our conditionals were TLA+ expressions. PlusCal was just a framing structure, a simplified assignment rule, and a few extra keywords.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2018 Hillel Wayne
About this chapter
Cite this chapter
Wayne, H. (2018). Operators and Functions. In: Practical TLA+. Apress, Berkeley, CA. https://doi.org/10.1007/978-1-4842-3829-5_3
Download citation
DOI: https://doi.org/10.1007/978-1-4842-3829-5_3
Published:
Publisher Name: Apress, Berkeley, CA
Print ISBN: 978-1-4842-3828-8
Online ISBN: 978-1-4842-3829-5
eBook Packages: Professional and Applied ComputingProfessional and Applied Computing (R0)Apress Access Books