Re: [tlaplus] Curious: stuttering vs recursive

Unlike process algebras, TLA has no program / process structure (and in particular no recursive definitions of process behavior) but represents systems as state machines: all recursion is embodied by the [] operator of temporal logic.

Stephan

On 31 May 2021, at 23:30, Huailin <huailin@xxxxxxxxx> wrote:

Interesting discussion. Sometimes, it's really fascinating.

I kinda feel:

*TLA/TLA+ is more focused on a "stateful" spec/system. So, the stuttering here is for describing a behavior of the STATE's *repeating*
vs
*CSP, a process algebra, is more about event-based systems. CSP does not, or even could NOT describe an internal state's changes. So, the recursive term is more
being used for describing the observable behavior from the environment viewpoint.

My 2 cents,

Michael

On Mon, May 31, 2021 at 10:15 AM Calvin Loncaric <c.a.loncaric@xxxxxxxxx> wrote:
"Stuttering" describes behaviors, and "recursive" describes definitions.

The clock example is a recursive system definition (Clock = (tick --> Clock)) that exhibits stuttering behavior (tick, tick, ...). I don't think these are different words for the same concept; they are different words with different meanings that can happily coexist.

--
Calvin

On Sat, May 29, 2021 at 12:09 PM Huailin <huailin@xxxxxxxxx> wrote:
A good example would be Hoare's CSP( http://www.usingcsp.com/cspbook.pdf ).
For example,
Clock = (tick --> Clock).
And the behavior would be: tick,tick tick....

CSP theory heavily uses the "recursive" concept/term to describe an infinite loop PROCESS.

I was just curious why we adopted the "stuttering", instead of "recursive", to describe the consecutive STEPs that do not change states.

Have a nice weekend,

Mike

On Fri, May 28, 2021 at 11:43 PM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:
I am not aware of the use of "recursive" that you refer to. Could you give a reference?

Stephan

On 27 May 2021, at 05:56, Huailin <huailin@xxxxxxxxx> wrote:

Team,

While the word "stuttering" is really precise for describing that a state is not being updated/changed and stay as is after an action got applied, I am wondering why i feel the "stuttering" semantics herein in TLA+ is equal to the "recursive" in PL or some Formal Method fields.

I am very curious why Lamport proposed the "stuttering", instead of using the "recursive", to describe a state not being changed?:--))))

Thanks,

Mike

--
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/77ba2baf-e2f6-4058-a393-a9b6eabf1016n%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/DE6B704D-5F30-4AB8-9E64-81D4B0BA4119%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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAE7Z%3D%2B7COo4R3GSTEDbD7%2Bnit824RsNR5DSJgL4N95x9W2v9HA%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/CABf5HMgEzfF9oMtW-8dvSupyn-kEgGQVoFjjU-7vX0O1t_z-uQ%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/CAE7Z%3D%2B62SpsmMwhjA613g5zBG9_CPmEtJqTFQfZdLw4eYxRtiA%40mail.gmail.com.