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 ...
