Use CHECK_DEADLOCK config file parameter

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>

.github/scripts/check_manifest_features.py

@@ -12,6 +12,7 @@
 import glob
 from os.path import basename, dirname, join, normpath, splitext
 from typing import Any
+import re
 import tla_utils
 from tree_sitter import Language, Parser
 
@@ -89,32 +90,32 @@ def get_module_features(examples_root, path, parser, queries):
     tree, _, _ = parse_module(examples_root, parser, path)
     return get_tree_features(tree, queries)
 
-# Keywords mapping to features for models
+# Regexes mapping to features for models
 model_features = {
-    'PROPERTY': 'liveness',
-    'PROPERTIES': 'liveness',
-    'SYMMETRY': 'symmetry',
-    'ALIAS': 'alias',
-    'VIEW': 'view',
-    'CONSTRAINT': 'state constraint',
-    'CONSTRAINTS': 'state constraint',
+    re.compile('^PROPERTY', re.MULTILINE) : 'liveness',
+    re.compile('^PROPERTIES', re.MULTILINE): 'liveness',
+    re.compile('^SYMMETRY', re.MULTILINE): 'symmetry',
+    re.compile('^ALIAS', re.MULTILINE): 'alias',
+    re.compile('^VIEW', re.MULTILINE): 'view',
+    re.compile('^CONSTRAINT', re.MULTILINE): 'state constraint',
+    re.compile('^CONSTRAINTS', re.MULTILINE): 'state constraint',
+    re.compile('^CHECK_DEADLOCK\\s+FALSE', re.MULTILINE) : 'ignore deadlock'
 }
 
 def get_model_features(examples_root, path):
     """
     Finds features present in the given .cfg model file.
-    This will be a best-effort text search until a tree-sitter grammar is
+    This will be a best-effort regex search until a tree-sitter grammar is
     created for .cfg files.
     """
     path = tla_utils.from_cwd(examples_root, path)
     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]])
+    for regex, feature in model_features.items():
+        if regex.search(model_text):
+            features.append(feature)
     return set(features)
 
 # All the standard modules available when using TLC

.github/scripts/check_small_models.py

@@ -41,7 +41,6 @@ def check_model(module_path, model, expected_runtime):
         tlapm_lib_path,
         community_jar_path,
         model['mode'],
-        model['config'],
         hard_timeout_in_seconds
     )
     end_time = timer()

.github/scripts/generate_manifest.py

@@ -14,7 +14,6 @@
 from pathlib import PureWindowsPath
 import glob
 import tla_utils
-from tree_sitter import Language, Parser
 
 def to_posix(path):
     """
@@ -89,7 +88,6 @@ def generate_new_manifest(examples_root, ignored_dirs, parser, queries):
                                 'runtime': 'unknown',
                                 'size': 'unknown',
                                 'mode': 'exhaustive search',
-                                'config': [],
                                 'features': sorted(list(get_model_features(examples_root, cfg_path))),
                                 'result': 'unknown'
                             }
@@ -138,7 +136,7 @@ def find_corresponding_model(old_model, new_module):
     return models[0] if any(models) else None
 
 def integrate_model_info(old_model, new_model):
-    fields = ['runtime', 'size', 'mode', 'config', 'result']
+    fields = ['runtime', 'size', 'mode', 'result']
     for field in fields:
         new_model[field] = old_model[field]
 

.github/scripts/smoke_test_large_models.py

@@ -38,7 +38,6 @@ def check_model(module_path, model):
         tlapm_lib_path,
         community_jar_path,
         model['mode'],
-        model['config'],
         smoke_test_timeout_in_seconds
     )
     match tlc_result:

.github/scripts/tla_utils.py

@@ -67,14 +67,7 @@ def get_run_mode(mode):
     else:
         raise NotImplementedError(f'Undefined model-check mode {mode}')
 
-def get_config(config):
-    """
-    Converts the model config found in manifest.json into TLC CLI
-    parameters.
-    """
-    return ['-deadlock'] if 'ignore deadlock' in config else []
-
-def check_model(tools_jar_path, module_path, model_path, tlapm_lib_path, community_jar_path, mode, config, hard_timeout_in_seconds):
+def check_model(tools_jar_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.
     """
@@ -98,7 +91,7 @@ def check_model(tools_jar_path, module_path, model_path, tlapm_lib_path, communi
                 '-workers', 'auto',
                 '-lncheck', 'final',
                 '-cleanup'
-            ] + get_config(config) + get_run_mode(mode),
+            ] + get_run_mode(mode),
             timeout=hard_timeout_in_seconds,
             stdout=subprocess.PIPE,
             stderr=subprocess.STDOUT,

README.md

@@ -10,6 +10,8 @@ It serves as:
 
 All TLA<sup>+</sup> 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.
+Beginner-friendly specs can be found by searching for the "beginner" tag in that file.
+Similarly, PlusCal specs can be found by searching for the "pluscal" feature, or "proof" for specs with proofs.
 
 ## List of Examples
 
@@ -171,8 +173,6 @@ Otherwise, follow these directions:
         - `"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
@@ -181,3 +181,4 @@ Otherwise, follow these directions:
     - Other fields are auto-generated by the script; if you are adding an entry manually, ensure their values are present and correct (see other entries or the [`manifest-schema.json`](manifest-schema.json) file)
 
 Before submitted your changes to run in the CI, you can quickly check your [`manifest.json`](manifest.json) for errors and also check it against [`manifest-schema.json`](manifest-schema.json) at https://www.jsonschemavalidator.net/.
+

manifest-schema.json

@@ -44,7 +44,7 @@
                   "items": {
                     "type": "object",
                     "additionalProperties": false,
-                    "required": ["path", "runtime", "size", "mode", "config", "features", "result"],
+                    "required": ["path", "runtime", "size", "mode", "features", "result"],
                     "properties": {
                       "path": {"type": "string"},
                       "runtime": {
@@ -74,13 +74,9 @@
                           }
                         ]
                       },
-                      "config": {
-                        "type": "array",
-                        "items": {"enum": ["ignore deadlock"]}
-                      },
                       "features": {
                         "type": "array",
-                        "items": {"enum": ["liveness", "symmetry", "view", "alias", "state constraint"]}
+                        "items": {"enum": ["liveness", "symmetry", "view", "alias", "state constraint", "ignore deadlock"]}
                       },
                       "result": {"enum": ["success", "safety failure", "liveness failure", "deadlock failure", "unknown"]}
                     }