diff --git a/.github/scripts/check_small_models.py b/.github/scripts/check_small_models.py index 7546e8ed..f3d5689c 100644 --- a/.github/scripts/check_small_models.py +++ b/.github/scripts/check_small_models.py @@ -7,16 +7,10 @@ from argparse import ArgumentParser import logging from os.path import dirname, normpath +from subprocess import CompletedProcess, TimeoutExpired from timeit import default_timer as timer import tla_utils -tlc_result = { - 0 : 'success', - 11 : 'deadlock failure', - 12 : 'safety failure', - 13 : 'liveness failure' -} - parser = ArgumentParser(description='Checks all small TLA+ models in the tlaplus/examples repo using TLC.') parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=True) parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=True) @@ -36,9 +30,9 @@ def check_model(module_path, model, expected_runtime): module_path = tla_utils.from_cwd(examples_root, module_path) model_path = tla_utils.from_cwd(examples_root, model['path']) logging.info(model_path) - expected_result = model['result'] + hard_timeout_in_seconds = 60 start_time = timer() - tlc, hit_timeout = tla_utils.check_model( + tlc_result = tla_utils.check_model( tools_jar_path, module_path, model_path, @@ -46,19 +40,26 @@ def check_model(module_path, model, expected_runtime): community_jar_path, model['mode'], model['config'], - 60 + hard_timeout_in_seconds ) end_time = timer() - if hit_timeout: - logging.error(f'{model_path} timed out') - return False - logging.info(f'{model_path} in {end_time - start_time:.1f}s vs. {expected_runtime.seconds}s expected') - actual_result = tlc_result[tlc.returncode] if tlc.returncode in tlc_result else str(tlc.returncode) - if expected_result != actual_result: - logging.error(f'Model {model_path} expected result {expected_result} but got {actual_result}') - logging.error(tlc.stdout.decode('utf-8')) - return False - return True + match tlc_result: + case CompletedProcess(): + logging.info(f'{model_path} in {end_time - start_time:.1f}s vs. {expected_runtime.seconds}s expected') + expected_result = model['result'] + actual_result = tla_utils.resolve_tlc_exit_code(tlc_result.returncode) + if expected_result != actual_result: + logging.error(f'Model {model_path} expected result {expected_result} but got {actual_result}') + logging.error(tlc_result.stdout) + return False + return True + case TimeoutExpired(): + logging.error(f'{model_path} hit hard timeout of {hard_timeout_in_seconds} seconds') + logging.error(tlc_result.output.decode('utf-8')) + return False + case _: + logging.error(f'Unhandled TLC result type {type(tlc_result)}: {tlc_result}') + return False # Ensure longest-running modules go first manifest = tla_utils.load_json(manifest_path) diff --git a/.github/scripts/smoke_test_large_models.py b/.github/scripts/smoke_test_large_models.py index 2f4eadf5..de08cc3d 100644 --- a/.github/scripts/smoke_test_large_models.py +++ b/.github/scripts/smoke_test_large_models.py @@ -8,6 +8,7 @@ import logging import os from os.path import dirname, normpath +from subprocess import CompletedProcess, TimeoutExpired import tla_utils parser = ArgumentParser(description='Smoke-tests all larger TLA+ models in the tlaplus/examples repo using TLC.') @@ -27,7 +28,8 @@ def check_model(module_path, model): module_path = tla_utils.from_cwd(examples_root, module_path) model_path = tla_utils.from_cwd(examples_root, model['path']) logging.info(model_path) - tlc, hit_timeout = tla_utils.check_model( + smoke_test_timeout_in_seconds = 5 + tlc_result = tla_utils.check_model( tools_jar_path, module_path, model_path, @@ -35,15 +37,23 @@ def check_model(module_path, model): community_jar_path, model['mode'], model['config'], - 5 + smoke_test_timeout_in_seconds ) - if hit_timeout: - return True - if 0 != tlc.returncode: - logging.error(f'Model {model_path} expected error code 0 but got {tlc.returncode}') - logging.error(tlc.stdout.decode('utf-8')) - return False - return True + match tlc_result: + case TimeoutExpired(): + return True + case CompletedProcess(): + logging.warning(f'Model {model_path} finished quickly, within {smoke_test_timeout_in_seconds} seconds; consider labeling it a small model') + expected_result = model['result'] + actual_result = tla_utils.resolve_tlc_exit_code(tlc_result.returncode) + if expected_result != actual_result: + logging.error(f'Model {model_path} expected result {expected_result} but got {actual_result}') + logging.error(tlc_result.stdout) + return False + return True + case _: + logging.error(f'Unhandled TLC result type {type(tlc_result)}: {tlc_result}') + return False logging.basicConfig(level=logging.INFO) diff --git a/.github/scripts/tla_utils.py b/.github/scripts/tla_utils.py index e6c2476d..6c99263d 100644 --- a/.github/scripts/tla_utils.py +++ b/.github/scripts/tla_utils.py @@ -74,7 +74,7 @@ def get_config(config): """ return ['-deadlock'] if 'ignore deadlock' in config else [] -def check_model(tools_jar_path, module_path, model_path, tlapm_lib_path, community_jar_path, mode, config, timeout): +def check_model(tools_jar_path, module_path, model_path, tlapm_lib_path, community_jar_path, mode, config, hard_timeout_in_seconds): """ Model-checks the given model against the given module. """ @@ -99,10 +99,26 @@ def check_model(tools_jar_path, module_path, model_path, tlapm_lib_path, communi '-lncheck', 'final', '-cleanup' ] + get_config(config) + get_run_mode(mode), - capture_output=True, - timeout=timeout + timeout=hard_timeout_in_seconds, + stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, + text=True ) - return (tlc, False) - except subprocess.TimeoutExpired: - return (None, True) + return tlc + except subprocess.TimeoutExpired as e: + return e + +def resolve_tlc_exit_code(code): + """ + Resolves TLC's exit code to a standardized human-readable form. + Returns the stringified exit code number if unknown. + """ + tlc_exit_codes = { + 0 : 'success', + 11 : 'deadlock failure', + 12 : 'safety failure', + 13 : 'liveness failure' + } + + return tlc_exit_codes[code] if code in tlc_exit_codes else str(code) diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index 3da175bb..abe2399a 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -28,7 +28,7 @@ jobs: shell: bash steps: - name: Clone repo - uses: actions/checkout@v2 + uses: actions/checkout@v3 - name: Install python uses: actions/setup-python@v4 with: diff --git a/manifest.json b/manifest.json index d5528b4b..991a2a95 100644 --- a/manifest.json +++ b/manifest.json @@ -2886,15 +2886,15 @@ "models": [ { "path": "specifications/ewd426/TokenRing.cfg", - "runtime": "unknown", - "size": "unknown", + "runtime": "00:00:05", + "size": "small", "mode": "exhaustive search", "config": [], "features": [ "alias", "liveness" ], - "result": "unknown" + "result": "success" } ] } @@ -3202,8 +3202,8 @@ "models": [ { "path": "specifications/ewd998/EWD998ChanID.cfg", - "runtime": "unknown", - "size": "large", + "runtime": "00:00:05", + "size": "small", "mode": "exhaustive search", "config": [ "ignore deadlock" @@ -3213,7 +3213,7 @@ "state constraint", "view" ], - "result": "unknown" + "result": "success" } ] }, @@ -3315,8 +3315,8 @@ "models": [ { "path": "specifications/ewd998/SmokeEWD998.cfg", - "runtime": "unknown", - "size": "large", + "runtime": "00:00:05", + "size": "small", "mode": { "simulate": { "traceCount": 100 @@ -3327,7 +3327,7 @@ "liveness", "state constraint" ], - "result": "unknown" + "result": "success" } ] }, @@ -3656,4 +3656,4 @@ ] } ] -} \ No newline at end of file +}