Manifest: removed model size field in favor of runtime

Also remove tlaLanguageVersion field

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

Author: ahelwer

.github/scripts/check_small_models.py

@@ -1,10 +1,11 @@
 """
-Check all models marked as size "small" in each manifest with TLC. Small
+Check all models with less than 30 second recorded runtime with TLC. Small
 models should finish executing in less than ten seconds on the GitHub CI
 machines.
 """
 
 from argparse import ArgumentParser
+from datetime import timedelta
 import logging
 from os.path import dirname, normpath
 from subprocess import CompletedProcess, TimeoutExpired
@@ -53,9 +54,9 @@ def check_model(module, model, expected_runtime):
         hard_timeout_in_seconds
     )
     end_time = timer()
-    output = ' '.join(tlc_result.args) + '\n' + tlc_result.stdout
     match tlc_result:
         case CompletedProcess():
+            output = ' '.join(tlc_result.args) + '\n' + tlc_result.stdout
             logging.info(f'{model_path} in {end_time - start_time:.1f}s vs. {expected_runtime.seconds}s expected')
             expected_result = model['result']
             actual_result = tla_utils.resolve_tlc_exit_code(tlc_result.returncode)
@@ -77,6 +78,8 @@ def check_model(module, model, expected_runtime):
             logging.debug(output)
             return True
         case TimeoutExpired():
+            args, _ = tlc_result.args
+            output = ' '.join(args) + '\n' + tlc_result.stdout
             logging.error(f'{model_path} hit hard timeout of {hard_timeout_in_seconds} seconds')
             logging.error(output)
             return False
@@ -88,11 +91,11 @@ def check_model(module, model, expected_runtime):
 manifest = tla_utils.load_all_manifests(examples_root)
 small_models = sorted(
     [
-        (module, model, tla_utils.parse_timespan(model['runtime']))
+        (module, model, runtime)
         for path, spec in manifest
         for module in spec['modules']
         for model in module['models']
-            if model['size'] == 'small'
+            if (runtime := tla_utils.parse_timespan(model['runtime'])) <= timedelta(seconds=30)
             and model['path'] not in skip_models
             and (only_models == [] or model['path'] in only_models)
     ],

.github/scripts/generate_manifest.py

@@ -3,7 +3,7 @@
 .tla and .cfg files in the specifications dir then attempting to sort them
 into a spec/module/model hierarchy. Files are parsed to check for features
 and imports. Human-written fields (title/description/source/authors for
-specs, runtime/size/result for models) are either taken from any existing
+specs, runtime & result for models) are either taken from any existing
 manifest.json file or set as blank/unknown as appropriate.
 """
 
@@ -73,13 +73,11 @@ def generate_new_manifest(examples_root, spec_path, spec_name, parser, queries):
             {
                 'path': tla_utils.to_posix(tla_path),
                 'communityDependencies': sorted(list(get_community_module_imports(examples_root, parser, tla_path, queries))),
-                'tlaLanguageVersion': 2,
                 'features': sorted(list(get_module_features(examples_root, tla_path, parser, queries))),
                 'models': [
                     {
                         'path': tla_utils.to_posix(cfg_path),
                         'runtime': 'unknown',
-                        'size': 'unknown',
                         'mode': 'exhaustive search',
                         'result': 'unknown'
                     }
@@ -109,7 +107,7 @@ def find_corresponding_module(old_module, new_spec):
     return modules[0] if any(modules) else None
 
 def integrate_module_info(old_module, new_module):
-    fields = ['tlaLanguageVersion']
+    fields = []
     for field in fields:
         new_module[field] = old_module[field]
 
@@ -121,7 +119,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', 'result', 'distinctStates', 'totalStates', 'stateDepth']
+    fields = ['runtime', 'mode', 'result', 'distinctStates', 'totalStates', 'stateDepth']
     for field in fields:
         if field in old_model:
             new_model[field] = old_model[field]

.github/scripts/record_model_state_space.py

@@ -4,6 +4,7 @@
 """
 
 from argparse import ArgumentParser
