From cdebe89eec4b6846b9d1776f8dd38825e3372ead Mon Sep 17 00:00:00 2001
From: Philip Offtermatt <p.offtermatt@gmail.com>
Date: Mon, 18 Sep 2023 16:08:52 +0200
Subject: [PATCH] Revert "Revert "Merge branch 'ph/quint-model-v2' of
 https://github.com/cosmos/interchain-security into ph/quint-model-v2""

This reverts commit 3afd30043e71d866ef8276001e589eeacc4708f9.
---
 tests/difference/core/quint_model/ccv.qnt         | 8 +++++++-
 tests/difference/core/quint_model/extraSpells.qnt | 4 +++-
 2 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt
index 131a490d8a..d18930ae1d 100644
--- a/tests/difference/core/quint_model/ccv.qnt
+++ b/tests/difference/core/quint_model/ccv.qnt
@@ -1,3 +1,4 @@
+-*- mode: Bluespec; -*-
 module ccv {
     import extraSpells.* from "./extraSpells"
 
@@ -5,6 +6,11 @@ module ccv {
     // * Reward distribution
     // * Starting/Stopping chains during execution
     // * Slashes
+
+    // Things that explicitly are modelled:
+    // * Validator set changes are propagated from provider to consumers
+    // * VSC packets mature
+    // * Consumers can be forcefully dropped due to timeouts, or stop on their own volition
     
     // TYPE DEFINITIONS
     type Node = str
@@ -610,4 +616,4 @@ module ccv {
     }
 
 
-}
\ No newline at end of file
+}
diff --git a/tests/difference/core/quint_model/extraSpells.qnt b/tests/difference/core/quint_model/extraSpells.qnt
index a32a74ad8f..cd2105beb7 100644
--- a/tests/difference/core/quint_model/extraSpells.qnt
+++ b/tests/difference/core/quint_model/extraSpells.qnt
@@ -1,3 +1,5 @@
+-*- mode: Bluespec; -*-
+// This module is just a library with utility functions (sometimes called spells in Quint).
 module extraSpells {
 
   pure def prepend(__list: List[a], __elem: a): List[a] = {
@@ -188,4 +190,4 @@ module extraSpells {
         __set.union(Set(elem))
     }
 
-}
\ No newline at end of file
+}