Differences

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

--- using:vscode:getting_started [2025/09/17 10:09] – fponzi
+++ using:vscode:getting_started [2025/09/17 18:00] (current) – fponzi
@@ Line 44: / 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:
-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.
+<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.