From 16598923d0a537efe4252d6f39a7d60351c1061e Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Mon, 11 Dec 2023 11:26:22 +0100 Subject: [PATCH] Address comments --- tests/mbt/driver/generate_more_traces.sh | 4 ++-- tests/mbt/driver/generate_traces.sh | 4 ++-- tests/mbt/driver/mbt_test.go | 10 +++++----- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/tests/mbt/driver/generate_more_traces.sh b/tests/mbt/driver/generate_more_traces.sh index 2b9fad2d90..74e73eb262 100755 --- a/tests/mbt/driver/generate_more_traces.sh +++ b/tests/mbt/driver/generate_more_traces.sh @@ -5,6 +5,6 @@ go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -tr echo "Generating bounded drift traces with maturations" go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -invariant CanReceiveMaturations -traceFolder traces/bound_mat -numTraces 20 -numSteps 100 -numSamples 20 echo "Generating synced traces with maturations" -go run ./... -modelPath=../model/ccv_sync.qnt -init initHappy -step stepSync -invariant CanReceiveMaturations -traceFolder traces/sync_mat -numTraces 20 -numSteps 300 -numSamples 20 +go run ./... -modelPath=../model/ccv_sync.qnt -init initSync -step stepSync -invariant CanReceiveMaturations -traceFolder traces/sync_mat -numTraces 20 -numSteps 300 -numSamples 20 echo "Generating long synced traces without invariants" -go run ./... -modelPath=../model/ccv_sync.qnt -init initHappy -step stepSync -traceFolder traces/sync_noinv -numTraces 20 -numSteps 500 -numSamples 1 \ No newline at end of file +go run ./... -modelPath=../model/ccv_sync.qnt -init initSync -step stepSync -traceFolder traces/sync_noinv -numTraces 20 -numSteps 500 -numSamples 1 \ No newline at end of file diff --git a/tests/mbt/driver/generate_traces.sh b/tests/mbt/driver/generate_traces.sh index e792a2cf3c..ea13d82653 100755 --- a/tests/mbt/driver/generate_traces.sh +++ b/tests/mbt/driver/generate_traces.sh @@ -5,6 +5,6 @@ go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -tr echo "Generating bounded drift traces with maturations" go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -invariant CanReceiveMaturations -traceFolder traces/bound_mat -numTraces 1 -numSteps 100 -numSamples 20 echo "Generating synced traces with maturations" -go run ./... -modelPath=../model/ccv_sync.qnt -init initHappy -step stepSync -invariant CanReceiveMaturations -traceFolder traces/sync_mat -numTraces 1 -numSteps 300 -numSamples 20 +go run ./... -modelPath=../model/ccv_sync.qnt -init initSync -step stepSync -invariant CanReceiveMaturations -traceFolder traces/sync_mat -numTraces 1 -numSteps 300 -numSamples 20 echo "Generating long synced traces without invariants" -go run ./... -modelPath=../model/ccv_sync.qnt -init initHappy -step stepSync -traceFolder traces/sync_noinv -numTraces 1 -numSteps 500 -numSamples 1 \ No newline at end of file +go run ./... -modelPath=../model/ccv_sync.qnt -init initSync -step stepSync -traceFolder traces/sync_noinv -numTraces 1 -numSteps 500 -numSamples 1 \ No newline at end of file diff --git a/tests/mbt/driver/mbt_test.go b/tests/mbt/driver/mbt_test.go index 4164d623fd..8fbed30661 100644 --- a/tests/mbt/driver/mbt_test.go +++ b/tests/mbt/driver/mbt_test.go @@ -93,7 +93,7 @@ func RunItfTrace(t *testing.T, path string) { _, ok := varNames[expectedVarName] require.True(t, ok, "Expected var name %v not found in actual var names %v", expectedVarName, varNames) } - // extra var names are ok, so no need to change the length + // extra var names are ok, so no need to check inclusion the other way around t.Log("Reading params...") params := trace.States[0].VarValues["params"].Value.(itf.MapExprType) @@ -140,7 +140,6 @@ func RunItfTrace(t *testing.T, path string) { valNames[i] = val.Value.(string) } - // initialValSet has the right vals, but not yet the right powers valSet, addressMap, signers, err := CreateValSet(initialValSet) require.NoError(t, err, "Error creating validator set") @@ -167,9 +166,9 @@ func RunItfTrace(t *testing.T, path string) { for index, state := range trace.States { t.Logf("Reading state %v of trace %v", index, path) - // modelState := state.VarValues["currentState"] trace := state.VarValues["trace"].Value.(itf.ListExprType) - // fmt.Println(modelState) + // lastAction will get the last action that was executed so far along the model trace, + // i.e. the action we should perform before checking model vs actual system equivalence lastAction := trace[len(trace)-1].Value.(itf.MapExprType) currentModelState := state.VarValues["currentState"].Value.(itf.MapExprType) @@ -207,7 +206,7 @@ func RunItfTrace(t *testing.T, path string) { // we need 2 blocks, because for a packet sent at height H, the receiving chain // needs a header of height H+1 to accept the packet // so we do one time advancement with a very small increment, - // and then increment the rest of the time] + // and then increment the rest of the time runningConsumersBefore := driver.runningConsumers() driver.endAndBeginBlock("provider", 1*time.Nanosecond) driver.endAndBeginBlock("provider", time.Duration(timeAdvancement)*time.Second-1*time.Nanosecond) @@ -262,6 +261,7 @@ func RunItfTrace(t *testing.T, path string) { // for all connected consumers, update the clients... // unless it was the last consumer to be started, in which case it already has the header + // as we called driver.setupConsumer for _, consumer := range driver.runningConsumers() { if len(consumersToStart) > 0 && consumer.ChainId == consumersToStart[len(consumersToStart)-1].Value.(string) { continue