TLC: capture stderr, print captured output on hard timeout (#86)

* TLC: capture stderr, print captured output on hard timeout
* Reclassified some models as small
* Updated to checkoutv3 to silence node runtime warnings

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

.github/scripts/check_small_models.py

@@ -7,16 +7,10 @@
 from argparse import ArgumentParser
 import logging
 from os.path import dirname, normpath
+from subprocess import CompletedProcess, TimeoutExpired
 from timeit import default_timer as timer
 import tla_utils
 
-tlc_result = {
-    0   : 'success',
-    11  : 'deadlock failure',
-    12  : 'safety failure',
-    13  : 'liveness failure'
-}
-
 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('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=True)
@@ -36,29 +30,36 @@ def check_model(module_path, 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)
-    expected_result = model['result']
+    hard_timeout_in_seconds = 60
     start_time = timer()
-    tlc, hit_timeout = tla_utils.check_model(
+    tlc_result = tla_utils.check_model(
         tools_jar_path,
         module_path,
         model_path,
         tlapm_lib_path,
         community_jar_path,
         model['mode'],
         model['config'],
-        60
+        hard_timeout_in_seconds
     )
     end_time = timer()
-    if hit_timeout:
-        logging.error(f'{model_path} timed out')
-        return False
-    logging.info(f'{model_path} in {end_time - start_time:.1f}s vs. {expected_runtime.seconds}s expected')
-    actual_result = tlc_result[tlc.returncode] if tlc.returncode in tlc_result else str(tlc.returncode)
-    if expected_result != actual_result:
-        logging.error(f'Model {model_path} expected result {expected_result} but got {actual_result}')
-        logging.error(tlc.stdout.decode('utf-8'))
-        return False
-    return True
+    match tlc_result:
+        case CompletedProcess():
+            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)
+            if expected_result != actual_result:
+                logging.error(f'Model {model_path} expected result {expected_result} but got {actual_result}')
+                logging.error(tlc_result.stdout)
+                return False
+            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'))
+            return False
+        case _:
+            logging.error(f'Unhandled TLC result type {type(tlc_result)}: {tlc_result}')
+            return False
 
 # Ensure longest-running modules go first
 manifest = tla_utils.load_json(manifest_path)

.github/scripts/smoke_test_large_models.py

@@ -8,6 +8,7 @@
 import logging
 import os
 from os.path import dirname, normpath
+from subprocess import CompletedProcess, TimeoutExpired
 import tla_utils
 
 parser = ArgumentParser(description='Smoke-tests all larger TLA+ models in the tlaplus/examples repo using TLC.')
@@ -27,23 +28,32 @@ def check_model(module_path, 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)
-    tlc, hit_timeout = tla_utils.check_model(
+    smoke_test_timeout_in_seconds = 5
+    tlc_result = tla_utils.check_model(
         tools_jar_path,
         module_path,
         model_path,
         tlapm_lib_path,
         community_jar_path,
         model['mode'],
         model['config'],
-        5
+        smoke_test_timeout_in_seconds
     )
-    if hit_timeout:
-        return True
-    if 0 != tlc.returncode:
-        logging.error(f'Model {model_path} expected error code 0 but got {tlc.returncode}')
-        logging.error(tlc.stdout.decode('utf-8'))
-        return False
-    return True
+    match tlc_result:
+        case TimeoutExpired():
+            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')
+            expected_result = model['result']
+            actual_result = tla_utils.resolve_tlc_exit_code(tlc_result.returncode)
+            if expected_result != actual_result:
+                logging.error(f'Model {model_path} expected result {expected_result} but got {actual_result}')
+                logging.error(tlc_result.stdout)
+                return False
+            return True
+        case _:
+            logging.error(f'Unhandled TLC result type {type(tlc_result)}: {tlc_result}')
+            return False
 
 logging.basicConfig(level=logging.INFO)
 

.github/scripts/tla_utils.py

@@ -74,7 +74,7 @@ def get_config(config):
     """
     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, timeout):
+def check_model(tools_jar_path, module_path, model_path, tlapm_lib_path, community_jar_path, mode, config, hard_timeout_in_seconds):
     """
     Model-checks the given model against the given module.
     """
@@ -99,10 +99,26 @@ def check_model(tools_jar_path, module_path, model_path, tlapm_lib_path, communi
                 '-lncheck', 'final',
                 '-cleanup'
             ] + get_config(config) + get_run_mode(mode),
-            capture_output=True,
-            timeout=timeout
+            timeout=hard_timeout_in_seconds,
+            stdout=subprocess.PIPE,
+            stderr=subprocess.STDOUT,
+            text=True
         )
-        return (tlc, False)
-    except subprocess.TimeoutExpired:
-        return (None, True)
+        return tlc
+    except subprocess.TimeoutExpired as e:
+        return e
+
+def resolve_tlc_exit_code(code):
+    """
+    Resolves TLC's exit code to a standardized human-readable form.
+    Returns the stringified exit code number if unknown.
+    """
+    tlc_exit_codes = {
+        0   : 'success',
+        11  : 'deadlock failure',
+        12  : 'safety failure',
+        13  : 'liveness failure'
+    }
+
+    return tlc_exit_codes[code] if code in tlc_exit_codes else str(code)
 

.github/workflows/CI.yml

@@ -28,7 +28,7 @@ jobs:
         shell: bash
     steps:
       - name: Clone repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
       - name: Install python
         uses: actions/setup-python@v4
         with:

manifest.json

@@ -2886,15 +2886,15 @@
           "models": [
             {
               "path": "specifications/ewd426/TokenRing.cfg",
-              "runtime": "unknown",
-              "size": "unknown",
+              "runtime": "00:00:05",
+              "size": "small",
               "mode": "exhaustive search",
               "config": [],
               "features": [
                 "alias",
                 "liveness"
               ],
-              "result": "unknown"
+              "result": "success"
             }
           ]
         }
@@ -3202,8 +3202,8 @@
           "models": [
             {
               "path": "specifications/ewd998/EWD998ChanID.cfg",
-              "runtime": "unknown",
-              "size": "large",
+              "runtime": "00:00:05",
+              "size": "small",
               "mode": "exhaustive search",
               "config": [
                 "ignore deadlock"
@@ -3213,7 +3213,7 @@
                 "state constraint",
                 "view"
               ],
-              "result": "unknown"
+              "result": "success"
             }
           ]
         },
@@ -3315,8 +3315,8 @@
           "models": [
             {
               "path": "specifications/ewd998/SmokeEWD998.cfg",
-              "runtime": "unknown",
-              "size": "large",
+              "runtime": "00:00:05",
+              "size": "small",
               "mode": {
                 "simulate": {
                   "traceCount": 100
@@ -3327,7 +3327,7 @@
                 "liveness",
                 "state constraint"
               ],
-              "result": "unknown"
+              "result": "success"
             }
           ]
         },
@@ -3656,4 +3656,4 @@
       ]
     }
   ]
-}
+}