From 3f9996006add8399ebb92a708a949b82b357b9b8 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 4 Sep 2024 08:54:00 -0700 Subject: [PATCH] Do not parse *all* specs because Apalache module is not there. Signed-off-by: Markus Alexander Kuppe --- .github/workflows/tla.yml | 4 ---- 1 file changed, 4 deletions(-) diff --git a/.github/workflows/tla.yml b/.github/workflows/tla.yml index b00a499..1e84217 100644 --- a/.github/workflows/tla.yml +++ b/.github/workflows/tla.yml @@ -91,8 +91,6 @@ jobs: cd tla-bin ./download_or_update_tla.sh --nightly sudo ./install.sh - - name: Sany - run: sany *.tla - name: Random generation with TLC run: JAVA_OPTS="-Dtlc2.TLC.stopAfter=600 -XX:+UseParallelGC" tlc -workers auto -generate MCpbft.tla @@ -106,7 +104,5 @@ jobs: cd tla-bin ./download_or_update_tla.sh --nightly sudo ./install.sh - - name: Sany - run: sany *.tla - name: Random simulation with TLC run: JAVA_OPTS="-Dtlc2.TLC.stopAfter=600 -XX:+UseParallelGC" tlc -workers auto -simulate MCpbft.tla \ No newline at end of file