Support projecting an error trace based on the logical processes in a system

Creating useful visualizations Many TLA+ specifications model systems with multiple processes, and users often want to project traces (counterexamples) based on these processes. To address this need, some users have created custom visualizations, while others have requested integrations with third-party tools.

However, TLC already integrates with ShiViz, a tool that can render TLA+ traces as interactive communication graphs (also known as swim lanes). ShiViz, implemented in JavaScript, is easy to integrate into existing tools and is extensible by the community. An enhancement that comes to mind is render all TLA+ variable values of each node. For specifications with a program counter (e.g., a pc variable in PlusCal), the ShiViz module from the CommunityModules repository can automatically reformat traces for use with ShiViz. However, ShiViz itself does not parse TLA+ directly and relies on user-defined regular expressions. This limitation could be addressed by using the TLA+ tree-sitter parser.

An alternative approach is to project variables using TLC primitives, such as an Alias, ANSI colors, and the TLCGetAndSet operator. An example of this technique can be found here, and a real-world use case is in this consensus specification.

This feature should be supported by trace expressions in the command-line interface (see #393 and #555), the VSCode extension, and the TLA+ Toolbox. Additionally, exporting based on this feature could enable integration with third-party tools like UML.

Lastly, @will62794’s tla-web automatically "explodes" variables based on a constant set, offering another potential solution.