From d103bdafd46a8f0a46837e47e1565e820ddd19b3 Mon Sep 17 00:00:00 2001
From: Philip Offtermatt <p.offtermatt@gmail.com>
Date: Fri, 8 Dec 2023 10:55:24 +0100
Subject: [PATCH] Add Quint tests to CI

---
 .github/workflows/test.yml | 20 ++++++++++++++++++++
 Makefile                   | 10 ++++++++++
 2 files changed, 30 insertions(+)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 9876f48888..39cfffbb17 100644
--- 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/get-diff-action@v6.1.2
+        id: git_diff
+        with:
+          PATTERNS: |
+            tests/mbt/model/**.qnt
+      - name: verify the Quint model
+        run: make verify-models
diff --git a/Makefile b/Makefile
index 57110fd3b0..dfa42b3e82 100644
--- 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                                  ###
 ###############################################################################