Switch to TLC's generate mode to prevent it from generating an acti…

…on's complete set of successor states. Signed-off-by: Markus Alexander Kuppe <[email protected]>
heidihoward · Aug 19, 2024 · 69fd16b · 69fd16b
1 parent b2bba8f
commit 69fd16b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/.github/workflows/tla.yml b/.github/workflows/tla.yml
@@ -43,4 +43,4 @@ jobs:
       - name: Sany
         run: sany *.tla
       - name: Random exploration with TLC
-        run: tlc -workers auto -simulate num=1000 MCpbft.tla
+        run: tlc -workers auto -generate -depth 25 num=1000 MCpbft.tla