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

*From*: Giuliano <giulia...@xxxxxxx>*Date*: Wed, 7 Nov 2012 09:47:10 -0800 (PST)*References*: <2ab1bb48-698c-4cb6-a5ed-de9af96d423a@googlegroups.com> <3175abd4-8c23-4e44-8e3b-7ab20bcd9a0b@googlegroups.com>

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

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 themwith the Courrier New font (with my setup selectable from the menu barabove 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 errorTLC encountered a non-enumerable quantifier bound

Seq({n1, n2, n3}).

line 18, col 38 to line 18, col 38 of module Testwhere 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.

**References**:**Problem debugging my definition of a tree with TLC.***From:*Giuliano

**Re: Problem debugging my definition of a tree with TLC.***From:*Leslie Lamport

- Prev by Date:
**Re: Problem debugging my definition of a tree with TLC.** - Next by Date:
**Re: Problem debugging my definition of a tree with TLC.** - Previous by thread:
**Re: Problem debugging my definition of a tree with TLC.** - Next by thread:
**Re: Problem debugging my definition of a tree with TLC.** - Index(es):