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

*From*: Hillel Wayne <hwa...@xxxxxxxxx>*Date*: Wed, 30 Aug 2017 14:09:48 -0700 (PDT)*References*: <5aee0701-cc94-4ed1-81af-1929d596edb7@googlegroups.com>

TLA+2 (standard with toolbox) adds a RECURSIVE operator, so you can do

RECURSIVE Node

Node == [

key : Key,

value : Value,

leftChild : Node,

rightChild : Node

]

On Tuesday, 29 August 2017 15:46:02 UTC-5, Andrew Helwer wrote:

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.

**Follow-Ups**:**Re: [tlaplus] Recursive data structures***From:*Stephan Merz

**References**:**Recursive data structures***From:*Andrew Helwer

- Prev by Date:
**RE: [tlaplus] Recursive data structures** - Next by Date:
**Re: [tlaplus] Recursive data structures** - Previous by thread:
**RE: [tlaplus] Recursive data structures** - Next by thread:
**Re: [tlaplus] Recursive data structures** - Index(es):