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