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

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,

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),

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

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

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/ed274f2e-1849-43fe-bc9d-2d2d2b6f2e0d%40googlegroups.com.