Add Apalache to CI (#141)

Signed-off-by: Andrew Helwer <[email protected]>

.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)

.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)
 

.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

.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)

.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 \

.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,20 +24,27 @@
 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):
     """
     Parse the given module using SANY.
     """
     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:

.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:

.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
 

.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}')