How to generate permutations (with a small footprint)

[marc magrans de abril <marcmagra...@xxxxxxxxx>]

As part of a longer spec, I would like that some of the steps generate a permutation function of a given set.

However, when I use the Permutations macro of the standard TLC module I have two problems (likely due to my lack of experience with TLA+).

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 (see PermTest module at the end).

For example, when S={1,2,3,4,5} the output is just:

<<1, 2, 3, 4, 5>>

2) When S={1,2,3,4,5,6,7,8,9,10} then I get the error "Attempted to construct a set with too many elements (>1000000).".

This error is understandable (10! > 1000000). However, I was wondering if there is a way to generate permutations one per step without a priori generating the complete set of all permutations? This could be useful in simulation mode.

Thanks!
marc

---------------------------- MODULE PermTest ---------------------------- 
EXTENDS TLC 

VARIABLES p 
CONSTANTS S 

Next == /\ p' = CHOOSE x \in Permutations(S): TRUE  
             /\ PrintT(p') 

Init == /\ p = []

Spec == Init /\ [][Next]_<<p>>  

=============================================================================