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

*From*: Alex Tim <alex.timimin@xxxxxxxxx>*Date*: Sat, 4 Apr 2020 08:58:52 -0700 (PDT)*References*: <50d348f8-4b04-43d6-98bd-5045540ca1d6@googlegroups.com> <10D23B2C-C1F1-419D-A3C1-CD16C78A75CD@gmail.com>

Thanks a lot.

Now i see. This condition guaranties that
we have constructed SpecUP right (it is implemented by initial spec)
using prophecy vars.

Thanksсуббота, 4 апреля 2020 г., 15:42:25 UTC+3 пользователь Stephan Merz написал:

Hello,that condition is necessary for proving(1) Spec => \EE p : SpecUPAs a trivial example, consider definingPredSend(f) == FALSEWith that definition, you can still show that(2) SpecUP => SS!Specholds but you wouldn't be able to concludeSpec => SS!Specbecause you don't have (1). This is explained in more detail in section 4.5.Regards,StephanOn 4 Apr 2020, at 13:20, Alex Tim <alex....@xxxxxxxxx> wrote:Hi all

I'm reading Auxiliary Variables in TLA+ (http://lamport.azurewebsites.net/pubs/auxiliary.pdf ) to understand better

the technique of checking a low level spec satisfying a higher level spec.

There is a question concerning prophecy variables. In the module SendSetUndoP (p. 29) we add a prophecy array var

and check a Theorem

theorem SpecUP => SS!Spec

obviously to show that the spec specUP implements the lower level spec of the module SendSet.

Then it is said (p.29)

We should also check that condition (4.11) holds for each subaction A. To do this, we need to create a model with specication SpecU and have TLC check

the property:

[] [^ Choose => Ef \in [DOM->Pi] : PredChoose(f)

^ Send => Ef \in [DOM->Pi] : PredSend(f )

^ Rcv => Ef \in [DOM->Pi] : PredRcv(f )

^ AS \in subset y:Undo(S) ) => Ef \in [DOM->Pi] : PredUndo(f,S)

]vars

can someone explain why do we need to check this second condition?

or this is just the alternate option of how we check that the spec specUP implements the lower level spec of the module SendSet?

By proving this condition we show that Choose action is equivalent to ChooseP action, Send action is equivalent to SendP action, etc...

Thanks in advance.--

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

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/50d348f8-4b04- .43d6-98bd-5045540ca1d6% 40googlegroups.com

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/42138832-23e9-4a85-8928-d0e036e28dbf%40googlegroups.com.

**References**:**[tlaplus] on prophecy variables***From:*Alex Tim

**Re: [tlaplus] on prophecy variables***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] on prophecy variables** - Next by Date:
**[tlaplus] Re: on prophecy variables** - Previous by thread:
**Re: [tlaplus] on prophecy variables** - Next by thread:
**[tlaplus] Re: on prophecy variables** - Index(es):