Address comments

cosmos · Dec 11, 2023 · 1659892 · 1659892
1 parent 2396038
commit 1659892
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 9 deletions.
diff --git 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
+go run ./... -modelPath=../model/ccv_sync.qnt -init initSync -step stepSync -traceFolder traces/sync_noinv -numTraces 20 -numSteps 500 -numSamples 1
diff --git 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
+go run ./... -modelPath=../model/ccv_sync.qnt -init initSync -step stepSync -traceFolder traces/sync_noinv -numTraces 1 -numSteps 500 -numSamples 1
diff --git 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