[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 >>)

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

   <<{{n1, n2}}, n1>>
   <<{{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.