Introduction
In this chapter we’ll be introducing PlusCal. PlusCal is a language that compiles down to TLA+. Lamport developed it in 2009 to make TLA+ more accessible to programmers. Most of the things we’ll want to do will be significantly easier in PlusCal than in TLA+. This chapter will cover all of PlusCal with the exception of multiprocess algorithms, which is Chapter 5; and fair processes, which is Chapter 6.
Specifications
Layout of a Spec
To start, let’s take one of the examples of the bank transfer from the last chapter.
---- (1) MODULE wire (2) ----
EXTENDS Integers \* (3)
(*--algorithm wire \* (4)
variables ...
