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

*From*: marc magrans de abril <marcmagra...@xxxxxxxxx>*Date*: Tue, 11 Jun 2013 02:21:24 -0700 (PDT)

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

CONSTANTS S

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

/\ PrintT(p')

Init == /\ p = []

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

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

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

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