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

*From*: Ramon Bejar Torres <ramon.bejartorres@xxxxxxxxx>*Date*: Thu, 8 Jun 2023 23:10:12 -0700 (PDT)*References*: <CAE7Z=+5ZP00oiNr26TKr0+=uxsaGsGMUWRm10+mASAUHF3wSRQ@mail.gmail.com> <BEAFBF1F-DF15-4016-BAFE-A3505E719D93@gmail.com> <CAE7Z=+5S3C-okkWvtBvVZqJ=++4y32jjRCMKmTeF4TKXZ_R0Xw@mail.gmail.com> <A5EF09FB-E286-4265-A972-24D8D7A6274F@gmail.com>

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 isInit /\ [][Next]_vBehaviors that end in infinite stuttering satisfy this formula, even if Next (or some sub-action) remains always enabled.StephanOn 23 Nov 2022, at 23:17, Huailin <hua...@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 <stepha...@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,StephanOn 23 Nov 2022, at 20:03, Huailin <hua...@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+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.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.

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.

**Follow-Ups**:**Re: [tlaplus] About WF***From:*Stephan Merz

**References**:**[tlaplus] About WF***From:*Huailin

**Re: [tlaplus] About WF***From:*Stephan Merz

**Re: [tlaplus] About WF***From:*Huailin

**Re: [tlaplus] About WF***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Installation on Ubuntu 22.04** - Next by Date:
**Re: [tlaplus] About WF** - Previous by thread:
**Re: [tlaplus] About WF** - Next by thread:
**Re: [tlaplus] About WF** - Index(es):