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

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