diff --git a/verification/spec/connection-handshake/Environment.tla b/verification/spec/connection-handshake/Environment.tla index 6c9acf6def..0b0bb87f8b 100644 --- a/verification/spec/connection-handshake/Environment.tla +++ b/verification/spec/connection-handshake/Environment.tla @@ -5,7 +5,7 @@ This module is part of the TLA+ specification for the IBC Connection Handshake protocol (identifier 'ICS3'). This is a high-level spec of ICS3. - This module captures the operators and actions outside of the CH protocol + This module captures the operators and actions outside of the ICS3 protocol itself (i.e., the environment). Among others, the environment does the following: - creates two instances of ConnectionHandshakeModule, diff --git a/verification/spec/connection-handshake/README.md b/verification/spec/connection-handshake/README.md index 3cc273b189..ec22ca6fb4 100644 --- a/verification/spec/connection-handshake/README.md +++ b/verification/spec/connection-handshake/README.md @@ -1,7 +1,7 @@ -# IBC Connection Handshake (CH) TLA+ spec +# IBC Connection Handshake (ICS3) TLA+ spec -This is a high-level TLA+ spec for the IBC Connection Handshake (CH) protocol. +This is a high-level TLA+ spec for the IBC Connection Handshake (ICS3) protocol. The spec has three modules: - `Environment.tla` (main model lives here)