You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
After extending Tendermint Validator Set with the total_voting_power field, the model-based tests stopped to work.
The reason for that behavior is that validator sets are not first class citizens in the Testgen. Instead, when generating validator sets via Jsonatr transform, we map Testgen validator generation over the array of abstract validator identifiers, as produced by Apalache. This was ok, until total_voting_power, that requires treating Validator Set as a datastructure on its own.
The solution is as follows:
add ValidatorSet to Testgen, and generate it in the same way as all other datastructures.
add valset command to tendermint-testgen binary.
in the Jsonatr transform above, invoke tendermint_valset for the array of identifiers, instead of mapping the tendermint_validator.
The text was updated successfully, but these errors were encountered:
Thanks @andrey-kuprianov , we definitely need to make this improvement to Testgen. On a second thought, does it make sense to use validator::Set::new(validators, voting_power) instead of the old valset constructor since we do not currently make use of total_voting_power in Testgen apart from construction. I think it'll be easier to quickly unblock things this way.
With #730, we have introduced the ValidatorSet to testgen and can be generated like other data structures. But, we still need to integrate it with other data structures (header, commit, etc.) - see this comment. Doing that will require both steps 2 & 3 to be implemented.
After extending Tendermint Validator Set with the total_voting_power field, the model-based tests stopped to work.
The reason for that behavior is that validator sets are not first class citizens in the Testgen. Instead, when generating validator sets via Jsonatr transform, we map Testgen validator generation over the array of abstract validator identifiers, as produced by Apalache. This was ok, until
total_voting_power
, that requires treating Validator Set as a datastructure on its own.The solution is as follows:
ValidatorSet
to Testgen, and generate it in the same way as all other datastructures.valset
command totendermint-testgen
binary.tendermint_valset
for the array of identifiers, instead of mapping thetendermint_validator
.The text was updated successfully, but these errors were encountered: