Differences

This shows you the differences between two versions of the page.

--- using:vscode:getting_started [2025/05/31 22:47] – fponzi
+++ using:vscode:getting_started [2025/09/17 18:00] (current) – fponzi
@@ Line 7: / Line 7: @@
 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.
+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:
@@ Line 42: / Line 44: @@
 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 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.
+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%%''.
-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.
+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 [[alygin/vscode-tlaplus/wiki/Troubleshooting|Troubleshooting]] page, it might provide a solution.
+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.