Add Quint tests to CI

cosmos · Dec 8, 2023 · d103bda · d103bda
1 parent e730ebf
commit d103bda
Show file tree

Hide file tree

Showing 2 changed files with 30 additions and 0 deletions.
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
@@ -248,3 +248,23 @@ jobs:
             Makefile
       - name: trace-e2e tests
         run: make test-trace
+  model-analysis:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          lfs: true
+      - name: checkout LFS objects
+        run: git lfs checkout
+      - uses: actions/setup-node@v4
+        with:
+          node-version: ">= 18"
+          check-latest: true
+      - run: npm i @informalsystems/quint -g
+      - uses: technote-space/[email protected]
+        id: git_diff
+        with:
+          PATTERNS: |
+            tests/mbt/model/**.qnt
+      - name: verify the Quint model
+        run: make verify-models
diff --git a/Makefile b/Makefile
@@ -105,6 +105,16 @@ test-no-cache:
 test-trace:
 	go run ./tests/e2e/... --test-file tests/e2e/tracehandler_testdata/happyPath.json::default
 
+# tests and verifies the Quint models.
+# Note: this is *not* using the Quint models to test the system,
+# this tests/verifies the Quint models *themselves*.
+verify-models:
+	quint test tests/mbt/model/ccv_test.qnt;\
+	quint test tests/mbt/model/ccv_model.qnt;\
+	quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" tests/mbt/model/ccv_model.qnt --max-steps 200 --max-samples 200
+
+
+
 ###############################################################################
 ###                                Linting                                  ###
 ###############################################################################