# HG changeset patch
# User Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
# Date 1423246332 28800
# Node ID 3a19eedcc13ddc871f8d246920697c43d7cc96bc
# Parent  1ba6ea44e5f91069aafbc34d6ad80cfb44334a32
added a UniqueRandomPermGenerator that makes sure we don't return duplicates. It also checks the (unlikely and pointless) case that we request more permutations than N! and caps the number of samples accordingly

diff -r 1ba6ea44e5f9 -r 3a19eedcc13d src/main/gov/nasa/jpf/util/OATHash.java
--- a/src/main/gov/nasa/jpf/util/OATHash.java	Thu Feb 05 19:13:42 2015 -0800
+++ b/src/main/gov/nasa/jpf/util/OATHash.java	Fri Feb 06 10:12:12 2015 -0800
@@ -84,6 +84,13 @@
     h = hashMixin( h, key3);
     
     return hashFinalize(h);
-    
+  }
+  
+  public static int hash (int[] keys){
+    int h = 0;
+    for (int i=0; i<keys.length; i++){
+      h = hashMixin( h, keys[i]);
+    }
+    return hashFinalize(h);
   }
 }
diff -r 1ba6ea44e5f9 -r 3a19eedcc13d src/main/gov/nasa/jpf/util/PermutationGenerator.java
--- a/src/main/gov/nasa/jpf/util/PermutationGenerator.java	Thu Feb 05 19:13:42 2015 -0800
+++ b/src/main/gov/nasa/jpf/util/PermutationGenerator.java	Fri Feb 06 10:12:12 2015 -0800
@@ -88,5 +88,11 @@
     return (nGenerated < nPermutations);
   }
   
+  /**
+   * return the next permutation or throw a NoSuchElementException if there is none.
+   * 
+   * NOTE - this does not guarantee to return a different object on each call,
+   * i.e. the caller has to clone if the result is stored directly
+   */
   public abstract int[] next(); // the work horse, throws NoSuchElementException
 }
diff -r 1ba6ea44e5f9 -r 3a19eedcc13d src/main/gov/nasa/jpf/util/RandomPermutationGenerator.java
--- a/src/main/gov/nasa/jpf/util/RandomPermutationGenerator.java	Thu Feb 05 19:13:42 2015 -0800
+++ b/src/main/gov/nasa/jpf/util/RandomPermutationGenerator.java	Fri Feb 06 10:12:12 2015 -0800
@@ -34,7 +34,7 @@
   protected Random rand;
   
   protected int[] orig;
-  
+    
   public RandomPermutationGenerator (int nElements, int nPermutations, int seed){
     super(nElements);
     this.nPermutations = nPermutations;
diff -r 1ba6ea44e5f9 -r 3a19eedcc13d src/main/gov/nasa/jpf/util/UniqueRandomPermGenerator.java
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/main/gov/nasa/jpf/util/UniqueRandomPermGenerator.java	Fri Feb 06 10:12:12 2015 -0800
@@ -0,0 +1,57 @@
+/*
+ * 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 RandomPermutationGenerator that keeps track of previously produced values
+ * to avoid duplicates.
+ * Note this only makes sense for relatively small sample sizes, but then again
+ * that is what RandomPermutationGenerators are used for (to avoid N!)
+ */
+public class UniqueRandomPermGenerator extends RandomPermutationGenerator {
+  
+  protected SortedArrayIntSet visited;
+  
+  public UniqueRandomPermGenerator (int nElements, int nPermutations, int seed){
+    super(nElements, nPermutations, seed);
+    
+    visited = new SortedArrayIntSet();
+    this.nPermutations = Math.min( TotalPermutationGenerator.computeNumberOfPermutations(nElements), nPermutations);
+  }
+  
+  public void reset(){
+    super.reset();
+    visited = new SortedArrayIntSet();
+  }
+    
+  public int[] next(){    
+    while (nGenerated < nPermutations){
+      int[] p = super.next();
+      int h = OATHash.hash(p);
+      
+      if (visited.add(h)){
+        return p;
+      } else {
+        nGenerated--; // that one didn't count, we already have seen it
+      }
+    }
+    throw new NoSuchElementException();
+  }
+}
diff -r 1ba6ea44e5f9 -r 3a19eedcc13d src/tests/gov/nasa/jpf/util/PermutationGeneratorTest.java
--- a/src/tests/gov/nasa/jpf/util/PermutationGeneratorTest.java	Thu Feb 05 19:13:42 2015 -0800
+++ b/src/tests/gov/nasa/jpf/util/PermutationGeneratorTest.java	Fri Feb 06 10:12:12 2015 -0800
@@ -58,10 +58,61 @@
     long nPerm = pg.getNumberOfPermutations();
     assertTrue( nPerm == nPermutations);
     
+    System.out.println("this CAN have duplicates");
     while (pg.hasNext()){
       int[] perms = pg.next();
       assertTrue(perms != null);
       pg.printOn(System.out);
     }    
   }
+  
+  boolean isEqual (int[] a, int[] b){
+    if (a.length == b.length){
+      for (int i=0; i<a.length; i++){
+        if (a[i] != b[i]){
+          return false;
+        }
+      }
+      return true;
+    }
+    return false;
+  }
+  
+  @Test
+  public void testUniqueRandomPermutation(){
+    int nPermutations = 14;
+    PermutationGenerator pg = new UniqueRandomPermGenerator(4, nPermutations, 42);
+    long nPerm = pg.getNumberOfPermutations();
+    assertTrue( nPerm == nPermutations);
+    
+    int[][] seen = new int[nPermutations][];
+    int n = 0;
+    
+    System.out.println("this should NOT have duplicates");
+    
+    while (pg.hasNext()){
+      int[] perms = pg.next();
+      assertTrue(perms != null);
+      pg.printOn(System.out);
+      
+      for (int i=0; i<n; i++){
+        assertFalse(isEqual(seen[i], perms));
+      }
+      seen[n++] = perms.clone();
+    }    
+  }
+
+  @Test
+  public void testMaxUniqueRandomPermutation(){
+    int nPermutations = 14; // too high, this only has 3! different permutations
+    PermutationGenerator pg = new UniqueRandomPermGenerator(3, nPermutations, 42);
+    long nPerm = pg.getNumberOfPermutations();
+    assertTrue( nPerm == 6);
+
+    while (pg.hasNext()){
+      int[] perms = pg.next();
+      assertTrue(perms != null);
+      pg.printOn(System.out);
+    }
+  }
 }