Re: [tlaplus] About WF

Stephan

On 23 Nov 2022, at 23:17, Huailin <huailin@xxxxxxxxx> wrote:
Thanks, Stephan.

>>>because they are not universally true.

Why you say it might NOT be universally true? I kind of feel it should be. That's why I was wondering whether we can provide a proof.

My gut feeling is: If ALWAYS *enabled*, and the state sequence is infinite, then it MUST be: exhibit at least once.
On Wed, Nov 23, 2022 at 12:00 PM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:
Hello,

this is the definition of weak fairness. An equivalent definition is

[](([]ENABLED <<A>>_v) => <> <<A>>_v)

and you may check your understanding of temporal logic by proving that the two formulas are equivalent.

In system specifications, fairness conditions are assumptions on the behavior of (the platform that runs) the system. They need to be validated in order to make sure that they correspond to the understanding that you have of the system, but they are not (and cannot be) proved because they are not universally true.

Regards,

Stephan

On 23 Nov 2022, at 20:03, Huailin <huailin@xxxxxxxxx> wrote:
Team,

Happy holiday.
<>[](ENABLED <<A>>_v) => []<><<A>>_v
For the above WF definition, which means: If eventually ALWAYS possible for an event, then the event will infinitely occur.
This is just temporal logics's definition,conjecture, or do we need to think of a proof? Intuitively, it is true, but do we need to prove it?

For example, if there is always a possible twin-prime when no matter how big the n is, then we can say, there MUST have a new twin-prime...?

Thanks,

Huailin
--
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/CAE7Z%3D%2B5ZP00oiNr26TKr0%2B%3DuxsaGsGMUWRm10%2BmASAUHF3wSRQ%40mail.gmail.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/BEAFBF1F-DF15-4016-BAFE-A3505E719D93%40gmail.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/CAE7Z%3D%2B5S3C-okkWvtBvVZqJ%3D%2B%2B4y32jjRCMKmTeF4TKXZ_R0Xw%40mail.gmail.com.