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

*From*: Giuliano <giulia...@xxxxxxx>*Date*: Thu, 8 Nov 2012 02:31:42 -0800 (PST)*References*: <2ab1bb48-698c-4cb6-a5ed-de9af96d423a@googlegroups.com> <99b7175c-f2c9-4fe2-8778-56489983fa3c@googlegroups.com>

Thanks a lot, I now understand a bit better how TLC works :)

Giuliano

On Wednesday, November 7, 2012 11:00:14 PM UTC+1, Leslie Lamport wrote:

On Wednesday, November 7, 2012 11:00:14 PM UTC+1, Leslie Lamport wrote:

Here is the explanation of why a stack overflow occurs when evaluating

the initial predicate Init but not when evaluating the "equivalent"

constant formula.First of all, if you tell Java to use a 2 Mbyte stack, the model runs

fine and there is no stack overflow. Currently, there is no way to

specify the stack size when running TLC from the Toolbox. There

should be and there will be in a future release.Now for the explanation. TLC expands all quantifiers as conjunctions

or disjunctions. It also effectively translates an implication into a

disjunction. If you perform this expansion, you will see that for a

model with 9 nodes, evaluating isTree(edges, root) requires evaluating

a conjunction of the form(*) (A_1 \/ B_1) /\ ... /\ (A_1600 \/ B_1600)

where the \/ comes from the => in the definition of existsUnique.

With the usual recursive procedure for _expression_ evaluation, in the

worst possible case (each A_i false and each B_i true), the recursion

would reach depth 1600 when evaluating (*). This worst case

apparently never happens, and ordinary evaluation works fine.However, if you understand how TLC evaluates the set of intial states,

you will realize that whenever evaluation of Init requires evaluating

an _expression_ of the form A \/ B, TLC has to explore both

possibilities to find the set of all states satisfying Init.

Therefore, TLC always goes to depth 1600 when evaluating _expression_

(*) as part of the initial predicate. Hence the overflow. (In this

particular case, it's not necessary to do this because the preceding

conjuncts of Init have determined the values of all variables, but TLC

doesn't handle this case specially.)

**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:
**How to read the graph generated by TLC? Is there a way to specify its location?** - Previous by thread:
**Re: Problem debugging my definition of a tree with TLC.** - Next by thread:
**How to read the graph generated by TLC? Is there a way to specify its location?** - Index(es):