Refactor CLI parsing for synthesis entrypoint (#6)

* Refactor CLI parsing for synthesis entrypoint

* Fix precedence of time variable

* Replace global reference to nonIdempotent

.github/workflows/ci.yml

@@ -124,11 +124,11 @@ jobs:
     - name: Test CRDT Synthesis (fixed)
       shell: nix develop --command bash -e {0}
       run: |
-        python -m tests.synthesize_crdt synth g_set fixed
-        python -m tests.synthesize_crdt synth 2p_set fixed
-        python -m tests.synthesize_crdt synth flag_ew fixed
-        python -m tests.synthesize_crdt synth flag_dw fixed
-        python -m tests.synthesize_crdt synth grow_only_counter fixed
+        python -m tests.synthesize_crdt synth g_set --fixed
+        python -m tests.synthesize_crdt synth 2p_set --fixed
+        python -m tests.synthesize_crdt synth flag_ew --fixed
+        python -m tests.synthesize_crdt synth flag_dw --fixed
+        python -m tests.synthesize_crdt synth grow_only_counter --fixed
 
     - name: Save Nix cache
       if: steps.cache.outputs.cache-hit != 'true'

README.md

@@ -61,3 +61,14 @@ For example, we can synthesize for the 2P-Set benchmark with
 ```bash
 python -m tests.synthesize_crdt synth 2p_set
 ```
+
+In general, you can use the following command structure:
+```bash
+python -m tests.synthesize_crdt <mode> <benchmark> [--fixed] [--first <N>] [--repeat <N>]
+```
+Where:
+- `<mode>` is either `synth` for bounded synthesis with pruning or `synth-unbounded` for direct unbounded synthesis.
+- `<benchmark>` is the name of the benchmark or `all` to run all benchmarks.
+- `--fixed` (optional) uses a fixed lattice structure instead of exploring all structures.
+- `--first <N>` (optional) synthesizes the first N structures.
+- `--repeat <N>` (optional) specifies the number of repetitions for the synthesis process.

tests/synthesize_crdt.py

@@ -1,3 +1,4 @@
+import argparse
 import contextlib
 import csv
 from time import time
@@ -249,7 +250,7 @@ def has_node_id(tup):
             return True
     return False
 
-def increasing_depth_structures(underlying):
+def increasing_depth_structures(underlying, nonIdempotent):
     base_depth = 1
     while True:
         # we synthesize structures of complexity base_depth + 1
@@ -261,12 +262,21 @@ def increasing_depth_structures(underlying):
             yield (base_depth, struct)
         base_depth += 1
 
-if __name__ == "__main__":
-    mode = sys.argv[1]
-    bench = sys.argv[2]
-    fixed_structure = len(sys.argv) >= 4 and sys.argv[3] == "fixed"
-    first_n = int(sys.argv[3].split("first_")[1]) if (len(sys.argv) >= 4 and sys.argv[3].startswith("first_")) else None
-    reps = int(sys.argv[3].split("repeat_")[1]) if (len(sys.argv) >= 4 and sys.argv[3].startswith("repeat_")) else 1
+def main():
+    parser = argparse.ArgumentParser(description='Synthesize CRDTs from sequential types.')
+    parser.add_argument('mode', choices=['synth', 'synth-unbounded'], help='synthesis mode')
+    parser.add_argument('benchmark', help='benchmark name or "all"')
+    parser.add_argument('--fixed', action='store_true', help='use fixed lattice structure')
+    parser.add_argument('--first', type=int, help='synthesize the first N structures')
+    parser.add_argument('--repeat', type=int, default=1, help='number of repetitions')
+
+    args = parser.parse_args()
+
+    mode = args.mode
+    bench = args.benchmark
+    fixed_structure = args.fixed
+    first_n = args.first
+    reps = args.repeat
 
     if bench == "all":
         benches = list(benchmarks.keys())
@@ -296,7 +306,8 @@ def increasing_depth_structures(underlying):
                     (lambda base_depth: lat.gen_structures(base_depth))
                     if not fixed_structure
                     else
-                    (lambda _: [bench_data["fixedLatticeType"]])
+                    (lambda _: [bench_data["fixedLatticeType"]]),
+                    nonIdempotent
                 )
 
                 start_time = time()
@@ -350,6 +361,9 @@ def increasing_depth_structures(underlying):
                         times = sorted([float(row[1]) for row in report_reader])
                         with open(f"benchmarks-{bench}-{bounded_bench_str}-first_{first_n}-distribution.csv", "w") as distribution_file:
                             distribution_file.write(f"time,percent\n")
-                            for (i, time) in enumerate(times):
+                            for (i, measured_time) in enumerate(times):
                                 percent = (i + 1) / len(times)
-                                distribution_file.write(f"{time},{percent}\n")
+                                distribution_file.write(f"{measured_time},{percent}\n")
+
+if __name__ == "__main__":
+    main()