Add more diverse traces

tests/difference/core/quint_model/ccv.qnt

@@ -721,7 +721,10 @@ module ccv {
             // prune the sentVscPacket
             val newSentVscPacket = currentState.providerState.sentVscPacketsToConsumer.get(sender).tail()
             val newState = currentState.with(
-                "providerState", newProviderState
+                "providerState", 
+                    {...newProviderState,
+                    sentVscPacketsToConsumer: currentState.providerState.sentVscPacketsToConsumer.set(sender, newSentVscPacket)
+                    }
             )
             Ok(newState)
         }

tests/difference/core/quint_model/driver/generate_traces.sh

@@ -1 +1,10 @@
-go run ./... -modelPath=../ccv_model.qnt -init init -step step -traceFolder traces -numTraces 100 --numSamples 1
+echo "Generating bounded drift traces with timeouts"
+go run ./... -modelPath=../ccv_boundeddrift.qnt -step stepBoundedDrift  -invariant CanTimeoutConsumer -traceFolder traces/bound_timeout -numTraces 10 -numSteps 200 -numSamples 200
+echo "Generating long bounded drift traces without invariants"
+go run ./... -modelPath=../ccv_boundeddrift.qnt -step stepBoundedDrift -traceFolder traces/bound_noinv -numTraces 10 -numSteps 500 -numSamples 1
+echo "Generating bounded drift traces with maturations"
+go run ./... -modelPath=../ccv_boundeddrift.qnt -step stepBoundedDrift -invariant CanReceiveMaturations -traceFolder traces/bound_mat -numTraces 10 -numSteps 100 -numSamples 20
+echo "Generating synched traces with maturations"
+go run ./... -modelPath=../ccv_sync.qnt -init initHappy -step stepHappy -invariant CanReceiveMaturations -traceFolder traces/sync_mat -numTraces 10 -numSteps 300 -numSamples 20
+echo "Generating long synched traces without invariants"
+go run ./... -modelPath=../ccv_sync.qnt -init initHappy -step stepHappy -traceFolder traces/sync_noinv -numTraces 10 -numSteps 500 -numSamples 1

tests/difference/core/quint_model/driver/mbt_test.go

@@ -4,43 +4,59 @@ import (
 	"fmt"
 	"log"
 	"os"
+	"path/filepath"
 	"reflect"
 	"sort"
 	"testing"
 	"time"
 
 	cmttypes "github.com/cometbft/cometbft/types"
 	sdktypes "github.com/cosmos/cosmos-sdk/types"
-	ibctesting "github.com/cosmos/ibc-go/v7/testing"
 	providertypes "github.com/cosmos/interchain-security/v3/x/ccv/provider/types"
 	"github.com/kylelemons/godebug/pretty"
 
 	"github.com/informalsystems/itf-go/itf"
 	"github.com/stretchr/testify/require"
+
+	ibctesting "github.com/cosmos/ibc-go/v7/testing"
 )
 
