Here is the explanation of why a stack overflow occurs when evaluating
the initial predicate Init but not when evaluating the "equivalent"
constant formula.First of all, if you tell Java to use a 2 Mbyte stack, the model runs
fine and there is no stack overflow. Currently, there is no way to
specify the stack size when running TLC from the Toolbox. There
should be and there will be in a future release.Now for the explanation. TLC expands all quantifiers as conjunctions
or disjunctions. It also effectively translates an implication into a
disjunction. If you perform this expansion, you will see that for a
model with 9 nodes, evaluating isTree(edges, root) requires evaluating
a conjunction of the form(*) (A_1 \/ B_1) /\ ... /\ (A_1600 \/ B_1600)
where the \/ comes from the => in the definition of existsUnique.
With the usual recursive procedure for _expression_ evaluation, in the
worst possible case (each A_i false and each B_i true), the recursion
would reach depth 1600 when evaluating (*). This worst case
apparently never happens, and ordinary evaluation works fine.However, if you understand how TLC evaluates the set of intial states,
you will realize that whenever evaluation of Init requires evaluating
an _expression_ of the form A \/ B, TLC has to explore both
possibilities to find the set of all states satisfying Init.
Therefore, TLC always goes to depth 1600 when evaluating _expression_
(*) as part of the initial predicate. Hence the overflow. (In this
particular case, it's not necessary to do this because the preceding
conjuncts of Init have determined the values of all variables, but TLC
doesn't handle this case specially.)