[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Choose and TLC
On 30.01.2016 15:39, fl wrote:
> "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.
I added your idea to the Codeplex issue tracker  to look into it
later. I personally don't have the necessary bandwidth in the
foreseeable future though.