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

*From*: Andrew Helwer <andrew...@xxxxxxxxx>*Date*: Tue, 29 Aug 2017 13:46:02 -0700 (PDT)

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:

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.

CONSTANTS Key, Value

Node ==

Node ==

[key : Key,

value : Value,

leftChild : Node,

rightChild : Node]

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.

**Follow-Ups**:**Re: Recursive data structures***From:*Hillel Wayne

**RE: [tlaplus] Recursive data structures***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] New to TLA, made my first ever specification, thoughts?** - Next by Date:
**RE: [tlaplus] Recursive data structures** - Previous by thread:
**Re: [tlaplus] New to TLA, made my first ever specification, thoughts?** - Next by thread:
**RE: [tlaplus] Recursive data structures** - Index(es):