|
| 1 | +""" |
| 2 | +Runs PlusCal translation on all PlusCal specs. |
| 3 | +""" |
| 4 | + |
| 5 | +from argparse import ArgumentParser |
| 6 | +from concurrent.futures import ThreadPoolExecutor |
| 7 | +import logging |
| 8 | +from os import cpu_count |
| 9 | +from os.path import dirname, normpath |
| 10 | +import subprocess |
| 11 | +from subprocess import CompletedProcess |
| 12 | +import tla_utils |
| 13 | + |
| 14 | +parser = ArgumentParser(description='Run PlusCal translation on all modules.') |
| 15 | +parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=True) |
| 16 | +parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True) |
| 17 | +parser.add_argument('--skip', nargs='+', help='Space-separated list of .tla modules to skip converting', required=False, default=[]) |
| 18 | +parser.add_argument('--only', nargs='+', help='If provided, only convert models in this space-separated list', required=False, default=[]) |
| 19 | +parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true') |
| 20 | +args = parser.parse_args() |
| 21 | + |
| 22 | +logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO) |
| 23 | + |
| 24 | +tools_path = normpath(args.tools_jar_path) |
| 25 | +manifest_path = normpath(args.manifest_path) |
| 26 | +examples_root = dirname(manifest_path) |
| 27 | +skip_modules = [normpath(path) for path in args.skip] |
| 28 | +only_modules = [normpath(path) for path in args.only] |
| 29 | + |
| 30 | +manifest = tla_utils.load_json(manifest_path) |
| 31 | + |
| 32 | +# List of all modules to translate |
| 33 | +modules = [ |
| 34 | + tla_utils.from_cwd(examples_root, module['path']) |
| 35 | + for spec in manifest['specifications'] |
| 36 | + for module in spec['modules'] |
| 37 | + if 'pluscal' in module['features'] |
| 38 | + and normpath(module['path']) not in skip_modules |
| 39 | + and (only_modules == [] or normpath(module['path']) in only_modules) |
| 40 | +] |
| 41 | + |
| 42 | +for path in skip_modules: |
| 43 | + logging.info(f'Skipping {path}') |
| 44 | + |
| 45 | +def translate_module(module_path): |
| 46 | + logging.info(f'Translating {module_path}') |
| 47 | + result = subprocess.run( |
| 48 | + ['java', '-cp', tools_path, 'pcal.trans', '-nocfg', module_path], |
| 49 | + stdout=subprocess.PIPE, |
| 50 | + stderr=subprocess.STDOUT, |
| 51 | + text=True |
| 52 | + ) |
| 53 | + match result: |
| 54 | + case CompletedProcess(): |
| 55 | + if result.returncode == 0: |
| 56 | + return True |
| 57 | + else: |
| 58 | + logging.error(f'Module {module_path} conversion failed with return code {result.returncode}; output:\n{result.stdout}') |
| 59 | + return False |
| 60 | + case _: |
| 61 | + logging.error(f'Unhandled result type {type(result)}: {result.stdout}') |
| 62 | + return False |
| 63 | + |
| 64 | +success = True |
| 65 | +thread_count = cpu_count() if not args.verbose else 1 |
| 66 | +logging.info(f'Translating PlusCal using {thread_count} threads') |
| 67 | +with ThreadPoolExecutor(thread_count) as executor: |
| 68 | + results = executor.map(translate_module, modules) |
| 69 | + exit(0 if all(results) else 1) |
| 70 | + |
0 commit comments