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
universal quantification. You will learn more by figuring out for
yourself why that's the case than by having me explain it.