Added action composition feature flag

Also updated tree-sitter-tlaplus version

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

Author: ahelwer

.github/scripts/check_manifest_features.py

@@ -47,6 +47,7 @@ def build_queries(language):
     feature_query = language.query(
         '(pcal_algorithm_start) @pluscal'
         + '[(terminal_proof) (non_terminal_proof)] @proof'
+        + '(cdot) @action_composition'
     )
 
     return Queries(import_query, module_name_query, feature_query)
@@ -62,7 +63,11 @@ def get_tree_features(tree, queries):
     """
     Returns any notable features in the parse tree, such as pluscal or proofs
     """
-    return set([name for _, name in queries.features.captures(tree.root_node)])
+    return set([
+        capture_name.replace('_', ' ')
+        for capture_name, _
+        in queries.features.captures(tree.root_node).items()
+    ])
 
 def get_module_features(examples_root, path, parser, queries):
     """
@@ -147,13 +152,13 @@ def get_community_imports(examples_root, tree, text, dir, has_proof, queries):
     imports = set(
         [
             tla_utils.node_to_string(text, node)
-            for node, _ in queries.imports.captures(tree.root_node)
+            for node in tla_utils.all_nodes_of(queries.imports.captures(tree.root_node))
         ]
     )
     modules_in_file = set(
         [
             tla_utils.node_to_string(text, node)
-            for node, _ in queries.module_names.captures(tree.root_node)
+            for node in tla_utils.all_nodes_of(queries.module_names.captures(tree.root_node))
         ]
     )
     imports = (

.github/scripts/check_small_models.py

@@ -33,8 +33,8 @@
 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)
+def check_model(module, model, expected_runtime):
+    module_path = tla_utils.from_cwd(examples_root, module['path'])
     model_path = tla_utils.from_cwd(examples_root, model['path'])
     logging.info(model_path)
     hard_timeout_in_seconds = 60
@@ -47,6 +47,8 @@ def check_model(module_path, model, expected_runtime):
         tlapm_lib_path,
         community_jar_path,
         model['mode'],
+        module['features'],
+        model['features'],
         hard_timeout_in_seconds
     )
     end_time = timer()
@@ -85,7 +87,7 @@ def check_model(module_path, model, expected_runtime):
 manifest = tla_utils.load_json(manifest_path)
 small_models = sorted(
     [
-        (module['path'], model, tla_utils.parse_timespan(model['runtime']))
+        (module, model, tla_utils.parse_timespan(model['runtime']))
         for spec in manifest['specifications']
         for module in spec['modules']
         for model in module['models']

.github/scripts/requirements.txt

@@ -1,5 +1,5 @@
 jsonschema==4.20.0
 mistletoe==1.2.1
-tree-sitter==0.22
-tree-sitter-tlaplus
+tree-sitter==0.23.1
+tree-sitter-tlaplus==1.5.0
 

.github/scripts/smoke_test_large_models.py

@@ -31,8 +31,8 @@
 skip_models = args.skip
 only_models = args.only
 
-def check_model(module_path, model):
-    module_path = tla_utils.from_cwd(examples_root, module_path)
+def check_model(module, model):
+    module_path = tla_utils.from_cwd(examples_root, module['path'])
     model_path = tla_utils.from_cwd(examples_root, model['path'])
     logging.info(model_path)
     smoke_test_timeout_in_seconds = 5
@@ -44,6 +44,8 @@ def check_model(module_path, model):
         tlapm_lib_path,
         community_jar_path,
         model['mode'],
+        module['features'],
+        model['features'],
         smoke_test_timeout_in_seconds
     )
     match tlc_result:
@@ -78,7 +80,7 @@ def check_model(module_path, model):
 manifest = tla_utils.load_json(manifest_path)
 
 large_models = [
-    (module['path'], model)
+    (module, model)
     for spec in manifest['specifications']
     for module in spec['modules']
     for model in module['models']

.github/scripts/tla_utils.py

@@ -62,6 +62,17 @@ def parse_module(examples_root, parser, path):
     tree = parser.parse(module_text)
     return (tree, module_text, tree.root_node.has_error)
 
+def all_nodes_of(query_map):
+    """
+    Flatten a query result to get all matched nodes. Returned in order of
+    occurrence in file.
+    """
+    return [
+        node
+        for capture in query_map.values()
+        for node in capture
+    ].sort(key=lambda node: node.start_byte)
+
 def node_to_string(module_bytes, node):
     """
     Gets the string covered by the given tree-sitter parse tree node.
@@ -93,6 +104,15 @@ def get_run_mode(mode):
     else:
         raise NotImplementedError(f'Undefined model-check mode {mode}')
 
+def get_tlc_feature_flags(module_features, model_features):
+    """
+    Selectively enables experimental TLC features according to needs.
+    """
+    jvm_parameters = []
+    if 'action composition' in module_features:
+        jvm_parameters.append('-Dtlc2.tool.impl.Tool.cdot=true')
+    return jvm_parameters
+
 def check_model(
         tools_jar_path,
         apalache_path,
@@ -101,6 +121,8 @@ def check_model(
         tlapm_lib_path,
         community_jar_path,
         mode,
+        module_features,
+        model_features,
         hard_timeout_in_seconds
     ):
     """
@@ -127,8 +149,7 @@ def check_model(
             )
             return apalache
         else:
-            tlc = subprocess.run([
-                'java',
+            jvm_parameters = [
                 '-enableassertions',
                 '-Dtlc2.TLC.ide=Github',
                 '-Dutil.ExecutionStatisticsCollector.id=abcdef60f238424fa70d124d0c77ffff',
@@ -140,13 +161,16 @@ def check_model(
                     community_jar_path,
                     tlapm_lib_path
                 ]),
-                'tlc2.TLC',
+            ] + get_tlc_feature_flags(module_features, model_features)
+            tlc_parameters = [
                 module_path,
                 '-config', model_path,
                 '-workers', 'auto',
                 '-lncheck', 'final',
                 '-cleanup'
-                ] + get_run_mode(mode),
+            ] + get_run_mode(mode)
+            tlc = subprocess.run(
+                ['java'] + jvm_parameters + ['tlc2.TLC'] + tlc_parameters,
                 timeout=hard_timeout_in_seconds,
                 stdout=subprocess.PIPE,
                 stderr=subprocess.STDOUT,

.github/scripts/unicode_number_set_shim.py

@@ -93,7 +93,7 @@ def replace_imports(module_bytes, tree, query):
     shim_modules = {shim.module : shim for shim in shims}
     imported_modules = [
         (imported_module, shim_modules[module_name])
-        for imported_module, _ in query.captures(tree.root_node)
+        for imported_module in tla_utils.all_nodes_of(query.captures(tree.root_node))
         if (module_name := tla_utils.node_to_string(module_bytes, imported_module)) in shim_modules
     ]
     byte_offset = 0

manifest-schema.json

@@ -40,7 +40,7 @@
                 "tlaLanguageVersion": {"type": "number"},
                 "features": {
                   "type": "array",
-                  "items": {"enum": ["pluscal", "proof"]}
+                  "items": {"enum": ["pluscal", "proof", "action composition"]}
                 },
                 "models": {
                   "type": "array",