From b7d2d8c2433854c391b43fe5557a8992cb601bbf Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Thu, 22 Feb 2024 10:24:43 -0500 Subject: [PATCH] Record state count info in manifest, check during CI (#122) Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com> --- .github/scripts/check_manifest_features.py | 34 +- .github/scripts/check_small_models.py | 11 + .github/scripts/generate_manifest.py | 9 +- .github/scripts/record_model_state_space.py | 94 +++++ .github/scripts/tla_utils.py | 52 +++ .github/workflows/CI.yml | 3 +- README.md | 5 +- manifest-schema.json | 3 + manifest.json | 442 ++++++++++++++++---- 9 files changed, 545 insertions(+), 108 deletions(-) create mode 100644 .github/scripts/record_model_state_space.py diff --git a/.github/scripts/check_manifest_features.py b/.github/scripts/check_manifest_features.py index 15d425e5..a666e44f 100644 --- a/.github/scripts/check_manifest_features.py +++ b/.github/scripts/check_manifest_features.py @@ -9,6 +9,7 @@ from argparse import ArgumentParser from dataclasses import dataclass +import logging import glob from os.path import basename, dirname, join, normpath, splitext from typing import Any @@ -16,6 +17,8 @@ import tla_utils from tree_sitter import Language, Parser +logging.basicConfig(level=logging.INFO) + def build_ts_grammar(ts_path): """ Builds the tree-sitter-tlaplus grammar and constructs the parser. @@ -199,33 +202,33 @@ def check_features(parser, queries, manifest, examples_root): for spec in manifest['specifications']: if spec['title'] == '': success = False - print(f'ERROR: Spec {spec["path"]} does not have a title') + logging.error(f'Spec {spec["path"]} does not have a title') if spec['description'] == '': success = False - print(f'ERROR: Spec {spec["path"]} does not have a description') + logging.error(f'Spec {spec["path"]} does not have a description') if not any(spec['authors']): success = False - print(f'ERROR: Spec {spec["path"]} does not have any listed authors') + logging.error(f'Spec {spec["path"]} does not have any listed authors') for module in spec['modules']: module_path = module['path'] tree, text, parse_err = parse_module(examples_root, parser, module_path) if parse_err: success = False - print(f'ERROR: Module {module["path"]} contains syntax errors') + logging.error(f'Module {module["path"]} contains syntax errors') expected_features = get_tree_features(tree, queries) actual_features = set(module['features']) if expected_features != actual_features: success = False - print( - f'ERROR: Module {module["path"]} has incorrect features in manifest; ' + logging.error( + f'Module {module["path"]} has incorrect features in manifest; ' + f'expected {list(expected_features)}, actual {list(actual_features)}' ) expected_imports = get_community_imports(examples_root, tree, text, dirname(module_path), 'proof' in expected_features, queries) actual_imports = set(module['communityDependencies']) if expected_imports != actual_imports: success = False - print( - f'ERROR: Module {module["path"]} has incorrect community dependencies in manifest; ' + logging.error( + f'Module {module["path"]} has incorrect community dependencies in manifest; ' + f'expected {list(expected_imports)}, actual {list(actual_imports)}' ) for model in module['models']: @@ -233,10 +236,17 @@ def check_features(parser, queries, manifest, examples_root): actual_features = set(model['features']) if expected_features != actual_features: success = False - print( - f'ERROR: Model {model["path"]} has incorrect features in manifest; ' + logging.error( + f'Model {model["path"]} has incorrect features in manifest; ' + f'expected {list(expected_features)}, actual {list(actual_features)}' ) + if tla_utils.has_state_count(model) and not tla_utils.is_state_count_valid(model): + success = False + logging.error( + f'Model {model["path"]} has state count info recorded; this is ' + + 'only valid for exhaustive search models that complete successfully.' + ) + return success if __name__ == '__main__': @@ -253,9 +263,9 @@ def check_features(parser, queries, manifest, examples_root): queries = build_queries(TLAPLUS_LANGUAGE) if check_features(parser, queries, manifest, examples_root): - print('SUCCESS: metadata in manifest is correct') + logging.info('SUCCESS: metadata in manifest is correct') exit(0) else: - print("ERROR: metadata in manifest is incorrect") + logging.error("Metadata in manifest is incorrect") exit(1) diff --git a/.github/scripts/check_small_models.py b/.github/scripts/check_small_models.py index 79f87273..228bdf75 100644 --- a/.github/scripts/check_small_models.py +++ b/.github/scripts/check_small_models.py @@ -55,6 +55,17 @@ def check_model(module_path, model, expected_runtime): logging.error(f'Model {model_path} expected result {expected_result} but got {actual_result}') logging.error(tlc_result.stdout) return False + if tla_utils.is_state_count_valid(model) and tla_utils.has_state_count(model): + 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) + return False + if not tla_utils.is_state_count_info_correct(model, *state_count_info): + logging.error("Recorded state count info differed from actual state counts:") + logging.error(f"(distinct/total/depth); expected: {tla_utils.get_state_count_info(model)}, actual: {state_count_info}") + logging.error(tlc_result.stdout) + return False return True case TimeoutExpired(): logging.error(f'{model_path} hit hard timeout of {hard_timeout_in_seconds} seconds') diff --git a/.github/scripts/generate_manifest.py b/.github/scripts/generate_manifest.py index b3a8463a..9ed04d41 100644 --- a/.github/scripts/generate_manifest.py +++ b/.github/scripts/generate_manifest.py @@ -140,9 +140,10 @@ def find_corresponding_model(old_model, new_module): return models[0] if any(models) else None def integrate_model_info(old_model, new_model): - fields = ['runtime', 'size', 'mode', 'result'] + fields = ['runtime', 'size', 'mode', 'result', 'distinctStates', 'totalStates', 'stateDepth'] for field in fields: - new_model[field] = old_model[field] + if field in old_model: + new_model[field] = old_model[field] def integrate_old_manifest_into_new(old_manifest, new_manifest): for old_spec in old_manifest['specifications']: @@ -180,7 +181,5 @@ def integrate_old_manifest_into_new(old_manifest, new_manifest): new_manifest = generate_new_manifest(examples_root, ignored_dirs, parser, queries) integrate_old_manifest_into_new(old_manifest, new_manifest) - # Write generated manifest to file - with open(manifest_path, 'w', encoding='utf-8') as new_manifest_file: - json.dump(new_manifest, new_manifest_file, indent=2, ensure_ascii=False) + tla_utils.write_json(new_manifest, manifest_path) diff --git a/.github/scripts/record_model_state_space.py b/.github/scripts/record_model_state_space.py new file mode 100644 index 00000000..32f9ebd5 --- /dev/null +++ b/.github/scripts/record_model_state_space.py @@ -0,0 +1,94 @@ +""" +Records the number of unique & total states encountered by TLC for each small +model where that info is not present, then writes it to the manifest.json. +""" + +from argparse import ArgumentParser +import logging +from os.path import dirname, normpath +from subprocess import CompletedProcess, TimeoutExpired +import tla_utils + +parser = ArgumentParser(description='Updates manifest.json with unique & total model states for each small model.') +parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=True) +parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=True) +parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', required=True) +parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True) +args = parser.parse_args() + +logging.basicConfig(level=logging.INFO) + +tools_jar_path = normpath(args.tools_jar_path) +tlapm_lib_path = normpath(args.tlapm_lib_path) +community_jar_path = normpath(args.community_modules_jar_path) +manifest_path = normpath(args.manifest_path) +examples_root = dirname(manifest_path) + +def check_model(module_path, model): + module_path = tla_utils.from_cwd(examples_root, module_path) + model_path = tla_utils.from_cwd(examples_root, model['path']) + logging.info(model_path) + hard_timeout_in_seconds = 60 + tlc_result = tla_utils.check_model( + tools_jar_path, + module_path, + model_path, + tlapm_lib_path, + community_jar_path, + model['mode'], + hard_timeout_in_seconds + ) + 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) + 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) + 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')) + return False + case _: + logging.error(f'Unhandled TLC result type {type(tlc_result)}: {tlc_result}') + return False + +# Ensure longest-running modules go first +manifest = tla_utils.load_json(manifest_path) +small_models = sorted( + [ + (module['path'], model, tla_utils.parse_timespan(model['runtime'])) + for spec in manifest['specifications'] + for module in spec['modules'] + 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' + ], + key = lambda m: m[2], + reverse=True +) + +for module_path, model, _ in small_models: + success = check_model(module_path, model) + if not success: + exit(1) + tla_utils.write_json(manifest, manifest_path) + +exit(0) + diff --git a/.github/scripts/tla_utils.py b/.github/scripts/tla_utils.py index 85ea568a..4b5f0b5f 100644 --- a/.github/scripts/tla_utils.py +++ b/.github/scripts/tla_utils.py @@ -2,6 +2,7 @@ import json from os.path import join, normpath, pathsep import subprocess +import re def from_cwd(root, path): """ @@ -42,6 +43,13 @@ def load_json(path): with open(normpath(path), 'r', encoding='utf-8') as file: return json.load(file) +def write_json(data, path): + """ + Writes the given json to the given file. + """ + with open(path, 'w', encoding='utf-8') as file: + json.dump(data, file, indent=2, ensure_ascii=False) + def parse_timespan(unparsed): """ Parses the timespan format used in the manifest.json format. @@ -116,3 +124,47 @@ def resolve_tlc_exit_code(code): return tlc_exit_codes[code] if code in tlc_exit_codes else str(code) +def is_state_count_valid(model): + """ + Whether state count info could be valid for the given model. + """ + return model['mode'] == 'exhaustive search' and model['result'] == 'success' + +def has_state_count(model): + """ + Whether the given model has state count info. + """ + return 'distinctStates' in model or 'totalStates' in model or 'stateDepth' in model + +def get_state_count_info(model): + """ + Gets whatever state count info is present in the given model. + """ + get_or_none = lambda key: model[key] if key in model else None + return (get_or_none('distinctStates'), get_or_none('totalStates'), get_or_none('stateDepth')) + +def is_state_count_info_correct(model, distinct_states, total_states, state_depth): + """ + Whether the given state count info concords with the model. + """ + expected_distinct_states, expected_total_states, expected_state_depth = get_state_count_info(model) + none_or_equal = lambda expected, actual: expected is None or expected == actual + # 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+).') + +def extract_state_count_info(tlc_output): + """ + Parse & extract state count info from TLC output. + """ + 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')) + return (distinct_states, total_states, state_depth) + diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index bfa62a00..4b1749b2 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -18,7 +18,8 @@ jobs: include: - { os: windows-latest } - { os: ubuntu-latest } - - { os: macos-14 } + # https://github.com/tlaplus/Examples/issues/119 + #- { os: macos-14 } fail-fast: false env: SCRIPT_DIR: .github/scripts diff --git a/README.md b/README.md index 06f0dc4a..48573b7b 100644 --- a/README.md +++ b/README.md @@ -52,6 +52,7 @@ Here is a list of specs included in this repository, with links to the relevant | [Minimal Circular Substring](specifications/LeastCircularSubstring) | Andrew Helwer | | | ✔ | ✔ | | | [Snapshot Key-Value Store](specifications/KeyValueStore) | Andrew Helwer, Murat Demirbas | | | ✔ | ✔ | | | [Chang-Roberts Algorithm for Leader Election in a Ring](specifications/chang_roberts) | Stephan Merz | | | ✔ | ✔ | | +| [MultiPaxos in SMR-Style](specifications/MultiPaxos-SMR) | Guanzhou Hu | | | ✔ | ✔ | | | [Resource Allocator](specifications/allocator) | Stephan Merz | | | | ✔ | | | [Transitive Closure](specifications/TransitiveClosure) | Stephan Merz | | | | ✔ | | | [Atomic Commitment Protocol](specifications/acp) | Stephan Merz | | | | ✔ | | @@ -86,7 +87,6 @@ Here is a list of specs included in this repository, with links to the relevant | [RFC 3506: Voucher Transaction System](specifications/byihive) | Santhosh Raju, Cherry G. Mathew, Fransisca Andriani | | | | ✔ | | | [TLA⁺ Level Checking](specifications/LevelChecking) | Leslie Lamport | | | | | | | [Condition-Based Consensus](specifications/cbc_max) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | | | -| [MultiPaxos in SMR-Style](specifications/MultiPaxos-SMR) | Guanzhou Hu | | | ✔ | ✔ | | ## Examples Elsewhere Here is a list of specs stored in locations outside this repository, including submodules. @@ -185,6 +185,9 @@ Otherwise, follow these directions: - `"safety failure"` if the model violates an invariant - `"liveness failure"` if the model fails to satisfy a liveness property - `"deadlock failure"` if the model encounters deadlock + - (Optional) Model state count info: distinct states, total states, and state depth + - These are all individually optional and only valid if your model uses exhaustive search and results in success + - Recording these turns your model into a powerful regression test for TLC - Other fields are auto-generated by the script; if you are adding an entry manually, ensure their values are present and correct (see other entries or the [`manifest-schema.json`](manifest-schema.json) file) Before submitted your changes to run in the CI, you can quickly check your [`manifest.json`](manifest.json) for errors and also check it against [`manifest-schema.json`](manifest-schema.json) at https://www.jsonschemavalidator.net/. diff --git a/manifest-schema.json b/manifest-schema.json index cdb72739..a8121585 100644 --- a/manifest-schema.json +++ b/manifest-schema.json @@ -55,6 +55,9 @@ "pattern": "^(([0-9][0-9]:[0-9][0-9]:[0-9][0-9])|unknown)$" }, "size": {"enum": ["small", "medium", "large", "unknown"]}, + "distinctStates": {"type": "integer"}, + "totalStates": {"type": "integer"}, + "stateDepth": {"type": "integer"}, "mode": { "oneOf": [ { diff --git a/manifest.json b/manifest.json index 22381d90..4645477e 100644 --- a/manifest.json +++ b/manifest.json @@ -45,7 +45,10 @@ "features": [ "ignore deadlock" ], - "result": "success" + "result": "success", + "distinctStates": 598608, + "totalStates": 3141768, + "stateDepth": 1 } ] }, @@ -107,7 +110,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 0, + "totalStates": 0, + "stateDepth": 0 } ] }, @@ -130,7 +136,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 0, + "totalStates": 0, + "stateDepth": 0 } ] }, @@ -185,7 +194,10 @@ "features": [ "ignore deadlock" ], - "result": "success" + "result": "success", + "distinctStates": 34534, + "totalStates": 104697, + "stateDepth": 13 } ] } @@ -267,7 +279,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 6, + "totalStates": 15, + "stateDepth": 2 } ] } @@ -311,7 +326,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 5150, + "totalStates": 20002, + "stateDepth": 1 }, { "path": "specifications/CoffeeCan/CoffeeCan3000Beans.cfg", @@ -408,7 +426,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 67, + "totalStates": 336, + "stateDepth": 29 } ] } @@ -479,7 +500,10 @@ "liveness", "state constraint" ], - "result": "success" + "result": "success", + "distinctStates": 50000, + "totalStates": 575001, + "stateDepth": 17 } ] }, @@ -497,7 +521,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 50000, + "totalStates": 585401, + "stateDepth": 17 } ] }, @@ -515,7 +542,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 56492, + "totalStates": 237626, + "stateDepth": 17 } ] }, @@ -552,7 +582,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 65536, + "totalStates": 131072, + "stateDepth": 1 } ] } @@ -796,7 +829,10 @@ "features": [ "state constraint" ], - "result": "success" + "result": "success", + "distinctStates": 742, + "totalStates": 1523, + "stateDepth": 5 } ] } @@ -843,7 +879,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 8554, + "totalStates": 8681, + "stateDepth": 95 } ] }, @@ -915,7 +954,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 27953, + "totalStates": 34383, + "stateDepth": 6 } ] }, @@ -933,7 +975,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 4548, + "totalStates": 11223, + "stateDepth": 9 } ] }, @@ -985,7 +1030,10 @@ "features": [ "ignore deadlock" ], - "result": "success" + "result": "success", + "distinctStates": 2733, + "totalStates": 3459, + "stateDepth": 6 } ] }, @@ -1055,7 +1103,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 0, + "totalStates": 0, + "stateDepth": 0 } ] }, @@ -1228,7 +1279,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 4122, + "totalStates": 14296, + "stateDepth": 36 } ] } @@ -1271,7 +1325,10 @@ "features": [ "symmetry" ], - "result": "success" + "result": "success", + "distinctStates": 343796, + "totalStates": 736012, + "stateDepth": 28 }, { "path": "specifications/MultiPaxos-SMR/MultiPaxos_MC.cfg", @@ -1413,7 +1470,10 @@ "features": [ "view" ], - "result": "success" + "result": "success", + "distinctStates": 3003, + "totalStates": 6083, + "stateDepth": 7 } ] }, @@ -1459,7 +1519,10 @@ "features": [ "ignore deadlock" ], - "result": "success" + "result": "success", + "distinctStates": 4, + "totalStates": 7, + "stateDepth": 1 } ] }, @@ -1478,7 +1541,10 @@ "liveness", "symmetry" ], - "result": "success" + "result": "success", + "distinctStates": 25, + "totalStates": 82, + "stateDepth": 9 } ] }, @@ -1498,7 +1564,10 @@ "liveness", "symmetry" ], - "result": "success" + "result": "success", + "distinctStates": 77, + "totalStates": 451, + "stateDepth": 12 } ] }, @@ -1555,7 +1624,10 @@ "features": [ "ignore deadlock" ], - "result": "success" + "result": "success", + "distinctStates": 4, + "totalStates": 4, + "stateDepth": 2 } ] }, @@ -1583,7 +1655,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 3921, + "totalStates": 23563, + "stateDepth": 17 } ] }, @@ -1602,7 +1677,10 @@ "ignore deadlock", "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 6752, + "totalStates": 41017, + "stateDepth": 16 } ] }, @@ -1657,7 +1735,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 214, + "totalStates": 860, + "stateDepth": 14 } ] } @@ -1687,7 +1768,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 21527, + "totalStates": 59674, + "stateDepth": 13 } ] }, @@ -1728,7 +1812,10 @@ "ignore deadlock", "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 2881, + "totalStates": 6826, + "stateDepth": 21 } ] }, @@ -1818,7 +1905,10 @@ "liveness", "symmetry" ], - "result": "success" + "result": "success", + "distinctStates": 1207, + "totalStates": 13290, + "stateDepth": 22 } ] } @@ -1848,7 +1938,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 3605, + "totalStates": 20181, + "stateDepth": 29 } ] }, @@ -1932,7 +2025,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 274678, + "totalStates": 1621541, + "stateDepth": 43 } ] } @@ -1963,7 +2059,10 @@ "ignore deadlock", "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 1236, + "totalStates": 10278, + "stateDepth": 5 } ] }, @@ -2000,7 +2099,10 @@ "ignore deadlock", "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 3984, + "totalStates": 21784, + "stateDepth": 4 }, { "path": "specifications/SpanningTree/SpanTreeTest5Nodes.cfg", @@ -2081,7 +2183,10 @@ "liveness", "state constraint" ], - "result": "success" + "result": "success", + "distinctStates": 3528, + "totalStates": 24368, + "stateDepth": 9 } ] }, @@ -2130,7 +2235,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 12, + "totalStates": 30, + "stateDepth": 2 } ] }, @@ -2146,7 +2254,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 12, + "totalStates": 30, + "stateDepth": 2 } ] }, @@ -2162,7 +2273,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 0, + "totalStates": 0, + "stateDepth": 0 } ] }, @@ -2185,7 +2299,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 4408, + "totalStates": 21400, + "stateDepth": 10 } ] }, @@ -2203,7 +2320,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 5196, + "totalStates": 28170, + "stateDepth": 18 } ] }, @@ -2333,7 +2453,10 @@ "features": [ "state constraint" ], - "result": "success" + "result": "success", + "distinctStates": 3864, + "totalStates": 9660, + "stateDepth": 11 } ] }, @@ -2349,7 +2472,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 12, + "totalStates": 24, + "stateDepth": 1 } ] }, @@ -2367,7 +2493,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 12, + "totalStates": 24, + "stateDepth": 1 } ] }, @@ -2399,7 +2528,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 12, + "totalStates": 24, + "stateDepth": 1 } ] }, @@ -2438,7 +2570,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 4408, + "totalStates": 21400, + "stateDepth": 10 } ] }, @@ -2456,7 +2591,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 5196, + "totalStates": 28170, + "stateDepth": 18 } ] }, @@ -2581,7 +2719,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 0, + "totalStates": 0, + "stateDepth": 0 } ] }, @@ -2667,7 +2808,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 20, + "totalStates": 36, + "stateDepth": 3 } ] }, @@ -2707,7 +2851,10 @@ "liveness", "state constraint" ], - "result": "success" + "result": "success", + "distinctStates": 240, + "totalStates": 392, + "stateDepth": 10 } ] } @@ -2737,7 +2884,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 0, + "totalStates": 0, + "stateDepth": 0 } ] } @@ -2776,7 +2926,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 2790, + "totalStates": 2990, + "stateDepth": 52 } ] } @@ -2811,7 +2964,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 723, + "totalStates": 1842, + "stateDepth": 11 } ] }, @@ -2830,7 +2986,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 277726, + "totalStates": 1454776, + "stateDepth": 25 } ] } @@ -2858,7 +3017,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 0, + "totalStates": 0, + "stateDepth": 0 } ] } @@ -2894,7 +3056,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 4, + "totalStates": 5, + "stateDepth": 4 } ] }, @@ -2985,7 +3150,10 @@ "ignore deadlock", "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 4284, + "totalStates": 23988, + "stateDepth": 19 } ] }, @@ -3030,7 +3198,10 @@ "ignore deadlock", "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 54944, + "totalStates": 218352, + "stateDepth": 21 } ] } @@ -3060,7 +3231,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 17701, + "totalStates": 64414, + "stateDepth": 16 } ] }, @@ -3078,7 +3252,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 1690, + "totalStates": 5854, + "stateDepth": 7 } ] }, @@ -3096,7 +3273,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 1690, + "totalStates": 5854, + "stateDepth": 7 } ] }, @@ -3114,7 +3294,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 400, + "totalStates": 633, + "stateDepth": 6 } ] } @@ -3148,7 +3331,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 14424, + "totalStates": 227344, + "stateDepth": 7 }, { "path": "specifications/bcastByz/bcastByzNoBcast.cfg", @@ -3158,7 +3344,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 45, + "totalStates": 90, + "stateDepth": 1 } ] } @@ -3254,7 +3443,10 @@ "features": [ "ignore deadlock" ], - "result": "success" + "result": "success", + "distinctStates": 4199, + "totalStates": 26848, + "stateDepth": 11 } ] }, @@ -3273,7 +3465,10 @@ "ignore deadlock", "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 4199, + "totalStates": 26848, + "stateDepth": 11 } ] }, @@ -3291,7 +3486,10 @@ "features": [ "ignore deadlock" ], - "result": "success" + "result": "success", + "distinctStates": 64, + "totalStates": 193, + "stateDepth": 7 } ] }, @@ -3309,7 +3507,10 @@ "features": [ "ignore deadlock" ], - "result": "success" + "result": "success", + "distinctStates": 4199, + "totalStates": 26848, + "stateDepth": 11 } ] }, @@ -3327,7 +3528,10 @@ "features": [ "ignore deadlock" ], - "result": "success" + "result": "success", + "distinctStates": 4197, + "totalStates": 26848, + "stateDepth": 11 } ] } @@ -3384,7 +3588,10 @@ "ignore deadlock", "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 4, + "totalStates": 4, + "stateDepth": 2 } ] }, @@ -3425,7 +3632,10 @@ "ignore deadlock", "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 6962, + "totalStates": 318877, + "stateDepth": 15 } ] } @@ -3550,7 +3760,10 @@ "ignore deadlock", "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 137, + "totalStates": 227, + "stateDepth": 10 } ] } @@ -3760,7 +3973,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 75, + "totalStates": 116, + "stateDepth": 16 } ] }, @@ -3824,7 +4040,10 @@ "ignore deadlock", "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 46656, + "totalStates": 248832, + "stateDepth": 1 } ] } @@ -3939,7 +4158,10 @@ "features": [ "ignore deadlock" ], - "result": "success" + "result": "success", + "distinctStates": 302, + "totalStates": 2001, + "stateDepth": 9 } ] }, @@ -3982,7 +4204,10 @@ "features": [ "ignore deadlock" ], - "result": "success" + "result": "success", + "distinctStates": 1566, + "totalStates": 15986, + "stateDepth": 12 } ] }, @@ -4009,7 +4234,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 129, + "totalStates": 722, + "stateDepth": 1 } ] }, @@ -4052,7 +4280,10 @@ "liveness", "state constraint" ], - "result": "success" + "result": "success", + "distinctStates": 4097, + "totalStates": 53271, + "stateDepth": 14 } ] }, @@ -4135,7 +4366,10 @@ "state constraint", "view" ], - "result": "success" + "result": "success", + "distinctStates": 14, + "totalStates": 15, + "stateDepth": 14 } ] }, @@ -4318,7 +4552,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 63, + "totalStates": 99, + "stateDepth": 10 } ] }, @@ -4337,7 +4574,10 @@ "ignore deadlock", "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 305, + "totalStates": 376, + "stateDepth": 23 } ] }, @@ -4356,7 +4596,10 @@ "ignore deadlock", "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 83, + "totalStates": 93, + "stateDepth": 23 } ] } @@ -4409,7 +4652,10 @@ "features": [ "state constraint" ], - "result": "success" + "result": "success", + "distinctStates": 724274, + "totalStates": 2729079, + "stateDepth": 61 } ] }, @@ -4469,7 +4715,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 3016, + "totalStates": 49592, + "stateDepth": 7 } ] } @@ -4501,7 +4750,10 @@ "features": [ "liveness" ], - "result": "success" + "result": "success", + "distinctStates": 24922, + "totalStates": 159538, + "stateDepth": 16 } ] } @@ -4568,7 +4820,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 0, + "totalStates": 0, + "stateDepth": 0 } ] }, @@ -4688,7 +4943,10 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 1245, + "totalStates": 5841, + "stateDepth": 15 } ] }, @@ -4722,7 +4980,10 @@ "features": [ "ignore deadlock" ], - "result": "success" + "result": "success", + "distinctStates": 34, + "totalStates": 94, + "stateDepth": 7 } ] }, @@ -4738,11 +4999,14 @@ "size": "small", "mode": "exhaustive search", "features": [], - "result": "success" + "result": "success", + "distinctStates": 288, + "totalStates": 1146, + "stateDepth": 11 } ] } ] } ] -} \ No newline at end of file +}