Re: [tlaplus] Fail to visualize my own error trace in ShiViz

Hi Markus,

"For ShiViz however you are copying the raw output."

As I understand, the trace fed into ShiViz should contain the "Clock" and "Host" info,

which are computed by "Exploring" the raw error trace.

I noticed that the example error trace provided in Issue #267: Self-referential error trace exploration: _TEPosition and _TETrace operators

has cryptic action names.

So, what do you mean by "copying the raw output"?

Thanks for your efforts.

Best regards,

hengxin

On Friday, August 2, 2019 at 1:16:10 AM UTC+8, Markus Alexander Kuppe wrote:

On 01.08.19 01:20, Hengfeng Wei wrote:
> By the way, how should I keep the name of the next action at each step
> in a counter-example?
>
> It seems that the resulting execution after "Explore" some
> variables/expressions using "Error-Trace Exploration"
> does not contain the action names;
> they are all replaced by something like "<next_156464730045352000 line
> 274, col 3 to line 308, col 2 of module TE>".

Hi hengxin,

replacing the cryptic "<next_156464730045352000 line 274, col 3 to line
308, col 2 of module TE>" with the action's location in the original
spec is handled by the Toolbox when it processes the raw output of TLC.

For ShiViz however you are copying the raw output. As a workaround you
can add an auxiliary variable to your spec that captures the name of the
action:

VARIABLES act

ActionA1 == /\ act' = "A1"
/\ ...

For a spec with a pc variable, a trace _expression_ can usually extract
the name of the current action from the value of pc.

Issue #344 [1] discusses ideas how a future Toolbox release [1] might
address this problem.

Hope this helps,
Markus

[1] https://github.com/tlaplus/tlaplus/issues/344