tests: MBT for votekeeper

[hvanz]

Closes #44
Depends on #18 and #40.
Also depends on #73.

This PR adds a CI workflow .github/workflows/mbt.yml that generates trace files from voteBookkeeperTest.qnt and then executes each trace in the code as a unit test. In particular:

• In the spec:
  • Update the spec with a new variable for the weighted vote that is passed as input to the applyVote function in each step.
  • Add a new Quint module voteBookkeeperSM for the parameterized state machine for the vote keeper.
• In the code:
  • Implement VotekeeperRunner that builds the initial state and the steps from an ITF trace.

[romac]

@rnbguy Any chance we can make the MBT tests count towards code coverage? Apparently we can just upload multiple coverage reports and Codecov will merge them, which is pretty neat :)

[romac]

Or is that the case already? I see that the coverage job now sets the QUINT_SEED env variable, so presumably it does generate the traces and runs the MBT tests?

If so, then I am not sure I understand why we need the MBT workflow?

[rnbguy]

You're right. we don't need the MBT workflow anymore - as MBT tests are already executed with Rust workflow and again in coverage workflow.

[rnbguy]

Since Rust and coverage workflows are picking up the default seed for Quint, I set MBT workflow to use a UNIX epoch as random seed.

[rnbguy]

Great work, guys ! 🎉

Just one last nit. Since the rust MBT tests now generate traces, fixing and executing them on the fly, maybe some of the Scripts are redundant. Feel free to remove them accordingly before merging.

[romac]

Amazing work guys, thanks so much! 🚀