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

[tlaplus] CSP vs. TLA+


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.


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.


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%2B6VGZUKb91ZQOvjLqJZsqLrz48c%3D%3DPbbN87id5d23Xomw%40mail.gmail.com.