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

*From*: Dmitry Kulagin <dmitry.kulagin@xxxxxxxxx>*Date*: Thu, 18 Apr 2024 07:10:25 -0700 (PDT)

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?

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/e847b7cb-10a5-4d4a-879d-8911825c2762n%40googlegroups.com.

**Follow-Ups**:**[tlaplus] Re: Refinement Mappings and Fairness***From:*divyanshu ranjan

- Prev by Date:
**Re: [tlaplus] how we can used the temporal properties in PlusCal algorithm and also removed the termination** - Next by Date:
**[tlaplus] Deadlock reach without invocation of main actions.** - Previous by thread:
**Re: [tlaplus] how we can used the temporal properties in PlusCal algorithm and also removed the termination** - Next by thread:
**[tlaplus] Re: Refinement Mappings and Fairness** - Index(es):