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

Re: [tlaplus] Re: How to generate permutations (with a small footprint)

   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

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


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.