diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index e7caaee..59d2059 100644 --- a/.github/workflows/ci.yml +++ b/.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' diff --git a/README.md b/README.md index 152e318..6f5f991 100644 --- a/README.md +++ b/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 [--fixed] [--first ] [--repeat ] +``` +Where: +- `` is either `synth` for bounded synthesis with pruning or `synth-unbounded` for direct unbounded synthesis. +- `` 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 ` (optional) synthesizes the first N structures. +- `--repeat ` (optional) specifies the number of repetitions for the synthesis process. diff --git a/tests/synthesize_crdt.py b/tests/synthesize_crdt.py index a0cab8d..d1f89a3 100644 --- a/tests/synthesize_crdt.py +++ b/tests/synthesize_crdt.py @@ -1,3 +1,4 @@ +import argparse import contextlib import csv from time import time @@ -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()) @@ -353,3 +363,6 @@ def increasing_depth_structures(underlying): for (i, time) in enumerate(times): percent = (i + 1) / len(times) distribution_file.write(f"{time},{percent}\n") + +if __name__ == "__main__": + main()