diff --git a/.ciignore b/.ciignore new file mode 100644 index 00000000..2887d259 --- /dev/null +++ b/.ciignore @@ -0,0 +1,7 @@ +# Every line starting with # is a comment line +# Every non-blank non-comment line lists a directory to ignore in the CI +# This will keep parse or model check failures from failing the CI workflow +# Note that directory names are case-sensitive +# Example: +specifications/doesnotexist + diff --git a/.github/scripts/check_manifest_features.py b/.github/scripts/check_manifest_features.py new file mode 100644 index 00000000..06538bd8 --- /dev/null +++ b/.github/scripts/check_manifest_features.py @@ -0,0 +1,223 @@ +""" +This script performs whatever validations are possible on the metadata in +the manifest.json file. Prominent checks include: + * .tla files containing pluscal or proofs are marked as such + * .tla files importing community modules have those modules listed + * .cfg files with certain features are marked as such + * Human-written fields are not empty +""" + +import glob +import json +from os.path import basename, dirname, splitext +import tla_utils +from tree_sitter import Language, Parser + +# Builds the tree-sitter-tlaplus grammar and constructs the parser +Language.build_library( + 'build/tree-sitter-languages.so', + ['tree-sitter-tlaplus'] +) + +TLAPLUS_LANGUAGE = Language('build/tree-sitter-languages.so', 'tlaplus') +parser = Parser() +parser.set_language(TLAPLUS_LANGUAGE) + +def parse_module(path): + """ + Parses a .tla file; returns the parse tree along with whether a parse + error was detected. + """ + module_text = None + with open(path, 'rb') as module_file: + module_text = module_file.read() + tree = parser.parse(module_text) + return (tree, module_text, tree.root_node.has_error) + +def get_module_names_in_dir(dir): + """ + Gets the module names of all .tla files in the given directory. + """ + return set([splitext(basename(path))[0] for path in glob.glob(f'{dir}/*.tla')]) + +# This query looks for pluscal and proof constructs +# It can be extended to look for other things if desired +feature_query = TLAPLUS_LANGUAGE.query( + '(pcal_algorithm_start) @pluscal' + + '[(terminal_proof) (non_terminal_proof)] @proof' +) + +def get_tree_features(tree): + """ + Returns any notable features in the parse tree, such as pluscal or proofs + """ + return set([name for _, name in feature_query.captures(tree.root_node)]) + +def get_module_features(path): + """ + Gets notable features for the .tla file at the given path + """ + tree, _, _ = parse_module(path) + return get_tree_features(tree) + +# Keywords mapping to features for models +model_features = { + 'PROPERTY': 'liveness', + 'PROPERTIES': 'liveness', + 'SYMMETRY': 'symmetry', + 'ALIAS': 'alias', + 'VIEW': 'view', + 'CONSTRAINT': 'state constraint', + 'CONSTRAINTS': 'state constraint', +} + +def get_model_features(path): + """ + Finds features present in the given .cfg model file. + This will be a best-effort text search until a tree-sitter grammar is + created for .cfg files. + """ + features = [] + model_text = None + with open(path, 'rt') as model_file: + model_text = model_file.read() + for line in model_text.split('\n'): + tokens = line.split() + if len(tokens) > 0 and tokens[0] in model_features: + features.append(model_features[tokens[0]]) + return set(features) + +# Query finding all module imports in a .tla file +import_query = TLAPLUS_LANGUAGE.query( + '(extends (identifier_ref) @extends)' + + '(instance (identifier_ref) @instance)' +) + +# Query finding all defined module names in a .tla file +# Especially useful for finding nested module names +module_name_query = TLAPLUS_LANGUAGE.query( + '(module name: (identifier) @module_name)' +) + +# All the standard modules available when using TLC +tlc_modules = { + 'Bags', + 'FiniteSets', + 'Integers', + 'Json', + 'Naturals', + 'Randomization', + 'RealTime', + 'Reals', + 'Sequences', + 'TLC', + 'TLCExt', + 'Toolbox' +} + +# All the standard modules available when using TLAPS +tlaps_modules = { + 'BagsTheorems', + 'FiniteSetTheorems', + 'FunctionTheorems', + 'NaturalsInduction', + 'SequencesExtTheorems', + 'SequenceTheorems', + 'TLAPS', + 'WellFoundedInduction' +} + +# Modules overloaded by TLAPS; some of these are ordinarily imported as +# community modules. +tlaps_module_overloads = { + 'Bags', + 'FiniteSets', + 'Functions', + 'RealTime', + 'SequencesExt' +} + +def get_community_imports(tree, text, dir, has_proof): + """ + Gets all modules imported by a given .tla file that are not standard + modules or modules in the same file or directory. Community module + imports are what's left. + """ + imports = set( + [ + text[node.start_byte:node.end_byte].decode('utf-8') + for node, _ in import_query.captures(tree.root_node) + ] + ) + modules_in_file = set( + [ + text[node.start_byte:node.end_byte].decode('utf-8') + for node, _ in module_name_query.captures(tree.root_node) + ] + ) + imports = ( + imports + - modules_in_file + - tlc_modules + - tlaps_modules + - get_module_names_in_dir(dir) + ) + return imports - tlaps_module_overloads if has_proof else imports + +def get_community_module_imports(path): + """ + Gets all community modules imported by the .tla file at the given path. + """ + tree, text, _ = parse_module(path) + dir = dirname(path) + has_proof = 'proof' in get_tree_features(tree) + return get_community_imports(tree, text, dir, has_proof) + +if __name__ == '__main__': + manifest = tla_utils.load_manifest() + + # Validates every field of the manifest that can be validated. + success = True + for spec in manifest['specifications']: + if spec['title'] == '': + success = False + print(f'Spec {spec["path"]} does not have a title') + if spec['description'] == '': + success = False + print(f'Spec {spec["path"]} does not have a description') + if not any(spec['authors']): + success = False + print(f'Spec {spec["path"]} does not have any listed authors') + for module in spec['modules']: + tree, text, parse_err = parse_module(module['path']) + if parse_err: + success = False + print(f'Module {module["path"]} contains syntax errors') + expected_features = get_tree_features(tree) + actual_features = set(module['features']) + if expected_features != actual_features: + success = False + print( + f'Module {module["path"]} has incorrect features in manifest; ' + + f'expected {list(expected_features)}, actual {list(actual_features)}' + ) + expected_imports = get_community_imports(tree, text, dirname(module['path']), 'proof' in expected_features) + actual_imports = set(module['communityDependencies']) + if expected_imports != actual_imports: + success = False + print( + f'Module {module["path"]} has incorrect community dependencies in manifest; ' + + f'expected {list(expected_imports)}, actual {list(actual_imports)}' + ) + for model in module['models']: + expected_features = get_model_features(model['path']) + actual_features = set(model['features']) + if expected_features != actual_features: + success = False + print( + f'Model {model["path"]} has incorrect features in manifest; ' + + f'expected {list(expected_features)}, actual {list(actual_features)}' + ) + + exit(0 if success else 1) + diff --git a/.github/scripts/check_manifest_files.py b/.github/scripts/check_manifest_files.py new file mode 100644 index 00000000..7581a5fc --- /dev/null +++ b/.github/scripts/check_manifest_files.py @@ -0,0 +1,79 @@ +""" +Checks to ensure all files in manifest.json exist, that all .tla and .cfg +files in repo are recorded in manifest.json (except for those in .ciignore), +and that no files are present twice in the manifest. Also checks to ensure +no files in .ciignore are in the manifest.json. +""" + +from collections import Counter +import json +from os.path import normpath +import glob +import tla_utils + +manifest = tla_utils.load_manifest() + +module_lists = [spec["modules"] for spec in manifest["specifications"]] +modules = [module for module_list in module_lists for module in module_list] +model_lists = [module["models"] for module in modules] + +# Get all .tla and .cfg paths from the manifest +tla_mf_paths_cnt = Counter([normpath(module["path"]) for module in modules]) +tla_mf_paths = set(tla_mf_paths_cnt) +cfg_mf_paths_cnt = Counter([normpath(model["path"]) for model_list in model_lists for model in model_list]) +cfg_mf_paths = set(cfg_mf_paths_cnt) + +# Get ignored directories +ignored_dirs = tla_utils.get_ignored_dirs() +ignore = lambda path : tla_utils.ignore(ignored_dirs, path) + +# Get paths of all non-ignored .tla and .cfg files in the specifications dir +tla_fs_paths = set([ + normpath(path) for path in glob.glob(f"./specifications/**/*.tla", recursive=True) + if '_TTrace_' not in path and not ignore(path) +]) +cfg_fs_paths = set([ + normpath(path) for path in glob.glob(f"./specifications/**/*.cfg", recursive=True) + if not ignore(path) +]) + +success = True + +# Check whether manifest includes any ignored paths +ignored_tla_in_manifest = set(filter(ignore, tla_mf_paths)) +ignored_cfg_in_manifest = set(filter(ignore, cfg_mf_paths)) +if any(ignored_tla_in_manifest): + success = False + print('Ignored .tla paths present in manifest:\n' + '\n'.join(ignored_tla_in_manifest)) + tla_mf_paths = tla_mf_paths - ignored_tla_in_manifest +if any(ignored_cfg_in_manifest): + success = False + print('Ignored .cfg paths present in manifest:\n' + '\n'.join(ignored_cfg_in_manifest)) + cfg_mf_paths = cfg_mf_paths - ignored_cfg_in_manifest + +# Check for duplicate paths in manifest +duplicate_tla_paths = [k for k, v in tla_mf_paths_cnt.items() if v > 1] +duplicate_cfg_paths = [k for k, v in cfg_mf_paths_cnt.items() if v > 1] +if any(duplicate_tla_paths): + success = False + print('.tla file paths duplicated in manifest:\n' + '\n'.join(duplicate_tla_paths)) +if any(duplicate_cfg_paths): + success = False + print('.cfg file paths duplicated in manifest:\n' + '\n'.join(duplicate_cfg_paths)) + +# Check paths in manifest match paths on filesystem +if tla_mf_paths < tla_fs_paths: + success = False + print('.tla files not recorded in manifest:\n' + '\n'.join(tla_fs_paths - tla_mf_paths)) +if tla_fs_paths < tla_mf_paths: + success = False + print('Manifest .tla files not found in specifications dir:\n' + '\n'.join(tla_mf_paths - tla_fs_paths)) +if cfg_mf_paths < cfg_fs_paths: + success = False + print('.cfg files not recorded in manifest:\n' + '\n'.join(cfg_fs_paths - cfg_mf_paths)) +if cfg_fs_paths < cfg_mf_paths: + success = False + print('Manifest .cfg files not found in specifications dir:\n' + '\n'.join(cfg_mf_paths - cfg_fs_paths)) + +exit(0 if success else 1) + diff --git a/.github/scripts/check_manifest_schema.py b/.github/scripts/check_manifest_schema.py new file mode 100644 index 00000000..c1d22bef --- /dev/null +++ b/.github/scripts/check_manifest_schema.py @@ -0,0 +1,21 @@ +""" +Checks to ensure manifest.json is valid according to schema; this can also +be done manually at https://www.jsonschemavalidator.net/ +Learn about the JSON schema format at +https://json-schema.org/understanding-json-schema/ +""" + +import json +from jsonschema import validate +import tla_utils + +schema = tla_utils.load_schema() +manifest = tla_utils.load_manifest() + +result = validate(instance=manifest, schema=schema) +if None == result: + exit(0) +else: + print(result) + exit(1) + diff --git a/.github/scripts/check_small_models.py b/.github/scripts/check_small_models.py new file mode 100644 index 00000000..bc6740eb --- /dev/null +++ b/.github/scripts/check_small_models.py @@ -0,0 +1,66 @@ +""" +Check all models marked as size "small" in the manifest with TLC. Small +models should finish executing in less than ten seconds on the GitHub CI +machines. +""" + +from datetime import datetime +import logging +from timeit import default_timer as timer +import tla_utils + +def parse_timespan(unparsed): + pattern = '%H:%M:%S' + return datetime.strptime(unparsed, pattern) - datetime.strptime('00:00:00', pattern) + +tlc_result = { + 0 : 'success', + 11 : 'deadlock failure', + 12 : 'safety failure', + 13 : 'liveness failure' +} + +def check_model(module_path, model, expected_runtime): + model_path = model['path'] + logging.info(model_path) + expected_result = model['result'] + start_time = timer() + tlc, hit_timeout = tla_utils.check_model( + 'tla2tools.jar', + module_path, + model_path, + model['mode'], + model['config'], + 60 + ) + end_time = timer() + if hit_timeout: + logging.error(f'{model_path} timed out') + return False + logging.info(f'{model_path} in {end_time - start_time:.1f}s vs. {expected_runtime.seconds}s expected') + actual_result = tlc_result[tlc.returncode] if tlc.returncode in tlc_result else str(tlc.returncode) + if expected_result != actual_result: + logging.error(f'Model {model_path} expected result {expected_result} but got {actual_result}') + logging.error(tlc.stdout.decode('utf-8')) + return False + return True + +logging.basicConfig(level=logging.INFO) + +manifest = tla_utils.load_manifest() + +# Ensure longest-running modules go first +small_models = sorted( + [ + (module['path'], model, parse_timespan(model['runtime'])) + for spec in manifest['specifications'] + for module in spec['modules'] + for model in module['models'] if model['size'] == 'small' + ], + key = lambda m: m[2], + reverse=True +) + +success = all([check_model(*model) for model in small_models]) +exit(0 if success else 1) + diff --git a/.github/scripts/generate_manifest.py b/.github/scripts/generate_manifest.py new file mode 100644 index 00000000..d2b42d60 --- /dev/null +++ b/.github/scripts/generate_manifest.py @@ -0,0 +1,158 @@ +""" +Generates a best-effort manifest.json file. This is done by scanning all +.tla and .cfg files in the specifications dir then attempting to sort them +into a spec/module/model hierarchy. Files are parsed to check for features +and imports. Human-written fields (title/description/source/authors for +specs, runtime/size/result for models) are either taken from any existing +manifest.json file or set as blank/unknown as appropriate. +""" + +from check_manifest_features import get_community_module_imports, get_module_features, get_module_names_in_dir, get_model_features +import json +import os +from os.path import basename, dirname, join, normpath, splitext +from pathlib import PureWindowsPath +import glob +import tla_utils +from tree_sitter import Language, Parser + +def to_posix(path): + """ + Converts paths to normalized Posix format. + https://stackoverflow.com/q/75291812/2852699 + """ + return PureWindowsPath(normpath(path)).as_posix() + +def get_tla_files(dir): + """ + Gets paths of all .tla files in the given directory, except for error + trace specs. + """ + return [ + path for path in glob.glob(f'{dir.path}/**/*.tla', recursive=True) + if '_TTrace_' not in path + ] + +def get_cfg_files(tla_path): + """ + Assume a .cfg file in the same directory as the .tla file and with the + same name is a model of that .tla file; also assume this of any .cfg + files where the .tla file name is only a prefix of the .cfg file name, + unless there are other .tla file names in the directory that exactly + match the .cfg file name. + """ + parent_dir = dirname(tla_path) + module_name, _ = splitext(basename(tla_path)) + other_module_names = [other for other in get_module_names_in_dir(parent_dir) if other != module_name] + return [ + path for path in glob.glob(f'{join(parent_dir, module_name)}*.cfg') + if splitext(basename(path))[0] not in other_module_names + ] + +Language.build_library( + 'build/tree-sitter-languages.so', + ['tree-sitter-tlaplus'] +) + +ignored_dirs = tla_utils.get_ignored_dirs() +ignore = lambda path : tla_utils.ignore(ignored_dirs, path) + +# Generate new base manifest.json from files in specifications dir +new_manifest = { + 'specifications': [ + { + 'path': to_posix(dir.path), + 'title': dir.name, + 'description': '', + 'source': '', + 'authors': [], + 'tags': [], + 'modules': [ + { + 'path': to_posix(tla_path), + 'communityDependencies': sorted(list(get_community_module_imports(tla_path))), + 'tlaLanguageVersion': 2, + 'features': sorted(list(get_module_features(tla_path))), + 'models': [ + { + 'path': to_posix(cfg_path), + 'runtime': 'unknown', + 'size': 'unknown', + 'mode': 'exhaustive search', + 'config': [], + 'features': sorted(list(get_model_features(cfg_path))), + 'result': 'unknown' + } + for cfg_path in sorted(get_cfg_files(tla_path)) + ] + } + for tla_path in sorted(get_tla_files(dir)) + ] + } + for dir in sorted( + os.scandir('specifications'), key=lambda d: d.name + ) if dir.is_dir() and any(get_tla_files(dir)) and not ignore(dir.path) + ] +} + +# Integrate human-written info from existing manifest.json + +def find_corresponding_spec(old_spec, new_manifest): + specs = [ + spec for spec in new_manifest['specifications'] + if to_posix(spec['path']) == old_spec['path'] + ] + return specs[0] if any(specs) else None + +def integrate_spec_info(old_spec, new_spec): + fields = ['title', 'description', 'source', 'tags'] + for field in fields: + new_spec[field] = old_spec[field] + new_spec['authors'] = sorted(old_spec['authors']) + +def find_corresponding_module(old_module, new_spec): + modules = [ + module for module in new_spec['modules'] + if to_posix(module['path']) == to_posix(old_module['path']) + ] + return modules[0] if any(modules) else None + +def integrate_module_info(old_module, new_module): + fields = ['tlaLanguageVersion'] + for field in fields: + new_module[field] = old_module[field] + +def find_corresponding_model(old_model, new_module): + models = [ + model for model in new_module['models'] + if to_posix(model['path']) == to_posix(old_model['path']) + ] + return models[0] if any(models) else None + +def integrate_model_info(old_model, new_model): + fields = ['runtime', 'size', 'mode', 'config', 'result'] + for field in fields: + new_model[field] = old_model[field] + +old_manifest = tla_utils.load_manifest() + +for old_spec in old_manifest['specifications']: + new_spec = find_corresponding_spec(old_spec, new_manifest) + if new_spec is None: + continue + integrate_spec_info(old_spec, new_spec) + for old_module in old_spec['modules']: + new_module = find_corresponding_module(old_module, new_spec) + if new_module is None: + continue + integrate_module_info(old_module, new_module) + for old_model in old_module['models']: + new_model = find_corresponding_model(old_model, new_module) + if new_model is None: + continue + integrate_model_info(old_model, new_model) + +# Write generated manifest to file +with open('manifest.json', 'w', encoding='utf-8') as new_manifest_file: + json.dump(new_manifest, new_manifest_file, indent=2, ensure_ascii=False) + diff --git a/.github/scripts/parse_modules.py b/.github/scripts/parse_modules.py new file mode 100644 index 00000000..7ecb4fa5 --- /dev/null +++ b/.github/scripts/parse_modules.py @@ -0,0 +1,60 @@ +""" +Parse all modules in the manifest with SANY. +""" + +from concurrent.futures import ThreadPoolExecutor +import logging +from os import cpu_count, pathsep +from os.path import dirname, normpath +import subprocess +import tla_utils + +tlaps_modules = normpath('tlapm/library') +community_modules = normpath('CommunityModules/modules') +logging.basicConfig(level=logging.INFO) + +def parse_module(module_tuple): + """ + Parse the given module using SANY. + """ + path, using_proofs = module_tuple + logging.info(path) + # If using proofs, TLAPS modules override community modules + search_paths = pathsep.join( + [dirname(path)] + + ([tlaps_modules] if using_proofs else []) + + [community_modules] + ) + sany = subprocess.run([ + 'java', + f'-DTLA-Library={search_paths}', + '-cp', 'tla2tools.jar', + 'tla2sany.SANY', + '-error-codes', + path + ], capture_output=True) + if sany.returncode != 0: + logging.error(sany.stdout.decode('utf-8')) + return False + return True + +manifest = tla_utils.load_manifest() + +# Skip these specs and modules as they do not currently parse +skip_specs = ['specifications/ewd998'] +skip_modules = [] + +# List of all modules to parse and whether they should use TLAPS imports +modules = [ + (normpath(module['path']), any(['proof' in module['features'] for module in spec['modules']])) + for spec in manifest['specifications'] if spec['path'] not in skip_specs + for module in spec['modules'] if module['path'] not in skip_modules +] + +# Parse specs in parallel +thread_count = cpu_count() +logging.info(f'Parsing using {thread_count} threads') +with ThreadPoolExecutor(thread_count) as executor: + results = executor.map(parse_module, modules) + exit(0 if all(results) else 1) + diff --git a/.github/scripts/requirements.txt b/.github/scripts/requirements.txt new file mode 100644 index 00000000..7dbb4656 --- /dev/null +++ b/.github/scripts/requirements.txt @@ -0,0 +1,3 @@ +jsonschema == 4.17.3 +tree-sitter==0.20.1 + diff --git a/.github/scripts/smoke_test_large_models.py b/.github/scripts/smoke_test_large_models.py new file mode 100644 index 00000000..5c51bcd0 --- /dev/null +++ b/.github/scripts/smoke_test_large_models.py @@ -0,0 +1,53 @@ +""" +Smoke-test all models not marked as size "small" in the manifest. This +entails running them for five seconds to ensure they can actually start +and work with the spec they're supposed to be modeling. +""" + +import logging +import os +import tla_utils + +def check_model(module_path, model): + model_path = model['path'] + logging.info(model_path) + tlc, hit_timeout = tla_utils.check_model( + 'tla2tools.jar', + module_path, + model_path, + model['mode'], + model['config'], + 5 + ) + if hit_timeout: + return True + if 0 != tlc.returncode: + logging.error(f'Model {model_path} expected error code 0 but got {tlc.returncode}') + logging.error(tlc.stdout.decode('utf-8')) + return False + return True + +logging.basicConfig(level=logging.INFO) + +manifest = tla_utils.load_manifest() + +skip_models = [ + # SimKnuthYao requires certain number of states to have been generated + # before termination or else it fails. This makes it not amenable to + # smoke testing. + 'specifications/KnuthYao/SimKnuthYao.cfg', + # SimTokenRing does not work on Windows systems. +] + (['specifications/ewd426/SimTokenRing.cfg'] if os.name == 'nt' else []) + +large_models = [ + (module['path'], model) + for spec in manifest['specifications'] + for module in spec['modules'] + for model in module['models'] + if model['size'] != 'small' + and model['path'] not in skip_models +] + +success = all([check_model(*model) for model in large_models]) +exit(0 if success else 1) + diff --git a/.github/scripts/tla_utils.py b/.github/scripts/tla_utils.py new file mode 100644 index 00000000..807ad77e --- /dev/null +++ b/.github/scripts/tla_utils.py @@ -0,0 +1,71 @@ +import json +from os.path import normpath +import subprocess + +def ignore(ignored_dirs, path): + return any([normpath(path).startswith(ignore_dir) for ignore_dir in ignored_dirs]) + +def is_blank(text): + all([c.isspace() for c in text]) + +def get_ignored_dirs(): + with open('.ciignore', 'r') as ignore_file: + return set([ + normpath(line.strip()) + for line in ignore_file.readlines() + if not line.startswith('#') and not is_blank(line) + ]) + +def load_json(path): + with open(normpath(path), 'r', encoding='utf-8') as file: + return json.load(file) + +def load_manifest(): + return load_json('manifest.json') + +def load_schema(): + return load_json('manifest-schema.json') + +def get_run_mode(mode): + if type(mode) is dict: + if 'simulate' in mode: + trace_count = mode['simulate']['traceCount'] + return ['-simulate', f'num={trace_count}'] + else: + raise NotImplementedError(f'Undefined model-check mode {mode}') + elif 'generate' == mode: + return ['-generate'] + elif 'exhaustive search' == mode: + return [] + else: + raise NotImplementedError(f'Undefined model-check mode {mode}') + +def get_config(config): + return ['-deadlock'] if 'ignore deadlock' in config else [] + +def check_model(jar_path, module_path, model_path, mode, config, timeout): + jar_path = normpath(jar_path) + module_path = normpath(module_path) + model_path = normpath(model_path) + try: + tlc = subprocess.run( + [ + 'java', + '-Dtlc2.TLC.ide=Github', + '-Dutil.ExecutionStatisticsCollector.id=abcdef60f238424fa70d124d0c77ffff', + '-XX:+UseParallelGC', + '-cp', jar_path, + 'tlc2.TLC', + module_path, + '-config', model_path, + '-workers', 'auto', + '-lncheck', 'final', + '-cleanup' + ] + get_config(config) + get_run_mode(mode), + capture_output=True, + timeout=timeout + ) + return (tlc, False) + except subprocess.TimeoutExpired: + return (None, True) + diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml new file mode 100644 index 00000000..2a5862be --- /dev/null +++ b/.github/workflows/CI.yml @@ -0,0 +1,91 @@ +name: Check Specs & Metadata +on: + push: + branches: + - master + pull_request: + branches: + - master + +jobs: + validate: + name: Validate Manifest, Specs, & Models + runs-on: ${{ matrix.os }} + strategy: + matrix: + include: + - { os: windows-latest, shell: msys2 } + - { os: ubuntu-latest, shell: bash } + - { os: macos-latest, shell: bash } + fail-fast: false + env: + SCRIPT_DIR: .github/scripts + TLAPS_VERSION: 202210041448 + defaults: + run: + shell: ${{ matrix.shell }} {0} + steps: + - name: Clone repo + uses: actions/checkout@v2 + - name: Install python + uses: actions/setup-python@v4 + with: + python-version: '3.11' + - name: Install Java + uses: actions/setup-java@v3 + with: + distribution: adopt + java-version: 17 + - name: Install MSYS2 on Windows + uses: msys2/setup-msys2@v2 + if: matrix.os == 'windows-latest' + - name: Install python packages + shell: bash + run: pip install -r $SCRIPT_DIR/requirements.txt + - name: Download TLA⁺ dependencies + run: | + # Fix tar symbolic link issues on Windows; see: + # https://github.com/msys2/MSYS2-packages/issues/1216 + export MSYS=winsymlinks:lnk + # Get tree-sitter-tlaplus + wget https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/main.tar.gz + tar -xf main.tar.gz + rm main.tar.gz + mv tree-sitter-tlaplus-main tree-sitter-tlaplus + # Get TLA⁺ tools + wget http://nightly.tlapl.us/dist/tla2tools.jar + # Get TLA⁺ community modules + wget https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar + wget https://github.com/tlaplus/CommunityModules/archive/master.tar.gz + tar -xf master.tar.gz + rm master.tar.gz + mv CommunityModules-master CommunityModules + # Get TLAPS + wget https://github.com/tlaplus/tlapm/archive/refs/tags/$TLAPS_VERSION.tar.gz + tar -xf $TLAPS_VERSION.tar.gz + rm $TLAPS_VERSION.tar.gz + mv tlapm-$TLAPS_VERSION tlapm + - name: Check manifest.json format + shell: bash + run: python $SCRIPT_DIR/check_manifest_schema.py + - name: Check manifest files + shell: bash + run: python $SCRIPT_DIR/check_manifest_files.py + - name: Check manifest feature flags + shell: bash + run: python $SCRIPT_DIR/check_manifest_features.py + - name: Parse all modules + shell: bash + run: python $SCRIPT_DIR/parse_modules.py + - name: Check small models + shell: bash + run: python $SCRIPT_DIR/check_small_models.py + - name: Smoke-test large models + shell: bash + run: python $SCRIPT_DIR/smoke_test_large_models.py + - name: Smoke-test manifest generation script + shell: bash + run: | + python $SCRIPT_DIR/generate_manifest.py + git diff -a + diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml deleted file mode 100644 index 171a9e70..00000000 --- a/.github/workflows/main.yml +++ /dev/null @@ -1,15 +0,0 @@ -name: CI - -on: [push, workflow_dispatch, workflow_call] - -jobs: - build: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v1 - - name: Get (nightly) TLC - run: wget https://nightly.tlapl.us/dist/tla2tools.jar - - name: Get (nightly) CommunityModules - run: wget https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar - - name: Run - run: /bin/bash .github/workflows/run.sh diff --git a/.github/workflows/run.sh b/.github/workflows/run.sh deleted file mode 100755 index 5c0145d1..00000000 --- a/.github/workflows/run.sh +++ /dev/null @@ -1,109 +0,0 @@ -#!/bin/bash - -TLC_COMMAND="java -Dtlc2.TLC.stopAfter=180 -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=abcdef60f238424fa70d124d0c77ffff -cp tla2tools.jar tlc2.TLC -workers auto -lncheck final -tool -deadlock" - -echo Check EWD840 -$TLC_COMMAND specifications/ewd840/EWD840 -echo Check CarTalkPuzzle Model_1 -$TLC_COMMAND specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_1/MC -echo Check CarTalkPuzzle Model_2 -$TLC_COMMAND specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_2/MC -echo Check MCDieHarder -$TLC_COMMAND specifications/DieHard/MCDieHarder || (($? == 12)) ## Expect a safety violation -echo Check DieHard -$TLC_COMMAND specifications/DieHard/DieHard || (($? == 12)) ## Expect a safety violation -echo Check DiningPhilosophers -$TLC_COMMAND specifications/DiningPhilosophers/DiningPhilosophers -echo Check TransitiveClosure -$TLC_COMMAND specifications/TransitiveClosure/TransitiveClosure -echo Check Hanoi -java -Dtlc2.TLC.stopAfter=600 -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=abcdef60f238424fa70d124d0c77ffff -cp tla2tools.jar:specifications/tower_of_hanoi/Hanoi.toolbox/Model_1/MC tlc2.TLC -workers auto -lncheck final -tool -deadlock specifications/tower_of_hanoi/Hanoi.toolbox/Model_1/MC -echo Check MCEcho -$TLC_COMMAND specifications/echo/MCEcho -echo Check Prisoners -$TLC_COMMAND specifications/Prisoners/Prisoners -echo Check LSpec-model -$TLC_COMMAND specifications/dijkstra-mutex/DijkstraMutex.toolbox/LSpec-model/MC -echo Check Safety-4-processors -$TLC_COMMAND specifications/dijkstra-mutex/DijkstraMutex.toolbox/Safety-4-processors/MC -## This spec used to be accepted by Apalache, but since Apalache has started to require type annotations for all variables. -## https://github.com/tlaplus/Examples/pull/31#issuecomment-796354291 -#echo Check EinsteinRiddle -#$TLC_COMMAND specifications/EinsteinRiddle/Einstein -echo Check MCInnerSequential -$TLC_COMMAND specifications/SpecifyingSystems/AdvancedExamples/MCInnerSequential -#echo Check MCInnerSerial -#$TLC_COMMAND specifications/SpecifyingSystems/AdvancedExamples/MCInnerSerial -echo Check MCLiveWriteThroughCache -$TLC_COMMAND specifications/SpecifyingSystems/Liveness/MCLiveWriteThroughCache -echo Check LiveHourClock -$TLC_COMMAND specifications/SpecifyingSystems/Liveness/LiveHourClock -echo Check MCLiveInternalMemory -$TLC_COMMAND specifications/SpecifyingSystems/Liveness/MCLiveInternalMemory -echo Check SimpleMath -$TLC_COMMAND specifications/SpecifyingSystems/SimpleMath/SimpleMath -echo Check HourClock2 -$TLC_COMMAND specifications/SpecifyingSystems/HourClock/HourClock2 -echo Check HourClock -$TLC_COMMAND specifications/SpecifyingSystems/HourClock/HourClock -echo Check MCInternalMemory -$TLC_COMMAND specifications/SpecifyingSystems/CachingMemory/MCInternalMemory -echo Check MCWriteThroughCache -$TLC_COMMAND specifications/SpecifyingSystems/CachingMemory/MCWriteThroughCache -echo Check PrintValues -$TLC_COMMAND specifications/SpecifyingSystems/AsynchronousInterface/PrintValues -echo Check AsynchInterface -$TLC_COMMAND specifications/SpecifyingSystems/AsynchronousInterface/AsynchInterface -echo Check Channel -$TLC_COMMAND specifications/SpecifyingSystems/AsynchronousInterface/Channel -echo Check MCAlternatingBit -$TLC_COMMAND specifications/SpecifyingSystems/TLC/MCAlternatingBit -echo Check ABCorrectness -$TLC_COMMAND specifications/SpecifyingSystems/TLC/ABCorrectness -echo Check MCRealTimeHourClock -$TLC_COMMAND specifications/SpecifyingSystems/RealTime/MCRealTimeHourClock || (($? != 1)) ## Stuttering -echo Check MCInnerFIFO -$TLC_COMMAND specifications/SpecifyingSystems/FIFO/MCInnerFIFO -echo Check EWD840_anim -$TLC_COMMAND -simulate num=1 specifications/ewd840/EWD840_anim || (($? == 12)) ## Expect a safety violation -echo Check SyncTerminationDetection -$TLC_COMMAND specifications/ewd840/SyncTerminationDetection -echo Check EWD840 -$TLC_COMMAND specifications/ewd840/EWD840 -echo Check EWD840_json -sed -i '/^SendMsg/{n;d;}' specifications/ewd840/EWD840.tla ## Cause RealInv to be violated (see EWD840_json.tla) -$TLC_COMMAND specifications/ewd840/EWD840_json -echo Check MCVoting -$TLC_COMMAND specifications/Paxos/MCVoting -echo Check MCConsensus -$TLC_COMMAND specifications/Paxos/MCConsensus -echo Check MCPaxos -$TLC_COMMAND specifications/Paxos/MCPaxos -echo Check EWD998ChanID -$TLC_COMMAND specifications/ewd998/EWD998ChanID -echo Check EWD998Chan -$TLC_COMMAND specifications/ewd998/EWD998Chan -echo Check EWD998 -$TLC_COMMAND specifications/ewd998/EWD998 -echo Check TestGraphs -$TLC_COMMAND specifications/TLC/TestGraphs -echo Check SchedulingAllocator -$TLC_COMMAND specifications/allocator/SchedulingAllocator -echo Check AllocatorRefinement -$TLC_COMMAND specifications/allocator/AllocatorRefinement -echo Check SimpleAllocator -$TLC_COMMAND specifications/allocator/SimpleAllocator -echo Check AllocatorImplementation -$TLC_COMMAND specifications/allocator/AllocatorImplementation -echo Check FourQueens -$TLC_COMMAND specifications/N-Queens/Queens.toolbox/FourQueens/MC -echo Check FourQueens PlusCal -$TLC_COMMAND specifications/N-Queens/QueensPluscal.toolbox/FourQueens/MC -echo Check ReadersWriters -$TLC_COMMAND specifications/ReadersWriters/MC -echo Check EWD687a -$TLC_COMMAND specifications/ewd687a/MCEWD687a -echo Simulate EWD687a_anim -$TLC_COMMAND -simulate num=100 -note specifications/ewd687a/EWD687a_anim || (($? == 12)) ## Expect a safety violation -echo Check Huang -$TLC_COMMAND specifications/Huang/Huang diff --git a/.gitignore b/.gitignore index 2d16dd19..fdef1f7f 100644 --- a/.gitignore +++ b/.gitignore @@ -1,31 +1,47 @@ -## Blacklist all files +## Ignore all files by default * -## Whitelist TLA+ files +## Don't ignore TLA+ files !*.tla -## Whitelist TLC model config and results +## Don't ignore TLC model config and results !*.cfg !*.out ## Usually .out files are small -## Whitelist Toolbox model metadata +## Don't ignore Toolbox model metadata !*.launch -## Whitelist Toolbox spec metadata +## Don't ignore Toolbox spec metadata !.project !*.prefs -## Whitelist PDFs +## Don't ignore PDFs !*.pdf -## Whitelist all folders +## Don't ignore all folders !*/ -## Blacklist TLAPS cache folder +## 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 pycache +__pycache__ + +## Ignore directories used for local CI testing +CommunityModules/ +tlapm/ +tree-sitter-tlaplus/ + +# Ignore TTrace specs +*_TTrace_*.tla + ## Blacklist tools/ folder created by .devcontainer.json tools/ - diff --git a/README.md b/README.md index e971fba6..dec2fea2 100644 --- a/README.md +++ b/README.md @@ -1,16 +1,71 @@ -## Welcome to TLA+ Examples [![Gitpod ready-to-code](https://img.shields.io/badge/Gitpod-ready--to--spec-908a85?logo=gitpod)](https://gitpod.io/#https://github.com/tlaplus/examples/) +# TLA+ Examples +[![Gitpod ready-to-code](https://img.shields.io/badge/Gitpod-ready--to--spec-908a85?logo=gitpod)](https://gitpod.io/#https://github.com/tlaplus/examples/) +[![Validate Specs & Models](https://github.com/tlaplus/Examples/actions/workflows/CI.yml/badge.svg)](https://github.com/tlaplus/Examples/actions/workflows/CI.yml) -The page **TLA+ Examples** is a library of TLA+ specifications for distributed algorithms. The webpage supplies the TLA+ community with: +This is a repository of TLA+ specifications and models covering applications in a variety of fields. +It serves as: +- a comprehensive example library demonstrating how to specify an algorithm in TLA+ +- a diverse corpus facilitating development & testing of TLA+ language tools +- a collection of case studies in the application of formal specification in TLA+ -- A comprehensive library of the TLA+ specifications that are available today, in order to provide an overview of how to specify an algorithm in TLA+. -- A comprehensive list of references and other interesting information for each problem. +All TLA+ specs can be found in the `specifications` directory. +A central manifest of specs with descriptions and accounts of their various models and features can be found in the [`manifest.json`](manifest.json) file. -Do you have your own case study that you like to share with the community? Send a pointer to us and we will include it in the repository. Your specifications will help the community in improving the tools for TLA+ analysis. +## Contributing + +Do you have your own case study or TLA+ specification you'd like to share with the community? +Follow these instructions: +1. Ensure your spec is released under MIT or a similarly-permissive license +1. Fork this repository and create a new directory under `specifications` with the name of your spec +1. Place all TLA+ files in the directory, along with their `.cfg` model files; you are encouraged to include at least one model that completes execution in less than 10 seconds +1. Ensure name of each `.cfg` file matches the `.tla` file it models, or has its name as a prefix; for example `SpecName.tla` can have the models `SpecName.cfg` and `SpecNameLiveness.cfg`, etc. +1. Consider including a `README.md` in the spec directory explaining the significance of the spec with links to any relevant websites or publications, or integrate this info as comments in the spec itself +1. Add an entry to the below table in this top-level `README.md` summarizing your spec and its attributes + +## Adding Spec to Continuous Integration + +To combat bitrot, it is important to add your spec and model to the continuous integration system. +To do this, you'll have to update the `manifest.json` file with machine-readable records of your spec files. +If this process doesn't work for you, you can alternatively modify the [`.ciignore`](.ciignore) file to exclude your spec from validation. +Otherwise, follow these directions: + +1. Ensure you have Python 3.X installed +1. Download & extract tree-sitter-tlaplus ([zip](https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/refs/heads/main.zip), [tar.gz](https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/refs/heads/main.tar.gz)) to the root of the repository; ensure the extracted folder is named `tree-sitter-tlaplus` +1. Open a shell and navigate to the repo root; ensure a C++ compiler is installed and on your path + - On Windows, this might entail running the below script from the visual studio developer command prompt +1. Run `pip install -r .github/scripts/requirements.txt` +1. Run `python .github/scripts/generate_manifest.py` +1. Locate your spec's entry in the `manifest.json` file and ensure the following fields are filled out: + - Spec title: an appropriate title for your specification + - Spec description: a short description of your specification + - Spec source: if this spec was first published elsewhere, provide a link to this location + - Spec authors: a list of people who authored the spec + - Spec tags: + - `"beginner"` if your spec is appropriate for TLA+ newcomers + - Model runtime: approximate model runtime on an ordinary workstation, in `"HH:MM:SS"` format + - Model size: + - `"small"` if the model can be executed in less than 10 seconds + - `"medium"` if the model can be executed in less than five minutes + - `"large"` if the model takes more than five minutes to execute + - Model mode: + - `"exhaustive search"` by default + - `{"simulate": {"traceCount": N}}` for a simulation model + - `"generate"` for model trace generation + - Model config: + - `"ignore deadlock"` if your model should ignore deadlock + - Model result: + - `"success"` if the model completes successfully + - `"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 + - 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` file) + +Before submitted your changes to run in the CI, you can quickly check your `manifest.json` for errors and also check it against [`manifest-schema.json`](manifest-schema.json) at https://www.jsonschemavalidator.net/. ## List of Examples -| No | Name | Short description | Spec's authors | TLAPS Proof | TLC Check | Used modules | PlusCal | Apalache | -| :-: | --------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------ | :---------: | :-----------------------------------------------------------------------------------------------------------: | --------------------------------------------------------------------- | -------- | -------- | +| # | Name | Description | Authors | TLAPS Proof? | TLC Model? | Module Dependencies | PlusCal? | Apalache? | +|:-:|------|-------------|---------|:------------:|:----------:|---------------------|:--------:|:---------:| | 1 | 2PCwithBTM | A modified version of P2TCommit (Gray & Lamport, 2006) | Murat Demirbas | | ✔ | FinSet, Int, Seq | ✔ | | | 2 | 802.16 | IEEE 802.16 WiMAX Protocols | Prasad Narayana, Ruiming Chen, Yao Zhao, Yan Chen, Zhi (Judy) Fu, and Hai Zhou | | ✔ | Int, Seq, FinSet | | | | 3 | aba-asyn-byz | Asynchronous Byzantine agreement (Bracha & Toueg, 1985) | Thanh Hai Tran, Igor Konnov, Josef Widder | | ✔ | Nat | | | @@ -117,4 +172,6 @@ The repository is under the MIT license. However, we can upload your benchmarks ## Support or Contact -Do you have any questions or comments? Please open an issue or send an email to the [TLA+ group](https://groups.google.com/g/tlaplus). +Do you have any questions or comments? +Please open an issue or send an email to the [TLA+ group](https://groups.google.com/g/tlaplus). + diff --git a/manifest-schema.json b/manifest-schema.json new file mode 100644 index 00000000..f0906991 --- /dev/null +++ b/manifest-schema.json @@ -0,0 +1,97 @@ +{ + "type" : "object", + "required": ["specifications"], + "additionalProperties": false, + "properties" : { + "specifications" : { + "type": "array", + "items": { + "type": "object", + "required": ["title", "description", "source", "authors", "path", "tags", "modules"], + "additionalProperties": false, + "properties": { + "path": {"type": "string"}, + "title": {"type": "string"}, + "description": {"type": "string"}, + "source": {"type": "string"}, + "authors": { + "type": "array", + "items": {"type": "string"} + }, + "tags": { + "type": "array", + "items": {"enum": ["beginner"]} + }, + "modules": { + "type": "array", + "items": { + "type": "object", + "required": ["path", "communityDependencies", "tlaLanguageVersion", "features", "models"], + "additionalProperties": false, + "properties": { + "path": {"type": "string"}, + "communityDependencies": { + "type": "array", + "items": {"type": "string"} + }, + "tlaLanguageVersion": {"type": "number"}, + "features": { + "type": "array", + "items": {"enum": ["pluscal", "proof"]} + }, + "models": { + "type": "array", + "items": { + "type": "object", + "additionalProperties": false, + "required": ["path", "runtime", "size", "mode", "config", "features", "result"], + "properties": { + "path": {"type": "string"}, + "runtime": { + "type": "string", + "pattern": "^(([0-9][0-9]:[0-9][0-9]:[0-9][0-9])|unknown)$" + }, + "size": {"enum": ["small", "medium", "large", "unknown"]}, + "mode": { + "oneOf": [ + { + "enum": ["exhaustive search", "generate"] + }, + { + "type": "object", + "additionalProperties": false, + "required": ["simulate"], + "properties": { + "simulate": { + "type": "object", + "additionalProperties": false, + "required": ["traceCount"], + "properties": { + "traceCount": {"type": "number"} + } + } + } + } + ] + }, + "config": { + "type": "array", + "items": {"enum": ["ignore deadlock"]} + }, + "features": { + "type": "array", + "items": {"enum": ["liveness", "symmetry", "view", "alias", "state constraint"]} + }, + "result": {"enum": ["success", "safety failure", "liveness failure", "deadlock failure", "unknown"]} + } + } + } + } + } + } + } + } + } + } +} + diff --git a/manifest.json b/manifest.json new file mode 100644 index 00000000..f5550968 --- /dev/null +++ b/manifest.json @@ -0,0 +1,3442 @@ +{ + "specifications": [ + { + "path": "specifications/Bakery-Boulangerie", + "title": "The Boulangerie Algorithm", + "description": "Spec of a variant of the Bakery Algorithm", + "source": "", + "authors": [ + "Leslie Lamport", + "Stephan Merz" + ], + "tags": [], + "modules": [ + { + "path": "specifications/Bakery-Boulangerie/Bakery.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal", + "proof" + ], + "models": [] + }, + { + "path": "specifications/Bakery-Boulangerie/Boulanger.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal", + "proof" + ], + "models": [] + } + ] + }, + { + "path": "specifications/CarTalkPuzzle", + "title": "The Car Talk Puzzle", + "description": "Math puzzle involving a farmer, a stone, and a balance scale", + "source": "", + "authors": [ + "Leslie Lamport" + ], + "tags": [ + "beginner" + ], + "modules": [ + { + "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_1/CarTalkPuzzle.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_1/MC.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_1/MC.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "success" + } + ] + }, + { + "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_2/CarTalkPuzzle.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_2/MC.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_2/MC.cfg", + "runtime": "00:00:05", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "success" + } + ] + }, + { + "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_3/CarTalkPuzzle.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_3/MC.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_3/MC.cfg", + "runtime": "unknown", + "size": "large", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "unknown" + } + ] + } + ] + }, + { + "path": "specifications/Chameneos", + "title": "Chameneos, a Concurrency Game", + "description": "A concurrency game requiring concurrent & symmetric cooperation", + "source": "https://github.com/mryndzionek/tlaplus_specs#chameneostla", + "authors": [ + "Mariusz Ryndzionek" + ], + "tags": [], + "modules": [ + { + "path": "specifications/Chameneos/Chameneos.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/CigaretteSmokers", + "title": "The Cigarette Smokers Problem", + "description": "A concurrency problem described in 1971 by Suhas Patil", + "source": "https://github.com/mryndzionek/tlaplus_specs#cigarettesmokerstla", + "authors": [ + "Mariusz Ryndzionek" + ], + "tags": [], + "modules": [ + { + "path": "specifications/CigaretteSmokers/CigaretteSmokers.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/CoffeeCan", + "title": "The Coffee Can Black/White Bean Problem", + "description": "Math problem published by Dijkstra attributed to Carel Scholten", + "source": "https://stackoverflow.com/a/66304920/2852699", + "authors": [ + "Andrew Helwer" + ], + "tags": [ + "beginner" + ], + "modules": [ + { + "path": "specifications/CoffeeCan/CoffeeCan.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/CoffeeCan/CoffeeCan1000Beans.cfg", + "runtime": "00:00:15", + "size": "medium", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + }, + { + "path": "specifications/CoffeeCan/CoffeeCan100Beans.cfg", + "runtime": "00:00:05", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + }, + { + "path": "specifications/CoffeeCan/CoffeeCan3000Beans.cfg", + "runtime": "00:02:30", + "size": "medium", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + } + ] + } + ] + }, + { + "path": "specifications/DieHard", + "title": "The Die Hard Problem", + "description": "Obtain 4 gallons of water using only 3 and 5 gallon jugs", + "source": "", + "authors": [ + "Leslie Lamport" + ], + "tags": [ + "beginner" + ], + "modules": [ + { + "path": "specifications/DieHard/DieHard.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/DieHard/DieHard.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "safety failure" + } + ] + }, + { + "path": "specifications/DieHard/DieHarder.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/DieHard/MCDieHarder.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/DieHard/MCDieHarder.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "safety failure" + } + ] + } + ] + }, + { + "path": "specifications/DiningPhilosophers", + "title": "The Dining Philosophers Problem", + "description": "The Chandy-Misra solution to the Dining Philosophers concurrency problem", + "source": "", + "authors": [ + "Jeff Hemphill" + ], + "tags": [ + "beginner" + ], + "modules": [ + { + "path": "specifications/DiningPhilosophers/DiningPhilosophers.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal" + ], + "models": [ + { + "path": "specifications/DiningPhilosophers/DiningPhilosophers.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + } + ] + } + ] + }, + { + "path": "specifications/EinsteinRiddle", + "title": "Einstein's Riddle", + "description": "Five houses, five people, various facts, who lives in what house?", + "source": "", + "authors": [ + "Isaac DeFrain" + ], + "tags": [], + "modules": [ + { + "path": "specifications/EinsteinRiddle/Einstein.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/EinsteinRiddle/Einstein.cfg", + "runtime": "unknown", + "size": "large", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "safety failure" + } + ] + } + ] + }, + { + "path": "specifications/GameOfLife", + "title": "Conway's Game of Life", + "description": "The famous cellular automata simulation", + "source": "https://github.com/mryndzionek/tlaplus_specs#gameoflifetla", + "authors": [ + "Mariusz Ryndzionek" + ], + "tags": [], + "modules": [ + { + "path": "specifications/GameOfLife/GameOfLife.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/Huang", + "title": "Huang's Algorithm", + "description": "An algorithm for detecting termination in a distributed system", + "source": "", + "authors": [ + "Markus Kuppe" + ], + "tags": [], + "modules": [ + { + "path": "specifications/Huang/Huang.tla", + "communityDependencies": [ + "DyadicRationals", + "Functions", + "SequencesExt" + ], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/Huang/Huang.cfg", + "runtime": "00:00:40", + "size": "medium", + "mode": "exhaustive search", + "config": [ + "ignore deadlock" + ], + "features": [ + "alias", + "liveness", + "state constraint" + ], + "result": "success" + } + ] + } + ] + }, + { + "path": "specifications/KeyValueStore", + "title": "Key-Value Store with Snapshot Isolation", + "description": "A simple KVS implementing snapshot isolation", + "source": "", + "authors": [ + "Andrew Helwer" + ], + "tags": [], + "modules": [ + { + "path": "specifications/KeyValueStore/KeyValueStore.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/KeyValueStore/MCKVS.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/KeyValueStore/MCKVSSafetyLarge.cfg", + "runtime": "07:16:00", + "size": "large", + "mode": "exhaustive search", + "config": [], + "features": [ + "symmetry" + ], + "result": "success" + }, + { + "path": "specifications/KeyValueStore/MCKVSSafetyMedium.cfg", + "runtime": "00:04:30", + "size": "medium", + "mode": "exhaustive search", + "config": [], + "features": [ + "symmetry" + ], + "result": "success" + }, + { + "path": "specifications/KeyValueStore/MCKVSSafetySmall.cfg", + "runtime": "00:00:40", + "size": "medium", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "success" + } + ] + } + ] + }, + { + "path": "specifications/KnuthYao", + "title": "The Knuth-Yao Method", + "description": "A method for simulating a fair 6-sided die using only coin flips", + "source": "https://old.reddit.com/r/tlaplus/comments/j06ohw/how_do_you_reason_about_a_probabilistic/g6owlxy/", + "authors": [ + "Markus Kuppe", + "Ron Pressler" + ], + "tags": [], + "modules": [ + { + "path": "specifications/KnuthYao/KnuthYao.tla", + "communityDependencies": [ + "DyadicRationals" + ], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/KnuthYao/Prob.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/KnuthYao/SimKnuthYao.tla", + "communityDependencies": [ + "CSV", + "Functions", + "IOUtils", + "Statistics" + ], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/KnuthYao/SimKnuthYao.cfg", + "runtime": "unknown", + "size": "unknown", + "mode": "generate", + "config": [], + "features": [ + "state constraint" + ], + "result": "unknown" + } + ] + } + ] + }, + { + "path": "specifications/LevelChecking", + "title": "TLA⁺ Level Checking", + "description": "Level-checking of TLA⁺ formulas as described in Specifying Systems", + "source": "https://github.com/tlaplus/tlaplus/blob/6bc82f7746ccdfbdf49cdef24448666d11e5e218/tlatools/org.lamport.tlatools/src/tla2sany/semantic/LevelNode.java#L354-L2778", + "authors": [ + "Leslie Lamport" + ], + "tags": [], + "modules": [ + { + "path": "specifications/LevelChecking/LevelSpec.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/LoopInvariance", + "title": "Loop Invariance", + "description": "Examples of finding and proving loop invariants in PlusCal", + "source": "http://lamport.azurewebsites.net/tla/proving-safety.pdf", + "authors": [ + "Leslie Lamport" + ], + "tags": [], + "modules": [ + { + "path": "specifications/LoopInvariance/BinarySearch.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal", + "proof" + ], + "models": [] + }, + { + "path": "specifications/LoopInvariance/Quicksort.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal", + "proof" + ], + "models": [] + }, + { + "path": "specifications/LoopInvariance/SumSequence.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal", + "proof" + ], + "models": [] + } + ] + }, + { + "path": "specifications/MisraReachability", + "title": "Misra Reachability Algorithm", + "description": "A sequential algorithm for computing the set of reachable nodes in a directed graph", + "source": "", + "authors": [ + "Leslie Lamport" + ], + "tags": [], + "modules": [ + { + "path": "specifications/MisraReachability/ParReach.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal" + ], + "models": [] + }, + { + "path": "specifications/MisraReachability/ParReachProofs.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "proof" + ], + "models": [] + }, + { + "path": "specifications/MisraReachability/Reachability.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/MisraReachability/ReachabilityProofs.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "proof" + ], + "models": [] + }, + { + "path": "specifications/MisraReachability/ReachabilityTest.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/MisraReachability/Reachable.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal" + ], + "models": [] + }, + { + "path": "specifications/MisraReachability/ReachableProofs.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "proof" + ], + "models": [] + } + ] + }, + { + "path": "specifications/MissionariesAndCannibals", + "title": "Missionaries and Cannibals", + "description": "Spec of a river-crossing puzzle", + "source": "", + "authors": [ + "Leslie Lamport" + ], + "tags": [ + "beginner" + ], + "modules": [ + { + "path": "specifications/MissionariesAndCannibals/MissionariesAndCannibals.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/MissionariesAndCannibals/MissionariesAndCannibals.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "safety failure" + } + ] + } + ] + }, + { + "path": "specifications/MultiCarElevator", + "title": "Multi-Car Elevator System", + "description": "A simple multi-car elevator system servicing a multi-floor building", + "source": "https://groups.google.com/g/tlaplus/c/5Xd8kv288jE/m/IrliJIatBwAJ", + "authors": [ + "Andrew Helwer" + ], + "tags": [], + "modules": [ + { + "path": "specifications/MultiCarElevator/Elevator.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/MultiCarElevator/ElevatorLivenessLarge.cfg", + "runtime": "00:11:00", + "size": "large", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + }, + { + "path": "specifications/MultiCarElevator/ElevatorLivenessMedium.cfg", + "runtime": "00:00:30", + "size": "medium", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + }, + { + "path": "specifications/MultiCarElevator/ElevatorSafetyLarge.cfg", + "runtime": "00:10:00", + "size": "large", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "success" + }, + { + "path": "specifications/MultiCarElevator/ElevatorSafetyMedium.cfg", + "runtime": "00:03:00", + "size": "medium", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "success" + }, + { + "path": "specifications/MultiCarElevator/ElevatorSafetySmall.cfg", + "runtime": "00:00:15", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "success" + } + ] + } + ] + }, + { + "path": "specifications/N-Queens", + "title": "The N-Queens Puzzle", + "description": "Place N queens on an NxN chess board such that no two queens threaten each other", + "source": "", + "authors": [ + "Stephan Merz" + ], + "tags": [ + "beginner" + ], + "modules": [ + { + "path": "specifications/N-Queens/Queens.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/N-Queens/Queens.toolbox/FourQueens/MC.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/N-Queens/Queens.toolbox/FourQueens/MC.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [ + "ignore deadlock" + ], + "features": [], + "result": "safety failure" + } + ] + }, + { + "path": "specifications/N-Queens/Queens.toolbox/FourQueens/Queens.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/N-Queens/QueensPluscal.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal" + ], + "models": [] + }, + { + "path": "specifications/N-Queens/QueensPluscal.toolbox/FourQueens/MC.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/N-Queens/QueensPluscal.toolbox/FourQueens/MC.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "safety failure" + } + ] + }, + { + "path": "specifications/N-Queens/QueensPluscal.toolbox/FourQueens/QueensPluscal.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal" + ], + "models": [] + } + ] + }, + { + "path": "specifications/NanoBlockchain", + "title": "The Nano Blockchain Protocol", + "description": "A specification of the protocol originally used by the Nano blockchain", + "source": "", + "authors": [ + "Andrew Helwer" + ], + "tags": [], + "modules": [ + { + "path": "specifications/NanoBlockchain/MCNano.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/NanoBlockchain/MCNanoLarge.cfg", + "runtime": "00:20:00", + "size": "large", + "mode": "exhaustive search", + "config": [], + "features": [ + "view" + ], + "result": "success" + }, + { + "path": "specifications/NanoBlockchain/MCNanoMedium.cfg", + "runtime": "00:00:30", + "size": "medium", + "mode": "exhaustive search", + "config": [], + "features": [ + "view" + ], + "result": "success" + }, + { + "path": "specifications/NanoBlockchain/MCNanoSmall.cfg", + "runtime": "00:00:05", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "view" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/NanoBlockchain/Nano.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/Paxos", + "title": "The Paxos Protocol", + "description": "A protocol for error-tolerant consensus", + "source": "", + "authors": [ + "Leslie Lamport" + ], + "tags": [], + "modules": [ + { + "path": "specifications/Paxos/Consensus.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "proof" + ], + "models": [] + }, + { + "path": "specifications/Paxos/MCConsensus.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/Paxos/MCConsensus.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [ + "ignore deadlock" + ], + "features": [], + "result": "success" + } + ] + }, + { + "path": "specifications/Paxos/MCPaxos.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/Paxos/MCPaxos.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness", + "symmetry" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/Paxos/MCVoting.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/Paxos/MCVoting.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [ + "ignore deadlock" + ], + "features": [ + "liveness", + "symmetry" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/Paxos/Paxos.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/Paxos/Voting.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "proof" + ], + "models": [] + } + ] + }, + { + "path": "specifications/PaxosHowToWinATuringAward", + "title": "How to Win a Turing Award", + "description": "Exercises from the lecture The Paxos Algorithm - or How to Win a Turing Award", + "source": "https://www.youtube.com/watch?v=tw3gsBms-f8", + "authors": [ + "Leslie Lamport" + ], + "tags": [], + "modules": [ + { + "path": "specifications/PaxosHowToWinATuringAward/Consensus.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "proof" + ], + "models": [] + }, + { + "path": "specifications/PaxosHowToWinATuringAward/Paxos.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/PaxosHowToWinATuringAward/Voting.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "proof" + ], + "models": [] + } + ] + }, + { + "path": "specifications/Prisoners", + "title": "The Prisoners & Switches Puzzle", + "description": "Given a room containing two switches prisoners enter one by one, they must develop a strategy to free themselves", + "source": "", + "authors": [ + "Leslie Lamport" + ], + "tags": [ + "beginner" + ], + "modules": [ + { + "path": "specifications/Prisoners/MCPrisoners.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/Prisoners/Prisoners.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/Prisoners/Prisoners.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + } + ] + } + ] + }, + { + "path": "specifications/ReadersWriters", + "title": "The Readers-Writers Problem", + "description": "Controlling concurrent access to a resource", + "source": "", + "authors": [ + "Isaac DeFrain" + ], + "tags": [], + "modules": [ + { + "path": "specifications/ReadersWriters/MC.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/ReadersWriters/MC.cfg", + "runtime": "00:00:05", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/ReadersWriters/ReadersWriters.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/SDP_Verification", + "title": "Software-Defined Perimeter", + "description": "Specifying and verifying SDP-protocol-based zero trust architecture", + "source": "https://github.com/10227694/SDP_Verification", + "authors": [ + "Luming Dong", + "Zhi Niu" + ], + "tags": [], + "modules": [ + { + "path": "specifications/SDP_Verification/SDP_Attack_New_Solution_Spec/MC.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/SDP_Verification/SDP_Attack_New_Solution_Spec/MC.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [ + "ignore deadlock" + ], + "features": [ + "liveness" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/SDP_Verification/SDP_Attack_New_Solution_Spec/SPA_Attack_New.tla", + "communityDependencies": [ + "Bitwise", + "Functions" + ], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SDP_Verification/SDP_Attack_Spec/MC.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/SDP_Verification/SDP_Attack_Spec/MC.cfg", + "runtime": "00:00:05", + "size": "small", + "mode": "exhaustive search", + "config": [ + "ignore deadlock" + ], + "features": [ + "liveness" + ], + "result": "safety failure" + } + ] + }, + { + "path": "specifications/SDP_Verification/SDP_Attack_Spec/SPA_Attack.tla", + "communityDependencies": [ + "Bitwise", + "Functions" + ], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/SingleLaneBridge", + "title": "Single-Lane Bridge Problem", + "description": "Controlling cars moving over a single-lange bridge in opposite directions", + "source": "", + "authors": [ + "Younes Aka" + ], + "tags": [], + "modules": [ + { + "path": "specifications/SingleLaneBridge/MC.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/SingleLaneBridge/MC.cfg", + "runtime": "00:00:10", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/SingleLaneBridge/SingleLaneBridge.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/SlidingPuzzles", + "title": "Sliding Block Puzzle", + "description": "A spec of the Klotski sliding block puzzle", + "source": "", + "authors": [ + "Mariusz Ryndzionek" + ], + "tags": [], + "modules": [ + { + "path": "specifications/SlidingPuzzles/SlidingPuzzles.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/SlidingPuzzles/SlidingPuzzles.cfg", + "runtime": "00:00:05", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "safety failure" + } + ] + } + ] + }, + { + "path": "specifications/SlushProtocol", + "title": "The Slush Probabilistic Consensus Protocol", + "description": "An attempt to use TLA⁺ to analyze a probabilistic protocol in the Avalanche family", + "source": "https://github.com/ahelwer/avalanche-analysis", + "authors": [ + "Andrew Helwer" + ], + "tags": [], + "modules": [ + { + "path": "specifications/SlushProtocol/Slush.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal" + ], + "models": [ + { + "path": "specifications/SlushProtocol/SlushLarge.cfg", + "runtime": "00:50:00", + "size": "large", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "success" + }, + { + "path": "specifications/SlushProtocol/SlushMedium.cfg", + "runtime": "00:01:00", + "size": "medium", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "success" + }, + { + "path": "specifications/SlushProtocol/SlushSmall.cfg", + "runtime": "00:00:15", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "success" + } + ] + } + ] + }, + { + "path": "specifications/SpanningTree", + "title": "Span Tree Exercise", + "description": "Simplified algorithm from the Lamport paper *An Assertional Correctness Proof of a Distributed Program*", + "source": "", + "authors": [ + "Leslie Lamport" + ], + "tags": [], + "modules": [ + { + "path": "specifications/SpanningTree/SpanTree.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpanningTree/SpanTreeRandom.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpanningTree/SpanTreeTest.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/SpecifyingSystems", + "title": "Specs from Specifying Systems", + "description": "All specs seen in the textbook Specifying Systems by Leslie Lamport", + "source": "http://lamport.azurewebsites.net/tla/book.html", + "authors": [ + "Leslie Lamport" + ], + "tags": [], + "modules": [ + { + "path": "specifications/SpecifyingSystems/AdvancedExamples/BNFGrammars.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/AdvancedExamples/DifferentialEquations.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/AdvancedExamples/Graphs.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/AdvancedExamples/InnerSequential.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/AdvancedExamples/InnerSerial.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/AdvancedExamples/MCInnerSequential.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/AdvancedExamples/MCInnerSequential.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness", + "state constraint" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/SpecifyingSystems/AdvancedExamples/MCInnerSerial.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/AdvancedExamples/MCInnerSerial.cfg", + "runtime": "00:01:30", + "size": "medium", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness", + "state constraint" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/SpecifyingSystems/AdvancedExamples/RegisterInterface.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/AdvancedExamples/SerialMemory.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/AsynchronousInterface/AsynchInterface.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/AsynchronousInterface/AsynchInterface.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "success" + } + ] + }, + { + "path": "specifications/SpecifyingSystems/AsynchronousInterface/Channel.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/AsynchronousInterface/Channel.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "success" + } + ] + }, + { + "path": "specifications/SpecifyingSystems/AsynchronousInterface/PrintValues.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/AsynchronousInterface/PrintValues.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "success" + } + ] + }, + { + "path": "specifications/SpecifyingSystems/CachingMemory/InternalMemory.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/CachingMemory/MCInternalMemory.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/CachingMemory/MCInternalMemory.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "success" + } + ] + }, + { + "path": "specifications/SpecifyingSystems/CachingMemory/MCWriteThroughCache.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/CachingMemory/MCWriteThroughCache.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/SpecifyingSystems/CachingMemory/Memory.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/CachingMemory/MemoryInterface.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/CachingMemory/WriteThroughCache.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/CachingMemory/WriteThroughCacheInstanced.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Composing/BinaryHourClock.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Composing/Channel.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Composing/ChannelRefinement.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Composing/CompositeFIFO.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Composing/HourClock.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Composing/InternalMemory.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Composing/JointActionMemory.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Composing/MemoryInterface.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/FIFO/Channel.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/FIFO/FIFO.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/FIFO/InnerFIFO.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/FIFO/InnerFIFOInstanced.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/FIFO/MCInnerFIFO.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/FIFO/MCInnerFIFO.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "state constraint" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/SpecifyingSystems/HourClock/HourClock.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/HourClock/HourClock.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "success" + } + ] + }, + { + "path": "specifications/SpecifyingSystems/HourClock/HourClock2.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/HourClock/HourClock2.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/SpecifyingSystems/Liveness/HourClock.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Liveness/InternalMemory.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Liveness/LiveHourClock.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/Liveness/LiveHourClock.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/SpecifyingSystems/Liveness/LiveInternalMemory.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Liveness/LiveWriteThroughCache.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Liveness/MCInternalMemory.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Liveness/MCLiveInternalMemory.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/Liveness/MCLiveInternalMemory.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/SpecifyingSystems/Liveness/MCLiveWriteThroughCache.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/Liveness/MCLiveWriteThroughCache.cfg", + "runtime": "00:00:05", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/SpecifyingSystems/Liveness/Memory.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Liveness/MemoryInterface.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Liveness/WriteThroughCacheInstanced.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/RealTime/HourClock.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/RealTime/InternalMemory.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/RealTime/MCRealTime.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/RealTime/MCRealTimeHourClock.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/RealTime/MCRealTimeHourClock.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "liveness failure" + } + ] + }, + { + "path": "specifications/SpecifyingSystems/RealTime/Memory.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/RealTime/MemoryInterface.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/RealTime/RTMemory.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/RealTime/RTWriteThroughCache.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/RealTime/RealTime.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/RealTime/RealTimeHourClock.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/RealTime/WriteThroughCache.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/SimpleMath/SimpleMath.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/SimpleMath/SimpleMath.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "success" + } + ] + }, + { + "path": "specifications/SpecifyingSystems/Standard/Bags.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Standard/FiniteSets.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Standard/Integers.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Standard/Naturals.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Standard/Peano.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Standard/ProtoReals.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Standard/Reals.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Standard/Sequences.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Syntax/BNFGrammars.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/Syntax/TLAPlusGrammar.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/TLC/ABCorrectness.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/TLC/ABCorrectness.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "success" + } + ] + }, + { + "path": "specifications/SpecifyingSystems/TLC/AlternatingBit.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/TLC/BNFGrammars.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/TLC/ConfigFileGrammar.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/SpecifyingSystems/TLC/MCAlternatingBit.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/TLC/MCAlternatingBit.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness", + "state constraint" + ], + "result": "success" + } + ] + } + ] + }, + { + "path": "specifications/Stones", + "title": "Stone Scale Puzzle", + "description": "Alternative implementation of the Car Talk Puzzle", + "source": "", + "authors": [ + "Leslie Lamport" + ], + "tags": [], + "modules": [ + { + "path": "specifications/Stones/Stones.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/TLC", + "title": "The TLC Safety Checking Algorithm", + "description": "Spec of the safety checking algorithm used by the TLC model-checker", + "source": "", + "authors": [ + "Markus Kuppe" + ], + "tags": [], + "modules": [ + { + "path": "specifications/TLC/TLCMC.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal" + ], + "models": [] + }, + { + "path": "specifications/TLC/TestGraphs.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/TLC/TestGraphs.cfg", + "runtime": "00:00:05", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + } + ] + } + ] + }, + { + "path": "specifications/TeachingConcurrency", + "title": "Teaching Concurrency", + "description": "Simple problem useful for teaching and learning about concurrency", + "source": "http://lamport.azurewebsites.net/pubs/teaching-concurrency.pdf", + "authors": [ + "Leslie Lamport" + ], + "tags": [], + "modules": [ + { + "path": "specifications/TeachingConcurrency/Simple.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal", + "proof" + ], + "models": [] + }, + { + "path": "specifications/TeachingConcurrency/SimpleRegular.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal", + "proof" + ], + "models": [] + } + ] + }, + { + "path": "specifications/TransitiveClosure", + "title": "Transitive Closure", + "description": "Spec defining the transitive closure of a relation", + "source": "", + "authors": [ + "Stephan Merz" + ], + "tags": [], + "modules": [ + { + "path": "specifications/TransitiveClosure/TransitiveClosure.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/TransitiveClosure/TransitiveClosure.cfg", + "runtime": "00:00:05", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "success" + } + ] + } + ] + }, + { + "path": "specifications/TwoPhase", + "title": "Two-Phase Handshaking", + "description": "Specification of a very simple hardware protocol called two-phase handshaking", + "source": "", + "authors": [ + "Leslie Lamport", + "Stephan Merz" + ], + "tags": [], + "modules": [ + { + "path": "specifications/TwoPhase/Alternate.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/TwoPhase/TLAPS.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "proof" + ], + "models": [] + }, + { + "path": "specifications/TwoPhase/TwoPhase.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "proof" + ], + "models": [] + } + ] + }, + { + "path": "specifications/aba-asyn-byz", + "title": "Asynchronous Byzantine Consensus", + "description": "Spec of the protocol from paper *Asynchronous Consensus and Broadcast Protocols* (1985)", + "source": "", + "authors": [ + "Igor Konnov", + "Josef Widder", + "Thanh Hai Tran" + ], + "tags": [], + "modules": [ + { + "path": "specifications/aba-asyn-byz/aba_asyn_byz.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/allocator", + "title": "Resource Allocator", + "description": "Specification of a resource allocator", + "source": "", + "authors": [ + "Stephan Merz" + ], + "tags": [], + "modules": [ + { + "path": "specifications/allocator/AllocatorImplementation.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/allocator/AllocatorImplementation.cfg", + "runtime": "00:00:15", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/allocator/AllocatorRefinement.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/allocator/AllocatorRefinement.cfg", + "runtime": "00:00:05", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/allocator/SchedulingAllocator.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/allocator/SchedulingAllocator.cfg", + "runtime": "00:00:10", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/allocator/SimpleAllocator.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/allocator/SimpleAllocator.cfg", + "runtime": "00:00:05", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + } + ] + } + ] + }, + { + "path": "specifications/bcastByz", + "title": "Asynchronous Reliable Broadcast", + "description": "Algorithm from paper *Simulating authenticated broadcasts to derive simple fault-tolerant algorithms* (1987)", + "source": "", + "authors": [ + "Igor Konnov", + "Josef Widder", + "Thanh Hai Tran" + ], + "tags": [], + "modules": [ + { + "path": "specifications/bcastByz/bcastByz.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "proof" + ], + "models": [] + } + ] + }, + { + "path": "specifications/bcastFolklore", + "title": "Folklore Reliable Broadcast", + "description": "Algorithm from paper *Unreliable failure detectors for reliable distributed systems* (1996)", + "source": "", + "authors": [ + "Igor Konnov", + "Josev Widder", + "Thanh Hai Tran" + ], + "tags": [], + "modules": [ + { + "path": "specifications/bcastFolklore/bcastFolklore.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/bosco", + "title": "The Bosco Byzantine Consensus Algorithm", + "description": "Algorithm from paper *Bosco: One-step byzantine asynchronous consensus* (2008)", + "source": "", + "authors": [ + "Igor Konnov", + "Josev Widder", + "Thanh Hai Tran" + ], + "tags": [], + "modules": [ + { + "path": "specifications/bosco/bosco.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/c1cs", + "title": "Consensus in One Communication Step", + "description": "Algorithm from paper *Consensus in one communication step* (2001)", + "source": "", + "authors": [ + "Igor Konnov", + "Josev Widder", + "Thanh Hai Tran" + ], + "tags": [], + "modules": [ + { + "path": "specifications/c1cs/c1cs.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/cbc_max", + "title": "Condition-Based Consensus", + "description": "Algorithm from paper *Evaluating the condition-based approach to solve consensus* (2003)", + "source": "", + "authors": [ + "Igor Konnov", + "Josev Widder", + "Thanh Hai Tran" + ], + "tags": [], + "modules": [ + { + "path": "specifications/cbc_max/cbc_max.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/cf1s-folklore", + "title": "One-Step Consensus with Zero-Degradation", + "description": "Algorithm from paper *One-step Consensus with Zero-Degradation* (2006)", + "source": "", + "authors": [ + "Igor Konnov", + "Josev Widder", + "Thanh Hai Tran" + ], + "tags": [], + "modules": [ + { + "path": "specifications/cf1s-folklore/cf1s_folklore.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/chang_roberts", + "title": "Chang-Roberts Algorithm for Leader Election in a Ring", + "description": "Algorithm from paper *An improved algorithm for decentralized extrema-finding in circular configurations of processes* (1979)", + "source": "", + "authors": [ + "Stephan Merz" + ], + "tags": [], + "modules": [ + { + "path": "specifications/chang_roberts/ChangRoberts.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal" + ], + "models": [] + } + ] + }, + { + "path": "specifications/detector_chan96", + "title": "Failure Detector", + "description": "Algorithm from paper *Unreliable failure detectors for reliable distributed systems* (1996)", + "source": "", + "authors": [ + "Igor Konnov", + "Josev Widder", + "Thanh Hai Tran" + ], + "tags": [], + "modules": [ + { + "path": "specifications/detector_chan96/Age_Channel.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/detector_chan96/EPFailureDetector.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/detector_chan96/EnvironmentController.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/dijkstra-mutex", + "title": "Dijkstra's Mutual Exclusion Algorithm", + "description": "Algorithm from paper *Solution of a Problem in Concurrent Programming Control* (1965)", + "source": "", + "authors": [ + "Leslie Lamport" + ], + "tags": [], + "modules": [ + { + "path": "specifications/dijkstra-mutex/DijkstraMutex.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal" + ], + "models": [] + }, + { + "path": "specifications/dijkstra-mutex/DijkstraMutex.toolbox/LSpec-model/DijkstraMutex.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal" + ], + "models": [] + }, + { + "path": "specifications/dijkstra-mutex/DijkstraMutex.toolbox/LSpec-model/MC.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/dijkstra-mutex/DijkstraMutex.toolbox/LSpec-model/MC.cfg", + "runtime": "00:00:50", + "size": "medium", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/dijkstra-mutex/DijkstraMutex.toolbox/Safety-4-processors/DijkstraMutex.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal" + ], + "models": [] + }, + { + "path": "specifications/dijkstra-mutex/DijkstraMutex.toolbox/Safety-4-processors/MC.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/dijkstra-mutex/DijkstraMutex.toolbox/Safety-4-processors/MC.cfg", + "runtime": "00:02:00", + "size": "medium", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "success" + } + ] + } + ] + }, + { + "path": "specifications/diskpaxos", + "title": "diskpaxos", + "description": "A formalization of the SWMR-Shared-Memory Disk Paxos", + "source": "https://github.com/nano-o/MultiPaxos/blob/master/DiskPaxos.tla", + "authors": [ + "Giuliano Losa", + "Leslie Lamport" + ], + "tags": [], + "modules": [ + { + "path": "specifications/diskpaxos/DiskSynod.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/diskpaxos/HDiskSynod.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/diskpaxos/Synod.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/echo", + "title": "The Echo Algorithm", + "description": "Algorithm for constructing a spanning tree in an undirected graph", + "source": "", + "authors": [ + "Stephan Merz" + ], + "tags": [], + "modules": [ + { + "path": "specifications/echo/Echo.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal" + ], + "models": [] + }, + { + "path": "specifications/echo/MCEcho.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/echo/MCEcho.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "success" + } + ] + }, + { + "path": "specifications/echo/Relation.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/ewd426", + "title": "Token Stabilization", + "description": "Dijkstra's classical stabilizing token ring algorithm: EWD426", + "source": "", + "authors": [ + "Markus Kuppe", + "Murat Demirbas" + ], + "tags": [], + "modules": [ + { + "path": "specifications/ewd426/SimTokenRing.tla", + "communityDependencies": [ + "CSV", + "IOUtils" + ], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/ewd426/SimTokenRing.cfg", + "runtime": "unknown", + "size": "large", + "mode": "generate", + "config": [], + "features": [ + "state constraint" + ], + "result": "unknown" + } + ] + }, + { + "path": "specifications/ewd426/TokenRing.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/ewd426/TokenRing.cfg", + "runtime": "unknown", + "size": "unknown", + "mode": "exhaustive search", + "config": [], + "features": [ + "alias", + "liveness" + ], + "result": "unknown" + } + ] + } + ] + }, + { + "path": "specifications/ewd687a", + "title": "Detecting Termination in Distributed Computations", + "description": "Dijkstra's Termination Detection Algorithm", + "source": "", + "authors": [ + "Leslie Lamport", + "Markus Kuppe", + "Stephan Merz" + ], + "tags": [], + "modules": [ + { + "path": "specifications/ewd687a/EWD687a.tla", + "communityDependencies": [ + "Graphs" + ], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/ewd687a/EWD687aPlusCal.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal" + ], + "models": [] + }, + { + "path": "specifications/ewd687a/EWD687a_anim.tla", + "communityDependencies": [ + "IOUtils", + "SVG" + ], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/ewd687a/EWD687a_anim.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": { + "simulate": { + "traceCount": 100 + } + }, + "config": ["ignore deadlock"], + "features": [ + "alias", + "liveness" + ], + "result": "safety failure" + } + ] + }, + { + "path": "specifications/ewd687a/MCEWD687a.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/ewd687a/MCEWD687a.cfg", + "runtime": "00:01:00", + "size": "medium", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness", + "state constraint" + ], + "result": "success" + } + ] + } + ] + }, + { + "path": "specifications/ewd840", + "title": "ewd840", + "description": "Termination Detection in a Ring", + "source": "Dijkstra's termination detection algorithm for ring topologies", + "authors": [ + "Stephan Merz" + ], + "tags": [], + "modules": [ + { + "path": "specifications/ewd840/EWD840.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/ewd840/EWD840.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [ + "ignore deadlock" + ], + "features": [], + "result": "success" + } + ] + }, + { + "path": "specifications/ewd840/EWD840_anim.tla", + "communityDependencies": [ + "SVG" + ], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/ewd840/EWD840_anim.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": { + "simulate": { + "traceCount": 100 + } + }, + "config": ["ignore deadlock"], + "features": [ + "alias" + ], + "result": "safety failure" + } + ] + }, + { + "path": "specifications/ewd840/EWD840_json.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/ewd840/EWD840_json.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [ + "ignore deadlock" + ], + "features": [], + "result": "success" + } + ] + }, + { + "path": "specifications/ewd840/EWD840_proof.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "proof" + ], + "models": [] + }, + { + "path": "specifications/ewd840/SyncTerminationDetection.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/ewd840/SyncTerminationDetection.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/ewd840/TLAPS.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "proof" + ], + "models": [] + } + ] + }, + { + "path": "specifications/ewd998", + "title": "Termination Detection in a Ring with Asynchronous Message Delivery", + "description": "Variant of EWD 840 given by Shmuel Safra", + "source": "", + "authors": [ + "Markus Kuppe", + "Stephan Merz" + ], + "tags": [], + "modules": [ + { + "path": "specifications/ewd998/AsyncTerminationDetection.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/ewd998/AsyncTerminationDetection.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness", + "state constraint" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/ewd998/AsyncTerminationDetection_proof.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "proof" + ], + "models": [] + }, + { + "path": "specifications/ewd998/EWD998.tla", + "communityDependencies": [ + "Functions", + "SequencesExt" + ], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/ewd998/EWD998.cfg", + "runtime": "00:50:00", + "size": "large", + "mode": "exhaustive search", + "config": [ + "ignore deadlock" + ], + "features": [ + "state constraint" + ], + "result": "success" + }, + { + "path": "specifications/ewd998/EWD998Small.cfg", + "runtime": "00:00:30", + "size": "small", + "mode": "exhaustive search", + "config": [ + "ignore deadlock" + ], + "features": [ + "state constraint" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/ewd998/EWD998Chan.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/ewd998/EWD998Chan.cfg", + "runtime": "00:05:00", + "size": "medium", + "mode": "exhaustive search", + "config": [ + "ignore deadlock" + ], + "features": [ + "liveness", + "state constraint" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/ewd998/EWD998ChanID.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/ewd998/EWD998ChanID.cfg", + "runtime": "unknown", + "size": "large", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness", + "state constraint", + "view" + ], + "result": "unknown" + } + ] + }, + { + "path": "specifications/ewd998/EWD998ChanID_export.tla", + "communityDependencies": [ + "IOUtils" + ], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/ewd998/EWD998ChanID_export.cfg", + "runtime": "unknown", + "size": "large", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "unknown" + } + ] + }, + { + "path": "specifications/ewd998/EWD998ChanID_shiviz.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/ewd998/EWD998ChanID_shiviz.cfg", + "runtime": "unknown", + "size": "large", + "mode": "exhaustive search", + "config": [], + "features": [ + "alias" + ], + "result": "unknown" + } + ] + }, + { + "path": "specifications/ewd998/EWD998Chan_opts.tla", + "communityDependencies": [ + "CSV", + "IOUtils" + ], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/ewd998/EWD998_anim.tla", + "communityDependencies": [ + "IOUtils", + "SVG" + ], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/ewd998/EWD998_opts.tla", + "communityDependencies": [ + "CSV", + "IOUtils" + ], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/ewd998/EWD998_optsSC.tla", + "communityDependencies": [ + "CSV", + "IOUtils" + ], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/ewd998/EWD998_proof.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "proof" + ], + "models": [] + }, + { + "path": "specifications/ewd998/SmokeEWD998.tla", + "communityDependencies": [ + "CSV", + "IOUtils" + ], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/ewd998/SmokeEWD998.cfg", + "runtime": "unknown", + "size": "large", + "mode": { + "simulate": { + "traceCount": 100 + } + }, + "config": [], + "features": [ + "liveness", + "state constraint" + ], + "result": "unknown" + } + ] + }, + { + "path": "specifications/ewd998/SmokeEWD998_SC.tla", + "communityDependencies": [ + "CSV", + "IOUtils" + ], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/ewd998/SmokeEWD998_SC.cfg", + "runtime": "unknown", + "size": "unknown", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "unknown" + } + ] + }, + { + "path": "specifications/ewd998/Utils.tla", + "communityDependencies": [ + "Functions", + "SequencesExt" + ], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/glowingRaccoon", + "title": "PCR Testing for Snippets of DNA", + "description": "Specification of a PCR test process", + "source": "", + "authors": [ + "Martin Harrison" + ], + "tags": [], + "modules": [ + { + "path": "specifications/glowingRaccoon/clean.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/glowingRaccoon/product.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/glowingRaccoon/stages.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/lamport_mutex", + "title": "Distributed Mutual Exclusion", + "description": "Specification of Lamport's distributed mutual exclusion algorithm", + "source": "", + "authors": [ + "Stephan Merz" + ], + "tags": [], + "modules": [ + { + "path": "specifications/lamport_mutex/Functions.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/lamport_mutex/LamportMutex.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/lamport_mutex/LamportMutex_proofs.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "proof" + ], + "models": [] + }, + { + "path": "specifications/lamport_mutex/NaturalsInduction.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/lamport_mutex/SequenceTheorems.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/lamport_mutex/TLAPS.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "proof" + ], + "models": [] + }, + { + "path": "specifications/lamport_mutex/WellFoundedInduction.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/nbacc_ray97", + "title": "Asynchronous Non-Blocking Atomic Commit", + "description": "Algorithm from paper *A case study of agreement problems in distributed systems: non-blocking atomic commitment* (1997)", + "source": "", + "authors": [ + "Igor Konnov", + "Josef Widder", + "Thanh Hai Tran" + ], + "tags": [], + "modules": [ + { + "path": "specifications/nbacc_ray97/nbacc_ray97.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/nbacg_guer01", + "title": "Asynchronous Non-Blocking Atomic Commitment with Failure Detectors", + "description": "Algorithm from paper *On the hardness of failure-sensitive agreement problems* (2001)", + "source": "", + "authors": [ + "Igor Konnov", + "Josef Widder", + "Thanh Hai Tran" + ], + "tags": [], + "modules": [ + { + "path": "specifications/nbacg_guer01/nbacg_guer01.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/spanning", + "title": "Spanning Tree Broadcast Algorithm", + "description": "A spanning tree broadcast algorithm", + "source": "", + "authors": [ + "Igor Konnov", + "Josef Widder", + "Thanh Hai Tran" + ], + "tags": [], + "modules": [ + { + "path": "specifications/spanning/spanning.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/sums_even", + "title": "Proof x+x is Even", + "description": "Two proofs that x+x is even for every natural number x", + "source": "", + "authors": [ + "Stephan Merz" + ], + "tags": [], + "modules": [ + { + "path": "specifications/sums_even/TLAPS.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "proof" + ], + "models": [] + }, + { + "path": "specifications/sums_even/sums_even.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "proof" + ], + "models": [] + } + ] + }, + { + "path": "specifications/tower_of_hanoi", + "title": "The Tower of Hanoi Puzzle", + "description": "Famous puzzle involving stacking disks on towers", + "source": "", + "authors": [ + "Alexander Niederbühl", + "Markus Kuppe" + ], + "tags": [ + "beginner" + ], + "modules": [ + { + "path": "specifications/tower_of_hanoi/Bits.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/tower_of_hanoi/Hanoi.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/tower_of_hanoi/Hanoi.toolbox/Model_1/Bits.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/tower_of_hanoi/Hanoi.toolbox/Model_1/Hanoi.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/tower_of_hanoi/Hanoi.toolbox/Model_1/MC.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/tower_of_hanoi/Hanoi.toolbox/Model_1/MC.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [], + "result": "safety failure" + } + ] + }, + { + "path": "specifications/tower_of_hanoi/HanoiSeq.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, + { + "path": "specifications/transaction_commit", + "title": "Transaction Commit Models", + "description": "Ordinary transaction commit, two-phase commit, and Paxos commit", + "source": "http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#paxos-commit", + "authors": [ + "Jim Gray", + "Leslie Lamport" + ], + "tags": [], + "modules": [ + { + "path": "specifications/transaction_commit/PaxosCommit.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/transaction_commit/TCommit.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/transaction_commit/TwoPhase.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + } + ] +} diff --git a/specifications/CoffeeCan/1000BeanCoffeeCan.cfg b/specifications/CoffeeCan/CoffeeCan1000Beans.cfg similarity index 100% rename from specifications/CoffeeCan/1000BeanCoffeeCan.cfg rename to specifications/CoffeeCan/CoffeeCan1000Beans.cfg diff --git a/specifications/CoffeeCan/100BeanCoffeeCan.cfg b/specifications/CoffeeCan/CoffeeCan100Beans.cfg similarity index 100% rename from specifications/CoffeeCan/100BeanCoffeeCan.cfg rename to specifications/CoffeeCan/CoffeeCan100Beans.cfg diff --git a/specifications/CoffeeCan/3000BeanCoffeeCan.cfg b/specifications/CoffeeCan/CoffeeCan3000Beans.cfg similarity index 100% rename from specifications/CoffeeCan/3000BeanCoffeeCan.cfg rename to specifications/CoffeeCan/CoffeeCan3000Beans.cfg diff --git a/specifications/KeyValueStore/MCKeyValueStore.tla b/specifications/KeyValueStore/MCKVS.tla similarity index 67% rename from specifications/KeyValueStore/MCKeyValueStore.tla rename to specifications/KeyValueStore/MCKVS.tla index 6d9e4996..09b326dc 100644 --- a/specifications/KeyValueStore/MCKeyValueStore.tla +++ b/specifications/KeyValueStore/MCKVS.tla @@ -1,4 +1,4 @@ ----- MODULE MCKeyValueStore ---- +---- MODULE MCKVS ---- EXTENDS KeyValueStore, TLC TxIdSymmetric == Permutations(TxId) ==== diff --git a/specifications/KeyValueStore/KVSSafetyLarge.cfg b/specifications/KeyValueStore/MCKVSSafetyLarge.cfg similarity index 100% rename from specifications/KeyValueStore/KVSSafetyLarge.cfg rename to specifications/KeyValueStore/MCKVSSafetyLarge.cfg diff --git a/specifications/KeyValueStore/KVSSafetyMedium.cfg b/specifications/KeyValueStore/MCKVSSafetyMedium.cfg similarity index 100% rename from specifications/KeyValueStore/KVSSafetyMedium.cfg rename to specifications/KeyValueStore/MCKVSSafetyMedium.cfg diff --git a/specifications/KeyValueStore/KVSSafetySmall.cfg b/specifications/KeyValueStore/MCKVSSafetySmall.cfg similarity index 100% rename from specifications/KeyValueStore/KVSSafetySmall.cfg rename to specifications/KeyValueStore/MCKVSSafetySmall.cfg diff --git a/specifications/MissionariesAndCannibals/MissionariesAndCannibals.cfg b/specifications/MissionariesAndCannibals/MissionariesAndCannibals.cfg new file mode 100644 index 00000000..aed7a6e3 --- /dev/null +++ b/specifications/MissionariesAndCannibals/MissionariesAndCannibals.cfg @@ -0,0 +1,11 @@ +CONSTANTS + Missionaries = {m1, m2, m3} + Cannibals = {c1, c2, c3} + +INIT Init +NEXT Next + +INVARIANTS + TypeOK + Solution + diff --git a/specifications/MissionariesAndCannibals/MissionariesAndCannibals.tla b/specifications/MissionariesAndCannibals/MissionariesAndCannibals.tla index 4faff7f6..5f3fbd8a 100644 --- a/specifications/MissionariesAndCannibals/MissionariesAndCannibals.tla +++ b/specifications/MissionariesAndCannibals/MissionariesAndCannibals.tla @@ -217,6 +217,8 @@ Next == \E S \in SUBSET who_is_on_bank[bank_of_boat] : (* This problem was proposed to me by Jay Misra, who then suggested *) (* improvements to my first version of the spec. *) (***************************************************************************) +Solution == who_is_on_bank["E"] /= {} + ============================================================================= \* Modification History \* Last modified Sat Dec 22 14:17:18 PST 2018 by lamport diff --git a/specifications/MultiCarElevator/ElevatorLivenessSmall.cfg b/specifications/MultiCarElevator/ElevatorLivenessMedium.cfg similarity index 100% rename from specifications/MultiCarElevator/ElevatorLivenessSmall.cfg rename to specifications/MultiCarElevator/ElevatorLivenessMedium.cfg diff --git a/specifications/MultiCarElevator/ElevatorSafetySmall.cfg b/specifications/MultiCarElevator/ElevatorSafetySmall.cfg new file mode 100644 index 00000000..2a6dcaa7 --- /dev/null +++ b/specifications/MultiCarElevator/ElevatorSafetySmall.cfg @@ -0,0 +1,12 @@ +CONSTANTS + Person = {p1, p2} + Elevator = {e1, e2} + FloorCount = 2 + +SPECIFICATION + Spec + +INVARIANTS + TypeInvariant + SafetyInvariant + diff --git a/specifications/N-Queens/Queens.toolbox/FourQueens/MC.cfg b/specifications/N-Queens/Queens.toolbox/FourQueens/MC.cfg index 2e54e098..2b79a3d7 100644 --- a/specifications/N-Queens/Queens.toolbox/FourQueens/MC.cfg +++ b/specifications/N-Queens/Queens.toolbox/FourQueens/MC.cfg @@ -8,4 +8,6 @@ spec_129269484699017000 INVARIANT inv_129269484700018000 inv_129269484701019000 -\* Generated at Sat Dec 18 18:54:07 CET 2010 \ No newline at end of file +\* Generated at Sat Dec 18 18:54:07 CET 2010 +INVARIANT NoSolutions + diff --git a/specifications/N-Queens/QueensPluscal.toolbox/FourQueens/MC.cfg b/specifications/N-Queens/QueensPluscal.toolbox/FourQueens/MC.cfg index d8e4aeae..fbc8ba12 100644 --- a/specifications/N-Queens/QueensPluscal.toolbox/FourQueens/MC.cfg +++ b/specifications/N-Queens/QueensPluscal.toolbox/FourQueens/MC.cfg @@ -11,4 +11,5 @@ inv_129269506136536000 \* PROPERTY definition PROPERTY prop_129269506137537000 -\* Generated at Sat Dec 18 18:57:41 CET 2010 \ No newline at end of file +\* Generated at Sat Dec 18 18:57:41 CET 2010 +INVARIANT NoSolutions diff --git a/specifications/NanoBlockchain/MCNanoMedium.cfg b/specifications/NanoBlockchain/MCNanoMedium.cfg new file mode 100644 index 00000000..cd5dc8a0 --- /dev/null +++ b/specifications/NanoBlockchain/MCNanoMedium.cfg @@ -0,0 +1,24 @@ +CONSTANTS + CalculateHash <- CalculateHashImpl + Hash = {h1, h2, h3, h4} + NoHashVal = NoHashVal + PrivateKey = {prv1, prv2} + PublicKey = {pub1, pub2} + Node = {n1, n2} + GenesisBalance = 3 + NoBlockVal = NoBlockVal + +CONSTANTS + NoHash = [Nano]NoHashVal + NoBlock = [Nano]NoBlockVal + +VIEW + View + +SPECIFICATION + Spec + +INVARIANTS + TypeInvariant + SafetyInvariant + diff --git a/specifications/NanoBlockchain/MCNanoSmall.cfg b/specifications/NanoBlockchain/MCNanoSmall.cfg index cd5dc8a0..3aaef145 100644 --- a/specifications/NanoBlockchain/MCNanoSmall.cfg +++ b/specifications/NanoBlockchain/MCNanoSmall.cfg @@ -1,6 +1,6 @@ CONSTANTS CalculateHash <- CalculateHashImpl - Hash = {h1, h2, h3, h4} + Hash = {h1, h2, h3} NoHashVal = NoHashVal PrivateKey = {prv1, prv2} PublicKey = {pub1, pub2} diff --git a/specifications/SlidingPuzzles/SlidingPuzzles.cfg b/specifications/SlidingPuzzles/SlidingPuzzles.cfg new file mode 100644 index 00000000..9ff34234 --- /dev/null +++ b/specifications/SlidingPuzzles/SlidingPuzzles.cfg @@ -0,0 +1,5 @@ +INIT Init +NEXT Next +INVARIANTS + TypeOK + KlotskiGoal diff --git a/specifications/SlidingPuzzles/SlidingPuzzles.tla b/specifications/SlidingPuzzles/SlidingPuzzles.tla index 32372b3d..82b89599 100644 --- a/specifications/SlidingPuzzles/SlidingPuzzles.tla +++ b/specifications/SlidingPuzzles/SlidingPuzzles.tla @@ -13,7 +13,7 @@ Klotski == {{<<0, 0>>, <<0, 1>>}, {<<1, 2>>, <<2, 2>>},{<<3, 2>>, <<3, 3>>}, {<<1, 3>>}, {<<2, 3>>}, {<<0, 4>>}, {<<3, 4>>}} -KlotskiGoal == {<<1, 3>>, <<1, 4>>, <<2, 3>>, <<2, 4>>} \in board +KlotskiGoal == {<<1, 3>>, <<1, 4>>, <<2, 3>>, <<2, 4>>} \notin board ChooseOne(S, P(_)) == CHOOSE x \in S : P(x) /\ \A y \in S : P(y) => y = x diff --git a/specifications/SlushProtocol/SlushSmall.cfg b/specifications/SlushProtocol/SlushSmall.cfg index 004faa33..5bfa5422 100644 --- a/specifications/SlushProtocol/SlushSmall.cfg +++ b/specifications/SlushProtocol/SlushSmall.cfg @@ -3,7 +3,7 @@ CONSTANTS SlushLoopProcess = {l1, l2, l3} SlushQueryProcess = {q1, q2, q3} HostMapping = {{n1, l1, q1}, {n2, l2, q2}, {n3, l3, q3}} - SlushIterationCount = 2 + SlushIterationCount = 1 SampleSetSize = 2 PickFlipThreshold = 2 diff --git a/specifications/ewd998/EWD998Small.cfg b/specifications/ewd998/EWD998Small.cfg new file mode 100644 index 00000000..57656f73 --- /dev/null +++ b/specifications/ewd998/EWD998Small.cfg @@ -0,0 +1,17 @@ +CONSTANTS + N = 3 + +CONSTRAINTS + StateConstraint + +SPECIFICATION + Spec + +INVARIANT + TerminationDetection + Inv + TypeOK + +\* PROPERTIES +\* \* Liveness +\* TDSpec diff --git a/specifications/glowingRaccoon/product.tla b/specifications/glowingRaccoon/product.tla index c9e2d18b..3752c572 100644 --- a/specifications/glowingRaccoon/product.tla +++ b/specifications/glowingRaccoon/product.tla @@ -175,9 +175,6 @@ Spec == /\ Init TypeOK == /\ tee \in {"Warm", "Hot", "TooHot"} /\ primer \in Nat - /\ dna \in Nat - /\ template \in Nat - /\ hybrid \in Nat /\ stage \in {"init","ready","annealed","extended","denatured"} /\ cycle \in Nat /\ longTemplate \in Nat diff --git a/specifications/tower_of_hanoi/Hanoi.toolbox/Model_1/MC.cfg b/specifications/tower_of_hanoi/Hanoi.toolbox/Model_1/MC.cfg index d46b97b8..f2dd92d1 100644 --- a/specifications/tower_of_hanoi/Hanoi.toolbox/Model_1/MC.cfg +++ b/specifications/tower_of_hanoi/Hanoi.toolbox/Model_1/MC.cfg @@ -7,4 +7,6 @@ N <- const_146427254082040000 \* SPECIFICATION definition SPECIFICATION spec_146427254083041000 -\* Generated on Thu May 26 16:22:20 CEST 2016 \ No newline at end of file +\* Generated on Thu May 26 16:22:20 CEST 2016 +INVARIANT NotSolved +