Practical TLA+: Planning Driven Development

© Hillel Wayne 2018

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

3. Operators and Functions

Hillel Wayne¹ 

(1)

Chicago, Illinois, USA

 

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.

Now that we know this, we can express it more formally and leverage what it actually means.

Operators

An operator is the TLA+ equivalent of a procedure in programming. You write ...