Skip to content

Instantly share code, notes, and snippets.

@mx00s
Last active August 3, 2020 08:10
Show Gist options
  • Save mx00s/5cce9fb765a217b1858dd2017a688007 to your computer and use it in GitHub Desktop.
Save mx00s/5cce9fb765a217b1858dd2017a688007 to your computer and use it in GitHub Desktop.
Session Type Demo (based on WIP code)

Session Type Demo

Models interactions between a user and an ATM based on the expository example in http://www.di.unito.it/~dezani/papers/sto.pdf

User perspective

Session Type:

!String. &{ success: ⊕{ deposit: !Real. ?Real. end
                      | withdraw: !Real. &{ dispense: end
                                          | overdraft: end
                                          }. end
                      }
          | failure: end
          }. end

Sequence Diagram (mermaid):

sequenceDiagram
User-->ATM: link
User-->>ATM: identifier : String
alt
ATM->>User: success
alt
User->>ATM: deposit
User-->>ATM: amount : Real
ATM-->>User: balance : Real
else
User->>ATM: withdraw
User-->>ATM: amount : Real
alt
ATM->>User: dispense
else
ATM->>User: overdraft
end
end
else
ATM->>User: failure
end

Possible Session Flows (4):

!identifier:String. &success. ⊕deposit. !amount:Real. ?balance:Real. end. 
!identifier:String. &success. ⊕withdraw. !amount:Real. &dispense. end. 
!identifier:String. &success. ⊕withdraw. !amount:Real. &overdraft. end. 
!identifier:String. &failure. end. 

ATM perspective

Session Type:

?String. ⊕{ success: &{ deposit: ?Real. !Real. end
                      | withdraw: ?Real. ⊕{ dispense: end
                                          | overdraft: end
                                          }. end
                      }
          | failure: end
          }. end

Sequence Diagram (mermaid):

sequenceDiagram
ATM-->User: link
User-->>ATM: identifier : String
alt
ATM->>User: success
alt
User->>ATM: deposit
User-->>ATM: amount : Real
ATM-->>User: balance : Real
else
User->>ATM: withdraw
User-->>ATM: amount : Real
alt
ATM->>User: dispense
else
ATM->>User: overdraft
end
end
else
ATM->>User: failure
end

Possible Session Flows (4):

?identifier:String. ⊕success. &deposit. ?amount:Real. !balance:Real. end. 
?identifier:String. ⊕success. &withdraw. ?amount:Real. ⊕dispense. end. 
?identifier:String. ⊕success. &withdraw. ?amount:Real. ⊕overdraft. end. 
?identifier:String. ⊕failure. end. 
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment