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.

Signed-off-by: Andrew Helwer <[email protected]>

Author: ahelwer

.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<total_states>\d+) states generated, (?P<distinct_states>\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<state_depth>\d+).')
+state_count_regex = re.compile(r'(?P<total_states>[\d,]+) states generated, (?P<distinct_states>[\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<state_depth>[\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)
 

.gitignore

@@ -1,51 +1,2 @@
-## Ignore all files by default
+# Created by venv; see https://docs.python.org/3/library/venv.html
 *
-
-## Don't ignore TLA+ files
-!*.tla
-
-## Don't ignore TLC model config and results
-!*.cfg
-!*.out  ## Usually .out files are small
-
-## Don't ignore Toolbox model metadata
-!*.launch
-
-## Don't ignore Toolbox spec metadata
-!.project
-!*.prefs
-
-## Don't ignore PDFs
-!*.pdf
-
-## Don't ignore all folders
-!*/
-
-## Ignore TLAPS cache folder
-## See https://github.com/tlaplus/tlapm/issues/16
-__tlacache__
-.tlacache
-
-## Don't ignore CI files
-!.github/**
-
-## Don't ignore READMEs
-!*.md
-
-## Ignore Python artifacts
-__pycache__
-pyvenv.cfg
-
-## Ignore directories used for local CI testing
-deps/
-tree-sitter-tlaplus/
-
-# Ignore TTrace specs
-*_TTrace_*.tla
-
-## Ignore tools/ folder created by .devcontainer.json
-tools/
-
-# Ignore directory created by Apalache
-_apalache-out
-