Removed model (.cfg) file features from manifests (#182)

These unnecessary duplicate information readily found in .cfg files
README.md updated with instructions for searching .cfg files for these
features instead of manifest files. This change is meant to facilitate
ease of contribution to this repository.

Signed-off-by: Andrew Helwer <ahelwer@pm.me>

Author: ahelwer

.github/scripts/check_manifest_features.py

@@ -3,7 +3,6 @@
 the manifest.json files. 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
 """
 
@@ -76,34 +75,6 @@ def get_module_features(examples_root, path, parser, queries):
     tree, _, _ = tla_utils.parse_module(examples_root, parser, path)
     return get_tree_features(tree, queries)
 
-# Regexes mapping to features for models
-model_features = {
-    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 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 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
 tlc_modules = {
     'Bags',
@@ -216,14 +187,6 @@ def check_features(parser, queries, manifest, examples_root):
                     + f'expected {list(expected_imports)}, actual {list(actual_imports)}'
                 )
             for model in module['models']:
-                expected_features = get_model_features(examples_root, model['path'])
-                actual_features = set(model['features'])
-                if expected_features != actual_features:
-                    success = False
-                    logging.error(
-                        f'Model {model["path"]} has incorrect features in manifest; '
-                        + f'expected {list(expected_features)}, actual {list(actual_features)}'
-                    )
                 if tla_utils.has_state_count(model) and not tla_utils.is_state_count_valid(model):
                     success = False
                     logging.error(

.github/scripts/check_small_models.py

@@ -49,7 +49,6 @@ def check_model(module, model, expected_runtime):
         community_jar_path,
         model['mode'],
         module['features'],
-        model['features'],
         enable_assertions,
         hard_timeout_in_seconds
     )

.github/scripts/generate_manifest.py

@@ -92,7 +92,6 @@ def generate_new_manifest(examples_root, spec_path, spec_name, parser, queries):
                         'runtime': 'unknown',
                         'size': 'unknown',
                         'mode': 'exhaustive search',
-                        'features': sorted(list(get_model_features(examples_root, cfg_path))),
                         'result': 'unknown'
                     }
                     for cfg_path in sorted(get_cfg_files(examples_root, tla_path))

.github/scripts/record_model_state_space.py

@@ -45,7 +45,6 @@ def check_model(module, model):
         community_jar_path,
         model['mode'],
         module['features'],
-        model['features'],
         enable_assertions,
         hard_timeout_in_seconds
     )

.github/scripts/smoke_test_large_models.py

@@ -46,7 +46,6 @@ def check_model(module, model):
         community_jar_path,
         model['mode'],
         module['features'],
-        model['features'],
         enable_assertions,
         smoke_test_timeout_in_seconds
     )

.github/scripts/tla_utils.py

@@ -115,7 +115,7 @@ def get_run_mode(mode):
     else:
         raise NotImplementedError(f'Undefined model-check mode {mode}')
 
-def get_tlc_feature_flags(module_features, model_features):
+def get_tlc_feature_flags(module_features):
     """
     Selectively enables experimental TLC features according to needs.
     """
@@ -133,7 +133,6 @@ def check_model(
         community_jar_path,
         mode,
         module_features,
-        model_features,
         enable_assertions,
         hard_timeout_in_seconds
     ):
@@ -172,7 +171,7 @@ def check_model(
                     community_jar_path,
                     tlapm_lib_path
                 ]),
-            ] + get_tlc_feature_flags(module_features, model_features)
+            ] + get_tlc_feature_flags(module_features)
             tlc_parameters = [
                 module_path,
                 '-config', model_path,

README.md

@@ -18,9 +18,11 @@ Space contraints limit the information displayed in the table; detailed spec met
 You can search these files for examples exhibiting a number of features, either using the GitHub repository search or locally with the command `ls specifications/*/manifest.json | xargs grep -l $keyword`, where `$keyword` can be a value like:
  - `pluscal`, `proof`, or `action composition` (the `\cdot` operator)
  - Specs intended for trace generation (`generate`), `simulate`, or checked symbolically with Apalache (`symbolic`)
- - Models (`.cfg` files) using the `symmetry`, `view`, `alias`, `state constraint`, or `ignore deadlock` features
  - Models failing in interesting ways, like `deadlock failure`, `safety failure`, `liveness failure`, or `assumption failure`
 
+It is also helpful to consult model files using specific TLC features.
+For this, run `ls specifications/*/*.cfg | xargs grep -l $keyword`, where `$keyword` can be a feature like `SYMMETRY`, `VIEW`, `ALIAS`, `CONSTRAINT`, or `DEADLOCK`.
+
 ## Validated Examples Included Here
 Here is a list of specs included in this repository which are validated by the CI, with links to the relevant directory and flags for various features:
 | Name                                                                                                | Author(s)                                           | Beginner | TLAPS Proof | PlusCal | TLC Model | Apalache |

manifest-schema.json

@@ -40,7 +40,7 @@
             "items": {
               "type": "object",
               "additionalProperties": false,
-              "required": ["path", "runtime", "size", "mode", "features", "result"],
+              "required": ["path", "runtime", "size", "mode", "result"],
               "properties": {
                 "path": {"type": "string"},
                 "runtime": {
@@ -73,10 +73,6 @@
                     }
                   ]
                 },
-                "features": {
-                  "type": "array",
-                  "items": {"enum": ["liveness", "symmetry", "view", "alias", "state constraint", "ignore deadlock"]}
-                },
                 "result": {"enum": ["success", "assumption failure", "deadlock failure", "safety failure", "liveness failure", "unknown"]}
               }
             }

specifications/Bakery-Boulangerie/manifest.json

@@ -40,9 +40,6 @@
           "runtime": "00:00:10",
           "size": "small",
           "mode": "exhaustive search",
-          "features": [
-            "ignore deadlock"
-          ],
           "result": "success",
           "distinctStates": 655200,
           "totalStates": 3403584,
@@ -61,9 +58,6 @@
           "runtime": "00:01:00",
           "size": "medium",
           "mode": "exhaustive search",
-          "features": [
-            "state constraint"
-          ],
           "result": "success"
         }
       ]

specifications/CarTalkPuzzle/manifest.json

@@ -35,7 +35,6 @@
           "runtime": "00:00:01",
           "size": "small",
           "mode": "exhaustive search",
-          "features": [],
           "result": "success",
           "distinctStates": 0,
           "totalStates": 0,
@@ -61,7 +60,6 @@
           "runtime": "00:00:05",
           "size": "small",
           "mode": "exhaustive search",
-          "features": [],
           "result": "success",
           "distinctStates": 0,
           "totalStates": 0,
@@ -87,7 +85,6 @@
           "runtime": "unknown",
           "size": "large",
           "mode": "exhaustive search",
-          "features": [],
           "result": "unknown"
         }
       ]