manual.yml offers a simple way to run TLC on the specs in run.sh.

* Include TLC's ungarbled output
* Print command-line parameters
* Set TLC's command-line parameters at the spec level
* Assert exit/return values

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

Author: lemmy

.github/workflows/manual.yml

@@ -0,0 +1,23 @@
+name: CI
+
+on: [workflow_dispatch]
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v1
+    - name: Get (nightly) TLC
+      run: wget https://nightly.tlapl.us/dist/tla2tools.jar
+    - name: Get (nightly) CommunityModules
+      run: wget https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar
+    - name: Get TLAPS modules
+      run: |
+        wget https://raw.githubusercontent.com/tlaplus/tlapm/main/library/TLAPS.tla
+        wget https://raw.githubusercontent.com/tlaplus/tlapm/main/library/FunctionTheorems.tla
+        wget https://raw.githubusercontent.com/tlaplus/tlapm/main/library/FiniteSetTheorems.tla
+        wget https://raw.githubusercontent.com/tlaplus/tlapm/main/library/WellFoundedInduction.tla
+        wget https://raw.githubusercontent.com/tlaplus/tlapm/main/library/NaturalsInduction.tla
+        wget https://raw.githubusercontent.com/tlaplus/tlapm/main/library/SequenceTheorems.tla
+    - name: Run
+      run: /bin/bash .github/workflows/run.sh

.github/workflows/run.sh

@@ -1,9 +1,35 @@
 #!/bin/bash
 
-TLC_COMMAND="java -Dtlc2.TLC.stopAfter=180 -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=abcdef60f238424fa70d124d0c77ffff -cp tla2tools.jar tlc2.TLC -workers auto -lncheck final -tool -deadlock"
+set -ex
 
-echo Check EWD840
-$TLC_COMMAND specifications/ewd840/EWD840
+TLC_COMMAND="java -ea -XX:+UseParallelGC -Dtlc2.TLC.stopAfter=180 -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=abcdef60f238424fa70d124d0c77ffff -cp tla2tools.jar tlc2.TLC -workers auto -lncheck final -tool -deadlock"
+
+echo Check specifications/aba-asyn-byz/aba_asyn_byz
+$TLC_COMMAND specifications/aba-asyn-byz/aba_asyn_byz
+echo Check Constrain_CRDT
+$TLC_COMMAND specifications/FiniteMonotonic/Constrain_CRDT
+echo Check Finitize_CRDT
+$TLC_COMMAND specifications/FiniteMonotonic/Finitize_CRDT
+echo Check Finitize_ReplicatedLog
+$TLC_COMMAND specifications/FiniteMonotonic/Finitize_ReplicatedLog
+echo Check specifications/KeyValueStore/MCKVsnap
+$TLC_COMMAND specifications/KeyValueStore/MCKVsnap
+echo Check specifications/LoopInvariance/MCBinarySearch
+$TLC_COMMAND specifications/LoopInvariance/MCBinarySearch
+echo Check specifications/LoopInvariance/MCQuicksort
+$TLC_COMMAND specifications/LoopInvariance/MCQuicksort
+echo Check specifications/MisraReachability/MCParReach
+$TLC_COMMAND specifications/MisraReachability/MCParReach
+echo Check specifications/MisraReachability/MCReachable
+$TLC_COMMAND specifications/MisraReachability/MCReachable
+echo Check specifications/SDP_Verification/SDP_Attack_New_Solution_Spec/MC
+$TLC_COMMAND specifications/SDP_Verification/SDP_Attack_New_Solution_Spec/MC
+echo Check specifications/SingleLaneBridge/MC
+$TLC_COMMAND specifications/SingleLaneBridge/MC
+echo Check specifications/SpanningTree/SpanTree
+$TLC_COMMAND specifications/SpanningTree/SpanTree
+echo Check specifications/acp/ACP_NB_TLC
+$TLC_COMMAND specifications/acp/ACP_NB_TLC
 echo Check CarTalkPuzzle Model_1
 $TLC_COMMAND specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_1/MC
 echo Check CarTalkPuzzle Model_2
@@ -16,8 +42,6 @@ echo Check DiningPhilosophers
 $TLC_COMMAND specifications/DiningPhilosophers/DiningPhilosophers
 echo Check TransitiveClosure
 $TLC_COMMAND specifications/TransitiveClosure/TransitiveClosure
-echo Check Hanoi
-java -Dtlc2.TLC.stopAfter=600 -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=abcdef60f238424fa70d124d0c77ffff -cp tla2tools.jar:specifications/tower_of_hanoi/Hanoi.toolbox/Model_1/MC tlc2.TLC -workers auto -lncheck final -tool -deadlock specifications/tower_of_hanoi/Hanoi.toolbox/Model_1/MC
 echo Check MCEcho
 $TLC_COMMAND specifications/echo/MCEcho
 echo Check Prisoners
@@ -26,10 +50,6 @@ echo Check LSpec-model
 $TLC_COMMAND specifications/dijkstra-mutex/DijkstraMutex.toolbox/LSpec-model/MC
 echo Check Safety-4-processors
 $TLC_COMMAND specifications/dijkstra-mutex/DijkstraMutex.toolbox/Safety-4-processors/MC
-## This spec used to be accepted by Apalache, but since Apalache has started to require type annotations for all variables.
-## https://github.com/tlaplus/Examples/pull/31#issuecomment-796354291
-#echo Check EinsteinRiddle
-#$TLC_COMMAND  specifications/EinsteinRiddle/Einstein
 echo Check MCInnerSequential
 $TLC_COMMAND specifications/SpecifyingSystems/AdvancedExamples/MCInnerSequential
 #echo Check MCInnerSerial
@@ -68,8 +88,6 @@ echo Check EWD840_anim
 $TLC_COMMAND -simulate num=1 specifications/ewd840/EWD840_anim || (($? == 12))  ## Expect a safety violation
 echo Check SyncTerminationDetection
 $TLC_COMMAND specifications/ewd840/SyncTerminationDetection
-echo Check EWD840
-$TLC_COMMAND specifications/ewd840/EWD840
 echo Check EWD840_json
 sed -i '/^SendMsg/{n;d;}' specifications/ewd840/EWD840.tla ## Cause RealInv to be violated (see EWD840_json.tla)
 $TLC_COMMAND specifications/ewd840/EWD840_json
@@ -96,9 +114,9 @@ $TLC_COMMAND specifications/allocator/SimpleAllocator
 echo Check AllocatorImplementation
 $TLC_COMMAND specifications/allocator/AllocatorImplementation
 echo Check FourQueens
-$TLC_COMMAND specifications/N-Queens/Queens.toolbox/FourQueens/MC
+$TLC_COMMAND specifications/N-Queens/Queens.toolbox/FourQueens/MC || (($? == 12))  ## Expect a safety violation
 echo Check FourQueens PlusCal
-$TLC_COMMAND specifications/N-Queens/QueensPluscal.toolbox/FourQueens/MC
+$TLC_COMMAND specifications/N-Queens/QueensPluscal.toolbox/FourQueens/MC || (($? == 12))  ## Expect a safety violation
 echo Check ReadersWriters
 $TLC_COMMAND specifications/ReadersWriters/MC
 echo Check EWD687a