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, 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 model file" 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.