Getting Started

The easiest way to get a simple working model is to create an empty PlusCal algorithm, translate it into a TLA⁺ specification and run the TLC tool on it. Here's a step by step instruction:

Create a specification file. Let's name it squares.tla.

Make the file a TLA⁺ module. To do it, start typing module and select the "Create new module (TLA+)" snippet from the drop-down list. The snippet will expand into module header and footer.

Use another snippet pluscal ("Create PlusCal block (TLA+)") to create an empty PlusCal algorithm. So far, we've got the following file:

---- MODULE squares ----
EXTENDS TLC, Integers

(*--algorithm squares

begin
    skip;
end algorithm; *)
====

Add some simple logic to it. For instance, let's make it check that squares of numbers from 1 to 10 do not exceed 100:

---- MODULE squares ----
EXTENDS TLC, Integers

(*--algorithm squares
variables
    x \in 1..10;

begin
    assert x ^ 2 <= 100;
end algorithm; *)
====

Run command TLA+: Parse module. It will translate the PlusCal algorithm to a TLA⁺ specification (that will be added right into this file) and check it for errors.

We now have a simple specification that we can check by running the command TLA+: Check model. It will start the TLC tool on the currently open specification and display its progress and final result in a special panel.

One of the artifacts that the TLC command creates when running on a .tla file with a PlusCal algorithm is a .cfg file that contains the model parameters. If you don't use PlusCal in your specification, the model configuration file will not be created automatically, but the extension will warn you about its absence and propose you to create it from a simple template.

You can find the full output of the TLC tool in a .out file that will be created near your specification. Should you need to visualize an output from a previous model checking, use the command TLA+: Visualize TLC output on a .out file.

Should you have any problems while checking the TLA⁺ module or running TLC, please, refer to the Troubleshooting page, it might provide a solution.