From 7c8ceab9335296469d2263fba739c075771c5e00 Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Sat, 20 Apr 2024 07:30:24 -0700 Subject: [PATCH] Add Apalache to CI (#141) Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com> --- .github/scripts/check_manifest_features.py | 4 +- .github/scripts/check_proofs.py | 21 ++++++--- .github/scripts/check_small_models.py | 19 +++++--- .github/scripts/generate_manifest.py | 1 - .github/scripts/linux-setup.sh | 3 ++ .github/scripts/parse_modules.py | 20 ++++++--- .github/scripts/smoke_test_large_models.py | 14 ++++-- .github/scripts/tla_utils.py | 50 +++++++++++++++++----- .github/scripts/translate_pluscal.py | 9 ++-- .github/scripts/unicode_conversion.py | 9 ++-- .github/scripts/unicode_number_set_shim.py | 9 ++-- .github/scripts/windows-setup.sh | 5 +++ .github/workflows/CI.yml | 5 +++ .gitignore | 3 ++ README.md | 6 +-- manifest-schema.json | 2 +- manifest.json | 6 +-- specifications/EinsteinRiddle/Einstein.tla | 34 ++++++++------- 18 files changed, 149 insertions(+), 71 deletions(-) diff --git a/.github/scripts/check_manifest_features.py b/.github/scripts/check_manifest_features.py index 2b6c2ac0..e65106c7 100644 --- a/.github/scripts/check_manifest_features.py +++ b/.github/scripts/check_manifest_features.py @@ -112,7 +112,8 @@ def get_model_features(examples_root, path): 'Sequences', 'TLC', 'TLCExt', - 'Toolbox' + 'Toolbox', + 'Apalache' } # All the standard modules available when using TLAPS @@ -230,7 +231,6 @@ def check_features(parser, queries, manifest, examples_root): if __name__ == '__main__': parser = ArgumentParser(description='Checks metadata in tlaplus/examples manifest.json against module and model files in repository.') parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True) - parser.add_argument('--ts_path', help='[DEPRECATED, UNUSED] Path to tree-sitter-tlaplus directory', required=False) args = parser.parse_args() manifest_path = normpath(args.manifest_path) diff --git a/.github/scripts/check_proofs.py b/.github/scripts/check_proofs.py index e213d6c7..999dbf52 100644 --- a/.github/scripts/check_proofs.py +++ b/.github/scripts/check_proofs.py @@ -9,26 +9,30 @@ from timeit import default_timer as timer import tla_utils -logging.basicConfig(level=logging.INFO) - parser = ArgumentParser(description='Validate all proofs in all modules with TLAPM.') parser.add_argument('--tlapm_path', help='Path to TLAPM install dir; should have bin and lib subdirs', required=True) parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True) parser.add_argument('--skip', nargs='+', help='Space-separated list of .tla modules to skip checking', required=False, default=[]) +parser.add_argument('--only', nargs='+', help='If provided, only check proofs in this space-separated list', required=False, default=[]) +parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true') args = parser.parse_args() tlapm_path = normpath(args.tlapm_path) manifest_path = normpath(args.manifest_path) manifest = tla_utils.load_json(manifest_path) examples_root = dirname(manifest_path) -skip_modules = [normpath(path) for path in args.skip] +skip_modules = args.skip +only_modules = args.only + +logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO) proof_module_paths = [ module['path'] for spec in manifest['specifications'] for module in spec['modules'] if 'proof' in module['features'] - and normpath(module['path']) not in skip_modules + and module['path'] not in skip_modules + and (only_modules == [] or model['path'] in only_models) ] for path in skip_modules: @@ -45,14 +49,19 @@ [ tlapm_path, module_path, '-I', module_dir - ], capture_output=True + ], + stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, + text=True ) end_time = timer() logging.info(f'Checked proofs in {end_time - start_time:.1f}s') if tlapm.returncode != 0: logging.error(f'Proof checking failed in {module_path}:') - logging.error(tlapm.stderr.decode('utf-8')) + logging.error(tlapm.stdout) success = False + else: + logging.debug(tlapm.stdout) exit(0 if success else 1) diff --git a/.github/scripts/check_small_models.py b/.github/scripts/check_small_models.py index f54dc2c7..2171da82 100644 --- a/.github/scripts/check_small_models.py +++ b/.github/scripts/check_small_models.py @@ -13,22 +13,25 @@ parser = ArgumentParser(description='Checks all small TLA+ models in the tlaplus/examples repo using TLC.') parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=True) +parser.add_argument('--apalache_path', help='Path to the Apalache directory', required=True) parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=True) parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', required=True) parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True) parser.add_argument('--skip', nargs='+', help='Space-separated list of models to skip checking', required=False, default=[]) parser.add_argument('--only', nargs='+', help='If provided, only check models in this space-separated list', required=False, default=[]) +parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true') args = parser.parse_args() -logging.basicConfig(level=logging.INFO) +logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO) tools_jar_path = normpath(args.tools_jar_path) +apalache_path = normpath(args.apalache_path) tlapm_lib_path = normpath(args.tlapm_lib_path) community_jar_path = normpath(args.community_modules_jar_path) manifest_path = normpath(args.manifest_path) examples_root = dirname(manifest_path) -skip_models = [normpath(path) for path in args.skip] -only_models = [normpath(path) for path in args.only] +skip_models = args.skip +only_models = args.only def check_model(module_path, model, expected_runtime): module_path = tla_utils.from_cwd(examples_root, module_path) @@ -38,6 +41,7 @@ def check_model(module_path, model, expected_runtime): start_time = timer() tlc_result = tla_utils.check_model( tools_jar_path, + apalache_path, module_path, model_path, tlapm_lib_path, @@ -46,10 +50,10 @@ def check_model(module_path, model, expected_runtime): hard_timeout_in_seconds ) end_time = timer() + output = ' '.join(tlc_result.args) + '\n' + tlc_result.stdout match tlc_result: case CompletedProcess(): logging.info(f'{model_path} in {end_time - start_time:.1f}s vs. {expected_runtime.seconds}s expected') - output = ' '.join(tlc_result.args) + '\n' + tlc_result.stdout expected_result = model['result'] actual_result = tla_utils.resolve_tlc_exit_code(tlc_result.returncode) if expected_result != actual_result: @@ -67,10 +71,11 @@ def check_model(module_path, model, expected_runtime): logging.error(f"(distinct/total/depth); expected: {tla_utils.get_state_count_info(model)}, actual: {state_count_info}") logging.error(output) return False + logging.debug(output) return True case TimeoutExpired(): logging.error(f'{model_path} hit hard timeout of {hard_timeout_in_seconds} seconds') - logging.error(tlc_result.output.decode('utf-8')) + logging.error(output) return False case _: logging.error(f'Unhandled TLC result type {type(tlc_result)}: {tlc_result}') @@ -85,8 +90,8 @@ def check_model(module_path, model, expected_runtime): for module in spec['modules'] for model in module['models'] if model['size'] == 'small' - and normpath(model['path']) not in skip_models - and (only_models == [] or normpath(model['path']) in only_models) + and model['path'] not in skip_models + and (only_models == [] or model['path'] in only_models) ], key = lambda m: m[2], reverse=True diff --git a/.github/scripts/generate_manifest.py b/.github/scripts/generate_manifest.py index 7ffd6d1d..008eab2f 100644 --- a/.github/scripts/generate_manifest.py +++ b/.github/scripts/generate_manifest.py @@ -167,7 +167,6 @@ def integrate_old_manifest_into_new(old_manifest, new_manifest): parser = ArgumentParser(description='Generates a new manifest.json derived from files in the repo.') parser.add_argument('--manifest_path', help='Path to the current tlaplus/examples manifest.json file', default='manifest.json') parser.add_argument('--ci_ignore_path', help='Path to the CI ignore file', default='.ciignore') - parser.add_argument('--ts_path', help='[DEPRECATED, UNUSED] Path to tree-sitter-tlaplus directory', required=False) args = parser.parse_args() manifest_path = normpath(args.manifest_path) diff --git a/.github/scripts/linux-setup.sh b/.github/scripts/linux-setup.sh index fc5891f5..a6be00a7 100755 --- a/.github/scripts/linux-setup.sh +++ b/.github/scripts/linux-setup.sh @@ -40,6 +40,9 @@ main() { # Get TLA⁺ tools mkdir -p "$DEPS_DIR/tools" wget -nv http://nightly.tlapl.us/dist/tla2tools.jar -P "$DEPS_DIR/tools" + # Get Apalache + wget -nv https://github.com/informalsystems/apalache/releases/latest/download/apalache.tgz -O /tmp/apalache.tgz + tar -xzf /tmp/apalache.tgz --directory "$DEPS_DIR" # Get TLA⁺ community modules mkdir -p "$DEPS_DIR/community" wget -nv https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar \ diff --git a/.github/scripts/parse_modules.py b/.github/scripts/parse_modules.py index 1d61ad97..d1cf225d 100644 --- a/.github/scripts/parse_modules.py +++ b/.github/scripts/parse_modules.py @@ -6,12 +6,13 @@ from concurrent.futures import ThreadPoolExecutor import logging from os import cpu_count -from os.path import dirname, normpath, pathsep +from os.path import join, dirname, normpath, pathsep import subprocess import tla_utils parser = ArgumentParser(description='Parses all TLA+ modules in the tlaplus/examples repo using SANY.') parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=True) +parser.add_argument('--apalache_path', help='Path to the Apalache directory', required=True) parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=True) parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', required=True) parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True) @@ -23,12 +24,13 @@ logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO) tools_jar_path = normpath(args.tools_jar_path) +apalache_jar_path = normpath(join(args.apalache_path, 'lib', 'apalache.jar')) tlaps_modules = normpath(args.tlapm_lib_path) community_modules = normpath(args.community_modules_jar_path) manifest_path = normpath(args.manifest_path) examples_root = dirname(manifest_path) -skip_modules = [normpath(path) for path in args.skip] -only_modules = [normpath(path) for path in args.only] +skip_modules = args.skip +only_modules = args.only def parse_module(path): """ @@ -36,7 +38,13 @@ def parse_module(path): """ logging.info(path) # Jar paths must go first - search_paths = pathsep.join([tools_jar_path, dirname(path), community_modules, tlaps_modules]) + search_paths = pathsep.join([ + tools_jar_path, + apalache_jar_path, + dirname(path), + community_modules, + tlaps_modules + ]) sany = subprocess.run([ 'java', '-cp', search_paths, @@ -63,8 +71,8 @@ def parse_module(path): tla_utils.from_cwd(examples_root, module['path']) for spec in manifest['specifications'] for module in spec['modules'] - if normpath(module['path']) not in skip_modules - and (only_modules == [] or normpath(module['path']) in only_modules) + if module['path'] not in skip_modules + and (only_modules == [] or module['path'] in only_modules) ] for path in skip_modules: diff --git a/.github/scripts/smoke_test_large_models.py b/.github/scripts/smoke_test_large_models.py index bcd9d901..d9f0514c 100644 --- a/.github/scripts/smoke_test_large_models.py +++ b/.github/scripts/smoke_test_large_models.py @@ -13,18 +13,23 @@ parser = ArgumentParser(description='Smoke-tests all larger TLA+ models in the tlaplus/examples repo using TLC.') parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=True) +parser.add_argument('--apalache_path', help='Path to the Apalache directory', required=True) parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=True) parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', required=True) parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True) parser.add_argument('--skip', nargs='+', help='Space-separated list of models to skip checking', required=False, default=[]) +parser.add_argument('--only', nargs='+', help='If provided, only check models in this space-separated list', required=False, default=[]) +parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true') args = parser.parse_args() tools_jar_path = normpath(args.tools_jar_path) +apalache_path = normpath(args.apalache_path) tlapm_lib_path = normpath(args.tlapm_lib_path) community_jar_path = normpath(args.community_modules_jar_path) manifest_path = normpath(args.manifest_path) examples_root = dirname(manifest_path) -skip_models = [normpath(path) for path in args.skip] +skip_models = args.skip +only_models = args.only def check_model(module_path, model): module_path = tla_utils.from_cwd(examples_root, module_path) @@ -33,6 +38,7 @@ def check_model(module_path, model): smoke_test_timeout_in_seconds = 5 tlc_result = tla_utils.check_model( tools_jar_path, + apalache_path, module_path, model_path, tlapm_lib_path, @@ -42,6 +48,7 @@ def check_model(module_path, model): ) match tlc_result: case TimeoutExpired(): + logging.debug(tlc_result.stdout) return True case CompletedProcess(): logging.warning(f'Model {model_path} finished quickly, within {smoke_test_timeout_in_seconds} seconds; consider labeling it a small model') @@ -56,7 +63,7 @@ def check_model(module_path, model): logging.error(f'Unhandled TLC result type {type(tlc_result)}: {tlc_result}') return False -logging.basicConfig(level=logging.INFO) +logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO) manifest = tla_utils.load_json(manifest_path) @@ -66,7 +73,8 @@ def check_model(module_path, model): for module in spec['modules'] for model in module['models'] if model['size'] != 'small' - and normpath(model['path']) not in skip_models + and model['path'] not in skip_models + and (only_models == [] or model['path'] in only_models) ] for path in skip_models: diff --git a/.github/scripts/tla_utils.py b/.github/scripts/tla_utils.py index 73a6430d..cabfe194 100644 --- a/.github/scripts/tla_utils.py +++ b/.github/scripts/tla_utils.py @@ -87,37 +87,65 @@ def get_run_mode(mode): else: raise NotImplementedError(f'Undefined model-check mode {mode}') -def check_model(tools_jar_path, module_path, model_path, tlapm_lib_path, community_jar_path, mode, hard_timeout_in_seconds): +def check_model( + tools_jar_path, + apalache_path, + module_path, + model_path, + tlapm_lib_path, + community_jar_path, + mode, + hard_timeout_in_seconds + ): """ Model-checks the given model against the given module. """ tools_jar_path = normpath(tools_jar_path) + apalache_path = normpath(join(apalache_path, 'bin', 'apalache-mc')) + apalache_jar_path = normpath(join(apalache_path, 'lib', 'apalache.jar')) module_path = normpath(module_path) model_path = normpath(model_path) tlapm_lib_path = normpath(tlapm_lib_path) community_jar_path = normpath(community_jar_path) try: - tlc = subprocess.run( - [ + if mode == 'symbolic': + apalache = subprocess.run([ + apalache_path, 'check', + f'--config={model_path}', + module_path + ], + timeout=hard_timeout_in_seconds, + stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, + text=True + ) + return apalache + else: + tlc = subprocess.run([ 'java', '-Dtlc2.TLC.ide=Github', '-Dutil.ExecutionStatisticsCollector.id=abcdef60f238424fa70d124d0c77ffff', '-XX:+UseParallelGC', # Jar paths must go first - '-cp', pathsep.join([tools_jar_path, community_jar_path, tlapm_lib_path]), + '-cp', pathsep.join([ + tools_jar_path, + apalache_jar_path, + community_jar_path, + tlapm_lib_path + ]), 'tlc2.TLC', module_path, '-config', model_path, '-workers', 'auto', '-lncheck', 'final', '-cleanup' - ] + get_run_mode(mode), - timeout=hard_timeout_in_seconds, - stdout=subprocess.PIPE, - stderr=subprocess.STDOUT, - text=True - ) - return tlc + ] + get_run_mode(mode), + timeout=hard_timeout_in_seconds, + stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, + text=True + ) + return tlc except subprocess.TimeoutExpired as e: return e diff --git a/.github/scripts/translate_pluscal.py b/.github/scripts/translate_pluscal.py index 324fbf3d..bf0f18b9 100644 --- a/.github/scripts/translate_pluscal.py +++ b/.github/scripts/translate_pluscal.py @@ -24,8 +24,8 @@ tools_path = normpath(args.tools_jar_path) manifest_path = normpath(args.manifest_path) examples_root = dirname(manifest_path) -skip_modules = [normpath(path) for path in args.skip] -only_modules = [normpath(path) for path in args.only] +skip_modules = args.skip +only_modules = args.only manifest = tla_utils.load_json(manifest_path) @@ -35,8 +35,8 @@ for spec in manifest['specifications'] for module in spec['modules'] if 'pluscal' in module['features'] - and normpath(module['path']) not in skip_modules - and (only_modules == [] or normpath(module['path']) in only_modules) + and module['path'] not in skip_modules + and (only_modules == [] or module['path'] in only_modules) ] for path in skip_modules: @@ -53,6 +53,7 @@ def translate_module(module_path): match result: case CompletedProcess(): if result.returncode == 0: + logging.debug(result.stdout) return True else: logging.error(f'Module {module_path} conversion failed with return code {result.returncode}; output:\n{result.stdout}') diff --git a/.github/scripts/unicode_conversion.py b/.github/scripts/unicode_conversion.py index 7cffa8aa..0fddbff4 100644 --- a/.github/scripts/unicode_conversion.py +++ b/.github/scripts/unicode_conversion.py @@ -26,8 +26,8 @@ to_ascii = args.to_ascii manifest_path = normpath(args.manifest_path) examples_root = dirname(manifest_path) -skip_modules = [normpath(path) for path in args.skip] -only_modules = [normpath(path) for path in args.only] +skip_modules = args.skip +only_modules = args.only manifest = tla_utils.load_json(manifest_path) @@ -36,8 +36,8 @@ tla_utils.from_cwd(examples_root, module['path']) for spec in manifest['specifications'] for module in spec['modules'] - if normpath(module['path']) not in skip_modules - and (only_modules == [] or normpath(module['path']) in only_modules) + if module['path'] not in skip_modules + and (only_modules == [] or module['path'] in only_modules) ] for path in skip_modules: @@ -54,6 +54,7 @@ def convert_module(module_path): match result: case CompletedProcess(): if result.returncode == 0: + logging.debug(result.stdout) return True else: logging.error(f'Module {module_path} conversion failed with return code {result.returncode}; output:\n{result.stdout}') diff --git a/.github/scripts/unicode_number_set_shim.py b/.github/scripts/unicode_number_set_shim.py index 6ad246b5..84f4a1fc 100644 --- a/.github/scripts/unicode_number_set_shim.py +++ b/.github/scripts/unicode_number_set_shim.py @@ -117,7 +117,6 @@ def write_module(examples_root, module_path, module_bytes): if __name__ == '__main__': parser = ArgumentParser(description='Adds ℕ/ℤ/ℝ Unicode number set shim definitions to modules as needed.') parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True) - parser.add_argument('--ts_path', help='[DEPRECATED, UNUSED] Path to tree-sitter-tlaplus directory', required=False) parser.add_argument('--skip', nargs='+', help='Space-separated list of .tla modules to skip', required=False, default=[]) parser.add_argument('--only', nargs='+', help='If provided, only modify models in this space-separated list', required=False, default=[]) args = parser.parse_args() @@ -125,8 +124,8 @@ def write_module(examples_root, module_path, module_bytes): manifest_path = normpath(args.manifest_path) manifest = tla_utils.load_json(manifest_path) examples_root = dirname(manifest_path) - skip_modules = [normpath(path) for path in args.skip] - only_modules = [normpath(path) for path in args.only] + skip_modules = args.skip + only_modules = args.only TLAPLUS_LANGUAGE = Language(tree_sitter_tlaplus.language(), 'tlaplus') parser = Parser() @@ -137,8 +136,8 @@ def write_module(examples_root, module_path, module_bytes): module['path'] for spec in manifest['specifications'] for module in spec['modules'] - if normpath(module['path']) not in skip_modules - and (only_modules == [] or normpath(module['path']) in only_modules) + if module['path'] not in skip_modules + and (only_modules == [] or module['path'] in only_modules) ] for module_path in modules: diff --git a/.github/scripts/windows-setup.sh b/.github/scripts/windows-setup.sh index 3645de5d..9f0e5f18 100755 --- a/.github/scripts/windows-setup.sh +++ b/.github/scripts/windows-setup.sh @@ -37,6 +37,11 @@ main() { # Get TLA⁺ tools mkdir -p "$DEPS_DIR/tools" curl http://nightly.tlapl.us/dist/tla2tools.jar --output "$DEPS_DIR/tools/tla2tools.jar" + # Get Apalache + curl -L https://github.com/informalsystems/apalache/releases/latest/download/apalache.zip --output apalache.zip + 7z x apalache.zip + mv apalache "$DEPS_DIR/" + rm apalache.zip # Get TLA⁺ community modules mkdir -p "$DEPS_DIR/community" curl -L https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar --output "$DEPS_DIR/community/modules.jar" diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index d7075b6e..18e5c172 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -110,6 +110,7 @@ jobs: fi python $SCRIPT_DIR/parse_modules.py \ --tools_jar_path $DEPS_DIR/tools/tla2tools.jar \ + --apalache_path $DEPS_DIR/apalache \ --tlapm_lib_path $DEPS_DIR/tlapm/library \ --community_modules_jar_path $DEPS_DIR/community/modules.jar \ --manifest_path manifest.json \ @@ -121,9 +122,12 @@ jobs: if [ ${{ matrix.unicode }} ]; then # This redefines Real so cannot be shimmed SKIP+=("specifications/SpecifyingSystems/RealTime/MCRealTimeHourClock.cfg") + # Apalache does not yet support Unicode + SKIP+=("specifications/EinsteinRiddle/Einstein.cfg") fi python $SCRIPT_DIR/check_small_models.py \ --tools_jar_path $DEPS_DIR/tools/tla2tools.jar \ + --apalache_path $DEPS_DIR/apalache \ --tlapm_lib_path $DEPS_DIR/tlapm/library \ --community_modules_jar_path $DEPS_DIR/community/modules.jar \ --manifest_path manifest.json \ @@ -140,6 +144,7 @@ jobs: fi python $SCRIPT_DIR/smoke_test_large_models.py \ --tools_jar_path $DEPS_DIR/tools/tla2tools.jar \ + --apalache_path $DEPS_DIR/apalache \ --tlapm_lib_path $DEPS_DIR/tlapm/library \ --community_modules_jar_path $DEPS_DIR/community/modules.jar \ --manifest_path manifest.json \ diff --git a/.gitignore b/.gitignore index a542435b..abff5e71 100644 --- a/.gitignore +++ b/.gitignore @@ -46,3 +46,6 @@ tree-sitter-tlaplus/ ## Ignore tools/ folder created by .devcontainer.json tools/ +# Ignore directory created by Apalache +_apalache-out + diff --git a/README.md b/README.md index 0b039bae..540f4063 100644 --- a/README.md +++ b/README.md @@ -53,6 +53,7 @@ Here is a list of specs included in this repository, with links to the relevant | [Snapshot Key-Value Store](specifications/KeyValueStore) | Andrew Helwer, Murat Demirbas | | | ✔ | ✔ | | | [Chang-Roberts Algorithm for Leader Election in a Ring](specifications/chang_roberts) | Stephan Merz | | | ✔ | ✔ | | | [MultiPaxos in SMR-Style](specifications/MultiPaxos-SMR) | Guanzhou Hu | | | ✔ | ✔ | | +| [Einstein's Riddle](specifications/EinsteinRiddle) | Isaac DeFrain, Giuliano Losa | | | | | ✔ | | [Resource Allocator](specifications/allocator) | Stephan Merz | | | | ✔ | | | [Transitive Closure](specifications/TransitiveClosure) | Stephan Merz | | | | ✔ | | | [Atomic Commitment Protocol](specifications/acp) | Stephan Merz | | | | ✔ | | @@ -70,7 +71,6 @@ Here is a list of specs included in this repository, with links to the relevant | [Multi-Car Elevator System](specifications/MultiCarElevator) | Andrew Helwer | | | | ✔ | | | [Nano Blockchain Protocol](specifications/NanoBlockchain) | Andrew Helwer | | | | ✔ | | | [The Readers-Writers Problem](specifications/ReadersWriters) | Isaac DeFrain | | | | ✔ | | -| [Einstein's Riddle](specifications/EinsteinRiddle) | Isaac DeFrain, Giuliano Losa | | | | ✔ | ✔ | | [Asynchronous Byzantine Consensus](specifications/aba-asyn-byz) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | | [Folklore Reliable Broadcast](specifications/bcastFolklore) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | | [The Bosco Byzantine Consensus Algorithm](specifications/bosco) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | @@ -85,10 +85,10 @@ Here is a list of specs included in this repository, with links to the relevant | [Chameneos, a Concurrency Game](specifications/Chameneos) | Mariusz Ryndzionek | | | | ✔ | | | [PCR Testing for Snippets of DNA](specifications/glowingRaccoon) | Martin Harrison | | | | ✔ | | | [RFC 3506: Voucher Transaction System](specifications/byihive) | Santhosh Raju, Cherry G. Mathew, Fransisca Andriani | | | | ✔ | | -| [TLA⁺ Level Checking](specifications/LevelChecking) | Leslie Lamport | | | | | | -| [Condition-Based Consensus](specifications/cbc_max) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | | | | [Yo-Yo Leader Election](specifications/YoYo) | Ludovic Yvoz, Stephan Merz | | | | ✔ | | | [TCP as defined in RFC 9293](specifications/tcp) | Markus Kuppe | | | | ✔ | | +| [TLA⁺ Level Checking](specifications/LevelChecking) | Leslie Lamport | | | | | | +| [Condition-Based Consensus](specifications/cbc_max) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | | | ## Examples Elsewhere Here is a list of specs stored in locations outside this repository, including submodules. diff --git a/manifest-schema.json b/manifest-schema.json index a8121585..11297238 100644 --- a/manifest-schema.json +++ b/manifest-schema.json @@ -61,7 +61,7 @@ "mode": { "oneOf": [ { - "enum": ["exhaustive search", "generate"] + "enum": ["exhaustive search", "generate", "symbolic"] }, { "type": "object", diff --git a/manifest.json b/manifest.json index 4385e8f3..512f52ad 100644 --- a/manifest.json +++ b/manifest.json @@ -454,9 +454,9 @@ "models": [ { "path": "specifications/EinsteinRiddle/Einstein.cfg", - "runtime": "unknown", - "size": "large", - "mode": "exhaustive search", + "runtime": "00:00:01", + "size": "small", + "mode": "symbolic", "features": [], "result": "safety failure" } diff --git a/specifications/EinsteinRiddle/Einstein.tla b/specifications/EinsteinRiddle/Einstein.tla index eb67a5d3..02b7cfb1 100644 --- a/specifications/EinsteinRiddle/Einstein.tla +++ b/specifications/EinsteinRiddle/Einstein.tla @@ -38,7 +38,7 @@ (* Instructions to run `^Apalache^' appear at the end of the file. *) (*********************************************************************************) -EXTENDS Naturals, FiniteSets +EXTENDS Naturals, FiniteSets, Apalache House == 1..5 @@ -46,13 +46,17 @@ House == 1..5 \* would be evaluated faster. However, TLC!Permutations equals a \* set of records whereas Permutation below equals a set of tuples/ \* sequences. Also, Permutation expects Cardinality(S) = 5. -Permutation(S) == - { p \in [ House -> S ] : - /\ p[2] \in S \ {p[1]} - /\ p[3] \in S \ {p[1], p[2]} - /\ p[4] \in S \ {p[1], p[2], p[3]} - /\ p[5] \in S \ {p[1], p[2], p[3], p[4]} } - +\* @type: Set(Str) => Set(Seq(Str)); +Permutation(S) == { + FunAsSeq(p, 5, 5) : p \in { + p \in [ House -> S ] : + /\ p[2] \in S \ {p[1]} + /\ p[3] \in S \ {p[1], p[2]} + /\ p[4] \in S \ {p[1], p[2], p[3]} + /\ p[5] \in S \ {p[1], p[2], p[3], p[4]} + } + } + \* In most specs, the following parameterization would be defined as \* constants. Given that Einstein's riddle has only this \* parameterization, the constants are replaced with constant-level @@ -65,15 +69,15 @@ PETS == Permutation({ "bird", "cat", "dog", "fish", "horse" }) CIGARS == Permutation({ "blend", "bm", "dh", "pm", "prince" }) VARIABLES - \* @type: Int -> Str; + \* @type: Seq(Str); nationality, \* tuple of nationalities - \* @type: Int -> Str; + \* @type: Seq(Str); colors, \* tuple of house colors - \* @type: Int -> Str; + \* @type: Seq(Str); pets, \* tuple of pets - \* @type: Int -> Str; + \* @type: Seq(Str); cigars, \* tuple of cigars - \* @type: Int -> Str; + \* @type: Seq(Str); drinks \* tuple of drinks ------------------------------------------------------------ @@ -136,7 +140,7 @@ Init == \* Apalache cannot infer the type of `vars' because it could be a sequence or a tuple. \* So we explicitely tell Apalache that it is a sequence by adding the following annotation: -\* @type: Seq(Int -> Str); +\* @type: Seq(Seq(Str)); vars == <> Next == @@ -167,4 +171,4 @@ FindSolution == ~Solution \* `^apalache-mc check --init=Init --inv=FindSolution --length=0 --run-dir=./outout Einstein.tla^' \* You will then find the solution in `^./output/violation.tla^'. -============================================================ \ No newline at end of file +============================================================