changeset 4:d0a0ff1c0e10

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 fdc263e5806b
children 1ba6ea44e5f9
files src/main/gov/nasa/jpf/util/PairPermutationGenerator.java src/main/gov/nasa/jpf/util/Permutation.java src/main/gov/nasa/jpf/util/PermutationGenerator.java src/main/gov/nasa/jpf/util/RandomPermutationGenerator.java src/main/gov/nasa/jpf/util/TotalPermutationGenerator.java src/main/gov/nasa/jpf/vm/choice/PermutationCG.java src/tests/gov/nasa/jpf/util/PermutationGeneratorTest.java
diffstat 7 files changed, 486 insertions(+), 94 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/main/gov/nasa/jpf/util/PairPermutationGenerator.java	Thu Feb 05 18:53:33 2015 -0800
@@ -0,0 +1,87 @@
+/*
+ * Copyright (C) 2015, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ * 
+ *        http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and 
+ * limitations under the License.
+ */
+package gov.nasa.jpf.util;
+
+import java.util.NoSuchElementException;
+
+/**
+ * a generator for pair-wise permutations, which only considers permutations
+ * for each pair of elements, regardless of position. This reduces the
+ * number of generated permutations from N! to sum(i=1..N){N-i} + 1.
+ * This can be used to test order dependencies between two concurrent
+ * entities (threads, state machines etc), based on the same assumptions
+ * that are used in pair-wise testing
+ */
+public class PairPermutationGenerator extends PermutationGenerator {
+
+  protected int i, j;
+
+  PairPermutationGenerator (int nElements){
+    super(nElements);
+  }
+
+  @Override
+  public void reset(){
+    initPermutations();
+    i = 0;
+    j = 0;
+  }
+  
+  public static long computeNumberOfPermutations (int n){
+    long v = 1;
+    for (int l=1; l<n; l++){
+      v += (n - l);
+    }
+    return v;
+  }
+  
+  @Override
+  protected long computeNumberOfPermutations(){
+    return computeNumberOfPermutations(nElements);
+  }
+          
+  @Override
+  public int[] next (){
+    int n = permutation.length;
+
+    if (nGenerated == 0){ // the initial order
+      nGenerated = 1;
+      return permutation;
+      
+    } else if (nGenerated > 1){
+      if (nGenerated == nPermutations){
+        throw new NoSuchElementException();
+      }
+      swap(permutation, i, j); // revert last permutation
+    }
+
+
+    if (++j == n){
+      if (++i == n){
+        throw new NoSuchElementException();
+      } else {
+        j = i+1;
+      }
+    }
+
+    swap(permutation, i, j);
+    nGenerated++;
+    return permutation;
+  }
+
+}
--- a/src/main/gov/nasa/jpf/util/Permutation.java	Tue Feb 03 08:49:33 2015 -0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-/*
- * Copyright (C) 2014, United States Government, as represented by the
- * Administrator of the National Aeronautics and Space Administration.
- * All rights reserved.
- *
- * The Java Pathfinder core (jpf-core) platform is licensed under the
- * Apache License, Version 2.0 (the "License"); you may not use this file except
- * in compliance with the License. You may obtain a copy of the License at
- * 
- *        http://www.apache.org/licenses/LICENSE-2.0. 
- *
- * Unless required by applicable law or agreed to in writing, software
- * distributed under the License is distributed on an "AS IS" BASIS,
- * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
- * See the License for the specific language governing permissions and 
- * limitations under the License.
- */
-package gov.nasa.jpf.util;
-
-public final class Permutation {
-  public static final int defaultInitCap = 40;
-
-  /** the backing array. */
-  protected int[] data;
-  
-  /** growth strategy. */
-  protected Growth growth;
-  
-  /** the size of the inverse vector == next range value to be assigned. */
-  protected final IntVector inverse;
-  
-  public Permutation(Growth initGrowth, int initCap) {
-    inverse = new IntVector(initGrowth,initCap);
-    growth = initGrowth;
-    data = new int[initCap];
-  }
-  
-  public Permutation(Growth initGrowth) { this(initGrowth,defaultInitCap); }
-  
-  public Permutation(int initCap) { this(Growth.defaultGrowth, initCap); }
-  
-  public Permutation() { this(Growth.defaultGrowth,defaultInitCap); }
-  
-  
-  public void add(int x) {
-	if (x < 0) return;
-	ensureCapacity(x+1);
-    if (data[x] < 0) {
-      data[x] = inverse.size;
-      inverse.add(x);
-    }
-  }
-  
-  public int get(int x) {
-    if (x >= data.length) {
-      return -1;
-    } else {
-      return data[x];
-    }
-  }
-  
-  public int inverseGet(int v) {
-    if (v >= inverse.size) {
-      return -1;
-    } else {
-      return inverse.get(v);
-    }
-  }
-  
-  public void set(int x, int v) {
-    ensureCapacity(x+1);
-    data[x] = v;
-  }
-
-  public void clear() {
-    for (int i = 0; i < data.length; i++) {
-      data[i] = -1;
-    }
-    inverse.clear();
-  }
-
-  public int rangeSize() { return inverse.size; }
-  
-  public void ensureCapacity(int desiredCap) {
-    if (data.length < desiredCap) {
-      int[] newData = new int[growth.grow(data.length, desiredCap)];
-      System.arraycopy(data, 0, newData, 0, data.length);
-      for (int i = data.length; i < newData.length; i++) {
-        newData[i] = -1;
-      }
-      data = newData;
-    }
-  }
-}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/main/gov/nasa/jpf/util/PermutationGenerator.java	Thu Feb 05 18:53:33 2015 -0800
@@ -0,0 +1,92 @@
+/*
+ * Copyright (C) 2015, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ * 
+ *        http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and 
+ * limitations under the License.
+ */
+package gov.nasa.jpf.util;
+
+import java.io.PrintStream;
+
+/**
+ * base type for permutation generators
+ */
+public abstract class PermutationGenerator {
+  
+  protected final int nElements;
+  
+  protected int[] permutation;   // array containing permutation
+
+  protected long nPermutations;
+  protected long nGenerated;
+
+  protected PermutationGenerator (int nElements){
+    this.nElements = nElements;
+    nPermutations = computeNumberOfPermutations();
+    
+    initPermutations();
+  }
+  
+  protected void initPermutations (){
+    permutation = new int[nElements];
+    
+    // initialize element array in order, starting with firstIdx
+    for (int i=0; i<nElements; i++){
+      permutation[i] = i;
+    }
+    
+    nGenerated = 0;
+  }
+  
+  protected abstract long computeNumberOfPermutations();
+  public abstract void reset();
+  
+  public long getNumberOfPermutations(){
+    return nPermutations;
+  }
+  
+  public long getNumberOfGeneratedPermutations(){
+    return nGenerated;
+  }
+ 
+  static void swap(int[] a, int i, int j){
+    int tmp = a[j];
+    a[j] = a[i];
+    a[i] = tmp;
+  }
+
+  /**
+   * for debugging purposes 
+   */
+  public void printOn (PrintStream ps){
+    printOn( ps, nGenerated, permutation);
+  }
+
+  public static void printOn (PrintStream ps, long nGenerated, int[] perm){
+    ps.printf("%2d: [", nGenerated);
+    for (int k=0; k<perm.length; k++){
+      if (k > 0) ps.print(',');
+      ps.print(perm[k]);
+    }
+    ps.println(']');    
+  }
+  
+  
+  //--- the public iteration interface, following Iterator
+  public boolean hasNext(){
+    return (nGenerated < nPermutations);
+  }
+  
+  public abstract int[] next(); // the work horse, throws NoSuchElementException
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/main/gov/nasa/jpf/util/RandomPermutationGenerator.java	Thu Feb 05 18:53:33 2015 -0800
@@ -0,0 +1,74 @@
+/*
+ * Copyright (C) 2015, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ * 
+ *        http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and 
+ * limitations under the License.
+ */
+package gov.nasa.jpf.util;
+
+import java.util.NoSuchElementException;
+import java.util.Random;
+
+/**
+ * a permutation generator that uses the Fisher-Yates shuffle
+ * (Durstenfeld, R. (July 1964). "Algorithm 235: Random permutation". 
+ * Communications of the ACM 7 (7): 420)
+ * 
+ * use this if TotalPermutations would be too large and PairPermutations
+ * not enough
+ */
+public class RandomPermutationGenerator extends PermutationGenerator {
+
+  protected int seed;
+  protected Random rand;
+  
+  public RandomPermutationGenerator (int nElements, int nPermutations, int seed){
+    super(nElements);
+    this.nPermutations = nPermutations;
+    rand = new Random(seed);
+  }
+  
+  @Override
+  protected long computeNumberOfPermutations() {
+    return nPermutations; // it's input (set)
+  }
+
+  @Override
+  public void reset() {
+    initPermutations();
+    rand = new Random(seed);
+    nGenerated = 0;
+  }
+
+  @Override
+  public int[] next() {
+    if (nGenerated == 0){
+      nGenerated = 1;
+      return permutation;
+      
+    } else if (nGenerated < nPermutations){
+      int[] perm = permutation.clone();
+      for (int i=0; i<nElements; i++){
+        int r = i + rand.nextInt( nElements-i);  // i <= r < nElements-1
+        swap(perm, r, i);
+      }        
+      nGenerated++;
+      permutation = perm;
+      return permutation;
+        
+    } else {
+      throw new NoSuchElementException();
+    }
+  }
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/main/gov/nasa/jpf/util/TotalPermutationGenerator.java	Thu Feb 05 18:53:33 2015 -0800
@@ -0,0 +1,93 @@
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ * 
+ *        http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and 
+ * limitations under the License.
+ */
+package gov.nasa.jpf.util;
+
+import java.util.NoSuchElementException;
+
+/**
+ * a pull mode generator for permutations that executes in constant space,
+ * using Ives' algorithm (F. M. Ives: Permutation enumeration: four new 
+ * permutation algorithms, Comm. ACM, 19, 2, Feb 1976, pg. 68-72)
+ * 
+ * NOTE - this is mostly here for completeness, since use of full permutations
+ * in most cases is prohibitive due to N!
+ */
+public class TotalPermutationGenerator extends PermutationGenerator {
+  
+  protected int[] inverse; // inverse permutations array
+    
+  public TotalPermutationGenerator (int nElements){
+    super( nElements);
+    
+    initInverse();
+  }
+  
+  void initInverse (){
+    inverse = new int[nElements];
+    for (int i=0; i<nElements; i++){
+      inverse[i] = i;
+    }    
+  }
+  
+  @Override
+  public void reset(){
+    initPermutations();
+    initInverse();
+  }
+  
+  
+  public static long computeNumberOfPermutations(int nElements){
+    long n = 1;
+    for (int i=1; i<=nElements; i++){
+      n *= i;
+    }
+    return n;    
+  }
+  
+  @Override
+  protected long computeNumberOfPermutations(){
+    return computeNumberOfPermutations(nElements);
+  }
+    
+  @Override
+  public int[] next (){
+    if (nGenerated == 0){
+      nGenerated =1;
+      return permutation;
+      
+    } else {
+      for (int lower=0, upper=nElements-1; upper > lower; lower++, upper--){
+        int i = inverse[lower];
+        int j = (i == upper) ? lower : i+1;
+        int pj = permutation[j];
+
+        permutation[i] = pj;
+        permutation[j] = lower;
+
+        inverse[lower] = j;
+        inverse[pj] = i;
+
+        if ((permutation[lower] != lower) || (permutation[upper] != upper)){
+          nGenerated++;
+          return permutation;
+        }
+      }
+      throw new NoSuchElementException();
+    }
+  }  
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/main/gov/nasa/jpf/vm/choice/PermutationCG.java	Thu Feb 05 18:53:33 2015 -0800
@@ -0,0 +1,73 @@
+/*
+ * Copyright (C) 2015, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ * 
+ *        http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and 
+ * limitations under the License.
+ */
+package gov.nasa.jpf.vm.choice;
+
+import gov.nasa.jpf.util.PermutationGenerator;
+import gov.nasa.jpf.vm.ChoiceGeneratorBase;
+
+/**
+ * a CG that creates permutation choices
+ * 
+ * since PermutationCGs have a potentially huge number of choices, we don't
+ * compute and store them upfront, but rather keep the enumeration state in a
+ * low level pull-based generator
+ */
+public class PermutationCG extends ChoiceGeneratorBase<int[]>{
+  
+  protected PermutationGenerator pg;
+  protected int[] permutation;
+  
+  public PermutationCG (PermutationGenerator pg){
+    this.pg = pg;
+  }
+  
+  @Override
+  public int[] getNextChoice() {
+    return permutation;
+  }
+
+  @Override
+  public Class<int[]> getChoiceType() {
+    return int[].class;
+  }
+
+  @Override
+  public boolean hasMoreChoices() {
+    return pg.hasNext();
+  }
+
+  @Override
+  public void advance() {
+    permutation = pg.next();
+  }
+
+  @Override
+  public void reset() {
+    pg.reset();
+  }
+
+  @Override
+  public int getTotalNumberOfChoices() {
+    return (int) pg.getNumberOfPermutations();
+  }
+
+  @Override
+  public int getProcessedNumberOfChoices() {
+    return (int) pg.getNumberOfGeneratedPermutations();
+  }
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/tests/gov/nasa/jpf/util/PermutationGeneratorTest.java	Thu Feb 05 18:53:33 2015 -0800
@@ -0,0 +1,67 @@
+/*
+ * Copyright (C) 2015, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ * 
+ *        http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and 
+ * limitations under the License.
+ */
+package gov.nasa.jpf.util;
+
+import gov.nasa.jpf.util.test.TestJPF;
+import org.junit.Test;
+
+/**
+ * regression test for PermutationGenerator
+ */
+public class PermutationGeneratorTest extends TestJPF {
+  
+  @Test
+  public void testTotalPermutation(){
+    PermutationGenerator pg = new TotalPermutationGenerator(4);
+    long nPerm = pg.getNumberOfPermutations();
+    assertTrue( nPerm == 24);
+    
+    while (pg.hasNext()){
+      int[] perms = pg.next();
+      assertTrue(perms != null);
+      pg.printOn(System.out);
+    }
+  }
+  
+  @Test
+  public void testPairPermutation(){
+    PermutationGenerator pg = new PairPermutationGenerator(4);
+    long nPerm = pg.getNumberOfPermutations();
+    assertTrue( nPerm == 7);
+    
+    while (pg.hasNext()){
+      int[] perms = pg.next();
+      assertTrue(perms != null);
+      pg.printOn(System.out);
+    }
+  }
+
+  @Test
+  public void testRandomPermutation(){
+    int nPermutations = 14;
+    PermutationGenerator pg = new RandomPermutationGenerator(4, nPermutations, 42);
+    long nPerm = pg.getNumberOfPermutations();
+    assertTrue( nPerm == nPermutations);
+    
+    while (pg.hasNext()){
+      int[] perms = pg.next();
+      assertTrue(perms != null);
+      pg.printOn(System.out);
+    }    
+  }
+}