Additional testing (#158)

By submitting this pull request, I confirm that my contribution is made
under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).

.github/workflows/build_java.yml

@@ -12,4 +12,5 @@ jobs:
       - uses: actions/checkout@v4
       - run: bash scripts/prep.sh
       - run: DAFNY=dafny/dafny TARGET_LANG=java bash scripts/build.sh
-      - run: build/java/run.sh
+      - run: build/java/run_samplers.sh
+      - run: build/java/run_shuffling.sh

.github/workflows/build_py.yml

@@ -12,4 +12,5 @@ jobs:
       - uses: actions/checkout@v4
       - run: bash scripts/prep.sh
       - run: DAFNY=dafny/dafny TARGET_LANG=py bash scripts/build.sh
-      - run: build/py/run.sh
+      - run: build/py/run_samplers.sh
+      - run: build/py/run_shuffling.sh

build/java/run_samplers.sh

@@ -0,0 +1,3 @@
+#1/bin/bash
+
+java -classpath build/java/DafnyVMC.jar docs/java/TestSamplers.java

build/java/run_shuffling.sh

@@ -0,0 +1,3 @@
+#1/bin/bash
+
+java -classpath build/java/DafnyVMC.jar docs/java/TestShuffling.java

build/py/run_samplers.sh

@@ -0,0 +1,3 @@
+#1/bin/bash
+
+PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/TestSamplers.py

build/py/run_shuffling.sh

@@ -0,0 +1,3 @@
+#1/bin/bash
+
+PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/TestShuffling.py

docs/java/TestSamplers.java

@@ -0,0 +1,116 @@
+import java.security.SecureRandom;
+import java.math.BigInteger;
+import java.util.Arrays;
+
+import DafnyVMC.Random;
+
+class TestSamplers {
+
+    public static void main(String[] args) {
+
+            /* STANDARD RNG */
+            System.out.println("\nSTANDARD RNG TESTS\n");
+
+            DafnyVMC.Random r = new DafnyVMC.Random();
+
+            for (int a = 1; a < 1000; a++) {
+                BigInteger i = BigInteger.valueOf(a);
+
+                System.out.println("Testing Uniform(" + a + ")");
+                System.out.println(r.UniformSample(i));
+
+                for (int b = 1; b <= 1000; b++) {
+                    BigInteger j = BigInteger.valueOf(b);
+
+                    System.out.println("Testing Bernoulli(" + a + "/" + b + ")");
+                    System.out.println(r.BernoulliSample(i, j));
+
+                    System.out.println("Testing BernoulliExpNeg(" + a + "/" + b + ")");
+                    System.out.println(r.BernoulliExpNegSample(i, j));
+
+                    System.out.println("Testing DiscreteGaussian(" + a + "/" + b + ")");
+                    System.out.println(r.DiscreteGaussianSample(i, j));
+
+                    System.out.println("Testing DiscreteLaPlace(" + a + "/" + b + ")");
+                    System.out.println(r.DiscreteLaplaceSample(i, j));
+                }
+            }
+
+            // Edge cases
+
+            BigInteger k = BigInteger.valueOf(1000000);
+            BigInteger l = BigInteger.valueOf(1);
+
+            System.out.println("Testing Bernoulli(1000000, 1)");
+            System.out.println(r.BernoulliSample(k, l));
+            System.out.println("Testing Bernoulli(1, 1000000)");
+            System.out.println(r.BernoulliSample(l, k));
+
+            System.out.println("Testing BernoulliExpNeg(1000000, 1)");
+            System.out.println(r.BernoulliExpNegSample(k, l));
+            System.out.println("Testing BernoulliExpNeg(1, 1000000)");
+            System.out.println(r.BernoulliExpNegSample(l, k));
+
+            System.out.println("Testing DiscreteGaussianSample(1000000, 1)");
+            System.out.println(r.DiscreteGaussianSample(k, l));
+            System.out.println("Testing DiscreteGaussianSample(1, 1000000)");
+            System.out.println(r.DiscreteGaussianSample(l, k));
+
+            System.out.println("Testing DiscreteLaplace(1000000, 1)");
+            System.out.println(r.DiscreteLaplaceSample(k, l));
+            System.out.println("Testing DiscreteLaplace(1, 1000000)");
+            System.out.println(r.DiscreteLaplaceSample(l, k));
+
+            /* CUSTOM RNG */
+            System.out.println("\nCUSTOM RNG TESTS\n");
+
+            SecureRandom rng = new SecureRandom();
+            DafnyVMC.Random t = new DafnyVMC.Random(() -> rng);
+
+            for (int a = 1; a < 1000; a++) {
+                BigInteger i = BigInteger.valueOf(a);
+                System.out.println("Testing Uniform(" + a + ")");
+                System.out.println(t.UniformSample(i));
+
+                for (int b = 1; b <= 1000; b++) {
+                    BigInteger j = BigInteger.valueOf(b);
+                    System.out.println("Testing Bernoulli(" + a + "/" + b + ")");
+                    System.out.println(t.BernoulliSample(i, j));
+
+                    System.out.println("Testing BernoulliExpNeg(" + a + "/" + b + ")");
+                    System.out.println(t.BernoulliExpNegSample(i, j));
+
+                    System.out.println("Testing DiscreteGaussian(" + a + "/" + b + ")");
+                    System.out.println(t.DiscreteGaussianSample(i, j));
+
+                    System.out.println("Testing DiscreteLaPlace(" + a + "/" + b + ")");
+                    System.out.println(t.DiscreteLaplaceSample(i, j));
+                }
+            }
+
+
+            // Edge cases
+
+            System.out.println("Testing Bernoulli(1000000, 1)");
+            System.out.println(t.BernoulliSample(k, l));
+            System.out.println("Testing Bernoulli(1, 1000000)");
+            System.out.println(t.BernoulliSample(l, k));
+
+            System.out.println("Testing BernoulliExpNeg(1000000, 1)");
+            System.out.println(t.BernoulliExpNegSample(k, l));
+            System.out.println("Testing BernoulliExpNeg(1, 1000000)");
+            System.out.println(t.BernoulliExpNegSample(l, k));
+
+            System.out.println("Testing DiscreteGaussianSample(1000000, 1)");
+            System.out.println(t.DiscreteGaussianSample(k, l));
+            System.out.println("Testing DiscreteGaussianSample(1, 1000000)");
+            System.out.println(t.DiscreteGaussianSample(l, k));
+
+            System.out.println("Testing DiscreteLaplace(1000000, 1)");
+            System.out.println(t.DiscreteLaplaceSample(k, l));
+            System.out.println("Testing DiscreteLaplace(1, 1000000)");
+            System.out.println(t.DiscreteLaplaceSample(l, k));
+
+
+    }
+}

