Skip to content

Commit

Permalink
models: add dBFT 2.1 models
Browse files Browse the repository at this point in the history
  • Loading branch information
AnnaShaleva committed Mar 3, 2023
1 parent fc45057 commit 482abb8
Show file tree
Hide file tree
Showing 11 changed files with 1,278 additions and 5 deletions.
1 change: 1 addition & 0 deletions formal-models/.github/dbft2.1_centralizedCV.drawio
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
<mxfile host="app.diagrams.net" modified="2023-03-03T08:45:11.871Z" agent="5.0 (X11)" etag="A8OKiLLrr7VSt7hila6Z" version="20.8.23" type="google"><diagram name="Page-1" id="gx1AT7QsytIHyGW8taHa">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/</diagram></mxfile>
Binary file added formal-models/.github/dbft2.1_centralizedCV.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
1 change: 1 addition & 0 deletions formal-models/.github/dbft2.1_threeStagedCV.drawio
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
<mxfile host="app.diagrams.net" modified="2023-02-28T12:44:44.583Z" agent="5.0 (X11)" etag="VKb14Evzl_Epa14_ET2I" version="20.8.22" type="google"><diagram name="Page-1" id="gx1AT7QsytIHyGW8taHa">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</diagram></mxfile>
Binary file added formal-models/.github/dbft2.1_threeStagedCV.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading

0 comments on commit 482abb8

Please sign in to comment.