TLA+ Wiki

This is an old revision of the document!

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, create a .tla file, or open a new file and click on "select a language" and specify TLA:

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<html>^{</html>+<html>}</html> specification (that will be added right into this file) and check it for errors.

We now have a simple specification. In order to check it using TLC, we need to create a model file first. As an experiment, try running TLA+: Check model. It should fail because of the missing model file, and show two notification boxes that allow you to create a model file from a template: Create a new file "squares.cfg" in the same directory (either manually or by using the Create .cfg button), and use the following configuration:

SPECIFICATION Spec

Now we're ready to check the spec by running the command TLA+: Check model.

This will start the TLC tool on the currently open specification and display its progress and final result in a special panel.

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.

Getting Started