-const verbose = true
+const verbose = false
 
 // keep some interesting statistics
 var stats = Stats{}
 
 func TestMBT(t *testing.T) {
-	dirEntries, err := os.ReadDir("traces")
-	if err != nil {
-		t.Fatal("Error:", err)
-	}
+	dir := "traces"
 
-	t.Log("Running traces from the traces folder")
+	numTraces := 0
 
 	ibctesting.TimeIncrement = 1 * time.Nanosecond
 
-	for _, dirEntry := range dirEntries {
-		t.Log("Running trace ", dirEntry.Name())
-		RunItfTrace(t, "traces/"+dirEntry.Name())
+	err := filepath.Walk(dir, func(path string, info os.FileInfo, err error) error {
+		if err != nil {
+			return err
+		}
+
+		if info.IsDir() {
+			return nil
+		}
+
+		ext := filepath.Ext(path)
+		if ext == ".json" || ext == ".itf" {
+			fmt.Println("Running trace:", path)
+			numTraces++
+			RunItfTrace(t, path)
+		}
+
+		return nil
+	})
+	if err != nil {
+		t.Fatal("Error:", err)
 	}
 
 	t.Log("✅ Running traces from the traces folder done")
-	t.Log(len(dirEntries), "traces run")
+	t.Log(numTraces, "traces run")
 
 	// print some stats
 	t.Logf("Highest observed voting power: %v", stats.highestObservedValPower)
@@ -50,7 +66,7 @@ func TestMBT(t *testing.T) {
 	t.Logf("Number of sent packets: %v", stats.numSentPackets)
 	t.Logf("Number of blocks: %v", stats.numBlocks)
 	t.Logf("Number of transactions: %v", stats.numTxs)
-	t.Logf("Average summed block time delta passed per trace: %v", stats.totalBlockTimePassedPerTrace/time.Duration(len(dirEntries)))
+	t.Logf("Average summed block time delta passed per trace: %v", stats.totalBlockTimePassedPerTrace/time.Duration(numTraces))
 }
 
 func RunItfTrace(t *testing.T, path string) {
@@ -353,6 +369,9 @@ func RunItfTrace(t *testing.T, path string) {
 		}
 		t.Log("Packet queues match")
 
+		// compare that the sent packets on the proider match the model
+		CompareSentPacketsOnProvider(driver, currentModelState, timeOffset)
+
 		stats.EnterStats(driver)
 	}
 	t.Log("🟢 Trace is ok!")
@@ -510,6 +529,30 @@ func CompareValSet(modelValSet map[string]itf.Expr, systemValSet map[string]int6
 	return nil
 }
 
+func CompareSentPacketsOnProvider(driver *Driver, currentModelState map[string]itf.Expr, timeOffset time.Time) {
+	for _, consumer := range driver.runningConsumers() {
+		vscSendTimestamps := driver.providerKeeper().GetAllVscSendTimestamps(driver.providerCtx(), consumer.ChainId)
+
+		actualVscSendTimestamps := make([]time.Time, 0)
+		for _, vscSendTimestamp := range vscSendTimestamps {
+			actualVscSendTimestamps = append(actualVscSendTimestamps, vscSendTimestamp.Timestamp)
+		}
+
+		modelVscSendTimestamps := VscSendTimestamps(currentModelState, consumer.ChainId)
+
+		for i, modelVscSendTimestamp := range modelVscSendTimestamps {
+			actualTimeWithOffset := actualVscSendTimestamps[i].Unix() - timeOffset.Unix()
+			require.Equal(
+				driver.t,
+				modelVscSendTimestamp,
+				actualTimeWithOffset,
+				"Vsc send timestamps do not match for consumer %v",
+				consumer.ChainId,
+			)
+		}
+	}
+}
+
 func (s *Stats) EnterStats(driver *Driver) {
 	// highest observed voting power
 	for _, val := range driver.providerValidatorSet() {
@@ -527,6 +570,4 @@ func (s *Stats) EnterStats(driver *Driver) {
 	if inFlightPackets > s.maxNumInFlightPackets {
 		s.maxNumInFlightPackets = inFlightPackets
 	}
-
-	// number of sent packets
 }

tests/difference/core/quint_model/driver/model_viewer.go

@@ -87,3 +87,17 @@ func LocalClientExpired(curStateExpr itf.MapExprType, consumer string) bool {
 func GetTimeoutForPacket(packetExpr itf.MapExprType) int64 {
 	return packetExpr["timeoutTime"].Value.(int64)
 }
+
+func GetSendingTimeForPacket(packetExpr itf.MapExprType) int64 {
+	return packetExpr["sendingTime"].Value.(int64)
+}
+
+func VscSendTimestamps(curStateExpr itf.MapExprType, consumer string) []int64 {
+	sentVscPackets := ProviderState(curStateExpr)["sentVscPacketsToConsumer"].Value.(itf.MapExprType)[consumer].Value.(itf.ListExprType)
+
+	res := make([]int64, 0)
+	for _, packetExpr := range sentVscPackets {
+		res = append(res, GetSendingTimeForPacket(packetExpr.Value.(itf.MapExprType)))
+	}
+	return res
+}