Tree is a countably infinite set. The problem is your TypeOK definition. I think TLC tries to evaluate it by enumerating the Tree set and checking each element to see whether it matches your tree variable's value. I tried overriding this behavior by writing:
RECURSIVE IsRootOfTree(_)
IsRootOfTree(n) ==
IF n = Leaf
THEN TRUE
ELSE
/\ "value" \in DOMAIN n
/\ n.value \in Values
/\ "left" \in DOMAIN n
/\ IsRootOfTree(n.left)
/\ "right" \in DOMAIN n
/\ IsRootOfTree(n.right)
TypeOk == IsRootOfTree(tree)
However this then caused TLC to output a novel (to me) error:
TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.ClassCastException
: class tlc2.tool.coverage.ActionWrapper cannot be cast to class tlc2.tool.coverage.OpApplNodeWrapper (tlc2.tool.coverage.ActionWrapper and tlc2.tool.coverage.OpApplNodeWrapper are in unnamed module of loader 'app')
I think Hillel Wayne wrote a spec of a linked list at one point which might be useful to you, although I can't find it. Other than that the only method I've thought of to specify recursive data structures is to actually model their allocation & layout in memory.
Andrew
On Sunday, July 25, 2021 at 12:24:40 AM UTC-4 Alex Weisberger wrote:
Consider the following spec of a tree (extremely simplified, with only two possible node values):
CONSTANTS V1, V2, Leaf
VARIABLES tree
Values == {V1, V2}
RECURSIVE Tree
RECURSIVE Nodes
Tree == {Leaf} \union Nodes
Nodes == [value: Values, left: Tree, right: Tree]
TypeOk == tree \in Tree
Init == tree = [
value |-> V1,
left |-> [
value |-> V2,
left |-> Leaf,
right |-> Leaf
],
right |-> Leaf
]
Next == tree' = Leaf
This is obviously a trivial example (just two predefined states with a single transition), but I'm using it build up to reasoning about trees more. This fails when model checking in TLC with the following error:
"This was a Java StackOverflowError. It was probably the result
of an incorrect recursive function definition that caused TLC to enter
an infinite loop when trying to compute the function or its application
to an element in its putative domain.
While working on the initial state:
tree = [ value |-> V1,
left |-> [value |-> V2, left |-> Leaf, right |-> Leaf],
right |-> Leaf ]
The error occurred when TLC was evaluating the nested
expressions at the following positions:
The error call stack is empty."
I didn't know how TLC would handle mutually recursive definitions such as the above Tree definition, but I also don't exactly understand why it doesn't handle it. I could go with defining a Tree as a Graph, and use a similar definition to what is listed in Specifying Systems, but I thought this was an interesting example to ask about.
Does anyone have any insight into how to make a definition like this model-checkable?