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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Tue, 2 Feb 2016 10:15:53 -0800 (PST)*References*: <d5d95858-b877-40d4-b186-66821479fc53@googlegroups.com>

For the common case, in which there is a single element in the set satisfying the CHOOSE, this change would decrease the expected execution time of CHOOSE by a factor of two. However, if you think about how TLC is probably written, it would require a separate version of the code to evaluate a set-valued _expression_ for use in CHOOSE. Moreover, this is one of any number of optimizations that one can think of. For example, evaluating the common _expression_ S = {} is probably now done by computing the value of S and comparing it to {}. We need more than anecdotes to determine what optimizations are worth making. In particular, changes to the costs of various parts of the computation have made _expression_ evaluation an ever smaller part of the execution time of a TLC execution. I believe that the biggest gains per programming hour are now obtainable by optimizing parallel execution and maintenance of the fingerprint graph.

Leslie

On Saturday, January 30, 2016 at 6:39:45 AM UTC-8, fl wrote:

On Saturday, January 30, 2016 at 6:39:45 AM UTC-8, fl wrote:

Hi all,"Choose x \in A : P" is a nice construct that allows to express ideas succinctly butTLC evaluates it that way: it generates all the elements in A and then filter them using P.If A is large, an exception is thrown.A better way to evaluate the construct would be to generate an element of A, check that P is true,if yes stop the algorithm in the other case continue. Obviously we can get too long a loop in thatcase but in the better case we can have the opportunity to find the right element in a decenttime interval which cannot happen with the current algorithm. (Obviously if the loop is toolong we need a way to stop it.)Generating one element at a time and then visiting it, isthe basic philosophy to evaluate combinatorial objects such as all trees or all permutations favoredby Knuth in TAOCP 4A.--FL

**Follow-Ups**:**Re: [tlaplus] Re: Choose and TLC***From:*Markus Alexander Kuppe

**Re: Choose and TLC***From:*fl

**References**:**Choose and TLC***From:*fl

- Prev by Date:
**Re: A refinement mapping using "callbacks"** - Next by Date:
**Re: Choose and TLC** - Previous by thread:
**Re: [tlaplus] Choose and TLC** - Next by thread:
**Re: Choose and TLC** - Index(es):