Fail to visualize my own error trace in ShiViz

[Hengfeng Wei]

Dear all,

I am trying the "error-trace visualization" features introduced in the new TLC version (1.6.0 of 10 July 2019),

following Issue #267: Self-referential error trace exploration: _TEPosition and _TETrace operators.

I succeeded in visualizing error-trace.txt provided as an example in ShiViz.

However, I failed to visualize my own error-trace (see the attachment) and got the following error info:

"The parser RegExp you entered does not capture any events for the execution".

I don't quite understand the regexp and I just modify the one in the example file.

What is wrong with my error trace file?

Best regards,

hengxin

[Markus Kuppe]

Hi hengxin,

there are two issues:

First, the "state" and "msgs" groups of the regular expression do not match linebreaks ("\n").  Just change the regex to (non-greedily) match newline chars  and terminate matching "msgs" with "}": 

^(State ){0,1}(\d*): <(?<event>(?!Initial predicate).*)>\n\/\\ Clock = (?<clock>.*)\n\/\\ pc = (.*)\n\/\\ state = ((.|\n)*?)\n\/\\ Host = (?<host>.*)\n\/\\ msgs = (?<msgs>(.|\n)*?)}$

I found that it works best to check the regular expression in a regex tester such as [1] because of the limited error reporting in ShiViz.

Secondly, the "Clock" trace variable is ill-formed (quoting):

/\ Clock = {"'p1':'2'", "'p3':'2'", "'p2':'3'"}

has to be:

/\ Clock = {"p2":2, "p1":2, "p3":3}

Please share the "Clock" trace expression if things don't work out.

Hope this helps
Markus

[1] https://regex101.com/r/6Z3wKS/3

[Hengfeng Wei]

Hi Markus,

The regexp you suggest works well.

Great thanks.

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>".

Best regards,

hengxin

[Markus Kuppe]

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

[Hengfeng Wei]

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

[Markus Kuppe]

On 02.08.19 07:19, Hengfeng Wei wrote:
> So, what do you mean by "copying the raw output"?

Hi hengxin,

what I mean by it is the trace printed by TLC to the Toolbox's TLC
Console. It is what you copy&paste into ShiViz as input.

Best
Markus

[Hengfeng Wei]

Hi Markus,

Thanks.

Best

hengxin