Skip to content

Commit 04c1992

Browse files
ahelwerahelwer
committed
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 <[email protected]>
1 parent 1408f6c commit 04c1992

File tree

3 files changed

+66
-34
lines changed

3 files changed

+66
-34
lines changed

‎.github/scripts/record_model_state_space.py‎

Lines changed: 12 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@
1717
parser.add_argument('--skip', nargs='+', help='Space-separated list of models to skip checking', required=False, default=[])
1818
parser.add_argument('--only', nargs='+', help='If provided, only check models in this space-separated list', required=False, default=[])
1919
parser.add_argument('--enable_assertions', help='Enable Java assertions (pass -enableassertions to JVM)', action='store_true')
20+
parser.add_argument('--all', help='Redo all state counts, not just missing ones', action='store_true')
2021
args = parser.parse_args()
2122

2223
logging.basicConfig(level=logging.INFO)
@@ -28,6 +29,7 @@
2829
examples_root = dirname(manifest_path)
2930
skip_models = args.skip
3031
only_models = args.only
32+
run_all = args.all
3133
enable_assertions = args.enable_assertions
3234

3335
def check_model(module, model):
@@ -48,28 +50,30 @@ def check_model(module, model):
4850
enable_assertions,
4951
hard_timeout_in_seconds
5052
)
53+
output = ' '.join(tlc_result.args) + '\n' + tlc_result.stdout
5154
match tlc_result:
5255
case CompletedProcess():
5356
expected_result = model['result']
5457
actual_result = tla_utils.resolve_tlc_exit_code(tlc_result.returncode)
5558
if expected_result != actual_result:
5659
logging.error(f'Model {model_path} expected result {expected_result} but got {actual_result}')
57-
logging.error(tlc_result.stdout)
60+
logging.error(output)
5861
return False
5962
state_count_info = tla_utils.extract_state_count_info(tlc_result.stdout)
6063
if state_count_info is None:
6164
logging.error("Failed to find state info in TLC output")
62-
logging.error(tlc_result.stdout)
65+
logging.error(output)
6366
return False
6467
logging.info(f'States (distinct, total, depth): {state_count_info}')
6568
model['distinctStates'], model['totalStates'], model['stateDepth'] = state_count_info
6669
return True
6770
case TimeoutExpired():
6871
logging.error(f'{model_path} hit hard timeout of {hard_timeout_in_seconds} seconds')
69-
logging.error(tlc_result.output.decode('utf-8'))
72+
logging.error(output)
7073
return False
7174
case _:
7275
logging.error(f'Unhandled TLC result type {type(tlc_result)}: {tlc_result}')
76+
logging.error(output)
7377
return False
7478

7579
# Ensure longest-running modules go first
@@ -82,17 +86,17 @@ def check_model(module, model):
8286
for model in module['models']
8387
if model['size'] == 'small'
8488
and tla_utils.is_state_count_valid(model)
85-
and (
86-
'distinctStates' not in model
87-
or 'totalStates' not in model
88-
or 'stateDepth' not in model
89-
)
9089
# This model is nondeterministic due to use of the Random module
9190
and model['path'] != 'specifications/SpanningTree/SpanTreeRandom.cfg'
9291
# This model generates the same distinct states but order varies
9392
and model['path'] != 'specifications/ewd998/EWD998ChanTrace.cfg'
9493
and model['path'] not in skip_models
9594
and (only_models == [] or model['path'] in only_models)
95+
and (run_all or (
96+
'distinctStates' not in model
97+
or 'totalStates' not in model
98+
or 'stateDepth' not in model
99+
))
96100
],
97101
key = lambda m: m[2],
98102
reverse=True

‎.github/scripts/tla_utils.py‎

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
import locale
12
from datetime import datetime
23
import json
34
from os.path import join, normpath, pathsep
@@ -223,19 +224,20 @@ def is_state_count_info_correct(model, distinct_states, total_states, state_dept
223224
# State depth not yet deterministic due to TLC bug: https://github.com/tlaplus/tlaplus/issues/883
224225
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)
225226

226-
state_count_regex = re.compile(r'(?P<total_states>\d+) states generated, (?P<distinct_states>\d+) distinct states found, 0 states left on queue.')
227-
state_depth_regex = re.compile(r'The depth of the complete state graph search is (?P<state_depth>\d+).')
227+
state_count_regex = re.compile(r'(?P<total_states>[\d,]+) states generated, (?P<distinct_states>[\d,]+) distinct states found, 0 states left on queue.')
228+
state_depth_regex = re.compile(r'The depth of the complete state graph search is (?P<state_depth>[\d,]+).')
228229

229230
def extract_state_count_info(tlc_output):
230231
"""
231232
Parse & extract state count info from TLC output.
232233
"""
234+
locale.setlocale(locale.LC_ALL, 'en_US.UTF-8')
233235
state_count_findings = state_count_regex.search(tlc_output)
234236
state_depth_findings = state_depth_regex.search(tlc_output)
235237
if state_count_findings is None or state_depth_findings is None:
236238
return None
237-
distinct_states = int(state_count_findings.group('distinct_states'))
238-
total_states = int(state_count_findings.group('total_states'))
239-
state_depth = int(state_depth_findings.group('state_depth'))
239+
distinct_states = locale.atoi(state_count_findings.group('distinct_states'))
240+
total_states = locale.atoi(state_count_findings.group('total_states'))
241+
state_depth = locale.atoi(state_depth_findings.group('state_depth'))
240242
return (distinct_states, total_states, state_depth)
241243

‎manifest.json‎

