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

*From*: Huailin <huailin@xxxxxxxxx>*Date*: Fri, 23 Apr 2021 09:27:10 -0700*Ironport-hdrordr*: A9a23:xHnHTqrALqrgQULDZUuBBuEaV5tJL9V00zAX/kB9WHVpW+STncy2gbA/3Rj7lD4eVBgb6LO9EYOrKEmwybde544NMbC+GCzvv2W1JI9vhLGSoQHIMSv46+JbyONcY7FzYeeAdGRSoM7m7GCDcuoI78KA9MmT7tv261dIYUVUZ7p77wF/YzzranFeYAVdH5I2GN69y6N8xwaIQngcYsSlCnRtZYGqm/TwiJnkbRQabiRK1CCyjCil4LO/Mx+U0gZ2aV1y6Ioi6mTMnkjF4LyiuZiApSP06mm71f5rseqk7uEGJcSXzuAJNz3ni2+TFeFccozHmApwncaCxxIBlsLWrxIpIsJpgkmhGl2dsF/owU3twTwu43jtxRuEmnPlu9X+Xy9/BNFGgY5fbxvF+0sttNxxy8twrgWknosSCwjBkiT778XJUB8vllPcmwtFrdIu*References*: <CAE7Z=+6VGZUKb91ZQOvjLqJZsqLrz48c==PbbN87id5d23Xomw@mail.gmail.com> <2fce71ec-47a9-4724-84d5-7bac4c9ccab8n@googlegroups.com>

Yeah. The "different" understanding between Dr. Hoare and Dr. Lamport, about a concurrent system, or , generally say, a system, makes me really curious.

From CSP, a process can be STOPPed or SKIPPed, doing nothing like a zombie. a finite steps/events...

From Temporal Logic Action(TLA), with the [] operator everywhere, any system is infinite. If doing nothing, it is because it is stuttering....(or we say, recursive looping).

From my feeling, "x' = x" stuttering is a recursive iteration. I have been thinking that CSP's STOP should br re-defined as recursive doing nothing. And I wrote a paper about this idea and got rejected by peer-reviewers...

Huailin

On Fri, Apr 23, 2021 at 5:03 AM Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:

In TLA+, I usually model a process stopping or terminating by it entering a state where the only enabled action is one where the variables are all left unchanged.Andrew--On Friday, April 23, 2021 at 1:58:33 AM UTC-4 hua...@xxxxxxxxx wrote:folks,As a fan for both CSP and TLA+, I realized something pretty fascinating and 'd like to share my thoughts.For a CSP **Process**, e.g., the famous Vendor Machine, which is being used as an example in Hoare's CSP book, a process can be broken/halt.Hence, STOP and SKIP process are explicitly defined in CSP to describe that a process get terminated accidentally(STOP) or successfully(SKIP).In other words, in CSP, Tony Hoare think thata process's behavior can be FINITE steps.However,For TLA, Lamport proposed that a behavior is always infinite by introducing the stuttering step.From my perspective, the suffering step of a TLA+ spec is nearly equivalent to the recursive behavior for an CSP process.I am very curious to find a consistent mapping between CSP and TLA+. For example, how we gonna describe a STOP process by using TLA+ logic.I am working on this problem these days(I've been thinking that STOP is NOT simply STOP.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/2fce71ec-47a9-4724-84d5-7bac4c9ccab8n%40googlegroups.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%2B413Xnh6HaPqpf50H0Fxs5AkVcBku62aLf87cA28EJtAA%40mail.gmail.com.

**References**:**[tlaplus] CSP vs. TLA+***From:*Huailin

**[tlaplus] Re: CSP vs. TLA+***From:*Andrew Helwer

- Prev by Date:
**[tlaplus] Re: CSP vs. TLA+** - Next by Date:
**[tlaplus] Why is TLA_ complaining about this? (** - Previous by thread:
**[tlaplus] Re: CSP vs. TLA+** - Next by thread:
**[tlaplus] Why is TLA_ complaining about this? (** - Index(es):