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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Wed, 7 Nov 2012 08:58:01 -0800 (PST)*References*: <2ab1bb48-698c-4cb6-a5ed-de9af96d423a@googlegroups.com>

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.

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.

**Follow-Ups**:**Re: Problem debugging my definition of a tree with TLC.***From:*Giuliano

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

- Prev by Date:
**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:
**Problem debugging my definition of a tree with TLC.** - Next by thread:
**Re: Problem debugging my definition of a tree with TLC.** - Index(es):