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

Re: Problem debugging my definition of a tree with TLC.

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:
<<{}, 1>>
<<{}, 2>>
<<{}, 3>>
<<"$!@$!@$!@$!@$!", FALSE>>
Any idea about what is going on?


On Wednesday, November 7, 2012 5:58:01 PM UTC+1, Leslie Lamport wrote:
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.