Partial inductive invariant checking with Apalache.

Checks  SafetyInv  instead of  Inv  because TypeOK's  subsets of subsets of subsets makes Apalache's encoding explode.

Signed-off-by: Markus Alexander Kuppe <[email protected]>

.github/workflows/tla.yml

@@ -23,6 +23,13 @@ jobs:
       - name: Type- and (ordinary) invariant checking with Apalache
         run: |
           ./apalache/bin/apalache-mc check --config=APApbft.cfg APApbft.tla
+      - name: Partial inductive invariant checking with Apalache
+        if: always()
+        run: |
+          # Check that Init => SafetyInv
+          ./apalache/bin/apalache-mc check --config=APApbft.cfg --init=GenInit --inv=SafetyInv --length=0 APApbft.tla
+          # Check that SafetyInv /\ Next => SafetyInv'
+          ./apalache/bin/apalache-mc check --config=APApbft.cfg --init=GenInit --inv=SafetyInv --length=1 APApbft.tla
       - name: Upload Apalache's counterexample (if any)
         uses: actions/upload-artifact@v4
         if: always()

APApbft.cfg

@@ -1,4 +1,8 @@
-SPECIFICATION SpecByz
+\* Switched form  SPECIFICATION SpecByz  to  INIT/NEXT  because Apalache's command-line parameter
+\* --init  are no-ops with  SPECIFICATION SpecByz  .  However, our automation in tla.yml uses
+\* --init  to *redefine* the initial predicate.
+INIT Init
+NEXT NextByz
 
 CONSTANTS
     R <- MC_R
@@ -9,8 +13,6 @@ CONSTANTS
     \* (compare https://github.com/heidihoward/pbft-tlaplus/issues/5#issuecomment-2315767599)
     Tstamps <- MC_Tstamps
     Views <- MC_Views
-
-    Init <- GenInit
 
 INVARIANTS
     TypeOK