Re: [tlaplus] RECURSIVE and its meaning in TLA+

Recursive operator definitions were not part of TLA+ when Specifying Systems was written. Their semantics is described in a report by G. Gonthier and L. Lamport [1].

Stephan

[1] https://lamport.azurewebsites.net/pubs/pubs.html#recursive-ops

On Feb 19, 2024, at 22:07, Lee <fowler.lee8@xxxxxxxxx> wrote:

Hello All,

I hope to get some help to understand what RECURSIVE means in the following piece of a spec, as well as how the toolbox treats this piece of the spec. Could you please assist me or provide a link where i can read more about this? (Ive searched the Spec. Systems book and other resources but could not find an answer) Thanks in advance. Here is the snippet:

RECURSIVE Path(_, _)
Path(a, A) ==
IF S = {} THEN 0
ELSE
LET x == CHOOSE y \in A: TRUE
IN f[x] + Path(a, A \ {x})

Kind Greetings
Lee

--
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/91844c3d-598e-429c-8ed2-22a5cb7f8f65n%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/22BEF979-FCF5-46B4-8700-01A99B7A2913%40gmail.com.