====== 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:
{{:using:vscode:vscode_select_language.png?direct&400|}}
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.
{{:using:vscode:vscode-snippet-module.png?direct&400|}}
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. 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:
{{ :using:vscode:490491581-c07ab104-e45c-43e3-bbc1-29a32cad6c74.png?direct&400 |}}
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 [[using:vscode:troubleshooting|Troubleshooting]] page, it might provide a solution.