Skip to content

Commit

Permalink
mod: minor_fix
Browse files Browse the repository at this point in the history
  • Loading branch information
Stefano Angieri authored and Stefano Angieri committed Oct 27, 2023
1 parent 9c6eee1 commit f36f1b1
Showing 1 changed file with 32 additions and 32 deletions.
64 changes: 32 additions & 32 deletions spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand Down

0 comments on commit f36f1b1

Please sign in to comment.