Use -1 as last timestamp when no block was comitted

cosmos · Nov 28, 2023 · f229db7 · f229db7
1 parent 8681895
commit f229db7
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt
@@ -55,7 +55,7 @@ module ccv_types {
         {
             votingPowerHistory: List(),
             currentValidatorSet: Map(),
-            lastTimestamp: 0,
+            lastTimestamp: -1, // last timestamp -1 means that in the model, there was no block comitted on chain yet.
             runningTimestamp: 0,
         }
 

diff --git a/tests/difference/core/quint_model/ccv_model.qnt b/tests/difference/core/quint_model/ccv_model.qnt
@@ -464,7 +464,8 @@ module ccv_model {
                 assert(currentState.consumerStates.keys() == consumerChains),
                 assert(currentState.providerState.chainState.votingPowerHistory == List(InitialValidatorSet)),
                 assert(currentState.providerState.chainState.currentValidatorSet == InitialValidatorSet),
-                assert(currentState.providerState.chainState.lastTimestamp == 0),
+                assert(currentState.providerState.chainState.lastTimestamp == -1),
+                assert(currentState.providerState.chainState.runningTimestamp == 0),
                 VotingPowerChange("node1", 50)
             })
             .then(
@@ -623,7 +624,7 @@ module ccv_model {
         init.then(
             EndAndBeginBlockForProvider(1 * Second, Set("consumer1"), Set())
         ).then(
-            20.reps(
+            8.reps(
                 i => all {
                         {   
                             // if the trusting period has passed