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

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Fri, 23 Apr 2021 05:03:06 -0700 (PDT)*Ironport-hdrordr*: A9a23:UvTHcq9Q4HkjDQcviB1uk+FHdb1zdoIgy1knxilNYDZSddGVkN3roe8S0gX6hC1UdHYrn92BP6foex3h3LRy5pQcOqrnYRn+tAKTQ71KwIP+z1TbakjD38JHzqF6aexCDrTLfCdHpOng5g3QKbYd6fyG6r3tpeq29QYVcShPS4VNqzh0ERyaFEoefmV7LL40DoCV6MYChxfIQwV0Uu2DHXUOU+XOoNfG/aiWBSIuPBIs5AmQgT7A0teTeHL04j4lXzRDzaxKyxm4ryXC+q6hv/unoyW860bv6f1t6bjc4+oGL8CBjfUVJi7h4zzYA7hJavmmvCop5Mmj7FYskMPQuBc+P8wb0QKoQkiF5T/k2wzl2DFr1HP401+fhhLY0KrEbQN/LO57waZ2U1/840okhtt116VGxAuixuFqJCKFuwDHo/zndlVPnkqwm3ArlukelDhxSo0bAYUh3bA3zQdzNKxFOAzarKQuEOxVBsna4/pMNXO2Bkqpz1VH8ZiKek92OjmmBmwLusmu2TBQm3xji2sey8oFmn8c9JQ7IqM0mdjsA+BOsIoLauE2KYZ0BOI6S8OxDWDXBSjUOGa5IFjsFsg8Sgjwgq+y2qw84KWRZZQU0IFaouW9bG9l*References*: <CAE7Z=+6VGZUKb91ZQOvjLqJZsqLrz48c==PbbN87id5d23Xomw@mail.gmail.com>

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.

**Follow-Ups**:**Re: [tlaplus] Re: CSP vs. TLA+***From:*Huailin

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

- Prev by Date:
**Re: [tlaplus] TLAPS proof of increment and update** - Next by Date:
**Re: [tlaplus] Re: CSP vs. TLA+** - Previous by thread:
**[tlaplus] CSP vs. TLA+** - Next by thread:
**Re: [tlaplus] Re: CSP vs. TLA+** - Index(es):