Problem debugging my definition of a tree with TLC.

[Giuliano <giulia...@xxxxxxx>]

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