docs/java/BuildTest.java → docs/java/TestShuffling.java

@@ -4,7 +4,7 @@
 
 import DafnyVMC.Random;
 
-class Check {
+class TestShuffling {
     public static void main(String[] args) {
         BigInteger[] arr1 = {BigInteger.valueOf(0), BigInteger.valueOf(1), BigInteger.valueOf(2)};
         int[] arr2 = {0, 1, 2};
@@ -13,28 +13,12 @@ public static void main(String[] args) {
         boolean[] arr5 = {true, false, false, true};
         long[] arr6 = {111111L, 333333L, 999999L};
         short[] arr7 = {-3, 0, 3};
-        BigInteger num = BigInteger.valueOf(3);
-        BigInteger den = BigInteger.valueOf(5);
 
+
         /* STANDARD RNG */
         System.out.println("\nSTANDARD RNG TESTS\n");
-
-        DafnyVMC.Random r = new DafnyVMC.Random();
-
-        System.out.println("Example of Uniform sampling");
-        System.out.println(r.UniformSample(BigInteger.valueOf(4)));
-
-        System.out.println("Example of Bernoulli sampling");
-        System.out.println(r.BernoulliSample(num,den));
-
-        System.out.println("Example of BernoulliExpNeg sampling");
-        System.out.println(r.BernoulliExpNegSample(num,den));
-
-        System.out.println("Example of DiscreteGaussian sampling");
-        System.out.println(r.DiscreteGaussianSample(num,den));
 
-        System.out.println("Example of DiscreteLaplace sampling");
-        System.out.println(r.DiscreteLaplaceSample(num,den));
+        DafnyVMC.Random r = new DafnyVMC.Random();
 
         System.out.println("Example of Fisher-Yates: BigInteger");
         r.Shuffle(arr1);
@@ -70,21 +54,6 @@ public static void main(String[] args) {
         SecureRandom rng = new SecureRandom();
         DafnyVMC.Random t = new DafnyVMC.Random(() -> rng);
 
-        System.out.println("Example of Uniform sampling");
-        System.out.println(t.UniformSample(BigInteger.valueOf(4)));
-
-        System.out.println("Example of Bernoulli sampling");
-        System.out.println(t.BernoulliSample(num,den));
-
-        System.out.println("Example of BernoulliExpNeg sampling");
-        System.out.println(r.BernoulliExpNegSample(num,den));
-
-        System.out.println("Example of DiscreteGaussian sampling");
-        System.out.println(t.DiscreteGaussianSample(num,den));
-
-        System.out.println("Example of DiscreteLaplace sampling");
-        System.out.println(t.DiscreteLaplaceSample(num,den));
-
         System.out.println("Example of Fisher-Yates: BigInteger");
         t.Shuffle(arr1);
         System.out.println(Arrays.toString(arr1));

docs/py/TestSamplers.py

@@ -0,0 +1,49 @@
+import DafnyVMC
+
+def main():
+
+    # STANDARD RNG
+    print("\nSTANDARD RNG TESTS\n")
+
+    r = DafnyVMC.Random()
+
+    for i in range(1, 1000): 
+        print("Testing Uniform("+str(i)+")")
+        print(r.UniformSample(i))
+
+        for j in range(1, 1000):
+            print("Testing Bernoulli("+str(i)+"/"+str(j)+")\n")
+            print(r.BernoulliSample(i, j), end="\n")
+
+            print("Testing BernoulliExpNeg("+str(i)+"/"+str(j)+")\n")
+            print(r.BernoulliExpNegSample(i, j), end="\n")
+
+            print("Testing DiscreteGaussian("+str(i)+"/"+str(j)+")\n")
+            print(r.DiscreteGaussianSample(i, j), end="\n")
+
+            print("Testing DiscreteLaPlace("+str(i)+"/"+str(j)+")\n")
+            print(r.DiscreteLaplaceSample(i, j), end="\n")
+
+        # Edge cases    
+        print("Testing Bernoulli(1000000, 1)\n")
+        print(r.BernoulliSample(1000000, 1), end="\n")
+        print("Testing Bernoulli(1, 1000000)\n")
+        print(r.BernoulliSample(1, 1000000), end="\n")
+
+        print("Testing BernoulliExpNeg(1000000, 1)\n")
+        print(r.BernoulliExpNegSample(1000000, 1), end="\n")
+        print("Testing BernoulliExpNeg(1, 1000000)\n")
+        print(r.BernoulliExpNegSample(1, 1000000), end="\n")
+
+        print("Testing DiscreteGaussianSample(1000000, 1)\n")
+        print(r.DiscreteGaussianSample(1000000, 1), end="\n")
+        print("Testing DiscreteGaussianSample(1, 1000000)\n")
+        print(r.DiscreteGaussianSample(1, 1000000), end="\n")
+
+        print("Testing DiscreteLaplace(1000000, 1)\n")
+        print(r.DiscreteLaplaceSample(1000000, 1), end="\n")
+        print("Testing DiscreteLaplace(1, 1000000)\n")
+        print(r.DiscreteLaplaceSample(1, 1000000), end="\n")
+
+if __name__ == "__main__":
+    main()

docs/py/BuildTest.py → docs/py/TestShuffling.py

@@ -6,29 +6,12 @@ def main():
     arr3 = ["aa", "bb", "cc"]
     arr4 = ['a', 'b', 'c']
     arr5 = [True, False, False, True]
-    num = 3
-    den = 5
 
     # STANDARD RNG
     print("\nSTANDARD RNG TESTS\n")
 
     r = DafnyVMC.Random()
 
-    print("Example of Uniform sampling")
-    print(r.UniformSample(4))
-
-    print("Example of Bernoulli sampling")
-    print(r.BernoulliSample(num,den))
-
-    print("Example of BernoulliExpNeg sampling")
-    print(r.BernoulliExpNegSample(num,den))
-
-    print("Example of DiscreteGaussian sampling")
-    print(r.DiscreteGaussianSample(num,den))
-
-    print("Example of DiscreteLaplace sampling")
-    print(r.DiscreteLaplaceSample(num,den))
-
     print("Example of Fisher-Yates: int")
     arr1 = r.Shuffle(arr1)
     print(arr1)