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

*From*: Chris Ortiz <zitroomega@xxxxxxxxx>*Date*: Wed, 25 Oct 2023 14:08:19 -0700 (PDT)*References*: <bf96558c-ca17-4bc5-b551-d9b641d1c655n@googlegroups.com> <BF7136CB-531A-4117-991C-4D09C3F13E15@gmail.com>

Hi Stephan,

Thank you very much. That is exactly the kind of explanation I am looking for. It is so satisfying for me to now have such reasoning about that specific Strong Fairness formula.

Best regards,

Zitro

On Wednesday, October 25, 2023 at 5:57:32 AM UTC-7 Stephan Merz wrote:

All of these transformations are just tautologies of temporal logic and independent of fairness.Concerning strong fairness: I'll write F for ENABLED <<A>>_v and G for <<A>>_v.(1) => (3):[]([]<>F => <>G)=> [][]<>F => []<>G by the temporal logic rule [](A => B) => ([]A => []B)=> []<>F => []<>G since [][]A <=> []A(3) => (1): I'll reason semantically because it looks simpler.Assume that a behavior sigma satisfies (3), i.e. []<>F => []<>G.We need to show that sigma also satisfies []([]<>F => <>G).So assume that there is some suffix tau of sigma for which []<>F is true, we need to show that tau satisfies <>G.Since []<>F is true for tau, it is also true (a fortiori) for sigma, and by (3) we obtain that []<>G is true for sigma.Therefore <>G is true for tau.The equivalence of (2) and (3) is simply a consequence of the equivalence of F => G and ~F \/ G, plus of pushing negation across temporal operators (~[]F <=> <>~F, ~<>F <=> []~F).StephanOn 25 Oct 2023, at 00:52, Chris Ortiz <zitro...@xxxxxxxxx> wrote:Hello,I am trying to get a set of similar form of formulas between WF_vars(A) and SF_vars(A). In Specifying System book there are 3 formulas for WF_vars(A) which were derived by set of tautologies, namely:Weak Fairness in Specifying System:1) []([]ENABLED <<A>>_v => <><<A>>_v) <--- I called always the case imply form2) []<>(~ENABLED <<A>>_v) \/ []<><<A>>_v <--- I called disabled OR form3) <>[](~ENABLED <<A>>_v) => []<><<A>>_v <-- I called infinitely often action imply formStrong Fairness in Specifying System:2) <>[](~ENABLED <<A>>_v) \/ []<><<A>>_v <-- I called disabled OR form3) []<>ENABLED <<A>>_v => []<><<A>>_v <-- I called infinitely often action imply formI was searching for the "1) I called always the case imply form" of Strong Fairness and I stumble upon Ron Pressler's informative link: https://pron.github.io/posts/tlaplus_part3Strong Fairness from Ron Pressler's link:1) []([]<>ENABLED <<A>>_v => <><<A>>_v) <-- which I called always the case imply form. The one I am searching for.What I am then trying to do is find the derivation of this 1) with the other 2) and 3) of Strong Fairness by method of tautologies just like in the Specifying System book. I am having a hard time with my logic.I appreciate if you can help me with the derivation of equivalence for that Strong Fairness formulas.Thanks,Zitro--

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+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/bf96558c-ca17-4bc5-b551-d9b641d1c655n%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/f1a1d57b-80ef-4b42-9f9b-66a2d32fce4fn%40googlegroups.com.

**References**:**[tlaplus] Derivation of SF_vars(A) Strong Fairness***From:*Chris Ortiz

**Re: [tlaplus] Derivation of SF_vars(A) Strong Fairness***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Derivation of SF_vars(A) Strong Fairness** - Next by Date:
**Re: [tlaplus] Set vs Functions for modelling** - Previous by thread:
**Re: [tlaplus] Derivation of SF_vars(A) Strong Fairness** - Next by thread:
**[tlaplus] pluscal: with vs local variable - change in distinct states for action** - Index(es):