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

*From*: Ron Pressler <ron.pr...@xxxxxxxxx>*Date*: Sat, 19 May 2018 07:06:20 -0700 (PDT)*References*: <CAEvOcXLQzbceJr0XEABGdfQgo77rjCUponKdxHWjdTi6iZTdNg@mail.gmail.com> <ddf88736-1fb3-470b-a8e9-1930b675415e@googlegroups.com> <CAEvOcXJcHhY+OebsFfMEDRWBE_NX9bW9wS6xe3sk8MRPRGtR4w@mail.gmail.com>

Oh, even if they are different there is no need to change their names, but you will need to write a non-trivial refinement map (e.g. M1 ≜ INSTANCE M1 WITH y ← y*5, z ← z - w). If they are very different (the specs progress at different speeds etc.) you may need to add auxiliary variables to M2, which you'd use in the refinement mapping to calculate M2's y and z.

On Saturday, May 19, 2018 at 3:00:45 PM UTC+1, Pedro Paiva wrote:

Ok, so I should try with refinement maps. I did make it clear, but the variables y and z behave differently in M1 and M2, that's why I want to hide them. When TLC checks the property Spec => M1!Spec, it looks for variables with same names (in M1 and in M2) and compares their behaviors, is it correct? So my problem would be solved if I changed the names of y and z in module M1? ThanksPedro

**References**:**Checking implementation***From:*Pedro Paiva

**Re: Checking implementation***From:*Ron Pressler

**Re: [tlaplus] Re: Checking implementation***From:*Pedro Paiva

- Prev by Date:
**Re: [tlaplus] Re: Checking implementation** - Next by Date:
**No detailed information from TLA+ Parser Error** - Previous by thread:
**Re: [tlaplus] Re: Checking implementation** - Next by thread:
**No detailed information from TLA+ Parser Error** - Index(es):