This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |
| using:vscode:getting_started [2025/09/17 17:59] – fponzi | using:vscode:getting_started [2025/09/17 18:00] (current) – fponzi |
|---|
| 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: | 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 |}} | {{ :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 .cfg button), and use the following configuration: | 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> | <code> |
fponzi