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

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

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.

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

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