Curious: stuttering vs recursive

44 views
Skip to first unread message

Huailin

unread,
May 26, 2021, 11:56:03 PM5/26/21
to tlaplus
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

Stephan Merz

unread,
May 29, 2021, 2:43:28 AM5/29/21
to tla...@googlegroups.com
I am not aware of the use of "recursive" that you refer to. Could you give a reference?

Stephan

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/77ba2baf-e2f6-4058-a393-a9b6eabf1016n%40googlegroups.com.

Huailin

unread,
May 29, 2021, 3:09:42 PM5/29/21
to tla...@googlegroups.com
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



Calvin Loncaric

unread,
May 31, 2021, 1:15:34 PM5/31/21
to tla...@googlegroups.com
"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


Huailin

unread,
May 31, 2021, 5:31:07 PM5/31/21
to tla...@googlegroups.com
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

Clifford Heath

unread,
May 31, 2021, 7:47:16 PM5/31/21
to 'Nicholas Fiorentini' via tlaplus
Every time I consider the meaning of "stuttering" I think of the chess term "stalemate". I think that's a better term anyway, because stutterers do usually manage to finish words and sentences (i.e. make progress) whereas we are concerned with not chasing interminable dead-ends (cul-de-sacs).

There's my 2c.

Clifford Heath 

Stephan Merz

unread,
Jun 1, 2021, 2:57:26 AM6/1/21
to tla...@googlegroups.com
Process algebras have non-observable (\tau) actions that are discarded by weak bisimulation etc., couldn't these be seen as playing a similar role as stuttering steps in TLA? The analogy is imperfect due to the linear-vs.-branching view of system behaviors, however.

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

Reply all
Reply to author
Forward
0 new messages