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

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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

-- 
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/81eb7340-dbe9-e147-179b-315000382513%40lemmster.de.