using:vscode:getting_started

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
====== Getting Started ======

The easiest way to get a simple working model is to create an empty PlusCal algorithm, translate it into a TLA<sup>+</sup> 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<sup>+</sup> 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:

<code tla>
---- MODULE squares ----
EXTENDS TLC, Integers

(*--algorithm squares

begin
    skip;
end algorithm; *)
====
</code>

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:

<code tla>
---- MODULE squares ----
EXTENDS TLC, Integers

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

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

Run command ''%%TLA+: Parse module%%''. It will translate the PlusCal algorithm to a TLA<html><sup></html>+<html></sup></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:
{{ :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:

<code>
SPECIFICATION Spec
</code> 

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<sup>+</sup> module or running TLC, please, refer to the [[using:vscode:troubleshooting|Troubleshooting]] page, it might provide a solution.