Update modelator to 0.2.0

[jtremback]

Description

This updates to the new Modelator 0.2.0. Some caveats:

• I am manually setting the model checker to TLC (the default in Modelator 0.2.0 is Apalache), because the TLA+ spec seems not to run in Apalache.
• I had to get rid of an assert I don't understand on 60e3185#diff-ec1a9a4dbc3d8d3aa74543450bb465b3c01d62036a5449fbba077e185f4ce323L66 because it was failing.

Let me know if this looks OK otherwise, and I can add the unclog file and other housekeeping stuff to this PR.

---

For contributor use:

• Added a changelog entry, using unclog.
• (not applicable) If applicable: Unit tests written, added test to CI.
• (not applicable) Linked to Github issue with discussion and accepted design OR link to spec that describes this work.
• Updated relevant documentation (docs/) and code comments.
• Re-reviewed Files changed in the Github PR explorer.

[jtremback]

Security audit is failing but that appears to be a Tendermint dep?

[adizere]

I'm not sure I understand the relation between this PR and the previously-opened one #812. Could you clarify if the current PR complete supersedes (so we can close and ignore) #812?

[adizere]

Security audit is failing but that appears to be a Tendermint dep?

Indeed, not exactly Tendermint dep, but fixing the security audit is blocked by prost & tonic (ref #1166 (comment))

[jtremback]

I'm not sure I understand the relation between this PR and the previously-opened one #812. Could you clarify if the current PR complete supersedes (so we can close and ignore) #812?

We should probably wait for @andrey-kuprianov to weigh in, but #812 brings in a whole new API (the EventRunner API). It is also significantly behind master in other respects, which makes completing and merging it hard.

This PR uses the same API as the Modelator tests in master (the StepRunner API). This is a very straightforward PR, which just involved updating the modelator version and changing some function names etc. It unblocks my work on the ICS07 upgrade client mbt tests, since there were some bugs in the old modelator currently used on master.

We may want to finish #812 and switch over to the EventRunner API in the future, but IMO that is a separate task and this PR should be merged first.

[adizere]

I'm not sure I understand the relation between this PR and the previously-opened one #812. Could you clarify if the current PR complete supersedes (so we can close and ignore) #812?

We should probably wait for @andrey-kuprianov to weigh in, but #812 brings in a whole new API (the EventRunner API). It is also significantly behind master in other respects, which makes completing and merging it hard.

This PR uses the same API as the Modelator tests in master (the StepRunner API). This is a very straightforward PR, which just involved updating the modelator version and changing some function names etc. It unblocks my work on the ICS07 upgrade client mbt tests, since there were some bugs in the old modelator currently used on master.

We may want to finish #812 and switch over to the EventRunner API in the future, but IMO that is a separate task and this PR should be merged first.

Got it, thanks for the explanation Jehan, that's very helpful!

Copying @cezarad here if she wants to weight in by reviewing this PR.