diff --git a/formal-models/.github/dbft2.1_centralizedCV.drawio b/formal-models/.github/dbft2.1_centralizedCV.drawio
new file mode 100644
index 00000000..5ee02698
--- /dev/null
+++ b/formal-models/.github/dbft2.1_centralizedCV.drawio
@@ -0,0 +1 @@
+7V3rk5u2Fv9rPE06szu8sT+u7d020+y9me69SfMpg21s02CgmH04f30lkAC9MBgB3o3T6awR4iA4R+f8zkNipM92L7/FTrS9D1euP9KUTeytRvp8pGkq+B80RM7GJRpgjwfvB25UUOujt3L3RMckDP3Ei8jGZRgE7jIh2pw4Dp/JbuvQZ4fxsHR8l2n94q2SbdY6NpWi/XfX22zxjVQFndk5uDNq2G+dVfhcatJvR/osDsMk+7V7mbk+fDP4vWTX3QnO5gOL3SCpc8GXtf6f+OPqjwfFU+43D4sv9tq8GmdUnhz/ET0wGmxywG/ADVY38L2Bo6Xv7Pfe8n9bLxjp022y80GjCn7G4WOwclfoaOXst/nBPonD7+4s9MM4pacr4N9slp/BbxW8j+k6DJI7Z+f5B9AwC3feEgzlwQn24M/9A+qAREI1wLHrL9KBPblx4gGmwaZgdef5eGDZ07irDc3O4q2pOS+AhLrhzk3iA+jyXHAbM3tbYjRui13fSbwnkryDZGyTk8vv8Cn0wI015SXrYVvokgMp5ZjCPnyMly66qMzcI3SuxhShxIk3bsIQAj9KT100pbLTQI5UlSNIlg9e1nQBfmzgj19HUEKzRnCTvJ2VOMCuj87C9Ukhc3xvE0ApBKxzgTBNMddv0Imdt1pBGtPY3Xs/nEVKTwHHEXzs9EWY05E5JwVJG9eVvJIQz2ZQjFPJTwD/Q3j7iZI/DFI+aAiFDoAjdl+Eoiieoqx8IirKtW6aFsl7VYpoXpmkZE5IAuF6vXfbylL4wYmmv3/efVv/vX5a3v9pf1tZV7rCkSVKREiF87z1Evchcpbw7DOwMqTgNFYra6BASsy+Vefmrc3osiAMoLBtoFJEgpbr+EIUjrBcoH3QBXgWIx7oFjouKaeJxtFOmqGI2U3wqylztMmZMWc2u7srmZPhmKOqfTLnx3+tm2/bzytH2xyi+f/N2TT4fAXez3FzDpTrAzoM42QbbsLA8W+LVsqY//24i9Drh4qyuORjGEa4j5skB9TJeUxCksMt7bzFal9Dgf+lpJ04wegEsTxtQxBAyQABH7+QSCG9DN3TyM4SR4A/f0GK1yY+/JrfABzMX4ijQ/nokxt7gMHQZpVk7zgoAcg2tdoVHLf4EtpS9Rs2iSZ08zRUYk6oKWJ1hkr488EUopKV90TMC+ufRwjEU0m72qeMvwEdVCN6STmGzxegJaMD+7citAeCBs5/+tP9B/x5FwFRceLD+xJQym5B3hY0p09Atp7NQ4GJ+qrHXzBlH0GuLJzl98coZ8oi5jxPncccFOjmmrQJ0M1VbStgW2GtKpCtapMQVJeCa1VSt9HGWAqu5T6vXq2MThRhixFhZZ1hraKN5TMj8V7gJR4QvB/A8DeRaQeO8slzn0vOnYdPPpWu8YSzgMUHZfCwdSLYb/eygdGj67UfPi+3wFRfg6mx8wIngZLKBZmEqAP+xRvP4cwIJkBxe2NNLUsORtQNygKyGFHVK8IL0iEinkSDIkKpaEpCGGlweFkfEWbQ6xgirIEc7ZbIsZ0U8hyVTFXsIyfgKj5ogzepJF4tM15B/RdvFu80BZADA1E000Q/FOM9HyHYswJs5bcEEhRsxNp2jWQJ3i8Ik/Bb7G4efSfOtC01GBsNofj7HmllSnErUcIf4q02Go9HNzdkuAwPMuuEkUn2POklk9GNCQX86Isc4plKz5EO60jzsDgJq4QzwUmZyhaamCvlGk8nuQFAkqhpd4CT+CEm+xxM1IuX/IVVPPj9tbBW4KiwT/DgUDro0Tq95sDGKWaMKywC+NVW9C0StjF5GUHgAvDDOZS6IT0jvo9JBdkNk5pRGUW584uX9LOcHcTMwWIP/4Ah3oV04yjPZL5OzezDcU5zFMGLIbdS3hXKrEp525ZlS1Xf3XuyFiNAUezCV/Hgovnws/h3JqUoVG1wB888B+t5cfA6c/Dsmg6eIG/ck4PHqog2Dp6G/TpVRz90tcrBAzKx85Jq/+jidFQ6HeYxu6WO1TFptzQpbofWm5/RWlEO6FfkGjZXtyVK7TVsTaVHKjlaBVJ2RIy/bq25Mr/tXE124kC0qqYQa0lOSqBjxclD+63TaQ1zETjwNC83YjXHDFnspTRP0wnCUgNn7zrwR46pdYVS6nKSbldkMIm6vjtPxWYm2DKFBj+do2JrpKOij4d2VNgoxMIPl99vlks3SmAW8ifmjmUOzR1uQW//cKlxpVjheUrARY3gDSufhHdJwqiyk6mSeAu5oQXQwhAw86cNwypBR6iwtcbgUSLMmtT0RgU5jLa+AlUhMqYK1bquL9OE+K11CRIGN3zcMqyvem6FRNXKFSbIVI0KtMtBNVR90rgvWHMeKbJLkI/KpUny7WWr57Zqt2lWi46Jk0mtY93x+g9Rd0Mxq/qTOTO2+o8uyLJPrG2mh1EzQyhNA3CTeJzQAekcZ9HRz6ooNFr4znQ5yoS/dEt4wVgXXDAPwf3fsbWCv/CKBd+nUYtmHr6osLgodIRsSkpkjgyCvduzB9QUQD1bl0clgNWQPDJKFIdRuHf8+uO/BKUZs1dRMQwQILUWTk74wtLIud5F/IIbrjkLO4/MGv59KYXptxSG42L1WQpDB44m9QzdqyiFERvRjstQuXb5zZWl4qfE5u+uwpS/pXRsaVF4a0MoNgtVDq9lG3JcXGr2X/Vm+fLXcx5zsxlmzSYAK+udgW1DEthuNB0HqsjNocfX0pkTMudnHrY4t7qj2jCk7cqS3ssZeVsaMH7j8knl+2hATvmepD4HfaYqb6Yx0+ktJ7eYkEufNZJcEZ2ckzq7eFVde1Vib2mwxJVJwaoJRaGtU5UvbhaEXvP7Noy1TipirbKQnypeKN1zCRRCflpj5DcQ0msy0AvMe0Mwj5fi6lZX8vtpx/xSxbYmUvxSOlykm9T+ZLXzOBQhQ6cICVRxRwCV/17FvnCNZI/Wg1aqSvY00UqSkz00tR6SP3tn556Q/VFEz/SKw2CjNnGvIz4FE5eq2lRNkAomKOAUTw+z2TgnM/vG3Q+ZVlBg3U61ZNhy1dwUrSn2N9U+sLp4h7ULVr9g9TeiRKQutpKukaQA87GpdQPMrZrqrQ6ebptTNo+EO+j9Khv370XlanWcgeWTxkeUVeHqXy7x6lGpwgF7hLiqfLB4taadk7K/IMba+llyKkxQX6tIBpD822hmH3vTDLYxnLSs/yXLfw6QsuP18W9cZbVI85cgZV6M2+1yA41KUuE9V0Wojd6TtWn/SkXYa1iYXd0sq3DhggTTszTnMerrAwlyPwbTHgi20sm6hRebnr749PTNRngfe8qTfMDiEoq+OG6i6Wt+ukqmwmX1bXcruTgJfuM6fSz0TyM149i4PnF5FF3hoNLxdVll47pN3UcuSuXOQm7BGJW2argM2GS3TuHuhYI+PNX+0wfsvvEnErJlERrLIjSRRAhMaEmEVFmENFmEdFmEZH2LQ2NnwImEZEm2JkuytWOSnftyv7J6pDr9veC0CXY4ujQfa34FqfYae9h2/0XCo8kETaWM8iluILvbgk4QNcjrO3Sz6nlZJ8TbL07WiA2397ozFf8DlCzHPzAsAQ+cdKcYoBO2RxxgGIAK/MofQsRNBeM0s44+qS7dacXXCRU/1hWWrzy2dvbpSp1NnH14fXzVlaH5SgVFTIPla9UXk6XHRI5EwYb9ntxJH+NiUGCxbUclojmzFcMoFZItGhasGB7uFTdYbl3zzXT1JR8xfu3wG4oL+ikE2ao+xtK7cPCW4wu4MIBuGFJcz+xtCDYcyIYIaaV7DlSNuPEWPOcOEOo5khKAgE1v3IWXdpSAABfh2c2RADiMQ8j5wrGDvs59uILu+e2/
\ No newline at end of file
diff --git a/formal-models/.github/dbft2.1_centralizedCV.png b/formal-models/.github/dbft2.1_centralizedCV.png
new file mode 100644
index 00000000..2b5bde40
Binary files /dev/null and b/formal-models/.github/dbft2.1_centralizedCV.png differ
diff --git a/formal-models/.github/dbft2.1_threeStagedCV.drawio b/formal-models/.github/dbft2.1_threeStagedCV.drawio
new file mode 100644
index 00000000..4aeeeefe
--- /dev/null
+++ b/formal-models/.github/dbft2.1_threeStagedCV.drawio
@@ -0,0 +1 @@
+7V1tc6O2Fv41nmk/JMM79kfbiW87t9vuNG3u3U87BGObXYwoxom9v76SkQAJ8WIQGCfuTidBCAE6R+c85zkHZaTOt4f/hFaw+QSWjjdSpHXoLkfqw0hRZPg/bAistUM1oB5P7g/SKOHWvbt0dlTHCAAvcgO60Qa+79gR1WaFIXiju62Al3+MJ9vynFzr/9xltIlbx7qUtv/iuOsNuZEs4TNbi3TGDbuNtQRvmSb1caTOQwCi+LftYe54aGbIvMTXLQrOJg8WOn5U5wLwqxXMfnnefl19W73an/40vy6NO2USD/NqeXv8xvhpoyOZghDs/aWDRpFH6uxt40bOU2DZ6OwblChs20RbD59eAT9aWFvXO8KGOdi6NhzsyfJ38MenJ9wBS1XW0LHreXPggfB0M3U+Xyzmc9i+i0Lw3SFnfODDK2Zrz9oh+UmoA5lPdIDfwgkj51A4P3Iy61AXHbB1ovAIu+ALDCynYyLJ+PgtFbssj3HjJiNzRcONFlatdTJ2Kg74C5YIXzqL2X/BzvsCDru9s5Z2/jPQf7+Tc7JwllA78SEIow1YA9/yHtPWWdr6GwABlso3J4qOeNatfQRomTkHN/o/msh7HR99yZx5OOA5Ph0cMwefndCFL+qEpM2HL50ZCB1+yZ5LhzodHbNH7GC01sXaQFagcrpoOUXLGR7aSCtc+6+N68cnFq7nURdmFEw6/ZeoDJrQcoWB8w/2oY17/fjDmH7dPC8tZX0MHv7W5zP/+Q4vosgK105U0s/kK2DoeFbkvtLPwVMmfOln4MInTBR3zGiuYjL6GD8XvipVSTh91jHTLUAddsX3kVWdvo/OGBym/2Rc2h/+Ej9Buj6SOam1ZLgGTTUGZtBWq5Vi2wMwaEZtgyYrAgwaXzrSwKTzKD/oj+bZ0rFCmwxqdCIs1ejV+3CtFZyvSmFV+yNanN/22wDP3LiZs8p7grN0wMDHGR3QJPTvNLQVRsSpYBU4tWF/Ip3jduBl+J5afJY6Eugo6/uxSv9kdOKfNFOmdVunR4jda8495cbRJwxCM+r5uQauhb8edM56MDw4obOl+0qtC+OfPYL1J027250EP4UdZC04nCRGzsPf1vinR/q3GmgHFQ2e//yn8w/88VMAVcUKjz+T8eF7x7egbwubT29Atw7mpeBCvernT4WyC5BUXiz7+z5IhPISct6nzmtybPFv1guMrimDaXnu2kfmCpoDZDRmyE+5MMKd4hNbd7mMTbUDX8Z6OY2HLAsGhHBwfTbSHwosaaXp5ZnaUTZGx7dMItgqT1rirQr9q3QvmzQcVeOjlsbNUKhBWWcMVqud04k1UsuNUUMVNnIqLK0sm74mL+ecxru+G7lQ8X5Ax99Kp/PePgsFNlaA+m0Pa8Qs3a888GZvoOO9h4q+dX0rQnrHhZCU4kJphGvX4uh3Lnp8nBozQxDkU1l/xoF8Kgfx6V0BPrIkLorvhGKjlmBRGwJY7IXBMGoixLYMRjv95AUkFTYvabO2aN37L7sg02cXWD7XLnLQgDlPgVVyPZSNvy62rCusaci2+iACX0NnvfesEFtWxvhKQcGtH5XReDyaTjN3hhNIbh53Iugifs7TJZPRVEdqnX/7ZBgu9ohnpREkae+BCtEYnoSJ2CfKCnf+rKYTiJ5RKp8ncbdvoI5CxHVZBEnMayME6aHnnEEkvT55IF4KQTzIjD1koUe/k+6JjcI+nVD4LVGmTEfQsqZ1ADP5CSJzCJiAJChGaXoiTVbUT1B0CAeumRdqgg64ylKAd9vyR2x+Q+4mv6HpdIAoGzqzorrIV1RgmiHwFzn8gL2lLAwJ2fGKQifD9ctPKFJHt0h//twKGImDbB0/aAmCu2L+qwm84aA9MbD0WieEvwbBdutGOZ2BNkVaXIXOc4A3eVH82pKUe/VewpdB6En7mKfN3bNmvlg2xYIYTqiB4rnhhholwLs01FAmTGJNDKNNoy1CNHfPaOcrN4LQQfP05GBg91GYYVNmmGHt4tSwPoQw8EYNM/EijotJjNw0LhYYKpo1ieTxRYlkXpFYQ0a4AIKxsJ0GJe+Sd0tqqTrg3fQqZyiP5THttxQh3lBhBu2NeFPHQ7C4Q6wMrqGBQyf6ujW4fH0qWELnrY9zOTW2Blgbl9cMm2Zp/9YcXNkUZryBfTLqHw53ThQadyYVChfDneOcaF48YH+f2rYTRKi45ANJR5Z0WjzJYrmYeEheSmSJcAM3dXYFcOqPKG+UOqdz/BFbrkEbfsYJ5xWUihZol5INGmTa9+CwInU6xPXm3XXioS8RD9T9NKYgsdoWvTHuZMyUHnddMawUxhmtuUF49QIU8oKXDTCGVhpablcRlSYrTO5PSPBwp5q0PzU6iB74AdMg0vY3vobP17StY7hW+3xu9MDgHSYhX9WdfG1W1J3N9zP96VgjX5KjMQ9nNvysRZMY09PvVy1KHmLzq9aKSwB4xNf83KxdedUcKignzW7aL5tYTJotNLm+c0A/Xl3n7UpyVO1oOfFesyIBhfJPY4NZQEK85riHBBSXIhmEzxRE6Q+dARtqqRvHH/ZZ6lZEwLyHUre6jkZQaUz/5WnCC/p7r1vr85OEinKdelX03ZSUib/34Ku3xEq+ZlnX2TVc7wWthSCCbgL4o6qMVocFRpX1RYapiaFBNCYzywzQHQvC29wqt5ztV7mmhr3n5ILJRLN9Vhxx1XMyIDB+++6kczBeDLIvljxg6aQJM4IgLK7St9HkcpKL6X5nnklymSUklyikTyisZpyS0hOnxI4Wc0xSEX3kskNxb5nr9Y5QSysMUu5+FIlR68TZnPGRJDUC2Zijh0qtIfFGbSu1PmxxVV0HNKDiKta2X7q4ij81tUB4qS+44ji4iiro7vMrQi6UhtQDm9JKRqGIQ/rwZFHLh+S8rfjXysO7GyfUY2F9CXYpY4E0g6VvxGT5FHlC47Uudk7j7qqttIZrF8zrCa1czDFKmZKYhvttXyD672tPqrKHrKIYc0GkMmoeM75nHpLdFK/XEnS+icyL+NecSCLEF3TmY5A52WEJ5ASAC9ayG1uTpswH0Hob1yRArjIb4atSXrA8uYrY3povVyUv1+sTrNrqy3YRgpWZFavrecHqfS5YbRDbWApKHdy+nOuM3CH7kA+z9pXZAsCo4Plllj+Vz8wLMBd0QwaRfeuakUGZaoJbYmBIoetIeFyqlW+0CMNSzRBTnGD2Vl5K7E1VrKDewoDcDiiG1uOnjnyN5IQBN7zYBC+O+Z4tK1qjI8ly+aCzdtJvw+M25Uw/8qbTrUj3IWzAJvqJuMkAlkhflE71O9vIu0EO4rx9vntM/NxyHUJyHRV/a43Z4k5jP7mrgRqpAcz2EBIepn8KNu6e/rVc9fFf
\ No newline at end of file
diff --git a/formal-models/.github/dbft2.1_threeStagedCV.png b/formal-models/.github/dbft2.1_threeStagedCV.png
new file mode 100644
index 00000000..d0df26d0
Binary files /dev/null and b/formal-models/.github/dbft2.1_threeStagedCV.png differ
diff --git a/formal-models/README.md b/formal-models/README.md
index f5cecb14..7f476875 100644
--- a/formal-models/README.md
+++ b/formal-models/README.md
@@ -1,4 +1,4 @@
-## dBFT formal models
+# dBFT formal models
This section contains a set of dBFT's formal specifications written in
[TLA⁺](https://lamport.azurewebsites.net/tla/tla.html) language. The models
@@ -112,6 +112,250 @@ configuration:
* [TLA⁺ specification](./dbftMultipool/dbftMultipool.tla)
* [TLC Model Checker configuration](./dbftMultipool/dbftMultipool___AllGoodModel.launch)
+## Proposed dBFT 2.1 models
+
+Based on the liveness locks scenarios found by the TLC model checker in the
+[basic dBFT 2.0 model](#basic-dbft-20-model) we've developed two extensions of
+dBFT 2.0 protocol that allow to avoid the liveness lock problem and to preserve
+the safety properties of the algorithm. The extensions currently don't have
+any code-level implementation and presented as a TLA⁺ specifications ready to be
+reviewed and discussed. The improved protocol presented in the extensions will
+be referred below as dBFT 2.1.
+
+We've checked both dBFT 2.1 models with the TLC Model Checker against the same
+set of launch configurations that was used to reveal the liveness problems of the
+[basic dBFT 2.0 model](#basic-dbft-20-model). The improved models have larger
+set of states, thus, the TLC Model Checker wasn't able to finish the liveness
+requirements checks for *all* possible states. However, the checks have passed for
+a state graph diameter that was large enough to believe the presented models
+solve the dBFT 2.0 liveness lock problems.
+
+### Common `Commit` message improvement note
+
+Here and below we assume that `Commit` messages should bear preparation hashes
+from all nodes that have sent the preparation message (>= `M` but not including
+a whole `PrepareRequest`). This quickly synchronizes nodes still at the preparation
+stage when someone else collects enough preparations. It at the same time prevents
+malicious/byzantine nodes from sending spoofed `Commit` messages. The `Commit`
+message size becomes a little bigger, but since it's just hashes it still fits
+into a single packet in the vast majority of the cases, so it doesn't really matter.
+
+### dBFT 2.1 stages-based model
+
+The basic idea of this model is to split the consensus process into three subsequent
+stages marked as `I`, `II` and `III` at the scheme. To perform a transition between
+two subsequent stages each consensus node should wait for a set of messages from
+at least `M` consensus nodes to be received so that it's possible to complete a full
+picture of the neighbours' decisions in the current consensus round. In other words,
+no transition can happen unless we have `M` number of messages from the subsequent round,
+timers are only set up after we have this number of messages, just to wait for
+(potentially) a whole set of them. At the same time, each of the stages has
+its own `ChangeView[1,2,3]` message to exit to the next consensus round (view) if
+something goes wrong in the current one and there's definitely no ability to
+continue consensus process in the current view. Below there's a short description
+of each stage. Please, refer to the model scheme and specification for further
+details.
+
+#### Stage I
+
+Once initialized, consensus node has two ways:
+1. Send its `PrepareRequest`/`PrepareResponse` message (and transmit to the
+ `prepareSent` state).
+2. Decide to go to the next view on timeout or any other valid reason (like
+ transaction missing in the node's mempool or wrong proposal) via sending
+ `ChangeView1` message (and transmit to the `cv1` state).
+
+This scheme is quite similar to the basic dBFT 2.0 model except the new type of
+`ChangeView` message. After that the node enters stage `I` and waits for consensus
+messages of stage `I` (`PrepareRequest` or `PrepareResponse` or `ChangeView1`)
+from at least `M` neighbours which is needed to decide about the next actions.
+The set of received messages can be arranged in the following way:
+
+* `M` messages of `ChangeView1` type denote that `M` nodes have decided to change
+ their view directly after initialization due to invalid/missing `PrepareRequest`
+ which leads to immediate view changing. This is a "fail fast" route that is the
+ same as with dBFT 2.0 for the widespread case of missing primary. No additional
+ delay is added, everything works as usual.
+* `M` preparation messages (of type `PrepareRequest` or `PrepareResponse`) with
+ missing `ChangeView3` denote that the majority of nodes have decided to commit which
+ denotes the safe transition to stage `II` can be performed and `Commit` message
+ can safely be sent even if there's `ChangeView1` message in the network. Notice
+ that `ChangeView3` check is just a protection against node seriously lagging
+ behind.
+* `M` messages each of the type `PrepareRequest` or `PrepareResponse` or `ChangeView1`
+ where at least one message is of the type `ChangeView1` denote that at least `M`
+ nodes have reached the stage `I` and the node can safely take further steps.
+ The additional `| Commit | ≤ F ∪ | CV3 | > 0` condition requires the majority of
+ nodes not to have the `Commit` message to be sent so that it's still possible to
+ collect enough `ChangeView[2,3]` messages to change the view in further stages.
+ If so, then the safe transition to stage `II` can be performed and `ChangeView2`
+ message can safely be sent.
+
+#### Stage II
+
+Once the node has `Commit` or `ChangeView2` message sent, it enters the stage `II`
+of the consensus process and waits for at least `M` messages of stage `II`
+(`Commit` or `ChangeView2`) to perform the transition to the next stage. The set
+of accepted messages can be arranged in the following way:
+
+* `M` messages of `ChangeView2` type denote that `M` nodes have decided to change
+ their view directly after entering the stage `II` due to timeout while waiting
+ for the `Commit` messages which leads to immediate view changing.
+* `M` messages of type `Commit` denote that the majority of nodes have decided to
+ commit which denotes the block can be accepted immediately without entering the
+ stage `III`. Notice that this is the regular flow of normal dBFT 2.0 consensus,
+ it also hasn't been changed and proceeds the way it was before.
+* `M` messages each of the type `Commit` or `ChangeView2` where not more than `F`
+ messages are of the type `Commit` denotes that the majority of nodes decided to
+ change their view after entering the stage `II` and there's not enough `Commit`
+ messages to create the block (and produce the fork), thus, the safe transition
+ to stage `III` can be performed and `ChangeView3` message can safely be sent
+ even if there's `Commit` message in the network.
+
+In addition, the direct transition from `cv2` state to the `commitSent` state is
+added in case if it's clear that there's more than `F` nodes have decided to
+commit and no `ChangeView3` message has been received which means that it's possible
+to produce block in the current view. This path handles a corner case of missing
+stage `I` messages, in fact, because `Commit` messages prove that there are at
+least `M` preparation messages exist, but the node went `cv2` path just because
+it missed some of them.
+
+#### Stage III
+
+Unlike the basic dBFT 2.0 model where consensus node locks on the commit phase,
+stage `III` gives the ability to escape from the commit phase via collecting the set
+of `M` `ChangeView3` messages. This phase is reachable as soon as at least `M` nodes
+has reached the phase `II` (have `ChangeView2` or `Commit` messages sent) and if
+there's not enough `Commit` messages (<=`F`) to accept the block. This stage is
+added to avoid situation when the node is being locked on the `commitSent` state
+whereas the rest of the nodes (>`F`) is willing to go to the next view.
+
+Here's the scheme of transitions between consensus node states for the improved
+dBFT 2.1 stages-based model:
+
+![dBFT 2.1stages-based model](./.github/dbft2.1_threeStagedCV.png)
+
+Here you can find the specification file and the basic TLC Model Checker launch
+configuration:
+
+* [TLA⁺ specification](./dbft2.1_threeStagedCV/dbftCV3.tla)
+* [TLC Model Checker configuration](./dbft2.1_threeStagedCV/dbftCV3___AllGoodModel.launch)
+
+### dBFT 2.1 model with the centralized view changes
+
+The improvement which was taken as a base for this model is taken from the pBFT
+algorithm and is as follows.
+The consensus process is split into two stages with the following meaning:
+
+* Stage `I` holds the node states from which it's allowed to transmit to the subsequent
+ view under assumption that the *new* proposal will be generated (as the basic dBFT 2.0
+ model does).
+* Stage `II` holds the node states from which it's allowed to perform view change
+ *preserving* the proposal from the previous view.
+
+Another vital difference from the basic dBFT 2.0 model is that view changes are
+being performed by the node on the `DoCV[1,2]` command (consensus message) sent by the
+leader of the target view specified via `DoCV[1,2]` parameters. Aside from the target view
+parameter, `DoCV[1,2]` message contains the set of all related pre-received consensus messages
+so that the receivers of `DoCV[1,2]` are able to check its validness before the subsequent
+view change.
+
+Below presented the short description of the proposed consensus process. Please, refer to the
+model scheme and specification for further details.
+
+#### Stage I
+
+Once initialized at view `v`, the consensus node has two ways:
+
+1. Send its `PrepareRequest`/`PrepareResponse` message (and transmit to the
+ `prepareSent` state).
+2. Decide to go to the next view `v+1` on timeout or any other valid reason like
+ transaction missing in the node's mempool via sending `ChangeView1(v+1)` message
+ (and transmitting to the `cv1 to v'=v+1` state).
+
+After that the node enters stage `I` and perform as follows:
+
+* If the node has its `PrepareRequest` or `PrepareResponse` sent:
+ * If at least `M` preparation messages (including its own) collected, then
+ it's clear that the majority has proposal for view `v` being accepted as
+ valid and the node can safely send the `Commit` message and transmit to the
+ phase `II` (`commitSent` state).
+ * If there's not enough preparation payloads received from the neighbours for a
+ long time, then the node is allowed to transmit to the stage `II` via sending
+ its `ChangeView2` message (and changing its state to the `cv2 to v'=v+1`). It
+ denotes the node's desire to change view to the next one with the current proposal
+ to be preserved.
+* If the node entered the `cv1 to v'=v+1` state:
+ * If there's a majority (>=`M`) of `ChangeView1(v+1)` messages and the node is
+ primary in the view `v+1` then it should send the signal (`DoCV1(v+1)` message)
+ to the rest of the group to change their view to `v+1` with the new proposal
+ generated. The rest of the group (backup on `v+1` view that have sent their
+ `ChangeVeiew1(v+1)` messages) should change their view on `DoCV1(v+1)` receiving.
+ * If there's a majority (>=`M`) of `ChangeView1(v+1)` messages collected, but
+ `DoCV1(v+1)` is missing for a long time, then the node is able to "skip" view
+ `v+1` and send the `ChangeView1(v+2)` message hoping that the primary of `v+2`
+ will be faster enough to send the `DoCV1(v+2)` signal. The process can be repeated
+ on timeout for view `v+3`, etc.
+ * If there's more than `F` nodes that have sent their preparation messages
+ (and, consequently, announced their desire to transmit to the stage `II` of the
+ current view rather than to change view), then it's clear that it won't be more than `F` messages
+ of type `ChangeView1` to perform transition to the next view from the stage `II`.
+ Thus, the node is allowed to send its `ChangeView2` message (and change its
+ state to the `cv2 to v'=v+1`). Such situation may happen if the node haven't
+ proposal received in time (consider valid proposal).
+
+#### Stage II
+
+Once the node has entered the stage `II`, the proposal of the current round is
+considered to be valid. Depending on the node's state the following decisions are
+possible:
+
+* If the node has its `Commit` sent and is in the `commitSent` state:
+ * If the majority (>=`M`) of the `Commit` messages has been received, then the
+ block may be safely accepted for the current proposal.
+ * If there's not enough `Commit` messages for a long time, then it's legal to
+ send the `ChangeView2(v+1)` message, transmit to the `cv2 to v'=v+1` state
+ and decide to go to the next view `v+1` preserving the current proposal
+ and hoping that it would be possible to collect enough `Commit` messages
+ for it in the view `v+1`.
+* If the node is in the `cv2 to v'=v+1` state then:
+ * If there's a majority (>=`M`) of `ChangeView2(v+1)` messages and the node is
+ primary in the view `v+1` then it should send the signal (`DoCV2(v+1)` message)
+ to the rest of the group to change their view to `v+1` with the old proposal of view `v`
+ preserved. The rest of the group (backup on `v+1` view that have sent their
+ `ChangeVeiew2(v+1)` messages) should change their view on `DoCV2(v+1)` receiving.
+ * If there's a majority (>=`M`) of `ChangeView2(v+1)` messages collected, but
+ `DoCV2(v+1)` is missing for a long time, then the node is able to "skip" view
+ `v+1` and send the `ChangeView2(v+2)` message hoping that the primary of `v+2`
+ will be faster enough to send the `DoCV2(v+2)` signal. The process can be repeated
+ on timeout for view `v+3`, etc.
+ * Finally, if the node receives at least `M` messages from the stage `I` at max
+ `F` of which are preparations (the blue dotted arrow from `cv2 to v'=v+1` to
+ `cv1 to v'=v+1` state), it has the ability to go back to the `cv1` state to start
+ the new consensus round with the new proposal. This case is kind of special,
+ it allows to escape from the deadlock situation when the node is locked on `cv2`
+ state unable to perform any further steps whereas the rest of the network are
+ waiting in the `cv1` state. Consider the case of four-nodes network where the
+ first node is permanently "dead", the primary have sent its `PrepareRequest`
+ and went to the `cv2` state on the timeout and the rest two nodes are waiting
+ in the `cv1` state not able to move further.
+
+It should be noted that "preserving the proposal of view `v` in view `v+1`" means
+that the primary of view `v+1` broadcasts the `PrepareRequest` message at view `v+1`
+that contains the same set of block's fields (transactions, timestamp, primary, etc) as
+the `PrepareRequest` proposed in the view `v` has.
+
+Here's the scheme of transitions between consensus node states for the improved
+dBFT 2.1 model with the centralized view changes process:
+
+![dBFT 2.1 model with the centralized view changes](./.github/dbft2.1_centralizedCV.png)
+
+Here you can find the specification file and the basic TLC Model Checker launch
+configuration:
+
+* [TLA⁺ specification](./dbft2.1_centralizedCV/dbftCentralizedCV.tla)
+* [TLC Model Checker configuration](./dbft2.1_centralizedCV/dbftCentralizedCV___AllGoodModel.launch)
+
## How to run/check the TLA⁺ specification
### Prerequirements
@@ -137,5 +381,14 @@ configuration:
5. Open the `Model Overview` window in the TLA⁺ Toolbox and check that behaviour
specification, declared constants, invariants and properties of the model are
filled in with some values.
-6. Press `Run TLC on the model` bottom to start the model checking process and
- explore the progress in the `Model Checkng Results` window.
\ No newline at end of file
+6. Press `Run TLC on the model` button to start the model checking process and
+ explore the progress in the `Model Checkng Results` window.
+
+### Model checking note
+
+It should be noted that all TLA⁺ specifications provided in this repo can be perfectly checked
+with `MaxView` model constraint set to be 1 for the four-nodes network scenario. Larger
+`MaxView` values produces too many behaviours to be checked, so TLC Model Checker is likely
+to fail with OOM during the checking process. However, `MaxView` set to be 1 is enough to check
+the model liveness properties for the four-nodes scenario as there are two views to be checked
+in this case (0 and 1).
\ No newline at end of file
diff --git a/formal-models/dbft/dbft___AllGoodModel.launch b/formal-models/dbft/dbft___AllGoodModel.launch
index eb14599a..52b9984e 100644
--- a/formal-models/dbft/dbft___AllGoodModel.launch
+++ b/formal-models/dbft/dbft___AllGoodModel.launch
@@ -26,7 +26,7 @@
-
+
diff --git a/formal-models/dbft2.1_centralizedCV/dbftCentralizedCV.tla b/formal-models/dbft2.1_centralizedCV/dbftCentralizedCV.tla
new file mode 100644
index 00000000..5e1d6260
--- /dev/null
+++ b/formal-models/dbft2.1_centralizedCV/dbftCentralizedCV.tla
@@ -0,0 +1,507 @@
+-------------------------------- MODULE dbftCentralizedCV --------------------------------
+
+EXTENDS
+ Integers,
+ FiniteSets
+
+CONSTANTS
+ \* RM is the set of consensus node indexes starting from 0.
+ \* Example: {0, 1, 2, 3}
+ RM,
+
+ \* RMFault is a set of consensus node indexes that are allowed to become
+ \* FAULT in the middle of every considered behavior and to send any
+ \* consensus message afterwards. RMFault must be a subset of RM. An empty
+ \* set means that all nodes are good in every possible behaviour.
+ \* Examples: {0}
+ \* {1, 3}
+ \* {}
+ RMFault,
+
+ \* RMDead is a set of consensus node indexes that are allowed to die in the
+ \* middle of every behaviour and do not send any message afterwards. RMDead
+ \* must be a subset of RM. An empty set means that all nodes are alive and
+ \* responding in in every possible behaviour. RMDead may intersect the
+ \* RMFault set which means that node which is in both RMDead and RMFault
+ \* may become FAULT and send any message starting from some step of the
+ \* particular behaviour and may also die in the same behaviour which will
+ \* prevent it from sending any message.
+ \* Examples: {0}
+ \* {3, 2}
+ \* {}
+ RMDead,
+
+ \* MaxView is the maximum allowed view to be considered (starting from 0,
+ \* including the MaxView itself). This constraint was introduced to reduce
+ \* the number of possible model states to be checked. It is recommended to
+ \* keep this setting not too high (< N is highly recommended).
+ \* Example: 2
+ MaxView
+
+VARIABLES
+ \* rmState is a set of consensus node states. It is represented by the
+ \* mapping (function) with domain RM and range RMStates. I.e. rmState[r] is
+ \* the state of the r-th consensus node at the current step.
+ rmState,
+
+ \* msgs is the shared pool of messages sent to the network by consensus nodes.
+ \* It is represented by a subset of Messages set.
+ msgs,
+
+ \* blockAccepted holds the view number when the accepted block's proposal
+ \* was firstly created for each consensus node. It is represented by a
+ \* mapping RM -> Nat and needed for InvTwoBlocksAcceptedAdvanced invariant
+ \* evaluation.
+ blockAccepted
+
+\* vars is a tuple of all variables used in the specification. It is needed to
+\* simplify fairness conditions definition.
+vars == <>
+
+\* N is the number of validators.
+N == Cardinality(RM)
+
+\* F is the number of validators that are allowed to be malicious.
+F == (N - 1) \div 3
+
+\* M is the number of validators that must function correctly.
+M == N - F
+
+\* These assumptions are checked by the TLC model checker once at the start of
+\* the model checking process. All the input data (declared constants) specified
+\* in the "Model Overview" section must satisfy these constraints.
+ASSUME
+ /\ RM \subseteq Nat
+ /\ N >= 4
+ /\ 0 \in RM
+ /\ RMFault \subseteq RM
+ /\ RMDead \subseteq RM
+ /\ Cardinality(RMFault) <= F
+ /\ Cardinality(RMDead) <= F
+ /\ Cardinality(RMFault \cup RMDead) <= F
+ /\ MaxView \in Nat
+ /\ MaxView <= 2
+
+\* RMStates is a set of records where each record holds the node state and
+\* the node current view.
+RMStates == [
+ type: {"initialized", "prepareSent", "commitSent", "blockAccepted", "cv1", "cv2", "bad", "dead"},
+ view : Nat
+ ]
+\* Messages is a set of records where each record holds the message type,
+\* the message sender, sender's view by the moment when message was sent
+\* (view field), sender's view by the first moment the PrepareRequest was
+\* originally proposed (sourceView field) and the target view for
+\* ChangeView[1,2]/DoChangeView[1,2] messages (targetView field).
+Messages == [type : {"PrepareRequest", "PrepareResponse", "Commit", "ChangeView1", "ChangeView2", "DoChangeView1", "DoChangeView2"}, rm : RM, view : Nat, targetView : Nat, sourceView : Nat]
+
+\* -------------- Useful operators --------------
+
+\* IsPrimaryInTheView is an operator defining whether provided node r
+\* is primary in the consensus round view from the r's point of view.
+\* It is a mapping from RM to the set of {TRUE, FALSE}.
+IsPrimaryInTheView(r, view) == view % N = r
+
+\* IsPrimary is an operator defining whether provided node r is primary
+\* for the current round from the r's point of view. It is a mapping
+\* from RM to the set of {TRUE, FALSE}.
+IsPrimary(r) == IsPrimaryInTheView(r, rmState[r].view)
+
+\* GetPrimary is an operator defining mapping from round index to the RM that
+\* is primary in this round.
+GetPrimary(view) == CHOOSE r \in RM : view % N = r
+
+\* GetNewView returns new view number based on the previous node view value.
+\* Current specifications only allows to increment view.
+GetNewView(oldView) == oldView + 1
+
+\* PrepareRequestSentOrReceived denotes whether there's a PrepareRequest
+\* message received from the current round's speaker (as the node r sees it).
+PrepareRequestSentOrReceived(r) == Cardinality({msg \in msgs : msg.type = "PrepareRequest"/\ msg.rm = GetPrimary(rmState[r].view) /\ msg.view = rmState[r].view}) /= 0
+
+\* -------------- Safety temporal formula --------------
+
+\* Init is the initial predicate initializing values at the start of every
+\* behaviour.
+Init ==
+ /\ rmState = [r \in RM |-> [type |-> "initialized", view |-> 0]]
+ /\ msgs = {}
+ /\ blockAccepted = [r \in RM |-> 0]
+
+\* RMSendPrepareRequest describes the primary node r originally broadcasting PrepareRequest.
+RMSendPrepareRequest(r) ==
+ /\ rmState[r].type = "initialized"
+ /\ IsPrimary(r)
+ /\ rmState' = [rmState EXCEPT ![r].type = "prepareSent"]
+ /\ msgs' = msgs \cup {[type |-> "PrepareRequest", rm |-> r, view |-> rmState[r].view, targetView |-> 0, sourceView |-> rmState[r].view]}
+ /\ UNCHANGED <>
+
+\* RMSendPrepareResponse describes non-primary node r receiving PrepareRequest from
+\* the primary node of the current round (view) and broadcasting PrepareResponse.
+\* This step assumes that PrepareRequest always contains valid transactions and
+\* signatures.
+RMSendPrepareResponse(r) ==
+ /\ rmState[r].type = "initialized"
+ /\ \neg IsPrimary(r)
+ /\ PrepareRequestSentOrReceived(r)
+ /\ LET pReq == CHOOSE msg \in msgs : msg.type = "PrepareRequest" /\ msg.rm = GetPrimary(rmState[r].view) /\ msg.view = rmState[r].view
+ IN /\ rmState' = [rmState EXCEPT ![r].type = "prepareSent"]
+ /\ msgs' = msgs \cup {[type |-> "PrepareResponse", rm |-> r, view |-> rmState[r].view, targetView |-> 0, sourceView |-> pReq.sourceView]}
+ /\ UNCHANGED <>
+
+
+\* RMSendCommit describes node r sending Commit if there's enough PrepareResponse
+\* messages.
+RMSendCommit(r) ==
+ /\ rmState[r].type = "prepareSent"
+ /\ Cardinality({
+ msg \in msgs : (msg.type = "PrepareResponse" \/ msg.type = "PrepareRequest") /\ msg.view = rmState[r].view
+ }) >= M
+ /\ PrepareRequestSentOrReceived(r)
+ /\ LET pReq == CHOOSE msg \in msgs : msg.type = "PrepareRequest" /\ msg.rm = GetPrimary(rmState[r].view) /\ msg.view = rmState[r].view
+ IN /\ rmState' = [rmState EXCEPT ![r].type = "commitSent"]
+ /\ msgs' = msgs \cup {[type |-> "Commit", rm |-> r, view |-> rmState[r].view, targetView |-> 0, sourceView |-> pReq.sourceView]}
+ /\ UNCHANGED <>
+
+\* RMAcceptBlock describes node r collecting enough Commit messages and accepting
+\* the block.
+RMAcceptBlock(r) ==
+ /\ rmState[r].type /= "bad"
+ /\ rmState[r].type /= "dead"
+ /\ rmState[r].type /= "blockAccepted"
+ /\ PrepareRequestSentOrReceived(r)
+ /\ Cardinality({msg \in msgs : msg.type = "Commit" /\ msg.view = rmState[r].view}) >= M
+ /\ LET pReq == CHOOSE msg \in msgs : msg.type = "PrepareRequest" /\ msg.rm = GetPrimary(rmState[r].view) /\ msg.view = rmState[r].view
+ IN /\ rmState' = [rmState EXCEPT ![r].type = "blockAccepted"]
+ /\ blockAccepted' = [blockAccepted EXCEPT ![r] = pReq.sourceView]
+ /\ UNCHANGED <>
+
+\* FetchBlock describes node r that fetches the accepted block from some other node.
+RMFetchBlock(r) ==
+ /\ rmState[r].type /= "bad"
+ /\ rmState[r].type /= "dead"
+ /\ rmState[r].type /= "blockAccepted"
+ /\ \E rmAccepted \in RM : /\ rmState[rmAccepted].type = "blockAccepted"
+ /\ rmState' = [rmState EXCEPT ![r].type = "blockAccepted", ![r].view = rmState[rmAccepted].view]
+ /\ blockAccepted' = [blockAccepted EXCEPT ![r] = blockAccepted[rmAccepted]]
+ /\ UNCHANGED <>
+
+\* RMSendChangeView1 describes node r sending ChangeView1 message on timeout
+\* during waiting for PrepareResponse or node r in "cv2" state receiving M
+\* messages from the I stage not more than F of them are preparations.
+RMSendChangeView1(r) ==
+ /\ \/ /\ rmState[r].type = "initialized"
+ /\ \neg IsPrimary(r)
+ \/ /\ rmState[r].type = "cv2"
+ /\ Cardinality({msg \in msgs : /\ (msg.type = "ChangeView1" \/ msg.type = "PrepareRequest" \/ msg.type = "PrepareResponse")
+ /\ msg.view = rmState[r].view
+ }) >= M
+ /\ Cardinality({msg \in msgs : /\ (msg.type = "PrepareRequest" \/ msg.type = "PrepareResponse")
+ /\ msg.view = rmState[r].view
+ }) <= F
+ /\ rmState' = [rmState EXCEPT ![r].type = "cv1"]
+ /\ msgs' = msgs \cup {[type |-> "ChangeView1", rm |-> r, view |-> rmState[r].view, targetView |-> GetNewView(rmState[r].view), sourceView |-> rmState[r].view]}
+ /\ UNCHANGED <>
+
+\* RMSendChangeView1FromCV1 describes node r sending ChangeView1 message on timeout
+\* during waiting for DoCV1 signal from the next primary.
+RMSendChangeView1FromCV1(r) ==
+ /\ rmState[r].type = "cv1"
+ /\ LET cv1s == {msg \in msgs : msg.type = "ChangeView1" /\ msg.view = rmState[r].view}
+ myCV1s == {msg \in cv1s : msg.rm = r}
+ myBestCV1 == CHOOSE msg \in myCV1s : \A other \in myCV1s : msg.targetView >= other.targetView
+ IN /\ Cardinality({msg \in cv1s : msg.targetView = myBestCV1.targetView}) >= M
+ /\ \neg IsPrimaryInTheView(r, myBestCV1.targetView)
+ /\ msgs' = msgs \cup {[type |-> "ChangeView1", rm |-> r, view |-> rmState[r].view, targetView |-> GetNewView(myBestCV1.targetView), sourceView |-> rmState[r].view]}
+ /\ UNCHANGED <>
+
+\* RMSendChangeView2 describes node r sending ChangeView message on timeout
+\* during waiting for enough Prepare messages OR from CV1 after not receiving
+\* enough ChangeView1 messages.
+RMSendChangeView2(r) ==
+ /\ \/ rmState[r].type = "prepareSent"
+ \/ rmState[r].type = "commitSent"
+ \/ /\ rmState[r].type = "cv1"
+ /\ Cardinality({msg \in msgs : /\ (msg.type = "PrepareRequest" \/ msg.type = "PrepareResponse" \/ msg.type = "ChangeView1")
+ /\ msg.view = rmState[r].view
+ /\ (msg.targetView = 0 \/ msg.targetView = GetNewView(rmState[r].view))
+ }) >= M
+ /\ Cardinality({msg \in msgs : /\ (msg.type = "PrepareRequest" \/ msg.type = "PrepareResponse")
+ /\ msg.view = rmState[r].view
+ /\ (msg.targetView = 0 \/ msg.targetView = GetNewView(rmState[r].view))
+ }) > F
+ /\ LET pReq == CHOOSE msg \in msgs : msg.type = "PrepareRequest" /\ msg.rm = GetPrimary(rmState[r].view) /\ msg.view = rmState[r].view
+ IN /\ rmState' = [rmState EXCEPT ![r].type = "cv2"]
+ /\ msgs' = msgs \cup {[type |-> "ChangeView2", rm |-> r, view |-> rmState[r].view, targetView |-> GetNewView(rmState[r].view), sourceView |-> pReq.sourceView]}
+ /\ UNCHANGED <>
+
+\* RMSendChangeView2FromCV2 describes node r sending ChangeView2 message on timeout
+\* during waiting for DoCV2 signal from the next primary.
+RMSendChangeView2FromCV2(r) ==
+ /\ rmState[r].type = "cv2"
+ /\ LET cv2s == {msg \in msgs : msg.type = "ChangeView2" /\ msg.view = rmState[r].view}
+ myCV2s == {msg \in cv2s : msg.rm = r}
+ myBestCV2 == CHOOSE msg \in myCV2s : \A other \in myCV2s : msg.targetView >= other.targetView
+ pReq == CHOOSE msg \in msgs : msg.type = "PrepareRequest" /\ msg.rm = GetPrimary(rmState[r].view) /\ msg.view = rmState[r].view
+ IN /\ Cardinality({msg \in cv2s : msg.targetView = myBestCV2.targetView}) >= M
+ /\ \neg IsPrimaryInTheView(r, myBestCV2.targetView)
+ /\ msgs' = msgs \cup {[type |-> "ChangeView2", rm |-> r, view |-> rmState[r].view, targetView |-> GetNewView(myBestCV2.targetView), sourceView |-> pReq.sourceView]}
+ /\ UNCHANGED <>
+
+\* RMSendDoCV1ByLeader describes node r that collects enough ChangeView1 messages
+\* with target view such that the node r is leader in this view. The leader r
+\* broadcasts DoChangeView1 message and the newly-created PrepareRequest message
+\* for this view.
+RMSendDoCV1ByLeader(r) ==
+ /\ rmState[r].type /= "bad"
+ /\ rmState[r].type /= "dead"
+ /\ rmState[r].type /= "blockAccepted"
+ /\ LET cv1s == {msg \in msgs : msg.type = "ChangeView1" /\ msg.view = rmState[r].view}
+ followersCV1s == {msg \in cv1s : IsPrimaryInTheView(r, msg.targetView)} \* TODO: this condition won't work starting from N+1 view!
+ targetView == CHOOSE x \in 1..(MaxView+1) : IsPrimaryInTheView(r, x)
+ IN /\ Cardinality(followersCV1s) >= M
+ /\ rmState' = [rmState EXCEPT ![r].type = "prepareSent", ![r].view = targetView]
+ /\ msgs' = msgs \cup {[type |-> "DoChangeView1", rm |-> r, view |-> rmState[r].view, targetView |-> targetView, sourceView |-> targetView], [type |-> "PrepareRequest", rm |-> r, view |-> targetView, targetView |-> 0, sourceView |-> targetView]}
+ /\ UNCHANGED <>
+
+\* RMSendDoCV2ByLeader describes node r that collects enough ChangeView2 messages
+\* with target view such that the node r is leader in this view. The leader r
+\* broadcasts DoChangeView2 message and the old PrepareRequest message that
+\* was migrated from the previous view without changes.
+RMSendDoCV2ByLeader(r) ==
+ /\ rmState[r].type /= "bad"
+ /\ rmState[r].type /= "dead"
+ /\ rmState[r].type /= "blockAccepted"
+ /\ LET cv2s == {msg \in msgs : msg.type = "ChangeView2" /\ msg.view = rmState[r].view}
+ followersCV2s == {msg \in cv2s : IsPrimaryInTheView(r, msg.targetView)}
+ targetView == CHOOSE x \in 1..(MaxView+1) : IsPrimaryInTheView(r, x)
+ IN /\ Cardinality(followersCV2s) >= M
+ /\ LET pReq == CHOOSE msg \in msgs : msg.type = "PrepareRequest" /\ msg.rm = GetPrimary(rmState[r].view) /\ msg.view = rmState[r].view
+ IN /\ rmState' = [rmState EXCEPT ![r].type = "prepareSent", ![r].view = targetView]
+ /\ msgs' = msgs \cup {[type |-> "DoChangeView2", rm |-> r, view |-> rmState[r].view, targetView |-> targetView, sourceView |-> pReq.sourceView], [type |-> "PrepareRequest", rm |-> r, view |-> targetView, targetView |-> 0, sourceView |-> pReq.sourceView]}
+ /\ UNCHANGED <>
+
+\* RMReceiveDoCV1FromLeader descibes node r that receives DoChangeView1 message from
+\* the leader of the target DoCV1's view and changes its view.
+RMReceiveDoCV1FromLeader(r) ==
+ /\ rmState[r].type /= "bad"
+ /\ rmState[r].type /= "blockAccepted"
+ /\ rmState[r].type /= "dead"
+ /\ Cardinality({msg \in msgs : msg.type = "DoChangeView1" /\ msg.targetView > rmState[r].view}) /= 0
+ /\ LET doCV1s == {msg \in msgs : msg.type = "DoChangeView1" /\ msg.targetView > rmState[r].view}
+ latestDoCV1 == CHOOSE msg \in doCV1s : \A other \in doCV1s : msg.targetView >= other.targetView
+ IN /\ rmState' = [rmState EXCEPT ![r].type = "initialized", ![r].view = latestDoCV1.targetView]
+ /\ UNCHANGED <>
+
+\* RMReceiveDoCV2FromLeader descibes node r that receives DoChangeView2 message from
+\* the leader of the target DoCV2's view and changes its view.
+RMReceiveDoCV2FromLeader(r) ==
+ /\ rmState[r].type /= "bad"
+ /\ rmState[r].type /= "blockAccepted"
+ /\ rmState[r].type /= "dead"
+ /\ Cardinality({msg \in msgs : msg.type = "DoChangeView2" /\ msg.targetView > rmState[r].view}) /= 0
+ /\ LET doCV2s == {msg \in msgs : msg.type = "DoChangeView2" /\ msg.targetView > rmState[r].view}
+ latestDoCV2 == CHOOSE msg \in doCV2s : \A other \in doCV2s : msg.targetView >= other.targetView
+ IN /\ rmState' = [rmState EXCEPT ![r].type = "initialized", ![r].view = latestDoCV2.targetView]
+ /\ UNCHANGED <>
+
+\* RMBeBad describes the faulty node r that will send any kind of consensus message starting
+\* from the step it's gone wild. This step is enabled only when RMFault is non-empty set.
+RMBeBad(r) ==
+ /\ r \in RMFault
+ /\ Cardinality({rm \in RM : rmState[rm].type = "bad"}) < F
+ /\ rmState' = [rmState EXCEPT ![r].type = "bad"]
+ /\ UNCHANGED <>
+
+\* RMFaultySendCV1 describes sending CV1 message by the faulty node r. To reduce
+\* the number of reachable states, the target view of this message is restricted by
+\* the next one.
+RMFaultySendCV1(r) ==
+ /\ rmState[r].type = "bad"
+ /\ LET cv == [type |-> "ChangeView1", rm |-> r, view |-> rmState[r].view, targetView |-> GetNewView(rmState[r].view), sourceView |-> rmState[r].view]
+ IN /\ cv \notin msgs
+ /\ msgs' = msgs \cup {cv}
+ /\ UNCHANGED <>
+
+\* RMFaultySendCV2 describes sending CV2 message by the faulty node r. To reduce
+\* the number of reachable states, the target view of this message is restricted by
+\* the next one; the source view of this message is restricted by the current one.
+RMFaultySendCV2(r) ==
+ /\ rmState[r].type = "bad"
+ /\ LET cv == [type |-> "ChangeView2", rm |-> r, view |-> rmState[r].view, targetView |-> GetNewView(rmState[r].view), sourceView |-> rmState[r].view]
+ IN /\ cv \notin msgs
+ /\ msgs' = msgs \cup {cv}
+ /\ UNCHANGED <>
+
+\* RMFaultyDoCV describes view changing by the faulty node r.
+RMFaultyDoCV(r) ==
+ /\ rmState[r].type = "bad"
+ /\ rmState' = [rmState EXCEPT ![r].view = GetNewView(rmState[r].view)]
+ /\ UNCHANGED <>
+
+\* RMFaultySendPReq describes sending PrepareRequest message by the primary faulty node r.
+\* To reduce the number of reachable states, the sourceView is always restricted by the
+\* current r's view.
+RMFaultySendPReq(r) ==
+ /\ rmState[r].type = "bad"
+ /\ IsPrimary(r)
+ /\ LET pReq == [type |-> "PrepareRequest", rm |-> r, view |-> rmState[r].view, targetView |-> 0, sourceView |-> rmState[r].view]
+ IN /\ pReq \notin msgs
+ /\ msgs' = msgs \cup {pReq}
+ /\ UNCHANGED <>
+
+\* RMFaultySendPResp describes sending PrepareResponse message by the non-primary faulty node r.
+\* To reduce the number of reachable states, the sourceView is always restricted by the
+\* current r's view.
+RMFaultySendPResp(r) ==
+ /\ rmState[r].type = "bad"
+ /\ \neg IsPrimary(r)
+ /\ LET pResp == [type |-> "PrepareResponse", rm |-> r, view |-> rmState[r].view, targetView |-> 0, sourceView |-> rmState[r].view]
+ IN /\ pResp \notin msgs
+ /\ msgs' = msgs \cup {pResp}
+ /\ UNCHANGED <>
+
+\* RMFaultySendCommit describes sending Commit message by the faulty node r.
+\* To reduce the number of reachable states, the sourceView is always restricted by the
+\* current r's view.
+RMFaultySendCommit(r) ==
+ /\ rmState[r].type = "bad"
+ /\ LET commit == [type |-> "Commit", rm |-> r, view |-> rmState[r].view, targetView |-> 0, sourceView |-> rmState[r].view]
+ IN /\ commit \notin msgs
+ /\ msgs' = msgs \cup {commit}
+ /\ UNCHANGED <>
+
+\* We don't describe sending DoCV messages by faulty node, because it can't
+\* actually produce other than valid message, and valid message sending is described
+\* in the "good" node specification. We also don't describe receiving the DoCV message
+\* by the faulty node because it has a separate RMFaultyDoCV action enabled.
+
+\* RMDie describes node r that was removed from the network at the particular step
+\* of the behaviour. After this node r can't change its state and accept/send messages.
+RMDie(r) ==
+ /\ r \in RMDead
+ /\ Cardinality({rm \in RM : rmState[rm].type = "dead"}) < F
+ /\ rmState' = [rmState EXCEPT ![r].type = "dead"]
+ /\ UNCHANGED <>
+
+\* Terminating is an action that allows infinite stuttering to prevent deadlock on
+\* behaviour termination. We consider termination to be valid if at least M nodes
+\* have the block being accepted.
+Terminating ==
+ /\ Cardinality({rm \in RM : rmState[rm].type = "blockAccepted"}) >= M
+ /\ UNCHANGED vars
+
+
+\* Next is the next-state action describing the transition from the current state
+\* to the next state of the behaviour.
+Next ==
+ \/ Terminating
+ \/ \E r \in RM:
+ RMSendPrepareRequest(r) \/ RMSendPrepareResponse(r) \/ RMSendCommit(r)
+ \/ RMAcceptBlock(r)
+ \/ RMSendChangeView1(r) \/ RMSendChangeView1FromCV1(r)
+ \/ RMSendChangeView2(r) \/ RMSendChangeView2FromCV2(r)
+ \/ RMSendDoCV1ByLeader(r) \/ RMReceiveDoCV1FromLeader(r)
+ \/ RMSendDoCV2ByLeader(r) \/ RMReceiveDoCV2FromLeader(r)
+ \/ RMBeBad(r)
+ \/ RMFaultySendCV1(r) \/ RMFaultySendCV2(r) \/ RMFaultyDoCV(r) \/ RMFaultySendCommit(r) \/ RMFaultySendPReq(r) \/ RMFaultySendPResp(r)
+ \/ RMDie(r) \/ RMFetchBlock(r)
+
+\* Safety is a temporal formula that describes the whole set of allowed
+\* behaviours. It specifies only what the system MAY do (i.e. the set of
+\* possible allowed behaviours for the system). It asserts only what may
+\* happen; any behaviour that violates it does so at some point and
+\* nothing past that point makes difference.
+\*
+\* E.g. this safety formula (applied standalone) allows the behaviour to end
+\* with an infinite set of stuttering steps (those steps that DO NOT change
+\* neither msgs nor rmState) and never reach the state where at least one
+\* node is committed or accepted the block.
+\*
+\* To forbid such behaviours we must specify what the system MUST
+\* do. It will be specified below with the help of fairness conditions in
+\* the Fairness formula.
+Safety == Init /\ [][Next]_vars
+
+
+\* -------------- Fairness temporal formula --------------
+
+\* Fairness is a temporal assumptions under which the model is working.
+\* Usually it specifies different kind of assumptions for each/some
+\* subactions of the Next's state action, but the only think that bothers
+\* us is preventing infinite stuttering at those steps where some of Next's
+\* subactions are enabled. Thus, the only thing that we require from the
+\* system is to keep take the steps until it's impossible to take them.
+\* That's exactly how the weak fairness condition works: if some action
+\* remains continuously enabled, it must eventually happen.
+Fairness == WF_vars(Next)
+
+\* -------------- Specification --------------
+
+\* The complete specification of the protocol written as a temporal formula.
+Spec == Safety /\ Fairness
+
+\* -------------- Liveness temporal formula --------------
+
+\* For every possible behaviour it's true that eventually (i.e. at least once
+\* through the behaviour) block will be accepted. It is something that dBFT
+\* must guarantee (an in practice this condition is violated).
+TerminationRequirement == <>(Cardinality({r \in RM : rmState[r].type = "blockAccepted"}) >= M)
+
+\* A liveness temporal formula asserts only what must happen (i.e. specifies
+\* what the system MUST do). Any behaviour can NOT violate it at ANY point;
+\* there's always the rest of the behaviour that can always make the liveness
+\* formula true; if there's no such behaviour than the liveness formula is
+\* violated. The liveness formula is supposed to be checked as a property
+\* by the TLC model checker.
+Liveness == TerminationRequirement
+
+\* -------------- ModelConstraints --------------
+
+\* MaxViewConstraint is a state predicate restricting the number of possible
+\* behaviour states. It is needed to reduce model checking time and prevent
+\* the model graph size explosion. This formulae must be specified at the
+\* "State constraint" section of the "Additional Spec Options" section inside
+\* the model overview.
+MaxViewConstraint == /\ \A r \in RM : rmState[r].view <= MaxView
+ /\ \A msg \in msgs : msg.targetView = 0 \/ msg.targetView <= MaxView + 1
+
+\* -------------- Invariants of the specification --------------
+
+\* Model invariant is a state predicate (statement) that must be true for
+\* every step of every reachable behaviour. Model invariant is supposed to
+\* be checked as an Invariant by the TLC Model Checker.
+
+\* TypeOK is a type-correctness invariant. It states that all elements of
+\* specification variables must have the proper type throughout the behaviour.
+TypeOK ==
+ /\ rmState \in [RM -> RMStates]
+ /\ msgs \subseteq Messages
+ /\ blockAccepted \in [RM -> Nat]
+
+\* InvTwoBlocksAcceptedAdvanced ensures that the proposed and accepted block
+\* originally comes from the same view for every node that has the block
+\* being accepted.
+InvTwoBlocksAcceptedAdvanced == \A r1 \in RM:
+ \A r2 \in RM \ {r1}:
+ \/ rmState[r1].type /= "blockAccepted"
+ \/ rmState[r2].type /= "blockAccepted"
+ \/ blockAccepted[r1] = blockAccepted[r2]
+
+\* InvFaultNodesCount states that there can be F faulty or dead nodes at max.
+InvFaultNodesCount == Cardinality({
+ r \in RM : rmState[r].type = "bad" \/ rmState[r].type = "dead"
+ }) <= F
+
+\* This theorem asserts the truth of the temporal formula whose meaning is that
+\* the state predicates TypeOK, InvTwoBlocksAccepted and InvFaultNodesCount are
+\* the invariants of the specification Spec. This theorem is not supposed to be
+\* checked by the TLC model checker, it's here for the reader's understanding of
+\* the purpose of TypeOK, InvTwoBlocksAccepted and InvFaultNodesCount.
+THEOREM Spec => [](TypeOK /\ InvTwoBlocksAcceptedAdvanced /\ InvFaultNodesCount)
+=============================================================================
+\* Modification History
+\* Last modified Fri Mar 03 10:51:05 MSK 2023 by root
+\* Last modified Wed Feb 15 15:43:25 MSK 2023 by anna
+\* Last modified Mon Jan 23 21:49:06 MSK 2023 by rik
+\* Created Thu Dec 15 16:06:17 MSK 2022 by anna
\ No newline at end of file
diff --git a/formal-models/dbft2.1_centralizedCV/dbftCentralizedCV___AllGoodModel.launch b/formal-models/dbft2.1_centralizedCV/dbftCentralizedCV___AllGoodModel.launch
new file mode 100644
index 00000000..f7a19d40
--- /dev/null
+++ b/formal-models/dbft2.1_centralizedCV/dbftCentralizedCV___AllGoodModel.launch
@@ -0,0 +1,42 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/formal-models/dbft2.1_threeStagedCV/dbftCV3.tla b/formal-models/dbft2.1_threeStagedCV/dbftCV3.tla
new file mode 100644
index 00000000..536934ce
--- /dev/null
+++ b/formal-models/dbft2.1_threeStagedCV/dbftCV3.tla
@@ -0,0 +1,427 @@
+-------------------------------- MODULE dbftCV3 --------------------------------
+
+EXTENDS
+ Integers,
+ FiniteSets
+
+CONSTANTS
+ \* RM is the set of consensus node indexes starting from 0.
+ \* Example: {0, 1, 2, 3}
+ RM,
+
+ \* RMFault is a set of consensus node indexes that are allowed to become
+ \* FAULT in the middle of every considered behavior and to send any
+ \* consensus message afterwards. RMFault must be a subset of RM. An empty
+ \* set means that all nodes are good in every possible behaviour.
+ \* Examples: {0}
+ \* {1, 3}
+ \* {}
+ RMFault,
+
+ \* RMDead is a set of consensus node indexes that are allowed to die in the
+ \* middle of every behaviour and do not send any message afterwards. RMDead
+ \* must be a subset of RM. An empty set means that all nodes are alive and
+ \* responding in in every possible behaviour. RMDead may intersect the
+ \* RMFault set which means that node which is in both RMDead and RMFault
+ \* may become FAULT and send any message starting from some step of the
+ \* particular behaviour and may also die in the same behaviour which will
+ \* prevent it from sending any message.
+ \* Examples: {0}
+ \* {3, 2}
+ \* {}
+ RMDead,
+
+ \* MaxView is the maximum allowed view to be considered (starting from 0,
+ \* including the MaxView itself). This constraint was introduced to reduce
+ \* the number of possible model states to be checked. It is recommended to
+ \* keep this setting not too high (< N is highly recommended).
+ \* Example: 2
+ MaxView
+
+VARIABLES
+ \* rmState is a set of consensus node states. It is represented by the
+ \* mapping (function) with domain RM and range RMStates. I.e. rmState[r] is
+ \* the state of the r-th consensus node at the current step.
+ rmState,
+
+ \* msgs is the shared pool of messages sent to the network by consensus nodes.
+ \* It is represented by a subset of Messages set.
+ msgs
+
+\* vars is a tuple of all variables used in the specification. It is needed to
+\* simplify fairness conditions definition.
+vars == <>
+
+\* N is the number of validators.
+N == Cardinality(RM)
+
+\* F is the number of validators that are allowed to be malicious.
+F == (N - 1) \div 3
+
+\* M is the number of validators that must function correctly.
+M == N - F
+
+\* These assumptions are checked by the TLC model checker once at the start of
+\* the model checking process. All the input data (declared constants) specified
+\* in the "Model Overview" section must satisfy these constraints.
+ASSUME
+ /\ RM \subseteq Nat
+ /\ N >= 4
+ /\ 0 \in RM
+ /\ RMFault \subseteq RM
+ /\ RMDead \subseteq RM
+ /\ Cardinality(RMFault) <= F
+ /\ Cardinality(RMDead) <= F
+ /\ Cardinality(RMFault \cup RMDead) <= F
+ /\ MaxView \in Nat
+ /\ MaxView <= 2
+
+\* RMStates is a set of records where each record holds the node state and
+\* the node current view.
+RMStates == [
+ type: {"initialized", "prepareSent", "commitSent", "blockAccepted", "cv1", "cv2", "cv3", "bad", "dead"},
+ view : Nat
+ ]
+
+\* Messages is a set of records where each record holds the message type,
+\* the message sender and sender's view by the moment when message was sent.
+Messages == [type : {"PrepareRequest", "PrepareResponse", "Commit", "ChangeView1", "ChangeView2", "ChangeView3"}, rm : RM, view : Nat]
+
+\* -------------- Useful operators --------------
+
+\* IsPrimary is an operator defining whether provided node r is primary
+\* for the current round from the r's point of view. It is a mapping
+\* from RM to the set of {TRUE, FALSE}.
+IsPrimary(r) == rmState[r].view % N = r
+
+\* GetPrimary is an operator defining mapping from round index to the RM that
+\* is primary in this round.
+GetPrimary(view) == CHOOSE r \in RM : view % N = r
+
+\* GetNewView returns new view number based on the previous node view value.
+\* Current specifications only allows to increment view.
+GetNewView(oldView) == oldView + 1
+
+\* PrepareRequestSentOrReceived denotes whether there's a PrepareRequest
+\* message received from the current round's speaker (as the node r sees it).
+PrepareRequestSentOrReceived(r) == [type |-> "PrepareRequest", rm |-> GetPrimary(rmState[r].view), view |-> rmState[r].view] \in msgs
+
+\* -------------- Safety temporal formula --------------
+
+\* Init is the initial predicate initializing values at the start of every
+\* behaviour.
+Init ==
+ /\ rmState = [r \in RM |-> [type |-> "initialized", view |-> 0]]
+ /\ msgs = {}
+
+\* RMSendPrepareRequest describes the primary node r broadcasting PrepareRequest.
+RMSendPrepareRequest(r) ==
+ /\ rmState[r].type = "initialized"
+ /\ IsPrimary(r)
+ /\ rmState' = [rmState EXCEPT ![r].type = "prepareSent"]
+ /\ msgs' = msgs \cup {[type |-> "PrepareRequest", rm |-> r, view |-> rmState[r].view]}
+ /\ UNCHANGED <<>>
+
+\* RMSendPrepareResponse describes non-primary node r receiving PrepareRequest from
+\* the primary node of the current round (view) and broadcasting PrepareResponse.
+\* This step assumes that PrepareRequest always contains valid transactions and
+\* signatures.
+RMSendPrepareResponse(r) ==
+ /\ rmState[r].type = "initialized"
+ /\ \neg IsPrimary(r)
+ /\ PrepareRequestSentOrReceived(r)
+ /\ rmState' = [rmState EXCEPT ![r].type = "prepareSent"]
+ /\ msgs' = msgs \cup {[type |-> "PrepareResponse", rm |-> r, view |-> rmState[r].view]}
+ /\ UNCHANGED <<>>
+
+\* RMSendCommit describes node r sending Commit if there's enough PrepareRequest/PrepareResponse
+\* messages and no node has sent the ChangeView3 message. It is possible to send the Commit after
+\* the ChangeView1 or ChangeView2 message was sent with additional constraints.
+RMSendCommit(r) ==
+ /\ \/ rmState[r].type = "prepareSent"
+ \/ rmState[r].type = "cv1"
+ \/ /\ rmState[r].type = "cv2"
+ /\ Cardinality({
+ msg \in msgs : msg.type = "Commit" /\ msg.view = rmState[r].view
+ }) > F
+ /\ Cardinality({
+ msg \in msgs : (msg.type = "PrepareResponse" \/ msg.type = "PrepareRequest") /\ msg.view = rmState[r].view
+ }) >= M
+ /\ Cardinality({
+ msg \in msgs : msg.type = "ChangeView3" /\ msg.view = rmState[r].view
+ }) = 0
+ /\ PrepareRequestSentOrReceived(r)
+ /\ rmState' = [rmState EXCEPT ![r].type = "commitSent"]
+ /\ msgs' = msgs \cup {[type |-> "Commit", rm |-> r, view |-> rmState[r].view]}
+ /\ UNCHANGED <<>>
+
+\* RMAcceptBlock describes node r collecting enough Commit messages and accepting
+\* the block.
+RMAcceptBlock(r) ==
+ /\ rmState[r].type /= "bad"
+ /\ rmState[r].type /= "dead"
+ /\ rmState[r].type /= "blockAccepted"
+ /\ PrepareRequestSentOrReceived(r)
+ /\ Cardinality({
+ msg \in msgs : msg.type = "Commit" /\ msg.view = rmState[r].view
+ }) >= M
+ /\ rmState' = [rmState EXCEPT ![r].type = "blockAccepted"]
+ /\ UNCHANGED <>
+
+\* FetchBlock describes node r that fetches the accepted block from some other node.
+RMFetchBlock(r) ==
+ /\ rmState[r].type /= "bad"
+ /\ rmState[r].type /= "dead"
+ /\ rmState[r].type /= "blockAccepted"
+ /\ \E rmAccepted \in RM : /\ rmState[rmAccepted].type = "blockAccepted"
+ /\ rmState' = [rmState EXCEPT ![r].type = "blockAccepted", ![r].view = rmState[rmAccepted].view]
+ /\ UNCHANGED <>
+
+\* RMSendChangeView1 describes node r sending ChangeView1 message on timeout.
+\* Only non-primary node is allowed to send ChangeView1 message, as the primary
+\* must send the PrepareRequest if the timer fires.
+RMSendChangeView1(r) ==
+ /\ rmState[r].type = "initialized"
+ /\ \neg IsPrimary(r)
+ /\ rmState' = [rmState EXCEPT ![r].type = "cv1"]
+ /\ msgs' = msgs \cup {[type |-> "ChangeView1", rm |-> r, view |-> rmState[r].view]}
+
+\* RMSendChangeView2 describes node r sending ChangeView2 message on timeout either from
+\* "cv1" state or after the node has sent the PrepareRequest or PrepareResponse message.
+RMSendChangeView2(r) ==
+ /\ \/ /\ rmState[r].type = "prepareSent"
+ /\ Cardinality({
+ msg \in msgs : msg.type = "ChangeView1" /\ msg.view = rmState[r].view
+ }) > 0
+ \/ rmState[r].type = "cv1"
+ /\ Cardinality({
+ msg \in msgs : (msg.type = "ChangeView1" \/ msg.type = "PrepareRequest" \/ msg.type = "PrepareResponse") /\ msg.view = rmState[r].view
+ }) >= M
+ /\ \/ Cardinality({
+ msg \in msgs : msg.type = "Commit" /\ msg.view = rmState[r].view
+ }) <= F
+ \/ Cardinality({
+ msg \in msgs : msg.type = "ChangeView3" /\ msg.view = rmState[r].view
+ }) > 0
+ /\ rmState' = [rmState EXCEPT ![r].type = "cv2"]
+ /\ msgs' = msgs \cup {[type |-> "ChangeView2", rm |-> r, view |-> rmState[r].view]}
+
+\* RMSendChangeView3 describes node r sending ChangeView3 message on timeout either from
+\* "cv2" state or after the node has sent the Commit message.
+RMSendChangeView3(r) ==
+ /\ \/ rmState[r].type = "cv2"
+ \/ rmState[r].type = "commitSent"
+ /\ Cardinality({msg \in msgs : (msg.type = "ChangeView2" \/ msg.type = "Commit") /\ msg.view = rmState[r].view}) >= M
+ /\ Cardinality({msg \in msgs : (msg.type = "ChangeView2") /\ msg.view = rmState[r].view}) > 0
+ /\ Cardinality({msg \in msgs : msg.type = "Commit" /\ msg.view = rmState[r].view}) <= F
+ /\ rmState' = [rmState EXCEPT ![r].type = "cv3"]
+ /\ msgs' = msgs \cup {[type |-> "ChangeView3", rm |-> r, view |-> rmState[r].view]}
+
+\* RMReceiveChangeView describes node r receiving enough ChangeView[1,2,3] messages for
+\* view changing.
+RMReceiveChangeView(r) ==
+ /\ rmState[r].type /= "bad"
+ /\ rmState[r].type /= "dead"
+ /\ rmState[r].type /= "blockAccepted"
+ /\ \/ Cardinality({rm \in RM : Cardinality({msg \in msgs : /\ msg.rm = rm
+ /\ msg.type = "ChangeView1"
+ /\ GetNewView(msg.view) >= GetNewView(rmState[r].view)
+ }) # 0
+ }) >= M
+ \/ Cardinality({rm \in RM : Cardinality({msg \in msgs : /\ msg.rm = rm
+ /\ msg.type = "ChangeView2"
+ /\ GetNewView(msg.view) >= GetNewView(rmState[r].view)
+ }) # 0
+ }) >= M
+ \/ Cardinality({rm \in RM : Cardinality({msg \in msgs : /\ msg.rm = rm
+ /\ msg.type = "ChangeView3"
+ /\ GetNewView(msg.view) >= GetNewView(rmState[r].view)
+ }) # 0
+ }) >= M
+ /\ rmState' = [rmState EXCEPT ![r].type = "initialized", ![r].view = GetNewView(rmState[r].view)]
+ /\ UNCHANGED <>
+
+\* RMBeBad describes the faulty node r that will send any kind of consensus message starting
+\* from the step it's gone wild. This step is enabled only when RMFault is non-empty set.
+RMBeBad(r) ==
+ /\ r \in RMFault
+ /\ Cardinality({rm \in RM : rmState[rm].type = "bad"}) < F
+ /\ rmState' = [rmState EXCEPT ![r].type = "bad"]
+ /\ UNCHANGED <>
+
+\* RMFaultySendCV describes sending CV1 message by the faulty node r.
+RMFaultySendCV1(r) ==
+ /\ rmState[r].type = "bad"
+ /\ LET cv == [type |-> "ChangeView1", rm |-> r, view |-> rmState[r].view]
+ IN /\ cv \notin msgs
+ /\ msgs' = msgs \cup {cv}
+ /\ UNCHANGED <>
+
+\* RMFaultySendCV2 describes sending CV2 message by the faulty node r.
+RMFaultySendCV2(r) ==
+ /\ rmState[r].type = "bad"
+ /\ LET cv == [type |-> "ChangeView2", rm |-> r, view |-> rmState[r].view]
+ IN /\ cv \notin msgs
+ /\ msgs' = msgs \cup {cv}
+ /\ UNCHANGED <>
+
+\* RMFaultySendCV3 describes sending CV3 message by the faulty node r.
+RMFaultySendCV3(r) ==
+ /\ rmState[r].type = "bad"
+ /\ LET cv == [type |-> "ChangeView3", rm |-> r, view |-> rmState[r].view]
+ IN /\ cv \notin msgs
+ /\ msgs' = msgs \cup {cv}
+ /\ UNCHANGED <>
+
+\* RMFaultyDoCV describes view changing by the faulty node r.
+RMFaultyDoCV(r) ==
+ /\ rmState[r].type = "bad"
+ /\ rmState' = [rmState EXCEPT ![r].view = GetNewView(rmState[r].view)]
+ /\ UNCHANGED <>
+
+\* RMFaultySendPReq describes sending PrepareRequest message by the primary faulty node r.
+RMFaultySendPReq(r) ==
+ /\ rmState[r].type = "bad"
+ /\ IsPrimary(r)
+ /\ LET pReq == [type |-> "PrepareRequest", rm |-> r, view |-> rmState[r].view]
+ IN /\ pReq \notin msgs
+ /\ msgs' = msgs \cup {pReq}
+ /\ UNCHANGED <>
+
+\* RMFaultySendPResp describes sending PrepareResponse message by the non-primary faulty node r.
+RMFaultySendPResp(r) ==
+ /\ rmState[r].type = "bad"
+ /\ \neg IsPrimary(r)
+ /\ LET pResp == [type |-> "PrepareResponse", rm |-> r, view |-> rmState[r].view]
+ IN /\ pResp \notin msgs
+ /\ msgs' = msgs \cup {pResp}
+ /\ UNCHANGED <>
+
+\* RMFaultySendCommit describes sending Commit message by the faulty node r.
+RMFaultySendCommit(r) ==
+ /\ rmState[r].type = "bad"
+ /\ LET commit == [type |-> "Commit", rm |-> r, view |-> rmState[r].view]
+ IN /\ commit \notin msgs
+ /\ msgs' = msgs \cup {commit}
+ /\ UNCHANGED <>
+
+\* RMDie describes node r that was removed from the network at the particular step
+\* of the behaviour. After this node r can't change its state and accept/send messages.
+RMDie(r) ==
+ /\ r \in RMDead
+ /\ Cardinality({rm \in RM : rmState[rm].type = "dead"}) < F
+ /\ rmState' = [rmState EXCEPT ![r].type = "dead"]
+ /\ UNCHANGED <>
+
+\* Terminating is an action that allows infinite stuttering to prevent deadlock on
+\* behaviour termination. We consider termination to be valid if at least M nodes
+\* has the block being accepted.
+Terminating ==
+ /\ Cardinality({rm \in RM : rmState[rm].type = "blockAccepted"}) >= M
+ /\ UNCHANGED <>
+
+\* The next-state action.
+Next ==
+ \/ Terminating
+ \/ \E r \in RM:
+ RMSendPrepareRequest(r) \/ RMSendPrepareResponse(r) \/ RMSendCommit(r)
+ \/ RMAcceptBlock(r) \/ RMSendChangeView1(r) \/ RMReceiveChangeView(r) \/ RMBeBad(r) \/ RMSendChangeView2(r) \/ RMSendChangeView3(r)
+ \/ RMFaultySendCV1(r) \/ RMFaultyDoCV(r) \/ RMFaultySendCommit(r) \/ RMFaultySendPReq(r) \/ RMFaultySendPResp(r) \/ RMFaultySendCV2(r) \/ RMFaultySendCV3(r)
+ \/ RMDie(r) \/ RMFetchBlock(r)
+
+\* Safety is a temporal formula that describes the whole set of allowed
+\* behaviours. It specifies only what the system MAY do (i.e. the set of
+\* possible allowed behaviours for the system). It asserts only what may
+\* happen; any behaviour that violates it does so at some point and
+\* nothing past that point makes difference.
+\*
+\* E.g. this safety formula (applied standalone) allows the behaviour to end
+\* with an infinite set of stuttering steps (those steps that DO NOT change
+\* neither msgs nor rmState) and never reach the state where at least one
+\* node is committed or accepted the block.
+\*
+\* To forbid such behaviours we must specify what the system MUST
+\* do. It will be specified below with the help of fairness conditions in
+\* the Fairness formula.
+Safety == Init /\ [][Next]_vars
+
+\* -------------- Fairness temporal formula --------------
+
+\* Fairness is a temporal assumptions under which the model is working.
+\* Usually it specifies different kind of assumptions for each/some
+\* subactions of the Next's state action, but the only think that bothers
+\* us is preventing infinite stuttering at those steps where some of Next's
+\* subactions are enabled. Thus, the only thing that we require from the
+\* system is to keep take the steps until it's impossible to take them.
+\* That's exactly how the weak fairness condition works: if some action
+\* remains continuously enabled, it must eventually happen.
+Fairness == WF_vars(Next)
+
+\* -------------- Specification --------------
+
+\* The complete specification of the protocol written as a temporal formula.
+Spec == Safety /\ Fairness
+
+\* -------------- Liveness temporal formula --------------
+
+\* For every possible behaviour it's true that eventually (i.e. at least once
+\* through the behaviour) block will be accepted. It is something that dBFT
+\* must guarantee (an in practice this condition is violated).
+TerminationRequirement == <>(Cardinality({r \in RM : rmState[r].type = "blockAccepted"}) >= M)
+
+\* A liveness temporal formula asserts only what must happen (i.e. specifies
+\* what the system MUST do). Any behaviour can NOT violate it at ANY point;
+\* there's always the rest of the behaviour that can always make the liveness
+\* formula true; if there's no such behaviour than the liveness formula is
+\* violated. The liveness formula is supposed to be checked as a property
+\* by the TLC model checker.
+Liveness == TerminationRequirement
+
+\* -------------- ModelConstraints --------------
+
+\* MaxViewConstraint is a state predicate restricting the number of possible
+\* behaviour states. It is needed to reduce model checking time and prevent
+\* the model graph size explosion. This formulae must be specified at the
+\* "State constraint" section of the "Additional Spec Options" section inside
+\* the model overview.
+MaxViewConstraint == /\ \A r \in RM : rmState[r].view <= MaxView
+ /\ \A msg \in msgs : msg.view <= MaxView
+
+\* -------------- Invariants of the specification --------------
+
+\* Model invariant is a state predicate (statement) that must be true for
+\* every step of every reachable behaviour. Model invariant is supposed to
+\* be checked as an Invariant by the TLC Model Checker.
+
+\* TypeOK is a type-correctness invariant. It states that all elements of
+\* specification variables must have the proper type throughout the behaviour.
+TypeOK ==
+ /\ rmState \in [RM -> RMStates]
+ /\ msgs \subseteq Messages
+
+\* InvTwoBlocksAccepted states that there can't be two different blocks accepted in
+\* the two different views, i.e. dBFT must not allow forks.
+InvTwoBlocksAccepted == \A r1 \in RM:
+ \A r2 \in RM \ {r1}:
+ \/ rmState[r1].type /= "blockAccepted"
+ \/ rmState[r2].type /= "blockAccepted"
+ \/ rmState[r1].view = rmState[r2].view
+
+\* InvFaultNodesCount states that there can be F faulty or dead nodes at max.
+InvFaultNodesCount == Cardinality({
+ r \in RM : rmState[r].type = "bad" \/ rmState[r].type = "dead"
+ }) <= F
+
+\* This theorem asserts the truth of the temporal formula whose meaning is that
+\* the state predicates TypeOK, InvTwoBlocksAccepted and InvFaultNodesCount are
+\* the invariants of the specification Spec. This theorem is not supposed to be
+\* checked by the TLC model checker, it's here for the reader's understanding of
+\* the purpose of TypeOK, InvTwoBlocksAccepted and InvFaultNodesCount.
+THEOREM Spec => [](TypeOK /\ InvTwoBlocksAccepted /\ InvFaultNodesCount)
+
+=============================================================================
+\* Modification History
+\* Last modified Wed Mar 01 12:11:07 MSK 2023 by root
+\* Last modified Tue Feb 07 23:11:19 MSK 2023 by rik
+\* Last modified Fri Feb 03 18:09:33 MSK 2023 by anna
+\* Created Thu Dec 15 16:06:17 MSK 2022 by anna
diff --git a/formal-models/dbft2.1_threeStagedCV/dbftCV3___AllGoodModel.launch b/formal-models/dbft2.1_threeStagedCV/dbftCV3___AllGoodModel.launch
new file mode 100644
index 00000000..8f828243
--- /dev/null
+++ b/formal-models/dbft2.1_threeStagedCV/dbftCV3___AllGoodModel.launch
@@ -0,0 +1,42 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/formal-models/dbftMultipool/dbftMultipool___AllGoodModel.launch b/formal-models/dbftMultipool/dbftMultipool___AllGoodModel.launch
index e522df66..1171d273 100644
--- a/formal-models/dbftMultipool/dbftMultipool___AllGoodModel.launch
+++ b/formal-models/dbftMultipool/dbftMultipool___AllGoodModel.launch
@@ -27,7 +27,7 @@
-
+