+from datetime import timedelta
 import logging
 from os.path import dirname, normpath, join
 from subprocess import CompletedProcess, TimeoutExpired
@@ -78,11 +79,11 @@ def check_model(module, model):
 manifest = tla_utils.load_all_manifests(examples_root)
 small_models = sorted(
     [
-        (spec, module, model, tla_utils.parse_timespan(model['runtime']))
+        (path, spec, module, model, runtime)
         for path, spec in manifest
         for module in spec['modules']
         for model in module['models']
-            if model['size'] == 'small'
+        if (runtime := tla_utils.parse_timespan(model['runtime'])) <= timedelta(seconds=30)
             and tla_utils.is_state_count_valid(model)
             # This model is nondeterministic due to use of the Random module
             and model['path'] != 'specifications/SpanningTree/SpanTreeRandom.cfg'
@@ -96,15 +97,15 @@ def check_model(module, model):
                 or 'stateDepth' not in model
             ))
     ],
-    key = lambda m: m[3],
+    key = lambda m: m[4],
     reverse=True
 )
 
 for path in skip_models:
     logging.info(f'Skipping {path}')
 
-for spec, module, model, _ in small_models:
-    manifest_path = join(spec['path'], 'manifest.json')
+for manifest_dir, spec, module, model, _ in small_models:
+    manifest_path = join(manifest_dir, 'manifest.json')
     success = check_model(module, model)
     if not success:
         exit(1)

.github/scripts/smoke_test_large_models.py

@@ -1,10 +1,11 @@
 """
-Smoke-test all models not marked as size "small" in each manifest. This
+Smoke-test all models with runtime greater than thirty seconds. This
 entails running them for five seconds to ensure they can actually start
 and work with the spec they're supposed to be modeling.
 """
 
 from argparse import ArgumentParser
+from datetime import timedelta
 import logging
 import os
 from os.path import dirname, normpath
@@ -62,7 +63,7 @@ def check_model(module, model):
             return True
         case CompletedProcess():
             output = ' '.join(tlc_result.args) + '\n' + tlc_result.stdout
-            logging.warning(f'Model {model_path} finished quickly, within {smoke_test_timeout_in_seconds} seconds; consider labeling it a small model')
+            logging.warning(f'Model {model_path} finished quickly, within {smoke_test_timeout_in_seconds} seconds; consider updating recorded runtime')
             expected_result = model['result']
             actual_result = tla_utils.resolve_tlc_exit_code(tlc_result.returncode)
             if expected_result == actual_result:
@@ -85,7 +86,7 @@ def check_model(module, model):
     for path, spec in manifest
     for module in spec['modules']
     for model in module['models']
-        if model['size'] != 'small'
+        if tla_utils.parse_timespan(model['runtime']) > timedelta(seconds=30)
         and model['path'] not in skip_models
         and (only_models == [] or model['path'] in only_models)
 ]

.github/scripts/tla_utils.py

@@ -1,5 +1,6 @@
 import locale
 from datetime import datetime
+from datetime import timedelta
 import json
 from os.path import join, normpath, pathsep, dirname
 from pathlib import PureWindowsPath
@@ -101,10 +102,11 @@ def node_to_string(module_bytes, node):
 
 def parse_timespan(unparsed):
     """
-    Parses the timespan format used in the manifest.json format.
+    Parses the timespan format used in the manifest.json format. If unknown,
+    return the maximum possible timespan.
     """
     pattern = '%H:%M:%S'
