PGo Usage

This page shows how to use PGo. For a description of Modular PlusCal, see Modular PlusCal page.

How to install PGo

1. Install Go toolings (at least version 1.8; newer versions are supported).
2. Install a Java runtime environment (version 8 or 9), e.g. OpenJDK 8.
3. Get the latest TLA+ toolbox by downloading and extracting the appropriate zip file beginning with TLAToolbox.
4. Get the latest PGo release by downloading the jar file.

How to run PGo

Run PGo with the following command, replacing /path/to/pgo.jar with the path to PGo jar file downloaded earlier, and /path/to/spec.tla with the correct path to the specification file.

java -jar /path/to/pgo.jar -m /path/to/spec.tla

To see supported command line arguments, use the following command, replacing /path/to/pgo.jar with the path to PGo jar file downloaded earlier.

java -jar /path/to/pgo.jar --help

For example specifications, see PGo's examples.

Example verification workflow

In this section, we'll go over how to verify a load balancer. We'll get PGo's example load balancer specification, compile it to PlusCal using PGo, compile the resulting PlusCal to TLA+ using the TLA+ toolbox, and then verify some invariants and properties of the specification in the toolbox.

1) Download PGo's example load balancer specification.

2) Compile the specification to PlusCal (output in the same file) using PGo with the following command, replacing the example paths with appropriate paths.

java -jar /path/to/pgo.jar -m /path/to/load_balancer.tla

3) Open the load balancer specification in the TLA+ toolbox (by going to File > Open Spec > Add New Spec... > Browse...).

4) Press Ctrl-t to compile PlusCal to TLA+ (output in the same file).

5) On the left pane, right click on models, select New Models..., and name the new model. The created model is opened on the right pane.

6) In What is the model? on the lower right side, double click on each item and fill in the following values.

Item	Value
GET_PAGE	1
NUM_CLIENTS	1
NUM_SERVERS	1
BUFFER_SIZE	1
WEB_PAGE	1

You can vary the values as you see fit.

7) Scroll down and expand out Invariants and Properties on the lower left side.

8) In Invariants, click Add, type in BuffersOk, and click Finish.

BuffersOk (found on line 501) states that the buffer must not underflow nor overflow.

9) In Properties, click Add, type in ClientsOk, and click Finish.

ClientsOk (found on line 515) states that the client requesting a web page eventually receives that web page.

What to check? should now look like the following.

10) Click Run TLC on the model. (the green circle with a white triangle that looks like a play button)

Below is an example output.

The output shows that TLC ran for 6 seconds in breath-first search mode. It found 3033 states, out of which 1274 states are distinct (visited states are not rechecked). The specification satisfies the invariant BuffersOk and property ClientsOk so TLC output No errors.

Example invariant violation

In this section, we'll modify the example load balancer to see an example violation of desired invariant BuffersOk.

1) Open the load balancer specification in the TLA+ toolbox.

2) Comment out line 234, which instructs the client to wait until the buffer is not full before sending a message. Press Ctrl-s to save.

3) Recompile the file using PGo.

4) Reload the file when asked to do so in the toolbox.

5) Press Ctrl-t to recompile to TLA+.

6) Open the created model and run it.

TLC shows that invariant BuffersOk is violated.

The Error-Trace pane shows how BuffersOk is violated. In this case, the client sent two messages to the server, which overflows the network buffer of size one.