[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:23:49 -0700 (PDT)*References*: <3b2f034a-842f-4f72-b6d8-0d867bba14c4@googlegroups.com>

Sorry, the PermTest module have an error:

---------------------------- MODULE PermTest ----------------------------

EXTENDS TLC

CONSTANTS S

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

/\ PrintT(p')

Init == /\ p = [i \in S|->i]

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

On Tuesday, June 11, 2013 11:21:24 AM UTC+2, marc magrans de abril wrote:

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:VARIABLES p<<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: [tlaplus] Re: How to generate permutations (with a small footprint)***From:*TLA Plus

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

**References**:**How to generate permutations (with a small footprint)***From:*marc magrans de abril

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