Mercurial > hg > Members > kono > jpf-core

annotate src/main/gov/nasa/jpf/util/PairPermutationGenerator.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 ca88bd8e918c
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) 2015, 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 generator for pair-wise permutations, which only considers permutations
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
24 * for each pair of elements, regardless of position. This reduces the
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
25 * number of generated permutations from N! to sum(i=1..N){N-i} + 1.
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
26 * This can be used to test order dependencies between two concurrent
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
27 * entities (threads, state machines etc), based on the same assumptions
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
28 * that are used in pair-wise testing
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 PairPermutationGenerator 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 i, j;
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 PairPermutationGenerator (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
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
38 @Override
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
39 public void reset(){
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
40 initPermutations();
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
41 i = 0;
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
42 j = 0;
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
43 }
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 public static long computeNumberOfPermutations (int n){
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
46 long v = 1;
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
47 for (int l=1; l<n; l++){
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
48 v += (n - l);
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
49 }
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
50 return v;
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 @Override
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
54 protected long computeNumberOfPermutations(){
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
55 return computeNumberOfPermutations(nElements);
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
56 }
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
57
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
58 @Override
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
59 public int[] next (){
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
60 int n = permutation.length;
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 if (nGenerated == 0){ // the initial order
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
63 nGenerated = 1;
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
64 return permutation;
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 } else if (nGenerated > 1){
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
67 if (nGenerated == nPermutations){
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
68 throw new NoSuchElementException();
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
69 }
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
70 swap(permutation, i, j); // revert last permutation
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
71 }
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
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
74 if (++j == n){
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
75 if (++i == n){
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
76 throw new NoSuchElementException();
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
77 } else {
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
78 j = i+1;
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
79 }
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
80 }
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 swap(permutation, i, j);
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
83 nGenerated++;
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
84 return permutation;
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
85 }
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
86
d0a0ff1c0e10 added some infrastructure to pull-generate permutations (total, random and
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
87 }