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

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

On Wednesday, July 31, 2019 at 12:52:58 AM UTC+8, Markus Alexander Kuppe wrote:

On 29.07.19 20:21, Hengfeng Wei wrote:

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?

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