tlaplus/vscode-tlaplus

TLA+ language support for Visual Studio Code

TLA⁺ for Visual Studio Code

This extension adds support for the TLA⁺ formal specification language to VS Code. It also supports running the TLC model checker on TLA⁺ specifications.

Features

• TLA⁺ and PlusCal syntax highlighting and code snippets.
• Running the PlusCal-to-TLA⁺ translator and module parser.
• Running TLC model checker on TLA⁺ specifications.
• Model checking process and result visualization.
• Evaluating constant expressions.
• Converting TLA⁺ specifications to LaTeX and PDF documents.
• Code completion.
• Code on-type formatting.
• Powered by the official TLA⁺ tools.

Documentation

The project's Wiki provides information on how to install, configure and use the extension.

• How to Install
• Getting Started
• Settings
• Commands
• Setting up Environment
• Caveats
• Troubleshooting

Contributing

All forms of contribution are highly welcome! Feel free to file bugs, propose improvements, ask questions, send other feedback.

If you decide to pitch in and write some code, this document will provide you with useful information: CONTRIBUTING.md.

TLA⁺ Resources

If you're not familiar with TLA⁺, but want to get a grasp on it, the following list of resources is a good starting point:

• TLA⁺ Home Page on Leslie Lamport's website.
• Introduction to TLA⁺ and PlusCal by Hillel Wayne.
• TLA⁺ in Practice and Theory by Ron Pressler.
• A collection of TLA⁺ specification examples in the TLA⁺ repository.

License

MIT

vscode-tlaplus's Issues

Coverage total/distinct numbers are swapped

In the coverage table, the Total column now displays the distinct count and vise versa.

Show full TLC output in the same view column in which the visualization is displayed

When the user clicks the "Full output" link in the TLC output visualization panel, the corresponding .out file is opened in the ViewColumn.One. It would be better to open it in the view column where the visualization panel is placed, letting the user see both the specification and the output.

Better to have code formatting

TLC output not parsed correctly when there's no new line between messages

When running TLC on Windows, there're lines that contain both a message end marker and the next message start marker:

@!@!@STARTMSG 2193:0 @!@!@
Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = 1.1E-19
@!@!@ENDMSG 2193 @!@!@@!@!@STARTMSG 2201:0 @!@!@
The coverage statistics at 2019-08-17 00:11:08
@!@!@ENDMSG 2201 @!@!@

It must be handled correctly.

SANY output parser doesn't capture errors with no location

This error is not captured:

Parsing file /Users/tla/foo.tla
Parsing file /private/var/folders/7p/g0v7k97x1t3b06j8274rhh0h0000gn/T/TLC.tla

Fatal errors while parsing TLA+ spec in file operators

tla2sany.semantic.AbortException
*** Abort messages: 1

Unknown location

Cannot find source file for module Sequence imported in module foo.

Implement command for checking model

Implement command "Check model" that runs tla2tool.jar with a TLA⁺ module as a parameter.

The command output must be displayed somehow.

Handle tla2tools result codes

If tla2tools exits with a code 1-9 or 255, it means that there's a problem with tooling (probably with Java options). We must handle it properly, warn the user and guide him through the process of fixing the problem.

Display program output

Display output generated by Print and PrintT in the check model view.

Support constant operators detection

The TlaDocumentSymbolsProvider stumbles on operators while parsing constants and doesn't report them as model symbols. As a result, const operator names don't appear in the outline panel and in completion suggestions. Such operators also prevent parsing of the following constants.

A simple case:

CONSTANT Foo(_), Bar

Neither Foo nor Bar makes it to the model symbols list now.

Display TLC warnings

We now collect TLC warnings from its output but never display them. It would be cool to display them the same way we display errors -- to have the "Warnings" block in the output visualization panel.

SANY output parser doesn't capture paring errors with no leading line

This error is not captured at the moment:

***Parse Error***
Encountered "Beginning of definition" at line 21, column 38 and token ":" 

Unexpected end of message

The following output causes the Unexpected end of message error:

@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.14 of 10 July 2019 (rev: 0cae24f)
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 95 and seed -5827499341661814189 with 1 worker on 4 cores with 1820MB heap and 64MB offheap memory [pid: 47842] (Mac OS X 10.14.5 x86_64, Amazon.com Inc. 11.0.3 x86_64, MSBDiskFPSet, DiskStateQueue).
@!@!@ENDMSG 2187 @!@!@
@!@!@STARTMSG 1000:1 @!@!@
TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a tlc2.tool.ConfigFileException
: @!@!@STARTMSG 5006:0 @!@!@
TLC found an error in the configuration file at line 6
It was expecting = or <-, but did not find it.
@!@!@ENDMSG 5006 @!@!@
@!@!@ENDMSG 1000 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 262ms at (2019-08-18 21:16:19)
@!@!@ENDMSG 2186 @!@!@

Support custom TLA tools options

Allow the user to provide custom options for TLA tools.

Don't mix results of the running model checking process with data from .out file

1. Start model checking process
2. While it's still running, open the visualization of a .out file
3. When the running process produce some output, the .out file view will be overwritten

If the user opened a .out file, the visualization must not be overwritten by the running model checking process.

Parse and display PlusCal transpiler warnings

PlusCal transpiler output parser only captures errors, but the transpiler itself also generates warnings that would be cool to capture too. Those warning messages are one-liners of format Warning: {text} with no location information. For instance:

Warning: symbols were renamed.

associated generated errors with pluscal errors

In the toolbox if the generated TLA code has an error its often possible to jump to the line of pluscal that is the source for the generated error. Is it possible to add this?

Add language for .cfg files

.cfg files are used for configuring models. It'll be very handy to have their syntax highlighted.

Switch to asWebViewUri

VS Code 1.38 came with a new API for building URI's that are used inside WebViews: https://code.visualstudio.com/api/extension-guides/webview#loading-local-content

At the moment, the extension is compatible with VS Code 1.36. After moving to 1.38 as the lowest supported version, we should switch to the new API.

Stop button doesn't work

The button that stops the running TLC process doesn't work after adding security policies.

Function values are not parsed correctly

The following value is parsed with a warning:

foo = (2 :> 3),

It must be displayed as (2 :> 3) in the error trace.

Detect variables changes between states

When parsing states of the model, it's necessary to detect changes: which variables has been added, changed or deleted since the previous state.

Tools don't run if no custom Java options provided

When there're no custom Java options specified in the extension settings, TLA tools run with wrong Java options, hence causing an error.

Change default indentation to 2 spaces

At the moment, the default setting for the code formatter is 4 spaces. I'd like to change it to 2 spaces for TLA+, PlusCal and .cfg-files, but not sure yet.

4 spaces:

• the default setting in the Toolbox
• the default setting in most of the text editors

2 spaces:

• used in pretty all the TLA+ examples / books / tutorials
• feels more suitable to me, since
  • TLA+ code is usually indented in accordance with /\'s, \/'s and other operators or syntax constructions, so pure tabs are rare
  • PlusCal code is usually not very convoluted, and 2 spaces indentation seems enough to easily navigate its structure
  • .cfg files are even simpler
• IDEs and text editors now provide many tools for dealing with code structure (indentation guide lines, folding, current block highlighting etc.) that doing all this with long spaces seems redundant.

Any input on the issue is welcomed.

Highlight coverage items with no executions

Coverage table rows with zero executions should be highlighted as they usually indicate spec errors.

Support constant expression evaluation

Being able to quickly evaluate constant expressions is very useful, especially when learning TLA⁺.

The Toolbox provides such functionality via the "No Behavior Spec" field. In VS Code I see two options:

• Use a prompt dialog to allow the user to enter a constant expression.
• Treat the currently selected chunk of code as an expression and allow the user to evaluate it.

The expression along with its value or an error message should be send to a separate output channel.

Check sepc existence and create it if necessary

When starting TLC on .tla file, we should check existence of the corresponding .cfg file and suggest the user to create it if necessary.

"Not properly indented" SANY error is not parsed correctly

The error from the following SANY output is not parsed correctly:

TLC2 Version 2.14 of 10 July 2019 (rev: 0cae24f)
Running breadth-first ...
Starting SANY...
Parsing file /Users/bob/foo/foo.tla
***Parse Error***
Item at line 14, col 9 to line 14, col 9 of module foo is not properly indented inside conjunction or  disjunction list item at line 11, col 9 to line 14, col 9 of module foo
Residual stack trace follows:
AND-OR Junction starting at line 9, column 9.
ExtendableExpr starting at line 9, column 9.
Expression starting at line 9, column 9.
Definition starting at line 8, column 1.
Module body starting at line 5, column 1.
Fatal errors while parsing TLA+ spec in file foo
tla2sany.semantic.AbortException
*** Abort messages: 1
In module foo
Could not parse module foo from file foo.tla
SANY finished.
Starting... (2019-09-21 18:53:51)
Parsing or semantic analysis failed.
Finished in 620ms at (2019-09-21 18:53:51)

Save TLC output to a file

TLC output should be saved to a file and displayed to the user on request.

Display TLC output in an output panel

The extension now sends TLC output to a .out file. It would be better to send it to an output panel and let the user opt out .out-files creation.

Variable values in the range format are not parsed correctly

This value is parsed as a numeric constant 3 now:

Foo = 3..9

It must be parsed as a value with the string representation 3..9

Display TLC output in a separate view

TLC output must be parsed on the fly and displayed in a WebView.

Parse and display error traces

Error traces, emitted by TLC, must be parsed and displayed in the Model check result view.

Stuttering is not displayed correctly

When model checking fails because of stuttering, the final element of the error trace (Stuttering) is not displayed.

PlusCal syntax highlighting breaks if --algorithm is not on line of open comment

This is extremely minor, but maybe worth noting in a wiki page. PlusCal syntax highlighting won't work if the algorithm is written as:

(*
--algorithm WriteStealing
{
{
    skip;
}
}
*)

However, it does work if the algorithm is written as:

(*--algorithm WriteStealing
{
{
    skip;
}
}
*)

Display results of the last executed model checking, not for the last shown

1. Start model checking
2. While it's not finished, open some previously generated .out file
3. Close Model checking result view
4. Click on the button in the status bar to reveal the Model checking result view

It'll display either the currently running model checking process (if there was some output during our actions), or the previously opened .out file. It must always be the last checking process.

So, opening a .out file must not meddle in the ongoing checking process.

Check Java version

Check Java version when the user changes configuration and when there're problems with running tla2tools.

Allow to jump from the TLC visualization panel to spec files

Coverage statistics, error messages and error trace items provide locations of the corresponding specification elements. Such locations must be presented as links that would allow to jump right to the model or config file.

"Back to state" state is not parsed correctly

If model checking fails with the "Back to state" state, this state isn't displayed correctly.

Support custom Java options

Allow the user to provide custom Java options for the TLA tools.
Be careful with options that change GC, since we manually provide ParallelGC now.

How to install

Installation instruction would be nice to have.

This is awesome

No real issue, just wanted to say how much I appreciate you making this :D

Add code blocks formatting

The extension now supports on-type formatting, i.e. automatic code indentation while the user is typing.

It would be great to also support formatting of the selected code blocks (including the whole document), though there's a great deal of questions about the proper way of TLA⁺ code formatting that should be answered before the implementation.

Allow to stop TLC process

There must be a way to stop the running TLC process.

Add progress indicator to the status bar

Now, the only way to see the model checking progress is on the panel that is opened when check process is launched. If the user closes this panel, it's impossible to get it back and see what's going on.

There must be an indicator in the status bar that would show the current checking status and allow to reopen the Model Checking view page.

A command to generate PDF

TLA toolbox can generate PDF from a specification. It would be nice to able to generate PDF in VS Code too.

Add code completion in .cfg files

Implementing keywords completion in .cfg files should be very easy. It's just a small part of TlaCompletionItemProvider.

Add code completion in TLA+ code

The extension now has enough information to complete keywords, embedded constants, operators and some symbols in TLA+ code.

Handle PlusCal transpiler error when there's no PlusCal code

If PlusCal transpiler is running on a file with no PlusCal code, it returns a single error:

Unrecoverable error:
 -- Beginning of algorithm string --algorithm not found.

In this case, the error should be ignored.

It also makes sense to not not run the transpiler on such files at all.

Parse SANY messages when check model

When a model is being checked, there's a block fo SANY output that must be parsed and errors (if any) must be shown.

Merged functions are not parsed correctly

The following output is not parsed as a function:

("foo" :> 1 @@ "bar" :> 2)