-    return datetime.strptime(unparsed, pattern) - datetime.strptime('00:00:00', pattern)
+    return timedelta.max if unparsed == 'unknown' else datetime.strptime(unparsed, pattern) - datetime.strptime('00:00:00', pattern)
 
 def get_run_mode(mode):
     """

CONTRIBUTING.md

@@ -32,7 +32,7 @@ All specs & models in this repository are subject to many validation checks; for
 While many of these checks concern basic properties like whether the spec parses properly and its models do not crash, they also check whether the spec correctly reflects metadata stored about it in the spec's `manifest.json` file and a table in [`README.md`](README.md).
 
 CI validation requires creating a `manifest.json` metadata file in your specification's root directory.
-This can either be done manually (by looking at existing examples) or largely automated using the instructions below; note that if done manually you are very likely to miss tagging your spec with some feature flags detected & enforced by the CI.
+This can either be done manually (by looking at existing examples) or largely automated using the instructions below; note that if done manually might miss tagging your spec with some feature flags detected & enforced by the CI.
 Before submitted your changes to run in the CI, you can quickly check your `manifest.json` against the schema [`manifest-schema.json`](manifest-schema.json) at https://www.jsonschemavalidator.net/.
 Steps:
 
@@ -41,17 +41,12 @@ Steps:
 1. Run `pip install -r .github/scripts/requirements.txt`
 1. Run `python .github/scripts/generate_manifest.py` to auto-generate your spec's `manifest.json` file with as many details as possible
 1. Locate your spec directory's `manifest.json` file and ensure the following fields are filled out:
-   - Spec title: an appropriate title for your specification
-   - Spec description: a short description of your specification
    - Spec sources: links relevant to the source of the spec (papers, blog posts, repositories)
    - Spec authors: a list of people who authored the spec
    - Spec tags:
      - `"beginner"` if your spec is appropriate for TLA⁺ newcomers
    - Model runtime: approximate model runtime on an ordinary workstation, in `"HH:MM:SS"` format
-   - Model size:
-     - `"small"` if the model can be executed in less than 10 seconds
-     - `"medium"` if the model can be executed in less than five minutes
-     - `"large"` if the model takes more than five minutes to execute
+     - If less than 30 seconds, will be run in its entirety by the CI; otherwise will only be smoke-tested for 5 seconds
    - Model mode:
      - `"exhaustive search"` by default
      - `{"simulate": {"traceCount": N}}` for a simulation model
@@ -68,7 +63,7 @@ Steps:
      - Recording these turns your model into a powerful regression test for TLC
    - 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)
 1. Add your spec somewhere in the **topmost** table (not the bottom one, don't get them mixed up!) in [`README.md`](README.md); this must have:
-   - The spec name as a link to the spec's directory, matching the name in the `manifest.json`
+   - The spec name as a link to the spec's directory
    - A comma-separated list of authors, which must also match the list of authors in the `manifest.json`
    - A checkmark indicating whether the spec is appropriate for beginners
      - Checked IFF (if and only if) `beginner` is present in the `tags` field of your spec in `manifest.json`

manifest-schema.json

@@ -19,15 +19,14 @@
       "type": "array",
       "items": {
         "type": "object",
-        "required": ["path", "communityDependencies", "tlaLanguageVersion", "features", "models"],
+        "required": ["path", "communityDependencies", "features", "models"],
         "additionalProperties": false,
         "properties": {
           "path": {"type": "string"},
           "communityDependencies": {
             "type": "array",
             "items": {"type": "string"}
           },
-          "tlaLanguageVersion": {"type": "number"},
           "features": {
             "type": "array",
             "items": {"enum": ["pluscal", "proof", "action composition"]}
@@ -37,14 +36,13 @@
             "items": {
               "type": "object",
               "additionalProperties": false,
-              "required": ["path", "runtime", "size", "mode", "result"],
+              "required": ["path", "runtime", "mode", "result"],
               "properties": {
                 "path": {"type": "string"},
                 "runtime": {
                   "type": "string",
                   "pattern": "^(([0-9][0-9]:[0-9][0-9]:[0-9][0-9])|unknown)$"
                 },
-                "size": {"enum": ["small", "medium", "large", "unknown"]},
                 "distinctStates": {"type": "integer"},
                 "totalStates": {"type": "integer"},
                 "stateDepth": {"type": "integer"},

specifications/Bakery-Boulangerie/manifest.json

@@ -9,7 +9,6 @@
     {
       "path": "specifications/Bakery-Boulangerie/Bakery.tla",
       "communityDependencies": [],
-      "tlaLanguageVersion": 2,
       "features": [
         "pluscal",
         "proof"
@@ -19,7 +18,6 @@
     {
       "path": "specifications/Bakery-Boulangerie/Boulanger.tla",
       "communityDependencies": [],
-      "tlaLanguageVersion": 2,
       "features": [
         "pluscal",
         "proof"
@@ -29,13 +27,11 @@
     {
       "path": "specifications/Bakery-Boulangerie/MCBakery.tla",
       "communityDependencies": [],
-      "tlaLanguageVersion": 2,
       "features": [],
       "models": [
         {
           "path": "specifications/Bakery-Boulangerie/MCBakery.cfg",
           "runtime": "00:00:10",
-          "size": "small",
           "mode": "exhaustive search",
           "result": "success",
           "distinctStates": 655200,
@@ -47,13 +43,11 @@
     {
       "path": "specifications/Bakery-Boulangerie/MCBoulanger.tla",
       "communityDependencies": [],
-      "tlaLanguageVersion": 2,
       "features": [],
       "models": [
         {
           "path": "specifications/Bakery-Boulangerie/MCBoulanger.cfg",
           "runtime": "00:01:00",
-          "size": "medium",
           "mode": "exhaustive search",
           "result": "success"
         }

specifications/CarTalkPuzzle/manifest.json

@@ -10,27 +10,23 @@
     {
       "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.tla",
       "communityDependencies": [],
-      "tlaLanguageVersion": 2,
       "features": [],
       "models": []
     },
     {
       "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_1/CarTalkPuzzle.tla",
       "communityDependencies": [],
-      "tlaLanguageVersion": 2,
       "features": [],
       "models": []
     },
     {
       "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_1/MC.tla",
       "communityDependencies": [],
-      "tlaLanguageVersion": 2,
       "features": [],
       "models": [
         {
           "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_1/MC.cfg",
           "runtime": "00:00:01",
-          "size": "small",
           "mode": "exhaustive search",
           "result": "success",
           "distinctStates": 0,
@@ -42,20 +38,17 @@
     {
       "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_2/CarTalkPuzzle.tla",
       "communityDependencies": [],
-      "tlaLanguageVersion": 2,
       "features": [],
       "models": []
     },
     {
       "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_2/MC.tla",
       "communityDependencies": [],
-      "tlaLanguageVersion": 2,
       "features": [],
       "models": [
         {
           "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_2/MC.cfg",
           "runtime": "00:00:05",
-          "size": "small",
           "mode": "exhaustive search",
           "result": "success",
           "distinctStates": 0,
@@ -67,20 +60,17 @@
     {
       "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_3/CarTalkPuzzle.tla",
       "communityDependencies": [],
-      "tlaLanguageVersion": 2,
       "features": [],
       "models": []
     },
     {
       "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_3/MC.tla",
       "communityDependencies": [],
-      "tlaLanguageVersion": 2,
       "features": [],
       "models": [
         {
           "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_3/MC.cfg",
           "runtime": "unknown",
-          "size": "large",
           "mode": "exhaustive search",
           "result": "unknown"
         }

specifications/Chameneos/manifest.json

@@ -10,13 +10,11 @@
     {
       "path": "specifications/Chameneos/Chameneos.tla",
       "communityDependencies": [],
-      "tlaLanguageVersion": 2,
       "features": [],
       "models": [
         {
           "path": "specifications/Chameneos/Chameneos.cfg",
           "runtime": "00:00:01",
-          "size": "small",
           "mode": "exhaustive search",
           "result": "success",
           "distinctStates": 34534,