From e506f44496a923294cefd888ae90fe1c89bace00 Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Tue, 1 Jul 2025 09:58:14 -0400 Subject: [PATCH] CI: Fix state count validation regex When run under some system locales or Java versions, TLC will output the state count info with comma separators, like "1,000" instead of "1000". Before these changes, the Python regex used to extract & parse these values did not handle these comma separators. Now, it does. This was done by setting the Python locale to en_US.UTF-8 then using the locale.atoi() API. Some of the recorded state spaces were also incorrect due to this issue. Signed-off-by: Andrew Helwer --- .github/scripts/record_model_state_space.py | 20 +++--- .github/scripts/tla_utils.py | 12 ++-- manifest.json | 68 ++++++++++++++------- 3 files changed, 66 insertions(+), 34 deletions(-) diff --git a/.github/scripts/record_model_state_space.py b/.github/scripts/record_model_state_space.py index ecb7fc08..1da8e763 100644 --- a/.github/scripts/record_model_state_space.py +++ b/.github/scripts/record_model_state_space.py @@ -17,6 +17,7 @@ parser.add_argument('--skip', nargs='+', help='Space-separated list of models to skip checking', required=False, default=[]) parser.add_argument('--only', nargs='+', help='If provided, only check models in this space-separated list', required=False, default=[]) parser.add_argument('--enable_assertions', help='Enable Java assertions (pass -enableassertions to JVM)', action='store_true') +parser.add_argument('--all', help='Redo all state counts, not just missing ones', action='store_true') args = parser.parse_args() logging.basicConfig(level=logging.INFO) @@ -28,6 +29,7 @@ examples_root = dirname(manifest_path) skip_models = args.skip only_models = args.only +run_all = args.all enable_assertions = args.enable_assertions def check_model(module, model): @@ -48,28 +50,30 @@ def check_model(module, model): enable_assertions, hard_timeout_in_seconds ) + output = ' '.join(tlc_result.args) + '\n' + tlc_result.stdout match tlc_result: case CompletedProcess(): 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) + logging.error(output) return False state_count_info = tla_utils.extract_state_count_info(tlc_result.stdout) if state_count_info is None: logging.error("Failed to find state info in TLC output") - logging.error(tlc_result.stdout) + logging.error(output) return False logging.info(f'States (distinct, total, depth): {state_count_info}') model['distinctStates'], model['totalStates'], model['stateDepth'] = state_count_info 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')) + logging.error(output) return False case _: logging.error(f'Unhandled TLC result type {type(tlc_result)}: {tlc_result}') + logging.error(output) return False # Ensure longest-running modules go first @@ -82,17 +86,17 @@ def check_model(module, model): for model in module['models'] if model['size'] == 'small' and tla_utils.is_state_count_valid(model) - and ( - 'distinctStates' not in model - or 'totalStates' not in model - or 'stateDepth' not in model - ) # This model is nondeterministic due to use of the Random module and model['path'] != 'specifications/SpanningTree/SpanTreeRandom.cfg' # This model generates the same distinct states but order varies and model['path'] != 'specifications/ewd998/EWD998ChanTrace.cfg' and model['path'] not in skip_models and (only_models == [] or model['path'] in only_models) + and (run_all or ( + 'distinctStates' not in model + or 'totalStates' not in model + or 'stateDepth' not in model + )) ], key = lambda m: m[2], reverse=True diff --git a/.github/scripts/tla_utils.py b/.github/scripts/tla_utils.py index 0a4a2b4c..510bde56 100644 --- a/.github/scripts/tla_utils.py +++ b/.github/scripts/tla_utils.py @@ -1,3 +1,4 @@ +import locale from datetime import datetime import json from os.path import join, normpath, pathsep @@ -223,19 +224,20 @@ def is_state_count_info_correct(model, distinct_states, total_states, state_dept # State depth not yet deterministic due to TLC bug: https://github.com/tlaplus/tlaplus/issues/883 return none_or_equal(expected_distinct_states, distinct_states) and none_or_equal(expected_total_states, total_states) #and none_or_equal(expected_state_depth, state_depth) -state_count_regex = re.compile(r'(?P\d+) states generated, (?P\d+) distinct states found, 0 states left on queue.') -state_depth_regex = re.compile(r'The depth of the complete state graph search is (?P\d+).') +state_count_regex = re.compile(r'(?P[\d,]+) states generated, (?P[\d,]+) distinct states found, 0 states left on queue.') +state_depth_regex = re.compile(r'The depth of the complete state graph search is (?P[\d,]+).') def extract_state_count_info(tlc_output): """ Parse & extract state count info from TLC output. """ + locale.setlocale(locale.LC_ALL, 'en_US.UTF-8') state_count_findings = state_count_regex.search(tlc_output) state_depth_findings = state_depth_regex.search(tlc_output) if state_count_findings is None or state_depth_findings is None: return None - distinct_states = int(state_count_findings.group('distinct_states')) - total_states = int(state_count_findings.group('total_states')) - state_depth = int(state_depth_findings.group('state_depth')) + distinct_states = locale.atoi(state_count_findings.group('distinct_states')) + total_states = locale.atoi(state_count_findings.group('total_states')) + state_depth = locale.atoi(state_depth_findings.group('state_depth')) return (distinct_states, total_states, state_depth) diff --git a/manifest.json b/manifest.json index 3c0ab7e6..2450c4d2 100644 --- a/manifest.json +++ b/manifest.json @@ -1335,8 +1335,12 @@ "title": "The Moving Cat Puzzle", "description": "Demonstrating the solution for the moving cat puzzle is correct.", "sources": [], - "authors": ["Florian Schanda"], - "tags": ["beginner"], + "authors": [ + "Florian Schanda" + ], + "tags": [ + "beginner" + ], "modules": [ { "path": "specifications/Moving_Cat_Puzzle/Cat.tla", @@ -1349,19 +1353,29 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "features": ["liveness"], - "result": "success" + "features": [ + "liveness" + ], + "result": "success", + "distinctStates": 30, + "totalStates": 78, + "stateDepth": 1 }, { "path": "specifications/Moving_Cat_Puzzle/EvenBoxes.cfg", "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "features": ["liveness"], - "result": "success" + "features": [ + "liveness" + ], + "result": "success", + "distinctStates": 48, + "totalStates": 128, + "stateDepth": 1 } ] - } + } ] }, { @@ -1427,7 +1441,7 @@ "result": "success", "distinctStates": 4122, "totalStates": 14296, - "stateDepth": 36 + "stateDepth": 37 } ] } @@ -1712,7 +1726,7 @@ "result": "success", "distinctStates": 77, "totalStates": 451, - "stateDepth": 12 + "stateDepth": 11 } ] }, @@ -1895,7 +1909,7 @@ "description": "Given a room containing a single light switch prisoners enter one by one, they must develop a strategy to free themselves.", "sources": [], "authors": [ - "Florian Schanda" + "Florian Schanda" ], "tags": [ "beginner" @@ -1915,7 +1929,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 16, + "totalStates": 49, + "stateDepth": 5 }, { "path": "specifications/Prisoners_Single_Switch/PrisonerLightUnknown.cfg", @@ -1925,7 +1942,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 62, + "totalStates": 188, + "stateDepth": 11 }, { "path": "specifications/Prisoners_Single_Switch/SoloPrisoner.cfg", @@ -1935,7 +1955,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 2, + "totalStates": 3, + "stateDepth": 2 }, { "path": "specifications/Prisoners_Single_Switch/SoloPrisonerLightUnknown.cfg", @@ -1945,7 +1968,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 4, + "totalStates": 6, + "stateDepth": 2 } ] } @@ -2269,7 +2295,7 @@ "result": "success", "distinctStates": 1236, "totalStates": 10278, - "stateDepth": 5 + "stateDepth": 6 } ] }, @@ -3061,7 +3087,7 @@ ], "result": "success", "distinctStates": 240, - "totalStates": 392, + "totalStates": 1392, "stateDepth": 10 } ] @@ -3604,7 +3630,7 @@ ], "result": "success", "distinctStates": 400, - "totalStates": 633, + "totalStates": 1633, "stateDepth": 6 } ] @@ -3754,7 +3780,7 @@ "result": "success", "distinctStates": 3316, "totalStates": 128581, - "stateDepth": 10 + "stateDepth": 11 } ] } @@ -4507,7 +4533,7 @@ "result": "success", "distinctStates": 302, "totalStates": 2001, - "stateDepth": 9 + "stateDepth": 10 } ] }, @@ -4582,7 +4608,7 @@ ], "result": "success", "distinctStates": 129, - "totalStates": 722, + "totalStates": 3722, "stateDepth": 1 } ] @@ -5446,4 +5472,4 @@ ] } ] -} +} \ No newline at end of file