What is the canonical way to represent recursive data structures in TLA+? Consider the example of a binary tree; at first pass, we try to represent it as follows:
CONSTANTS Key, Value
Node ==
[key : Key,
value : Value,
leftChild : Node,
rightChild : Node]
However, the syntactic analyzer gives the parser error "Unknown operator: Node" since recursive definitions are not supported here.
We can borrow from Specifying Systems section 11.1.2 and define a generalized graph in terms of sets of nodes & edges with restrictions, but I'm interested in whether there are other ways to accomplish this goal.