Lines changed: 47 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1335,8 +1335,12 @@
13351335
"title": "The Moving Cat Puzzle",
13361336
"description": "Demonstrating the solution for the moving cat puzzle is correct.",
13371337
"sources": [],
1338-
"authors": ["Florian Schanda"],
1339-
"tags": ["beginner"],
1338+
"authors": [
1339+
"Florian Schanda"
1340+
],
1341+
"tags": [
1342+
"beginner"
1343+
],
13401344
"modules": [
13411345
{
13421346
"path": "specifications/Moving_Cat_Puzzle/Cat.tla",
@@ -1349,19 +1353,29 @@
13491353
"runtime": "00:00:01",
13501354
"size": "small",
13511355
"mode": "exhaustive search",
1352-
"features": ["liveness"],
1353-
"result": "success"
1356+
"features": [
1357+
"liveness"
1358+
],
1359+
"result": "success",
1360+
"distinctStates": 30,
1361+
"totalStates": 78,
1362+
"stateDepth": 1
13541363
},
13551364
{
13561365
"path": "specifications/Moving_Cat_Puzzle/EvenBoxes.cfg",
13571366
"runtime": "00:00:01",
13581367
"size": "small",
13591368
"mode": "exhaustive search",
1360-
"features": ["liveness"],
1361-
"result": "success"
1369+
"features": [
1370+
"liveness"
1371+
],
1372+
"result": "success",
1373+
"distinctStates": 48,
1374+
"totalStates": 128,
1375+
"stateDepth": 1
13621376
}
13631377
]
1364-
}
1378+
}
13651379
]
13661380
},
13671381
{
@@ -1427,7 +1441,7 @@
14271441
"result": "success",
14281442
"distinctStates": 4122,
14291443
"totalStates": 14296,
1430-
"stateDepth": 36
1444+
"stateDepth": 37
14311445
}
14321446
]
14331447
}
@@ -1712,7 +1726,7 @@
17121726
"result": "success",
17131727
"distinctStates": 77,
17141728
"totalStates": 451,
1715-
"stateDepth": 12
1729+
"stateDepth": 11
17161730
}
17171731
]
17181732
},
@@ -1895,7 +1909,7 @@
18951909
"description": "Given a room containing a single light switch prisoners enter one by one, they must develop a strategy to free themselves.",
18961910
"sources": [],
18971911
"authors": [
1898-
"Florian Schanda"
1912+
"Florian Schanda"
18991913
],
19001914
"tags": [
19011915
"beginner"
@@ -1915,7 +1929,10 @@
19151929
"features": [
19161930
"liveness"
19171931
],
1918-
"result": "success"
1932+
"result": "success",
1933+
"distinctStates": 16,
1934+
"totalStates": 49,
1935+
"stateDepth": 5
19191936
},
19201937
{
19211938
"path": "specifications/Prisoners_Single_Switch/PrisonerLightUnknown.cfg",
@@ -1925,7 +1942,10 @@
19251942
"features": [
19261943
"liveness"
19271944
],
1928-
"result": "success"
1945+
"result": "success",
1946+
"distinctStates": 62,
1947+
"totalStates": 188,
1948+
"stateDepth": 11
19291949
},
19301950
{
19311951
"path": "specifications/Prisoners_Single_Switch/SoloPrisoner.cfg",
@@ -1935,7 +1955,10 @@
19351955
"features": [
19361956
"liveness"
19371957
],
1938-
"result": "success"
1958+
"result": "success",
1959+
"distinctStates": 2,
1960+
"totalStates": 3,
1961+
"stateDepth": 2
19391962
},
19401963
{
19411964
"path": "specifications/Prisoners_Single_Switch/SoloPrisonerLightUnknown.cfg",
@@ -1945,7 +1968,10 @@
19451968
"features": [
19461969
"liveness"
19471970
],
1948-
"result": "success"
1971+
"result": "success",
1972+
"distinctStates": 4,
1973+
"totalStates": 6,
1974+
"stateDepth": 2
19491975
}
19501976
]
19511977
}
@@ -2269,7 +2295,7 @@
22692295
"result": "success",
22702296
"distinctStates": 1236,
22712297
"totalStates": 10278,
2272-
"stateDepth": 5
2298+
"stateDepth": 6
22732299
}
22742300
]
22752301
},
@@ -3061,7 +3087,7 @@
30613087
],
30623088
"result": "success",
30633089
"distinctStates": 240,
3064-
"totalStates": 392,
3090+
"totalStates": 1392,
30653091
"stateDepth": 10
30663092
}
30673093
]
@@ -3604,7 +3630,7 @@
36043630
],
36053631
"result": "success",
36063632
"distinctStates": 400,
3607-
"totalStates": 633,
3633+
"totalStates": 1633,
36083634
"stateDepth": 6
36093635
}
36103636
]
@@ -3754,7 +3780,7 @@
37543780
"result": "success",
37553781
"distinctStates": 3316,
37563782
"totalStates": 128581,
3757-
"stateDepth": 10
3783+
"stateDepth": 11
37583784
}
37593785
]
37603786
}
@@ -4507,7 +4533,7 @@
45074533
"result": "success",
45084534
"distinctStates": 302,
45094535
"totalStates": 2001,
4510-
"stateDepth": 9
4536+
"stateDepth": 10
45114537
}
45124538
]
45134539
},
@@ -4582,7 +4608,7 @@
45824608
],
45834609
"result": "success",
45844610
"distinctStates": 129,
4585-
"totalStates": 722,
4611+
"totalStates": 3722,
45864612
"stateDepth": 1
45874613
}
45884614
]
@@ -5446,4 +5472,4 @@
54465472
]
54475473
}
54485474
]
5449-
}
5475+
}

0 commit comments

Comments
 (0)