[tlaplus] Re: How to understand the concept "step simulation"

[hong.yang.19920124@xxxxxxxxx]

On Wednesday, March 6, 2019 at 10:53:35 PM UTC-8, Oliver Yang wrote:
> Hi All,
> 
> 
> In Section 5.8 of book "Specifying Systems", the "Proving Impl" is introduced. I have a rough understanding of refinement mapping, which
> essentially maps states of Spec A to the states of Spec B. However, I have a hard time understanding "step simulation". 
> 
> 
> 
> 1) What's the purpose of introducing the invariant Inv in Formula 5.3? What are we trying to achieve here?
> 2) How do we derive the mapping: omem = vmem, octl = ..., obuf = buf? It looks like we jumped to the conclusion without showing any proof?
> 
> 
> Thanks,
> 
> 
> Oliver

Any suggestion will be much appreciated : )

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