RECURSIVE and its meaning in TLA+

[Lee]

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

[Stephan Merz]

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

--
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/91844c3d-598e-429c-8ed2-22a5cb7f8f65n%40googlegroups.com.