From ab1430a0632553ee76b86496fd4606fe8db13204 Mon Sep 17 00:00:00 2001
From: Philip Offtermatt <p.offtermatt@gmail.com>
Date: Wed, 29 Nov 2023 11:10:51 +0100
Subject: [PATCH] Add logic for comparing timestamps of packets

---
 .../core/quint_model/driver/mbt_test.go       | 19 ++++++++++++++-----
 .../core/quint_model/driver/model_viewer.go   |  8 +++++++-
 2 files changed, 21 insertions(+), 6 deletions(-)

diff --git a/tests/difference/core/quint_model/driver/mbt_test.go b/tests/difference/core/quint_model/driver/mbt_test.go
index 7f996a9532..ec61c51462 100644
--- a/tests/difference/core/quint_model/driver/mbt_test.go
+++ b/tests/difference/core/quint_model/driver/mbt_test.go
@@ -393,12 +393,21 @@ func ComparePacketQueue(
 		sender,
 		receiver)
 
-	// for i := range modelSenderQueue {
-	// 	actualPacket := actualSenderQueue[i]
-	// 	modelPacket := modelSenderQueue[i]
+	for i := range modelSenderQueue {
+		actualPacket := actualSenderQueue[i]
+		modelPacket := modelSenderQueue[i].Value.(itf.MapExprType)
 
-	// 	actualPacket.Packet.TimeoutTimestamp - timeOffset
-	// }
+		actualTimeout := int64(actualPacket.Packet.TimeoutTimestamp) - timeOffset.Unix()
+		modelTimeout := GetTimeoutForPacket(modelPacket)
+
+		require.Equal(t,
+			modelTimeout,
+			actualTimeout,
+			"Timeouts do not match for packet %v, sender %v, receiver %v",
+			actualPacket,
+			sender,
+			receiver)
+	}
 }
 
 // CompareTimes compares the block times in the model to the block times in the system.
diff --git a/tests/difference/core/quint_model/driver/model_viewer.go b/tests/difference/core/quint_model/driver/model_viewer.go
index 0b0c9d014d..f274fb35e3 100644
--- a/tests/difference/core/quint_model/driver/model_viewer.go
+++ b/tests/difference/core/quint_model/driver/model_viewer.go
@@ -1,6 +1,8 @@
 package main
 
-import "github.com/informalsystems/itf-go/itf"
+import (
+	"github.com/informalsystems/itf-go/itf"
+)
 
 // This file contains logic to process
 // and access parts of the current state of the Quint trace.
@@ -81,3 +83,7 @@ func ConsumerStatus(curStateExpr itf.MapExprType, consumer string) string {
 func LocalClientExpired(curStateExpr itf.MapExprType, consumer string) bool {
 	return ConsumerState(curStateExpr, consumer)["localClientExpired"].Value.(bool)
 }
+
+func GetTimeoutForPacket(packetExpr itf.MapExprType) int64 {
+	return packetExpr["timeoutTime"].Value.(int64)
+}