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

*From*: fl <freder...@xxxxxxxxxxx>*Date*: Sat, 30 Jan 2016 06:39:45 -0800 (PST)

Hi all,

"Choose x \in A : P" is a nice construct that allows to express ideas succinctly but

TLC 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 that

case but in the better case we can have the opportunity to find the right element in a decent

time interval which cannot happen with the current algorithm. (Obviously if the loop is too

long we need a way to stop it.)

Generating one element at a time and then visiting it, is

the basic philosophy to evaluate combinatorial objects such as all trees or all permutations favored

by Knuth in TAOCP 4A.

--

FL

**Follow-Ups**:**Re: Choose and TLC***From:*Leslie Lamport

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

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