From bcdd85c445fb9508c61cfcba4cd2cb9a3f04cd7f Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Wed, 29 Nov 2023 17:44:04 +0100 Subject: [PATCH] Add more diverse traces --- tests/difference/core/quint_model/ccv.qnt | 5 +- .../driver/generate_boundeddrift_traces.sh | 1 - .../quint_model/driver/generate_traces.sh | 11 ++- .../core/quint_model/driver/mbt_test.go | 69 +++++++++++++++---- .../core/quint_model/driver/model_viewer.go | 14 ++++ 5 files changed, 83 insertions(+), 17 deletions(-) delete mode 100755 tests/difference/core/quint_model/driver/generate_boundeddrift_traces.sh diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt index e324d734a1..109a2e9ba4 100644 --- a/tests/difference/core/quint_model/ccv.qnt +++ b/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) } diff --git a/tests/difference/core/quint_model/driver/generate_boundeddrift_traces.sh b/tests/difference/core/quint_model/driver/generate_boundeddrift_traces.sh deleted file mode 100755 index 8d071d196b..0000000000 --- a/tests/difference/core/quint_model/driver/generate_boundeddrift_traces.sh +++ /dev/null @@ -1 +0,0 @@ -go run ./... -modelPath=../ccv_boundeddrift.qnt -step stepBoundedDrift -invariant CanTimeoutConsumer -traceFolder traces -numTraces 150 -numSteps 200 -numSamples 200 \ No newline at end of file diff --git a/tests/difference/core/quint_model/driver/generate_traces.sh b/tests/difference/core/quint_model/driver/generate_traces.sh index 2936b05455..0d08ea436b 100755 --- a/tests/difference/core/quint_model/driver/generate_traces.sh +++ b/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 \ No newline at end of file +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 \ No newline at end of file diff --git a/tests/difference/core/quint_model/driver/mbt_test.go b/tests/difference/core/quint_model/driver/mbt_test.go index c1bae4b26e..7fe1ea3772 100644 --- a/tests/difference/core/quint_model/driver/mbt_test.go +++ b/tests/difference/core/quint_model/driver/mbt_test.go @@ -4,6 +4,7 @@ import ( "fmt" "log" "os" + "path/filepath" "reflect" "sort" "testing" @@ -11,36 +12,51 @@ import ( 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 } diff --git a/tests/difference/core/quint_model/driver/model_viewer.go b/tests/difference/core/quint_model/driver/model_viewer.go index f274fb35e3..b2167febbb 100644 --- a/tests/difference/core/quint_model/driver/model_viewer.go +++ b/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 +}