# Re: Problem debugging my definition of a tree with TLC.

First of all, I'm sorry for the silly suggestion I made.  The formula
I suggested will probably just evaluate to FALSE and print nothing.  A
formula that works is:

\A root \in vertices,
edges \in SUBSET SUBSET vertices :
IF /\ (\A e \in edges : Cardinality(e) = 2)
/\ isTree(edges, root)
THEN PrintT("tree:") /\ PrintT(<< edges, root >>)
ELSE TRUE

If I try the corrected spec with vertices' a set of two elements,
the spec works fine and produces the correct output

"tree:"
<<{{n1, n2}}, n1>>
"tree:"
<<{{n1, n2}}, n2>>

So, the stack overflow is probably legitimate.  However, I don't
understand why TLC should produce a stack overflow when evaluating
your Init predicate when it doesn't have a problem evaluating the
constant _expression_ above for three vertices.  I will investigate
that further.

On evaluating the formula

\A root \in vertices, edges \in SUBSET SUBSET vertices :
/\ (\A e \in edges : Cardinality(e) = 2)
\* /\ isTree(edges, root)
/\ PrintT("tree:")
/\ PrintT(<< edges, root >>)

TLC is doing what it should, except that the

<<"$!@$!@$!@$!@\$!", FALSE>>

should not have appeared in the output and the Toolbox should have
reported FALSE as the value of the _expression_.  I believe this is a
bug that has been fixed; the fix will appear in the next release.  The
particular output that it produced is caused by { } (the empty set)
being the first value for edges' that TLC tried when evaluating the