--- 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);
   }
 }

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

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

--- /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();
+  }
+}

--- 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);
+    }
+  }
 }