test: Replace difftest model with Quint=>MBT

[p-offtermatt]

Description

Closes: #1241

Changes:

• Changes to the Quint model: bug fixes, things that make it easier to use to generate traces, ...
• Removes the difference tests in tests/difference
• Adds tests/mbt
• Adds a driver, which uses ibctesting to take Quint traces and run them against provider and consumer apps
• Adds infrastructure to generate traces from the Quint model
• Adds the mbt tests to the CI
• Adds a README explaining the MBT approach, how to use, etc
• Made some changes to the Quint model. There are 2 types of changes: Making the traces more useful for MBT (doing a change amount instead of new voting power for VotingPowerChange, keeping the parameter values in a variable, ...) and making the model actually correct (splitting timestamps into running and last timestamps, ...)

---

Author Checklist

All items are required. Please add a note to the item if the item is not applicable and
please add links to any relevant follow up issues.

I have...

• Included the correct type prefix in the PR title
• Targeted the correct branch (see PR Targeting)
• Provided a link to the relevant issue or specification
• Reviewed "Files changed" and left comments if necessary
• Confirmed all CI checks have passed

Reviewers Checklist

All items are required. Please add a note if the item is not applicable and please add
your handle next to the items reviewed if you only reviewed selected items.

I have...

• Confirmed the correct type prefix in the PR title
• Confirmed all author checklist items have been addressed
• Confirmed that this PR does not change production code

[MSalopek]

I don't see any glaring issues with the driver.

LGTM.

[sainoe]

Perhaps it'd be helpful to declare the consumer status as constant.

[sainoe]

Thank you for this big work @p-offtermatt. My review of the Quint code doesn't carry much weight as I'm not yet very familiar with the model yet. Apart from tiny nits, the driver code LGTM and is easier to read than the diff testing!