Add logic for comparing timestamps of packets

cosmos · Nov 29, 2023 · ab1430a · ab1430a
1 parent 6887906
commit ab1430a
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 6 deletions.
diff --git 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
@@ -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)
+}