in TLA+ of the Interledger Protocol Atomic ( ILP /A) Modeled after the excellent Raft specification by Diego Ongaro. Available at https://github.com/ongardie/raft.tla Copyright 2014 Diego Ongaro. This work is licensed under the Creative Commons Attribution-4.0 International License https://creativecommons.org/licenses/by/4.0/ extends Naturals, Sequences, Bags, TLC The set of ledger IDs constants Ledger The set of participant IDs constants Participant The notary constants Notary Sender states constants S Ready, S Waiting, S Done Notary states constants N Waiting, N Committed, N Aborted Ledger states constants L Proposed, L Prepared, L Executed, L Aborted Message types constants PrepareRequest, ExecuteRequest, AbortRequest, PrepareNotify, ExecuteNotify, AbortNotify, SubmitReceiptRequest Receipt signature constants R ReceiptSignature Global variables A bag of records representing requests and responses sent from one process to another variable messages Sender variables State of the sender ( S Ready , S Waiting , S Done ) variable senderState All sender variables senderVars = hsenderStatei The following variables are all per ledger (functions with domain Ledger ) The ledger state ( L Proposed , L Prepared , L Executed or L Aborted ) variable ledgerState 12 A.4 Formal Specification: Universal mode module Universal Formal Specification in TLA+ of the Interledger Protocol Universal ( ILP / U ) Modeled after the excellent Raft specification by Diego Ongaro. Available at https://github.com/ongardie/raft.tla Copyright 2014 Diego Ongaro. This work is licensed under the Creative Commons Attribution-4.0 International License https://creativecommons.org/licenses/by/4.0/ extends Naturals, Sequences, FiniteSets, Bags, TLC The set of ledger IDs constants Ledger The set of participant IDs constants Participant Sender states constants S Ready, S ProposalWaiting, S Waiting, S Done Connector states constants C Ready, C Proposed Ledger states constants L Proposed, L Prepared, L Executed, L Aborted Message types constants PrepareRequest, ExecuteRequest, AbortRequest, PrepareNotify, ExecuteNotify, AbortNotify, SubpaymentProposalRequest, SubpaymentProposalResponse Receipt signature constants R ReceiptSignature Global variables Under synchrony we are allowed to have a global clock variable clock A bag of records representing requests and responses sent from one process to another variable messages Sender variables State of the sender ( S Ready , S Waiting , S Done ) variable senderState Whether the sender has received a response from a given connector variable senderProposalResponses All sender variables senderVars = hsenderState, senderProposalResponsesi Connector variables 19