|
17 | 17 | parser.add_argument('--skip', nargs='+', help='Space-separated list of .tla modules to skip converting', required=False, default=[])
|
18 | 18 | parser.add_argument('--only', nargs='+', help='If provided, only convert models in this space-separated list', required=False, default=[])
|
19 | 19 | parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true')
|
| 20 | +parser.add_argument('--enable_assertions', help='Enable Java assertions (pass -enableassertions to JVM)', action='store_true') |
20 | 21 | args = parser.parse_args()
|
21 | 22 |
|
22 | 23 | logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO)
|
|
26 | 27 | examples_root = dirname(manifest_path)
|
27 | 28 | skip_modules = args.skip
|
28 | 29 | only_modules = args.only
|
| 30 | +enable_assertions = args.enable_assertions |
29 | 31 |
|
30 | 32 | manifest = tla_utils.load_json(manifest_path)
|
31 | 33 |
|
|
44 | 46 |
|
45 | 47 | def translate_module(module_path):
|
46 | 48 | logging.info(f'Translating {module_path}')
|
47 |
| - result = subprocess.run( |
48 |
| - ['java', '-cp', tools_path, 'pcal.trans', '-nocfg', module_path], |
| 49 | + jvm_parameters = ['-cp', tools_path] + (['-enableassertions'] if enable_assertions else []) |
| 50 | + pcal_parameters = ['-nocfg', module_path] |
| 51 | + pcal = subprocess.run( |
| 52 | + ['java'] + jvm_parameters + ['pcal.trans'] + pcal_parameters, |
49 | 53 | stdout=subprocess.PIPE,
|
50 | 54 | stderr=subprocess.STDOUT,
|
51 | 55 | text=True
|
52 | 56 | )
|
53 |
| - match result: |
54 |
| - case CompletedProcess(): |
55 |
| - if result.returncode == 0: |
56 |
| - logging.debug(result.stdout) |
57 |
| - return True |
58 |
| - else: |
59 |
| - logging.error(f'Module {module_path} conversion failed with return code {result.returncode}; output:\n{result.stdout}') |
60 |
| - return False |
61 |
| - case _: |
62 |
| - logging.error(f'Unhandled result type {type(result)}: {result.stdout}') |
63 |
| - return False |
| 57 | + output = ' '.join(pcal.args) + '\n' + pcal.stdout |
| 58 | + if 0 == pcal.returncode: |
| 59 | + logging.debug(output) |
| 60 | + return True |
| 61 | + else: |
| 62 | + logging.error(output) |
| 63 | + return False |
64 | 64 |
|
65 | 65 | success = True
|
66 | 66 | thread_count = cpu_count() if not args.verbose else 1
|
|
0 commit comments