models: add original dBFT 2.0 specifications

[AnnaShaleva]

An essential part of nspcc-dev/neo-go#2552 investigation.

TODO:

• Finish model description, documentation and usage notes.
• Add model schemas.
• Add model checker configurations.
• Attach error traces for known deadlocks. Will be done in a separate issue.
• Add .gitignore for TLC files.

[codecov]

Codecov Report

Merging #65 (9866323) into master (31c1bbd) will not change coverage.
The diff coverage is n/a.

❗ Current head 9866323 differs from pull request most recent head 93bb5bb. Consider uploading reports for the commit 93bb5bb to get more accurate results

@@           Coverage Diff           @@
##           master      #65   +/-   ##
=======================================
  Coverage   74.61%   74.61%           
=======================================
  Files          24       24           
  Lines        1296     1296           
=======================================
  Hits          967      967           
  Misses        275      275           
  Partials       54       54           

📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more

[roman-khimov]

In general it's very descriptive and nice, but maybe we need to specifically mention MoreThanFNodesCommittedOrLost in that this logic can't be reliable in detecting lost nodes (even with neo-project/neo#2057), because real nodes can go down at any time.