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
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
On Thursday, November 24, 2022 at 8:47:36 AM UTC+1 Stephan Merz wrote:
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.
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.
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
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+u...@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+u...@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+u...@xxxxxxxxxxxxxxxx.
--
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/58575068-1521-4927-9db3-e0f0226d9be1n%40googlegroups.com.