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.
On Thursday, November 7, 2019 at 8:25:54 PM UTC+3, Markus Alexander Kuppe wrote:
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