vacp2p
/
rfc
mirror of https://github.com/vacp2p/rfc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

mvds/formal-spec (#25)

This commit is contained in:
Dean Eigenmann 2019-11-12 12:11:35 +01:00 committed by GitHub
parent be5c5666e1
commit e78f957250
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 7 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
mvds.md
View File

@ -15,8 +15,9 @@
1. [State](#state) 1. [State](#state)
2. [Flow](#flow) 2. [Flow](#flow)
3. [Retransmission](#retransmission) 3. [Retransmission](#retransmission)
5. [Footnotes](#footnotes) 5. [Formal Specification](#formal-Specification)
6. [Acknowledgements](#acknowledgements) 6. [Footnotes](#footnotes)
7. [Acknowledgements](#acknowledgements)
## Abstract ## Abstract
@ -141,6 +142,10 @@ The record of the type `Type` SHOULD be retransmitted every time `Send Epoch` is
> ***NOTE:** We do not retransmission `ACK`s as we do not know when they have arrived, therefore we simply resend them every time we receive a `MESSAGE`.* > ***NOTE:** We do not retransmission `ACK`s as we do not know when they have arrived, therefore we simply resend them every time we receive a `MESSAGE`.*
## Formal Specification
MVDS has been formally specified using TLA+: <https://github.com/vacp2p/formalities/tree/master/MVDS>.
## Footnotes ## Footnotes
1. <https://code.briarproject.org/briar/briar-spec/blob/master/protocols/BSP.md> 1. <https://code.briarproject.org/briar/briar-spec/blob/master/protocols/BSP.md>