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

[tlaplus] RECURSIVE and its meaning in TLA+

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
         LET x == CHOOSE y \in A: TRUE
         IN f[x] + Path(a, A \ {x})

Kind Greetings

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.