Problem debugging my definition of a tree with TLC.

[Giuliano]

Hello,

I wrote the following specification of a tree, where a tree is a root and a set of edges satisfying "isTree".

I would like to debug my definition of "isTree" by having TLC generate "root,edges" pairs that satisfy "isTree".

My plan is to write an Init predicate that says that the initial state is a tree and not use any next-state action. I think that the set of initial states thereby generated should give me what I want.

(1) Is this a good plan or is there an easier way to debug my specification?

(2) I set up a model (in the toolbox GUI) with "Init: Init", "Next: Next", and constant "vertices <- {1,2}". It worked fine. Then I changed the vertices constant to "vertices <- {1,2,3}" and TLC produced the StackOverflowError copied below. Could someone help me find out what is going on?

Thanks,

Giuliano

***Specification:

-------------------------------- MODULE Tree --------------------------------

EXTENDS Sequences, Naturals, FiniteSets, TLC

CONSTANTS vertices

\*True of a sequence containing no repetitions.

unique(vs) == \A i \in DOMAIN vs : \A j \in (DOMAIN vs \ {i}) : vs[i] /= vs[j]

\*An edges is a set consisting of two vertices.

\*A path is a sequence of at least two vertices obtained by walking along edges without encountering the same vertice twice.

isPath(vs, edges) ==

    /\ Len(vs) > 1

    /\ unique(vs)

    /\ \A i \in 1..(Len(vs)-1) : {vs[i],vs[i+1]} \in edges

\*True when there exists a unique s in S satisfying predicate P.

existsUniqueIn(S, P(_)) == (\E x \in S : P(x)) /\ (\A x,y \in S : (P(x) /\ P(y)) => (x = y))

\*A tree is a set of edges and a root such that there is a unique path between any vertex which is not the root and the root.

isTree(edges, root) == 

    \A v \in (vertices \ {root}) : 

        LET isPathFromVToRoot(vs) == isPath(vs, edges) /\ vs[1] = v /\ vs[Len(vs)] = root

        IN  existsUniqueIn(Seq(vertices), isPathFromVToRoot)

VARIABLES edges, root

Init == 

    /\ root \in vertices

    /\ edges \in SUBSET SUBSET vertices 

    /\ (\A e \in edges : Cardinality(e) = 2)

    /\ isTree(edges, root)

    /\ PrintT("tree:") /\ PrintT(<< edges, root >>)

Next == UNCHANGED << edges,root >> 

***TLC error:

This was a Java StackOverflowError. It was probably the result

of an incorrect recursive function definition that caused TLC to enter

an infinite loop when trying to compute the function or its application

to an element in its putative domain.

The error occurred when TLC was evaluating the nested

expressions at the following positions:

0. Line 18, column 68 to line 18, column 71 in Tree

1. Line 23, column 38 to line 23, column 54 in Tree

2. Line 13, column 8 to line 13, column 18 in Tree

3. Line 13, column 8 to line 13, column 18 in Tree

4. Line 13, column 8 to line 13, column 14 in Tree

5. Line 13, column 12 to line 13, column 13 in Tree

6. Line 23, column 45 to line 23, column 46 in Tree

[Leslie Lamport]

A note to posters: Specs are a lot easier to read if you post them

with the Courrier New font (with my setup selectable from the menu bar

above the message you're typing).

 

I don't know what you were asking TLC to check when it produced
the error report in your post, and I don't know how to reproduce
the error.

 

I loaded your spec with the Toolbox, had it instantiate the constant
`vertices' with a set {n1, n2, n3} of model values, and ran TLC on the
spec.  It reported the error

   TLC encountered a non-enumerable quantifier bound
   Seq({n1, n2, n3}).
   line 18, col 38 to line 18, col 38 of module Test

where the location was the first S in the definition of

   existsUniqueIn(S, P(_))

If you read the section in Specifying Systems on how TLC checks a
spec, you should realize that evaluating isTree requires TLC to
enumerate the infinite set Seq(vertices).

The simplest way to fix this is to modify the definition of isTree so it
applies existsUniqueIn to a finite set of sequences--for example
sequences of length at most equal to the cardinality of `vertices'.

Your approach of defining a spec with a stuttering next-state action
works.  However, you can accomplish the same thing by not having
any variables or behavior spec, and simply having the Toolbox
tell TLC to evaluate the constant 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 >>)

However, my guess is that you'll run TLC out of memory with a set
`vertices' containing more than 3 nodes.

Personally, I have found it most convenient to define a tree to
be a set of vertices together with a function mapping each non-root
node to its parent.  However, what works best depends on what you're
going to use the definition for.

[Giuliano]

Thanks a lot for your answer!

Sorry, I forgot to mention that I had replaced the definition of Seq by BSeq (as described below) and that I did not ask TLC to check anything. I just wanted it to print trees. So the question about the StackOverflowError still stands.

BSeq(x) == UNION {[1..n -> x] : n \in {1,2,3}}

Seq(x) <- BSeq(x)

Following your suggestion, I removed the behavior spec and asked TLC to evaluate the expression

\A root \in vertices, edges \in SUBSET SUBSET vertices :

       /\ (\A e \in edges : Cardinality(e) = 2)

       /\ isTree(edges, root)

       /\ PrintT("tree:") 

       /\ PrintT(<< edges, root >>)

In the "User Output" window, I got the following message:

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

If I remove the "isTree(edges,root)" conjunct I get:

"tree:"

<<{}, 1>>

"tree:"

<<{}, 2>>

"tree:"

<<{}, 3>>

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

Any idea about what is going on?

Giuliano

[Leslie Lamport]

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.

[Leslie Lamport]

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

 

[Giuliano]

Thanks a lot, I now understand a bit better how TLC works :)

Giuliano