[tlaplus] Refinement Mappings and Fairness

[Dmitry Kulagin <dmitry.kulagin@xxxxxxxxx>]

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.