About WF

[Huailin]

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

[Stephan Merz]

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 <hua...@gmail.com> wrote:



--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAE7Z%3D%2B5ZP00oiNr26TKr0%2B%3DuxsaGsGMUWRm10%2BmASAUHF3wSRQ%40mail.gmail.com.

[Huailin]

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/BEAFBF1F-DF15-4016-BAFE-A3505E719D93%40gmail.com.

[Stephan Merz]

The standard form of TLA+ specifications is

Init /\ [][Next]_v

Behaviors that end in infinite stuttering satisfy this formula, even if Next (or some sub-action) remains always enabled.

Stephan

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.

[Ramon Bejar Torres]

Hi,

Regarding WF(A) applied to an action A that once executed in the resulting state s'  enabled(A) becomes false, I wonder how it is possible to satisfy WF(A) in a behaviour. I mean, in a behaviour where enabled(A) is always true, how can you execute the action A if this makes enabled(A) false once executed ? 

I need probably more information about the temporal logic used in TLA. I would appreciate any links you can provide about this.

Thank you,

Ramon

[Stephan Merz]

Hi,

understanding fairness is difficult: it is a mathematical abstraction of the property that you want to assert. A good start is reading section 8.4 of Specifying Systems, which introduces WF.

One way of thinking about fairness is to consider what behaviors you want to exclude from consideration. Since

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

the behaviors that violate that condition (i.e., that satisfy its negation) are those in which

(<>[] ENABLED <<A>>_v) /\ ~[]<> <<A>>_v

holds, which is equivalent to

(<>[] ENABLED <<A>>_v) /\ <>[][~A]_v

or again to

<>(([] ENABLED <<A>>_v) /\ [][~A]_v)

In other words, assuming WF_v(A) rules out behaviors in which, from some point on, <<A>>_v could always be taken but never is. Once <<A>>_v is disabled (perhaps because it was just performed), the condition holds vacuously.

I hope this helps,

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/58575068-1521-4927-9db3-e0f0226d9be1n%40googlegroups.com.

[Ramon Bejar Torres]

Hi Stephan,

Thanks for your explanation, it makes totally sense. I probably need to read more about the basics of temporal logic.

El dv., 9 de juny 2023, 8:51, Stephan Merz <stepha...@gmail.com> va escriure:

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/JbGN07xg8V8/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/868A7DA7-E9A7-4268-9C47-C3A0097E8F69%40gmail.com.

[Ramon Bejar Torres]

And now I understand my fault in the understanding of WF(A). In a behaviour where A is not  enabled forever from some time, this behaviour will satisfy WF(A), even if A is not executed in that behavior. So you can have a behavior where A changes from enabled to not enabled in infinitely many steps, and this behaviour will satisfy WF(A).

This is probably why we say this is  "weak" fairness.

Thanks again Stephan!