[tlaplus] RECURSIVE and its meaning in TLA+

[Lee <fowler.lee8@xxxxxxxxx>]

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.