Re: [tlaplus] How to watch the variables of the instantiated module in error trace caused by a wrong refinement mapping?

Hello,

have a look at the tab "Error-trace exploration" of the Toolbox: there you can enter any state-level _expression_ that you want TLC to evaluate at each state of the error trace. In particular, you can use it to evaluate the _expression_ va that you use as a refinement mapping.

Hope this helps,

Stephan

On 31 Oct 2018, at 13:06, Hengfeng Wei <hengx...@xxxxxxxxx> wrote:

To model check that module A implements/refines module B,
(for example, A is MinMax1 and B is MinMax2 in the paper "Auxiliary Variables in TLA+" by Leslie Lamport and Stephan Merz, 2017)
we add a refinement mapping like
M == INSTANCE B WITH vb <- va
to module A and check that
THEOREM Spec => M!Spec,
where vb is a variable of B, va is a variable of A,
Spec is the specification of A, and M!Spec refers to the specification of B.

Suppose that the refinement mapping is wrong.
This will raise an error like "Action property line xx of module B is violated" and produce an error trace.
However, the error trace only shows the variables of module A.

How to watch the variables (for example vb here) of the instantiated module B in the error trace?
It may help to "debug" the refinement mapping.

What is your experience in debugging a wrong refinement mapping
given that the error information "Action property line xx of module xx is violated" is hard to use.

Thanks.
Hengfeng Wei

--
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+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.