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 that a 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