Mercurial > hg > Members > kono > jpf-core

annotate src/main/gov/nasa/jpf/util/TotalPermutationGenerator.java @ 4:d0a0ff1c0e10

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added some infrastructure to pull-generate permutations (total, random and pair-wise so far). The generators produce index arrays, i.e. permutations of [0..N-1], which can be used to permute processing order of any indexable data structure, for instance in CGs. This also includes a bare-bones PermutationCG that takes the desired PermutationGenerator as input. Due to the N! nature of the beast, beware of TotalPermutations in such CGs, even if most permutations are handled by state matching.
author Peter Mehlitz <pcmehlitz@gmail.com>
date Thu, 05 Feb 2015 18:53:33 -0800
parents
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
4
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
1 /*
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
2 * Copyright (C) 2014, United States Government, as represented by the
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
3 * Administrator of the National Aeronautics and Space Administration.
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
4 * All rights reserved.
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
5 *
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
8 * in compliance with the License. You may obtain a copy of the License at
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
9 *
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
10 * http://www.apache.org/licenses/LICENSE-2.0.
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
11 *
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
12 * Unless required by applicable law or agreed to in writing, software
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
13 * distributed under the License is distributed on an "AS IS" BASIS,
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
15 * See the License for the specific language governing permissions and
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
16 * limitations under the License.
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
17 */
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
18 package gov.nasa.jpf.util;
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
19
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
20 import java.util.NoSuchElementException;
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
21
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
22 /**
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
23 * a pull mode generator for permutations that executes in constant space,
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
24 * using Ives' algorithm (F. M. Ives: Permutation enumeration: four new
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
25 * permutation algorithms, Comm. ACM, 19, 2, Feb 1976, pg. 68-72)
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
26 *
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
27 * NOTE - this is mostly here for completeness, since use of full permutations
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
28 * in most cases is prohibitive due to N!
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
29 */
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
30 public class TotalPermutationGenerator extends PermutationGenerator {
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
31
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
32 protected int[] inverse; // inverse permutations array
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
33
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
34 public TotalPermutationGenerator (int nElements){
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
35 super( nElements);
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
36
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
37 initInverse();
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
38 }
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
39
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
40 void initInverse (){
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
41 inverse = new int[nElements];
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
42 for (int i=0; i<nElements; i++){
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
43 inverse[i] = i;
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
44 }
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
45 }
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
46
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
47 @Override
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
48 public void reset(){
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
49 initPermutations();
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
50 initInverse();
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
51 }
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
52
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
53
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
54 public static long computeNumberOfPermutations(int nElements){
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
55 long n = 1;
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
56 for (int i=1; i<=nElements; i++){
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
57 n *= i;
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
58 }
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
59 return n;
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
60 }
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
61
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
62 @Override
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
63 protected long computeNumberOfPermutations(){
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
64 return computeNumberOfPermutations(nElements);
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
65 }
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
66
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
67 @Override
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
68 public int[] next (){
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
69 if (nGenerated == 0){
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
70 nGenerated =1;
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
71 return permutation;
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
72
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
73 } else {
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
74 for (int lower=0, upper=nElements-1; upper > lower; lower++, upper--){
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
75 int i = inverse[lower];
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
76 int j = (i == upper) ? lower : i+1;
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
77 int pj = permutation[j];
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
78
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
79 permutation[i] = pj;
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
80 permutation[j] = lower;
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
81
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
82 inverse[lower] = j;
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
83 inverse[pj] = i;
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
84
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
85 if ((permutation[lower] != lower) || (permutation[upper] != upper)){
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
86 nGenerated++;
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
87 return permutation;
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
88 }
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
89 }
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
90 throw new NoSuchElementException();
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
91 }
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
92 }
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
93 }