From 9f76bc22d363090d5cdb6038ee086f0d96db1714 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 18 Aug 2026 09:47:27 -0700 Subject: [PATCH] CI: fix the guard that skips Apalache on Unicode specs [ ${{ matrix.unicode }} ] is a single-argument test asking whether the string is non-empty, which both true and false are, so --skip_apalache reached every job. No small symbolic model has been checked since 38f89e1 added the flag; f1aaf96 recorded the truthiness the same day without fixing it. The two symbolic models above the 30s threshold, APFlashWithMutex and APGermanData, are smoke-tested rather than checked. That step allows five seconds and counts a timeout as success, so it only detects Apalache failing to start, which is all it caught when Apalache raised its minimum JVM. Also raise the hard timeout for symbolic models to 120s. APbosco takes 42s on the macOS runners and APtcp 32s, and the 60s that suffices for TLC does not cover Apalache's JVM and solver startup. Raising it rather than recording the measured runtimes, because the 30s threshold would then move these two models into smoke_test_large_models.py, where an Apalache model degenerates into a check that the launcher boots. Co-authored-by: Claude Opus 5 Signed-off-by: Markus Alexander Kuppe --- .github/scripts/check_small_models.py | 4 +++- .github/workflows/CI.yml | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/.github/scripts/check_small_models.py b/.github/scripts/check_small_models.py index 001e9f77..dce0071b 100644 --- a/.github/scripts/check_small_models.py +++ b/.github/scripts/check_small_models.py @@ -41,7 +41,9 @@ 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 + # Apalache pays for JVM and solver startup before the bounded check + # begins, so symbolic models need more room than TLC ones. + hard_timeout_in_seconds = 120 if model['mode'] == 'symbolic' else 60 start_time = timer() tlc_result = tla_utils.check_model( tools_jar_path, diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index 6ea2d533..8597a146 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -117,7 +117,7 @@ jobs: # Apalache does not yet support Unicode specs: # https://github.com/apalache-mc/apalache/issues/2995 APALACHE_FLAG=() - if [ ${{ matrix.unicode }} ]; then + if [[ "${{ matrix.unicode }}" == 'true' ]]; then APALACHE_FLAG+=("--skip_apalache") fi python $SCRIPT_DIR/check_small_models.py \