formal-models: extend dBFT with additional post-commit phase

[AnnaShaleva]

Close #111.

The extended model includes additional ackSent RM state and additional Ack message type. Speaking in terms of anti-MEV solution, preBlock approval corresponds to the commitSent RM state, and the only possible transition from commitSent stage is to move to ackSent stage via Ack message sending (Block approval).

Presented model has the same 4-nodes deadlock scenario with a single dead node described in neo-project/neo-modules#792 (comment):

Also, the presented model has additional TerminatingFourNodesDeadlock action that allows infinite stuttering in the described deadlock to enable further model checking. If this action is enabled, then one more deadlock is being found (not related to the additional phase), this deadlock is yet another face of the same liveness lock described previously:

TODO:

• Add description to the README;
• Add a picture;
• Update configuration;
• Improve commit message.

[codecov]

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 63.31%. Comparing base (96105d0) to head (de50c7b).

Additional details and impacted files

@@           Coverage Diff           @@
##           master     #116   +/-   ##
=======================================
  Coverage   63.31%   63.31%           
=======================================
  Files          27       27           
  Lines        1510     1510           
=======================================
  Hits          956      956           
  Misses        489      489           
  Partials       65       65           

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[AnnaShaleva]

Ready for review. @roman-khimov, I think the best way to review it is to check the diff between this model and our basic dBFT model.

[roman-khimov]

Looks OK otherwise.

[AnnaShaleva]

@roman-khimov, ready for review.