From aa72a4d14767eb8d4e7c57fbb35bc1532fee5423 Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Thu, 8 Aug 2024 11:33:50 +0200
Subject: [PATCH] VetoCooldown

---
 test/kontrol/VetoCooldown.t.sol   |  8 ++++----
 test/kontrol/VetoSignalling.t.sol | 26 +++++++++++++-------------
 2 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/test/kontrol/VetoCooldown.t.sol b/test/kontrol/VetoCooldown.t.sol
index 9d8f83b6..c4c029bf 100644
--- a/test/kontrol/VetoCooldown.t.sol
+++ b/test/kontrol/VetoCooldown.t.sol
@@ -3,7 +3,7 @@ pragma solidity 0.8.23;
 import "forge-std/Vm.sol";
 import "kontrol-cheatcodes/KontrolCheats.sol";
 
-import {Duration, Durations} from "contracts/types/Duration.sol";
+import {addTo, Duration, Durations} from "contracts/types/Duration.sol";
 import {Timestamp, Timestamps} from "contracts/types/Timestamp.sol";
 
 import "test/kontrol/DualGovernanceSetUp.sol";
@@ -11,13 +11,13 @@ import "test/kontrol/DualGovernanceSetUp.sol";
 contract VetoCooldownTest is DualGovernanceSetUp {
     function testVetoCooldownDuration() external {
         vm.assume(dualGovernance.getCurrentState() == State.VetoCooldown);
+        Timestamp timeEnteredAt = Timestamp.wrap(_getEnteredAt(dualGovernance));
+        Timestamp maxCooldownDuration = addTo(config.VETO_COOLDOWN_DURATION(), timeEnteredAt);
 
         dualGovernance.activateNextState();
 
         bool stillInVetoCooldown = (dualGovernance.getCurrentState() == State.VetoCooldown);
-        Timestamp timeEnteredAt = Timestamp.wrap(_getEnteredAt(dualGovernance));
-        Duration timeInVetoCooldown = Durations.between(Timestamps.now(), timeEnteredAt);
-        bool durationHasElapsed = (timeInVetoCooldown > config.VETO_COOLDOWN_DURATION());
+        bool durationHasElapsed = (Timestamps.now() > maxCooldownDuration);
         assert(stillInVetoCooldown != durationHasElapsed);
     }
 }
diff --git a/test/kontrol/VetoSignalling.t.sol b/test/kontrol/VetoSignalling.t.sol
index a9847b98..f9a4a3b9 100644
--- a/test/kontrol/VetoSignalling.t.sol
+++ b/test/kontrol/VetoSignalling.t.sol
@@ -261,19 +261,19 @@ contract VetoSignallingTest is DualGovernanceSetUp {
                 // Establish third invariant
                 _vetoSignallingDeactivationInvariant(Mode.Assert, current);
             }
-            // // Try establishing fourth invariant
-            // if (!_vetoSignallingMaxDelayInvariant(Mode.Try, current)) {
-            //     // Assume third invariant if not already assumed
-            //     if (!assumedDeactivationInvariant) {
-            //         _vetoSignallingDeactivationInvariant(Mode.Assume, previous);
-            //     }
-            //     // Assume fourth invariant if not already assumed
-            //     if (!assumedMaxDelayInvariant) {
-            //         _vetoSignallingMaxDelayInvariant(Mode.Assume, previous);
-            //     }
-            //     // Establish fourth invariant
-            //     _vetoSignallingMaxDelayInvariant(Mode.Assert, current);
-            // }
+            // Try establishing fourth invariant
+            if (!_vetoSignallingMaxDelayInvariant(Mode.Try, current)) {
+                // Assume third invariant if not already assumed
+                if (!assumedDeactivationInvariant) {
+                    _vetoSignallingDeactivationInvariant(Mode.Assume, previous);
+                }
+                // Assume fourth invariant if not already assumed
+                if (!assumedMaxDelayInvariant) {
+                    _vetoSignallingMaxDelayInvariant(Mode.Assume, previous);
+                }
+                // Establish fourth invariant
+                _vetoSignallingMaxDelayInvariant(Mode.Assert, current);
+            }
             return;
         }
         vm.assume(currentState == State.VetoSignalling || currentState == State.VetoSignallingDeactivation);