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

Recursive data structures



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.