Re: [tlaplus] Open an Error Trace in Toolbox

[Markus Kuppe]

On 07.11.19 05:12, William Schultz wrote:
> Is it possible to open a textual error trace generated by TLC in the
> Toolbox's Error Trace viewer? Sometimes I run TLC from the command line
> and then want to view the error trace in a nicer UI. It would also make
> it easier to share traces, since people could open up the trace in the
> Toolbox instead of reading through the raw text.

Hi Will,

if you run TLC from the command line with the "-tool" parameter, you can
import its output into an existing Toolbox model [1]. The Error Trace
viewer will then open up automatically if the output contains a trace.

Best
Markus

[1]
https://user-images.githubusercontent.com/88777/68412021-614a1080-0140-11ea-80d2-aa08dea55e05.gif

PS: Beware https://github.com/tlaplus/tlaplus/issues/389

[Andrew Lygin]

Hi Will, Marcus,

BTW, the VS Code extension also supports visualization of the existing .out files (there's the "Visualize TLC output" command for that). It works if the -tool option was used when running TLC to generate the file.

Thus, sharing error traces between users with different tools should be easy.

[william...@10gen.com]

Got it. Thanks!