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

*From*: marc magrans de abril <marcmagra...@xxxxxxxxx>*Date*: Tue, 11 Jun 2013 03:01:52 -0700 (PDT)*References*: <3b2f034a-842f-4f72-b6d8-0d867bba14c4@googlegroups.com> <1eda96b5-40ce-41df-aa1a-2c3c6e55087c@googlegroups.com> <CAAWQ4M4cUtZVLeYUepS+3CXsuY3N=X6iaxFhTP+T=5rHTDgSVw@mail.gmail.com>

Now, I see my error.

Thanks for your fast replies and the link!

On Tuesday, June 11, 2013 11:43:27 AM UTC+2, Leslie Lamport wrote:

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 casesWill 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

**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

**Re: [tlaplus] Re: How to generate permutations (with a small footprint)***From:*TLA Plus

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