Enable MBT on master

[Shivani912]

This PR enables model based testing on master. Some tests had to be disabled as they fail to parse because of more restrictive data structure construction and this will be addressed in a follow up PR. All of the other tests were fixed simply by adding the new total_voting_power field to validator set in testing :)

And with this, I think we're in good shape to close issue #567
(closes #567 )

• Referenced an issue explaining the need for the change
• Updated all relevant documentation in docs
• Updated all code comments where relevant
• Wrote tests
• Updated CHANGELOG.md

[codecov-io]

Codecov Report

Merging #686 (cc21652) into master (fa415e3) will increase coverage by 2.8%.
The diff coverage is 90.9%.

@@           Coverage Diff            @@
##           master    #686     +/-   ##
========================================
+ Coverage    39.2%   42.1%   +2.8%     
========================================
  Files         190     191      +1     
  Lines       12552   12600     +48     
  Branches     3237    3232      -5     
========================================
+ Hits         4927    5305    +378     
+ Misses       7381    6949    -432     
- Partials      244     346    +102     

Impacted Files	Coverage Δ
testgen/src/tester.rs	65.7% <ø> (+16.8%)	⬆️
light-client/tests/model_based.rs	21.4% <90.9%> (+21.1%)	⬆️
rpc/src/id.rs	90.6% <0.0%> (ø)
rpc/src/error.rs	50.0% <0.0%> (ø)
rpc/src/event.rs	10.9% <0.0%> (ø)
rpc/src/client.rs	8.5% <0.0%> (ø)
testgen/src/time.rs	44.4% <0.0%> (ø)
testgen/src/vote.rs	78.3% <0.0%> (ø)
light-node/src/rpc.rs	53.5% <0.0%> (ø)
rpc-probe/src/main.rs	4.5% <0.0%> (ø)
... and 73 more

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update fa415e3...cc21652. Read the comment docs.

[melekes]

Is there an issue for this sorting bug? Could you point us to any specific line where the bug occurs or you don't know?

[Shivani912]

No, but yes there should be one. I think the problem is somewhere with ser/de, it somehow changes the sequence of validators in the set which then produces a wrong valset hash. I'm not sure how this is happening. But I'm sure this is not coming from Testgen at least. Currently, these tests were disabled on master because of this and re-sorting seemed to be a quick solution. I need to dig further to know where this problem is coming from.

[Shivani912]

Issue for this: #687

[andrey-kuprianov]

Ok, I think I know what is happening here. When we transform tests from Apalache counterexamples, the validators are in no particular order. At the same time new deserialization requires them to be sorted according to the power, and then lexicographically. Therefore the validation fails. One more point for implementing #665.

[melekes]

👍

[Shivani912]

Thanks for reviewing @melekes :) I'll wait for one more approval from @romac or @andrey-kuprianov before merging!

[andrey-kuprianov]

Looks good to me! Thanks, @Shivani912 for fixing the tests!

We need to rethink the model-based testing for Tendermint-rs in general, besides fixing the current issues, and automate it further, to reduce such manual work as much as possible. Let's address this in the near future.

[Shivani912]

Looks good to me! Thanks, @Shivani912 for fixing the tests!

We need to rethink the model-based testing for Tendermint-rs in general, besides fixing the current issues, and automate it further, to reduce such manual work as much as possible. Let's address this in the near future.

Awesome, that's exactly where my thoughts were going!