The standard form of TLA+ specifications is
Init /\ [][Next]_v
Behaviors that end in infinite stuttering satisfy this formula, even if Next (or some subaction) remains always enabled.
Stephan
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 twinprime when no matter how big the n is, then we can say, there MUST have a new twinprime...?
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/BEAFBF1FDF154016BAFEA3505E719D93%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%2B5S3CokkWvtBvVZqJ%3D%2B%2B4y32jjRCMKmTeF4TKXZ_R0Xw%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/A5EF09FBE2864265A97224D8D7A6274F%40gmail.com.
