Markus Alexander Kuppe

I ran out of time! Any takers to *update/refactor* the now-removed tests in https://github.com/tlaplus/vscode-tlaplus/commit/1d9161c7cbb99a40682f14446aabf71c237cafbf#diff-5ad2ff4a54440bf2b50b351c7d6092744831ab604bc4f3cbbda8757029a50b1b?

The extension has only limited support for TLA+ functions, i.e., the domain ([ValueKey](https://github.com/tlaplus/vscode-tlaplus/blob/4a0d7233df210ebada17ba2252da7a6b14560c3d/src/model/check.ts#L117)) of its [StructureValue](https://github.com/tlaplus/vscode-tlaplus/blob/4a0d7233df210ebada17ba2252da7a6b14560c3d/src/model/check.ts#L295-L336) can only be string or numeric. However, the domain may be any value in...

It's impossible to see which elements have been added with bags:  @afonsonf Would it be possible to highlight the added elements of a set in addition to adding the...

Here's a screenshot of the same trace in both IDEs. If I recall correctly, Toolbox does a better job of highlighting added, removed, or modified values within deeply nested structures....

/cc @craft095

> TLA+ has a lot of boilerplate. One of the most notorious examples is UNCHANGED rules. Specifications are extremely precise — so precise that you have to specify what variables...

Updating `vars` is just one part of the process when adding new variables to a spec. @hwayne, did you intentionally leave out the other aspects—like updating the initial predicate and...

AI-assisted code completion in Cursor and Visual Studio Code seems quite effective at adding a newly introduced variable to the various UNCHANGED sections throughout a specification.

Ad-hoc solution with a Jupyter notebook: Python code used to generate the plot ```python import pandas as pd import matplotlib.pyplot as plt import matplotlib.cm as cm import seaborn as sns...

@melhindi If TLC is run with the `-coverage` parameter, a subset of the coverage data is made available in the `TLCGet(“spec”)` register. For instance, if `PrintCoverage` is configured as a...