Skip to content

CI: fix state count regex#176

Merged
ahelwer merged 1 commit intotlaplus:masterfrom
ahelwer:ci-state-count-regex
Jul 1, 2025
Merged

CI: fix state count regex#176
ahelwer merged 1 commit intotlaplus:masterfrom
ahelwer:ci-state-count-regex

Conversation

@ahelwer
Copy link
Copy Markdown
Collaborator

@ahelwer ahelwer commented Jul 1, 2025

Fixes error encountered in #175.

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 <ahelwer@pm.me>
@ahelwer ahelwer force-pushed the ci-state-count-regex branch from 2560577 to e506f44 Compare July 1, 2025 14:51
@ahelwer ahelwer merged commit 04c1992 into tlaplus:master Jul 1, 2025
7 checks passed
@ahelwer ahelwer deleted the ci-state-count-regex branch July 1, 2025 15:20
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Development

Successfully merging this pull request may close these issues.

1 participant