Skip to content

CI: fix state count regex #176

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
ahelwer merged 1 commit into from
Jul 1, 2025
Merged

CI: fix state count regex #176

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 12 additions & 8 deletions .github/scripts/record_model_state_space.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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):
Expand All @@ -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
Expand All @@ -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
Expand Down
12 changes: 7 additions & 5 deletions .github/scripts/tla_utils.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
import locale
from datetime import datetime
import json
from os.path import join, normpath, pathsep
Expand Down Expand Up @@ -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)

68 changes: 47 additions & 21 deletions manifest.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand All @@ -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
}
]
}
}
]
},
{
Expand Down Expand Up @@ -1427,7 +1441,7 @@
"result": "success",
"distinctStates": 4122,
"totalStates": 14296,
"stateDepth": 36
"stateDepth": 37
}
]
}
Expand Down Expand Up @@ -1712,7 +1726,7 @@
"result": "success",
"distinctStates": 77,
"totalStates": 451,
"stateDepth": 12
"stateDepth": 11
}
]
},
Expand Down Expand Up @@ -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"
Expand All @@ -1915,7 +1929,10 @@
"features": [
"liveness"
],
"result": "success"
"result": "success",
"distinctStates": 16,
"totalStates": 49,
"stateDepth": 5
},
{
"path": "specifications/Prisoners_Single_Switch/PrisonerLightUnknown.cfg",
Expand All @@ -1925,7 +1942,10 @@
"features": [
"liveness"
],
"result": "success"
"result": "success",
"distinctStates": 62,
"totalStates": 188,
"stateDepth": 11
},
{
"path": "specifications/Prisoners_Single_Switch/SoloPrisoner.cfg",
Expand All @@ -1935,7 +1955,10 @@
"features": [
"liveness"
],
"result": "success"
"result": "success",
"distinctStates": 2,
"totalStates": 3,
"stateDepth": 2
},
{
"path": "specifications/Prisoners_Single_Switch/SoloPrisonerLightUnknown.cfg",
Expand All @@ -1945,7 +1968,10 @@
"features": [
"liveness"
],
"result": "success"
"result": "success",
"distinctStates": 4,
"totalStates": 6,
"stateDepth": 2
}
]
}
Expand Down Expand Up @@ -2269,7 +2295,7 @@
"result": "success",
"distinctStates": 1236,
"totalStates": 10278,
"stateDepth": 5
"stateDepth": 6
}
]
},
Expand Down Expand Up @@ -3061,7 +3087,7 @@
],
"result": "success",
"distinctStates": 240,
"totalStates": 392,
"totalStates": 1392,
"stateDepth": 10
}
]
Expand Down Expand Up @@ -3604,7 +3630,7 @@
],
"result": "success",
"distinctStates": 400,
"totalStates": 633,
"totalStates": 1633,
"stateDepth": 6
}
]
Expand Down Expand Up @@ -3754,7 +3780,7 @@
"result": "success",
"distinctStates": 3316,
"totalStates": 128581,
"stateDepth": 10
"stateDepth": 11
}
]
}
Expand Down Expand Up @@ -4507,7 +4533,7 @@
"result": "success",
"distinctStates": 302,
"totalStates": 2001,
"stateDepth": 9
"stateDepth": 10
}
]
},
Expand Down Expand Up @@ -4582,7 +4608,7 @@
],
"result": "success",
"distinctStates": 129,
"totalStates": 722,
"totalStates": 3722,
"stateDepth": 1
}
]
Expand Down Expand Up @@ -5446,4 +5472,4 @@
]
}
]
}
}