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

Now I see.

Thanks.

Hengfeng Wei

On Wednesday, October 31, 2018 at 8:31:34 PM UTC+8, Stephan Merz wrote:

You'd have to write M!vb since vb is not known in module A, right? But then, this should produce the same result since you replaced vb by va in the module instantiation.

Stephan

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

Thanks for your instructions.

Now I can evaluate the _expression_ va used as a refinement mapping.
However, when I evaluate the variable vb of module B in "Error-Trace Exploration",
I get an error "unknown operator vb".

I want to evaluate the variable vb of module B, so that I can compare va and vb and debug the wrong refinement mapping.
Is it possible to do that?
Or is there a better way to debug a wrong refinement mapping?

Best regards,
Hengfeng Wei

On Wednesday, October 31, 2018 at 8:17:38 PM UTC+8, Stephan Merz wrote:
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...@gmail.com> 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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

--
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...@googlegroups.com.
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.