From f36f1b14e14252d76af90018718f1359992b5828 Mon Sep 17 00:00:00 2001 From: Stefano Angieri Date: Fri, 27 Oct 2023 18:18:25 +0200 Subject: [PATCH] mod: minor_fix --- .../FSM_UPGRADES.md | 64 +++++++++---------- 1 file changed, 32 insertions(+), 32 deletions(-) diff --git a/spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md b/spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md index 1c92285f1..49f738132 100644 --- a/spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md +++ b/spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md @@ -102,27 +102,27 @@ The private store is meant for an end (e.g. ChainA or ChainB) to store transient ### Functions Calls For State Transition ```typescript S0-->S1: (OPEN,OPEN) --> (OPEN,OPEN) :: A and R:A -**ChanUpgradeInit** --> IsAuthorizedUpgrader() - **InitUpgradeHandshake** --> getChan(ChanA) :: VerifyChanAis(OPEN); VerifyUpgradeVersion !== "" - getConn(ConnA):: Verify (ProposedConnection !== null && ProposedConnection.stateIs(OPEN)); VerifyOrderingSupported() - setUpgrade(UpgA) [Ordering and ConnHops]; +ChanUpgradeInit --> IsAuthorizedUpgrader() + InitUpgradeHandshake --> getChan(ChanA) :: VerifyChanAis(OPEN); VerifyUpgradeVersion(!== "") + getConn(ConnA):: Verify (ProposedConnection !== null && ProposedConnection.stateIs(OPEN)) VerifyOrderingSupported() + setUpgrade(UpgA) [Ordering and ConnHops] setUpgradeSequence(ChanA) -**ChanUpgradeInit** --> getUpgrade(UpgA); +ChanUpgradeInit --> getUpgrade(UpgA) setUpgrade(UpgA) [Version] ``` ```typescript S1 -->S2: (OPEN,OPEN) --> (OPEN,FLUSHING) :: R:B -**ChanUpgradeTry** --> getChan(ChanB) :: VerifyChanBis(OPEN) +ChanUpgradeTry --> getChan(ChanB) :: VerifyChanBis(OPEN) getUpgrade(UpgB) - **InitUpgradeHandshake** --> getChan(ChanB) :: VerifyChanBis(OPEN) ; VerifyUpgradeVersion !== "" - getConn(ConnB):: Verify (ProposedConnection !== null && ProposedConnection.stateIs(OPEN)) ;VerifyOrderingSupported() + InitUpgradeHandshake--> getChan(ChanB) :: VerifyChanBis(OPEN) ; VerifyUpgradeVersion(!== "") + getConn(ConnB):: Verify (ProposedConnection !== null && ProposedConnection.stateIs(OPEN)) VerifyOrderingSupported() setUpgrade(UpgB) [Ordering, ConnHops, Version]; setUpgradeSequence(ChanB) VerifyIsCompatibleUpgFields() -getConn(ConnA) :: ConstructCounterPartyChannelEnd(); VerifyChannelState; VerifyChannelUpgrade; - **StartFlushingUpgradeHandshake** --> getChan(ChanB):: VerifyChanBis(OPEN); - getUpgrade(UpgB):: VerifyUpgrade!==nil; +getConn(ConnA) :: ConstructCounterPartyChannelEnd(); VerifyChannelState(); VerifyChannelUpgrade() + StartFlushingUpgradeHandshake --> getChan(ChanB):: VerifyChanBis(OPEN) + getUpgrade(UpgB):: VerifyUpgrade(!==nil) setChanB(FLUSHING) getUpgradeTimeout(TimeoutA):: VerifyTimeoutNotExpired() getNextSeqSend(NextSeqSendA) @@ -135,11 +135,11 @@ setUpgrade(UpgB) [Version] ```typescript S2 --> S3_1: (OPEN,FLUSHING) --> (FLUSHING,FLUSHING) :: R:A -**ChanUpgradeAck** --> getChan(ChanA); VerifyChanAis(OPEN || FLUSHING) -getConn(ConnB) :: ConstructCounterPartyChannelEnd(); VerifyChannelState; VerifyChannelUpgrade; +ChanUpgradeAck --> getChan(ChanA); VerifyChanAis(OPEN || FLUSHING) +getConn(ConnB) :: ConstructCounterPartyChannelEnd(); VerifyChannelState(); VerifyChannelUpgrade() getUpgrade(UpgA) :: VerifyIsCompatibleUpgFields() - **StartFlushingUpgradeHandshake** --> getChan(ChanA) :: VerifyChanAis(OPEN) - getUpgrade(UpgA):: VerifyUpgrade!==nil; + StartFlushingUpgradeHandshake --> getChan(ChanA) :: VerifyChanAis(OPEN) + getUpgrade(UpgA):: VerifyUpgrade(!==nil) setChanA(FLUSHING) getUpgradeTimeout(TimeoutB):: VerifyTimeoutNotExpired() getNextSeqSend(NextSeqSendB) @@ -153,11 +153,11 @@ setUpgrade(UpgA) ```typescript S2 --> S3_2: (OPEN,FLUSHING) --> (FLUSHING_COMPLETE,FLUSHING) :: R:A -**ChanUpgradeAck** getChan(ChanA); VerifyChanAis(OPEN || FLUSHING) -getConn(ConnB) :: ConstructCounterPartyChannelEnd(); VerifyChannelState; VerifyChannelUpgrade +ChanUpgradeAck--> getChan(ChanA); VerifyChanAis(OPEN || FLUSHING) +getConn(ConnB) :: ConstructCounterPartyChannelEnd(); VerifyChannelState(); VerifyChannelUpgrade() getUpgrade(UpgA) :: VerifyIsCompatibleUpgFields() - **StartFlushingUpgradeHandshake** --> getChan(ChanA); VerifyChanIs(OPEN) - getUpgrade(UpgA) :: VerifyUpgrade!==nil + StartFlushingUpgradeHandshake --> getChan(ChanA); VerifyChanIs(OPEN) + getUpgrade(UpgA) :: VerifyUpgrade(!==nil) setChanA(FLUSHING) getUpgradeTimeout(TimeoutB):: VerifyTimeoutNotExpired() getNextSeqSend(NextSeqSendB) @@ -171,8 +171,8 @@ setUpgrade(UpgA) ```typescript S3_1 --> S4: (FLUSHING,FLUSHING) --> (FLUSHING,FLUSHING_COMPLETE) :: R:B -**ChanUpgradeConfirm** getChan(B) :: VerifyChanBis(FLUSHING) -getConn(ConnA) :: ConstructCounterPartyChannelEnd(); VerifyChannelState; VerifyChannelUpgrade +ChanUpgradeConfirm--> getChan(B) :: VerifyChanBis(FLUSHING) +getConn(ConnA) :: ConstructCounterPartyChannelEnd(); VerifyChannelState(); VerifyChannelUpgrade() VerifyTimeoutNotExpired() VerifyInflightsPackets(NotExist) setChanB(FLUSHING_COMPLETE) @@ -181,27 +181,27 @@ setChannel(ChanB) ```typescript S4 --> S5_1: (FLUSHING,FLUSHING_COMPLETE) --> (FLUSHING_COMPLETE,FLUSHING_COPMLETE) :: PH:A -**PacketHandlerChainA** VerifyInflightsPackets(NotExist) +PacketHandlerChainA_Function--> VerifyInflightsPackets(NotExist) setChanA(FLUSHING_COMPLETE) setChannel(ChanA) ``` ```typescript S3_2 --> S5_1: (FLUSHING_COMPLETE,FLUSHING) --> (FLUSHING_COMPLETE,FLUSHING_COPMLETE) :: PH:B -**PacketHandlerChainB** VerifyInflightsPackets(NotExist) +PacketHandlerChainB_Function--> VerifyInflightsPackets(NotExist) setChanB(FLUSHING_COMPLETE) setChannel(ChanB) ``` ```typescript S3_2 --> S5_2: (FLUSHING_COMPLETE,FLUSHING) --> (FLUSHING_COMPLETE,OPEN) :: R:B -**ChanUpgradeConfirm** getChan(B); VerifyChanBis(FLUSHING) -getConn(ConnA) :: ConstructCounterPartyChannelEnd(); VerifyChannelState; VerifyChannelUpgrade +ChanUpgradeConfirm--> getChan(B); VerifyChanBis(FLUSHING) +getConn(ConnA) :: ConstructCounterPartyChannelEnd(); VerifyChannelState(); VerifyChannelUpgrade() VerifyTimeoutNotExpired() VerifyInflightsPackets(NotExist) setChanB(FLUSHING_COMPLETE) setChannel(ChanB) - **openUpgradeHandshake** getChan(B) + openUpgradeHandshake--> getChan(B) getUpgrade(UpgB) setChanUpgradeParameter(ChanB) delUpgrade(UpgB) @@ -211,11 +211,11 @@ setChannel(ChanB) ```typescript S5_1 --> S6: (FLUSHING_COMPLETE,FLUSHING_COMPLETE) --> (OPEN,OPEN) :: R:B and R:A -**ChanUpgradeOpen** getChan(Chan); VerifyChanIs(FLUSHING_COMPLETE) +ChanUpgradeOpen--> getChan(Chan); VerifyChanIs(FLUSHING_COMPLETE) getConn(Conn); VerifyChanIs(OPEN || FLUSHING_COMPLETE) -ConstructCounterPartyChannelEnd(); VerifyChannelState - **openUpgradeHandshake** getChan(); +ConstructCounterPartyChannelEnd(); VerifyChannelState() + openUpgradeHandshake--> getChan(); getUpgrade(UpgA) setChanUpgradeParameter(Chan) delUpgrade(Upg) @@ -225,12 +225,12 @@ ConstructCounterPartyChannelEnd(); VerifyChannelState ```typescript S5_2 --> S6: (FLUSHING_COMPLETE,OPEN) --> (OPEN,OPEN) -**ChanUpgradeOpen** getChan(ChanA); VerifyChanAis(FLUSHING_COMPLETE) +ChanUpgradeOpen --> getChan(ChanA); VerifyChanAis(FLUSHING_COMPLETE) getConn(ConnB) VerifyChanBis(OPEN) getUpgrade(UpgA) -ConstructCounterPartyChannelEnd(); VerifyChannelState - **openUpgradeHandshake** getChan(A) +ConstructCounterPartyChannelEnd(); VerifyChannelState() + openUpgradeHandshake--> getChan(A) getUpgrade(UpgA) setChanUpgradeParameter(ChanA) delUpgrade(UpgA)