How to generate permutations (with a small footprint)

[marc magrans de abril]

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>>

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

[marc magrans de abril]

Sorry, the PermTest module have an error:

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

VARIABLES p 
CONSTANTS S 

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

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

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

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

[Stephan Merz]

1. In TLA+, CHOOSE is deterministic choice in the sense that (CHOOSE x : P(x)) = (CHOOSE x : Q(x)) if \A x : P(x) <=> Q(x).

In particular, the expression CHOOSE x \in Foo: P(x) will always return the same value for constant expressions Foo and P. (In fact, this is about the only instance in which TLC really guarantees that CHOOSE acts deterministically, cf. section 14.6 of "Specifying Systems".)

If you want to enumerate all possible permutations, you'll need to use existential quantification and write something like

  Next == \E pp \in Permutations(S) : p' = pp /\ PrintT(p')

2. If you want to avoid generating all permutations, you'll have to write an algorithm that generates them in the order that you have in mind (e.g., by writing a recursive function or an operator that yields the next permutation in sequence).

Hope this helps,

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.
 
 

[TLA Plus]

   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

[marc magrans de abril]

Now, I see my error. 

Thanks for your fast replies and the link!