[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Open an Error Trace in Toolbox

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.



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

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c8438cb1-15f4-433e-b0ea-53610e50ed11%40googlegroups.com.