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

*From*: divyanshu ranjan <idivyanshu.ranjan@xxxxxxxxx>*Date*: Mon, 22 Apr 2024 04:45:33 -0700 (PDT)*References*: <e847b7cb-10a5-4d4a-879d-8911825c2762n@googlegroups.com>

Hello,1. It is mentioned in section 8.9.4 of Specifying Systems that substitution does not distribute over ENABLED, and hence it does not distribute over WF or SF. Could someone give an example where it is indeed the case?

I believe this is covered in A science of concurrent programming (https://lamport.azurewebsites.net/tla/science.pdf) under section 5.4.4 (A Closer Look at E).

2. It is recommended in the same section that "you don't have to depend on this. You can instead expand the definitions of WF and SF [..] (and) compute the enabled predicates "by hand" and then perform the substitution." Are there conditions under which one could be sure that substitution distributes over entire specification formula so that there is no need to prove it "by hands"?Thank you,Dmitry

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/dfa13cd3-fff5-49e3-9e99-1bd82f7739den%40googlegroups.com.

**References**:**[tlaplus] Refinement Mappings and Fairness***From:*Dmitry Kulagin

- Prev by Date:
**Re: [tlaplus] Deadlock reach without invocation of main actions.** - Next by Date:
**[tlaplus] Lighthearted: TLA+ Syntax Puzzle** - Previous by thread:
**[tlaplus] Refinement Mappings and Fairness** - Next by thread:
**[tlaplus] Deadlock reach without invocation of main actions.** - Index(es):