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

*From*: TLA Plus <tlapl...@xxxxxxxxx>*Date*: Tue, 11 Jun 2013 01:43:27 -0800*References*: <3b2f034a-842f-4f72-b6d8-0d867bba14c4@googlegroups.com> <1eda96b5-40ce-41df-aa1a-2c3c6e55087c@googlegroups.com>

1) If I CHOOSE one permutation out of Permutations(S),

I always get the same one. I would have expected that

the model checker will use a different permutation at

each step, in order to cover all the cases

Will you please stop expecting the model checker to do

what you think it should do and figure out what it's

supposed to do--in this case by reading Specifying

Systems or the hyperbook to learn about the CHOOSE

operator.

I was wondering if there is a way to generate

permutations one per step without a priori generating

the complete set of all permutations?

Read this document

http://research.microsoft.com/en-us/um/people/lamport/tla/current-tools.pdf

to find out about the RandomElement operator now

defined in the TLC module. If that doesn't tell you

how to solve your problem, you will have to learn how

to write functional programs.

Leslie

**Follow-Ups**:**Re: [tlaplus] Re: How to generate permutations (with a small footprint)***From:*marc magrans de abril

**References**:**How to generate permutations (with a small footprint)***From:*marc magrans de abril

**Re: How to generate permutations (with a small footprint)***From:*marc magrans de abril

- Prev by Date:
**Re: [tlaplus] How to generate permutations (with a small footprint)** - Next by Date:
**Re: [tlaplus] Re: How to generate permutations (with a small footprint)** - Previous by thread:
**Re: [tlaplus] How to generate permutations (with a small footprint)** - Next by thread:
**Re: [tlaplus] Re: How to generate permutations (with a small footprint)** - Index(es):